Add testing infrastructure for LFSC signatures

This commit adds testing infrastructure for LFSC signatures that is
enabled when CVC4 is configured with LFSC. The testing infrastructure
adopts `run_test.py` from https://github.com/CVC4/LFSC with minor
modifications (mainly adding support for a list of include directories
that are searched to resolve *.plf dependencies). The commit uses the
existing examples and test files from `proofs/signatures` as the initial
set of tests.

Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>

22 files changed, 216 insertions, 17 deletions

diff --git a/cmake/FindLFSC.cmake b/cmake/FindLFSC.cmake
index 6135c7891..786af14be 100644
--- a/cmake/FindLFSC.cmake
+++ b/cmake/FindLFSC.cmake
@@ -3,15 +3,17 @@
 # LFSC_INCLUDE_DIR - the LFSC include directory
 # LFSC_LIBRARIES - Libraries needed to use LFSC
 
+find_program(LFSC_BINARY NAMES lfscc)
 find_path(LFSC_INCLUDE_DIR NAMES lfscc.h)
 find_library(LFSC_LIBRARIES NAMES lfscc)
 
 include(FindPackageHandleStandardArgs)
 find_package_handle_standard_args(LFSC
   DEFAULT_MSG
-  LFSC_INCLUDE_DIR LFSC_LIBRARIES)
+  LFSC_BINARY LFSC_INCLUDE_DIR LFSC_LIBRARIES)
 
-mark_as_advanced(LFSC_INCLUDE_DIR LFSC_LIBRARIES)
-if(LFSC_LIBRARIES)
+mark_as_advanced(LFSC_BINARY LFSC_INCLUDE_DIR LFSC_LIBRARIES)
+if(LFSC_FOUND)
+  message(STATUS "Found LFSC include dir: ${LFSC_INCLUDE_DIR}")
   message(STATUS "Found LFSC libs: ${LFSC_LIBRARIES}")
 endif()
diff --git a/proofs/signatures/drat.plf b/proofs/signatures/drat.plf
index 2f70bbfbd..ad3c8ec8d 100644
--- a/proofs/signatures/drat.plf
+++ b/proofs/signatures/drat.plf
@@ -1,4 +1,4 @@
-; Depends on lrat.plf
+; Deps: lrat.plf
 ;
 ; Implementation of DRAT checking.
 ;
diff --git a/proofs/signatures/er.plf b/proofs/signatures/er.plf
index 9fcc9d4e8..6a8a059a2 100644
--- a/proofs/signatures/er.plf
+++ b/proofs/signatures/er.plf
@@ -1,4 +1,4 @@
-; Depends on sat.plf
+; Deps: sat.plf
 
 ; This file exists to support the **definition introduction** (or **extension**)
 ; rule in the paper:
diff --git a/proofs/signatures/lrat.plf b/proofs/signatures/lrat.plf
index d16791624..b5d46be43 100644
--- a/proofs/signatures/lrat.plf
+++ b/proofs/signatures/lrat.plf
@@ -2,7 +2,7 @@
 ; LRAT format detailed in "Efficient Certified RAT Verification"
 ; Link: https://www.cs.utexas.edu/~marijn/publications/lrat.pdf
 ; Author: aozdemir
-; Depends On: sat.plf, smt.plf
+; Deps: sat.plf smt.plf
 
 
 ; A general note about the design of the side conditions:
diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf
index 57dc5bd1e..9f6e71986 100644
--- a/proofs/signatures/smt.plf
+++ b/proofs/signatures/smt.plf
@@ -3,7 +3,7 @@
 ; SMT syntax and semantics (not theory-specific)
 ;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-; depends on sat.plf
+; Deps: sat.plf
 
 (declare formula type)
 (declare th_holds (! f formula type))
diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf
index acfbd2f3b..5517d9a4f 100644
--- a/proofs/signatures/th_arrays.plf
+++ b/proofs/signatures/th_arrays.plf
@@ -3,7 +3,7 @@
 ; Theory of Arrays
 ;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-; depends on : th_base.plf
+; Deps: th_base.plf
 
 ; sorts
 
diff --git a/proofs/signatures/th_base.plf b/proofs/signatures/th_base.plf
index d6b283752..d5182007e 100644
--- a/proofs/signatures/th_base.plf
+++ b/proofs/signatures/th_base.plf
@@ -5,7 +5,7 @@
 ; Theory of Equality and Congruence Closure
 ;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-; depends on : smt.plf
+; Deps: smt.plf
 
 ; sorts :
 
diff --git a/proofs/signatures/th_lira.plf b/proofs/signatures/th_lira.plf
index 70cdfc733..af326bf27 100644
--- a/proofs/signatures/th_lira.plf
+++ b/proofs/signatures/th_lira.plf
@@ -1,4 +1,4 @@
-; Depends on th_real.plf, th_int.plf, smt.plf, sat.plf
+; Deps: th_real.plf th_int.plf smt.plf sat.plf
 
 ; Some axiom arguments are marked "; Omit", because they can be deduced from
 ; other arguments and should be replaced with a "_" when invoking the axiom.
diff --git a/proofs/signatures/th_real.plf b/proofs/signatures/th_real.plf
index 112328b63..dfedb28ed 100644
--- a/proofs/signatures/th_real.plf
+++ b/proofs/signatures/th_real.plf
@@ -1,4 +1,4 @@
-; Depends On: th_smt.plf
+; Deps: smt.plf
 (declare Real sort)
 
 (define arithpred_Real (! x (term Real)
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index ad946e3ca..52a999c1b 100644
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -31,3 +31,7 @@ if(ENABLE_UNIT_TESTING)
     add_subdirectory(java)
   endif()
 endif()
+
+if(LFSC_BINARY)
+  add_subdirectory(signatures)
+endif()
diff --git a/test/signatures/CMakeLists.txt b/test/signatures/CMakeLists.txt
new file mode 100644
index 000000000..64da9fad2
--- /dev/null
+++ b/test/signatures/CMakeLists.txt
@@ -0,0 +1,33 @@
+set(lfsc_test_file_list
+  drat_test.plf
+  er_test.plf
+  example-arrays.plf
+  example.plf
+  example-quant.plf
+  ex_bv.plf
+  ex-mem.plf
+  lrat_test.plf
+  th_lira_test.plf
+)
+
+set(test_script ${CMAKE_CURRENT_LIST_DIR}/run_test.py)
+
+macro(lfsc_test file)
+  set(test_name "signatures/${file}")
+  add_test(
+    NAME "${test_name}"
+    COMMAND
+      "${PYTHON_EXECUTABLE}"
+      "${test_script}"
+      "${LFSC_BINARY}"
+      "${CMAKE_CURRENT_LIST_DIR}/${file}"
+      "${CMAKE_SOURCE_DIR}/proofs/signatures"
+    WORKING_DIRECTORY ${CMAKE_CURRENT_LIST_DIR}
+  )
+
+  set_tests_properties("${test_name}" PROPERTIES LABELS "signatures")
+endmacro()
+
+foreach(file ${lfsc_test_file_list})
+  lfsc_test(${file})
+endforeach()
diff --git a/test/signatures/README.md b/test/signatures/README.md
new file mode 100644
index 000000000..4ac8cb131
--- /dev/null
+++ b/test/signatures/README.md
@@ -0,0 +1,32 @@
+# Signature Tests
+
+This directory contains tests of our LFSC proof signatures. To run just the
+tests in this directory, the test label `signatures` can be used (`ctest -L
+signatures`).
+
+## Adding a New Signature Test
+
+To add a new signature test file, add the file to git, for example:
+
+```
+git add test/signatures/new_signature_test.plf
+```
+
+Also add it to [CMakeLists.txt](CMakeLists.txt) in this directory and declare
+the dependencies of the test as explained below.
+
+The signature tests are prefixed with `signatures/`, so the test for
+`example.plf` will have the name `signatures/example.plf`.
+
+## Test Dependencies
+
+Tests can declare the signature files that they depend on using the `; Deps:`
+directive followed by a space-separated list of files. For example:
+
+```
+; Deps: sat.plf smt.plf
+```
+
+indicates that the test depends on `sat.plf` and `smt.plf`. The run script
+automatically searches for the listed files in `proofs/signatures` as well as
+the directory of the test input.
diff --git a/proofs/signatures/drat_test.plf b/test/signatures/drat_test.plf
index 2ede6df34..e5335a6bb 100644
--- a/proofs/signatures/drat_test.plf
+++ b/test/signatures/drat_test.plf
@@ -1,4 +1,4 @@
-;depends on drat.plf
+; Deps: drat.plf
 (declare TestSuccess type)
 
 ; Test for clause_eq
diff --git a/proofs/signatures/er_test.plf b/test/signatures/er_test.plf
index 1b5117a70..671efdb46 100644
--- a/proofs/signatures/er_test.plf
+++ b/test/signatures/er_test.plf
@@ -1,4 +1,4 @@
-; Depends on er.plf
+; Deps: er.plf
 
 ; This is a circuitous proof that uses the definition introduction and
 ; unrolling rules
diff --git a/proofs/signatures/ex-mem.plf b/test/signatures/ex-mem.plf
index 7e143c5b6..87d1053c4 100644
--- a/proofs/signatures/ex-mem.plf
+++ b/test/signatures/ex-mem.plf
@@ -1,3 +1,5 @@
+; Deps: sat.plf smt.plf th_base.plf
+
 (check
 (% s sort
 (% a (term s)
diff --git a/proofs/signatures/ex_bv.plf b/test/signatures/ex_bv.plf
index 332d7765c..a4f5ad816 100644
--- a/proofs/signatures/ex_bv.plf
+++ b/test/signatures/ex_bv.plf
@@ -1,3 +1,5 @@
+; Deps: sat.plf smt.plf th_base.plf th_bv.plf th_bv_bitblast.plf
+
 ; (a = b) ^ (a = b & 00000) ^ (b = 11111) is UNSAT
 
 (check
diff --git a/proofs/signatures/example-arrays.plf b/test/signatures/example-arrays.plf
index 03dc0831c..0e840274f 100644
--- a/proofs/signatures/example-arrays.plf
+++ b/test/signatures/example-arrays.plf
@@ -1,4 +1,4 @@
-; to check, run : lfscc sat.plf smt.plf th_base.plf th_arrays.plf example-arrays.plf
+; Deps: sat.plf smt.plf th_base.plf th_arrays.plf
 
 ; --------------------------------------------------------------------------------
 ; literals :
diff --git a/proofs/signatures/example-quant.plf b/test/signatures/example-quant.plf
index 086633be9..611fd182c 100644
--- a/proofs/signatures/example-quant.plf
+++ b/test/signatures/example-quant.plf
@@ -1,4 +1,4 @@
-; to check, run : lfsc sat.plf smt.plf th_base.plf example.plf
+; Deps: sat.plf smt.plf th_base.plf th_quant.plf
 
 ; --------------------------------------------------------------------------------
 ; literals :
diff --git a/proofs/signatures/example.plf b/test/signatures/example.plf
index ab690eb51..775557fa6 100644
--- a/proofs/signatures/example.plf
+++ b/test/signatures/example.plf
@@ -1,4 +1,4 @@
-; to check, run : lfsc sat.plf smt.plf th_base.plf example.plf
+; Deps: sat.plf smt.plf th_base.plf
 
 ; --------------------------------------------------------------------------------
 ; input :
diff --git a/proofs/signatures/lrat_test.plf b/test/signatures/lrat_test.plf
index 0663a08f7..466216ff9 100644
--- a/proofs/signatures/lrat_test.plf
+++ b/test/signatures/lrat_test.plf
@@ -1,3 +1,4 @@
+; Deps: lrat.plf
 (declare test_clause_append
          (! c1 clause
             (! c2 clause
diff --git a/test/signatures/run_test.py b/test/signatures/run_test.py
new file mode 100755
index 000000000..ac14267e9
--- /dev/null
+++ b/test/signatures/run_test.py
@@ -0,0 +1,123 @@
+#!/usr/bin/env python
+
+import argparse
+import re
+import os.path
+import sys
+import subprocess
+
+
+class TestConfiguration(object):
+    """Represents a test to run."""
+    def __init__(self):
+        """Initialized from program arguments.
+        Exists with code 2 and prints usage message on invalid arguments."""
+        parser = argparse.ArgumentParser(
+            description='Runs `lfscc on a test file.')
+        parser.add_argument('lfscc_binary')
+        parser.add_argument('input')
+        parser.add_argument('include_dirs', nargs='*')
+        args = parser.parse_args()
+
+        self.lfscc = args.lfscc_binary
+        self.dep_graph = DepGraph(args.input, args.include_dirs)
+
+
+class DepGraph(object):
+    """Represents a dependency graph of LFSC input files"""
+    def __init__(self, root_path, include_dirs):
+        """Creates a dependency graph rooted a `root_path`.
+        Computes a root-last topological sort.
+        Exits with exitcode 1 on cyclic dependencies"""
+
+        # Root of the graph
+        self._r = root_path
+
+        # Nodes (paths) that have been visited
+        self._visited = set()
+
+        # Nodes (paths) that have been ordered
+        self._ordered_set = set()
+
+        # The order of nodes (paths). Root is last.
+        self._ordered_paths = []
+
+        self.include_dirs = include_dirs
+
+        # Start DFS topo-order
+        self._visit(root_path)
+
+    def _visit(self, p):
+        """Puts the descendents of p in the order, parent-last"""
+        node = TestFile(p, self.include_dirs)
+        self._visited.add(p)
+        for n in node.dep_paths:
+            if n not in self._ordered_set:
+                if n in self._visited:
+                    # Our child is is an ancestor our ours!?
+                    print("{} and {} are in a dependency cycle".format(p, n))
+                    sys.exit(1)
+                else:
+                    self._visit(n)
+        self._ordered_paths.append(p)
+        self._ordered_set.add(p)
+
+    def getPathsInOrder(self):
+        return self._ordered_paths
+
+
+class TestFile(object):
+    """Represents a testable input file to LFSC"""
+    def __init__(self, path, include_dirs):
+        """Read the file at `path` and determine its immediate dependencies"""
+        self.path = path
+        self._get_config_map()
+        self.deps = self.config_map['deps'].split() if (
+            'deps' in self.config_map) else []
+        self.dir = os.path.dirname(self.path)
+        self.dep_paths = []
+        include_paths = include_dirs + [self.dir]
+        for dep in self.deps:
+            found_dep = False
+            for include_path in include_paths:
+                dep_path = os.path.join(include_path, dep)
+                if os.path.isfile(dep_path):
+                    self.dep_paths.append(dep_path)
+                    found_dep = True
+                    break
+            assert found_dep
+
+    def _get_comment_lines(self):
+        """Return an iterator over comment lines, ;'s included"""
+        with open(self.path, 'r') as test_file:
+            return (line for line in test_file.readlines() if \
+                    re.match(r'^\s*;.*$', line) is not None)
+
+    def _get_config_map(self):
+        """Populate self.config_map.
+        Config variables are set using the syntax
+        ; Var Name Spaces Okay: space separated values"""
+        m = {}
+        for l in self._get_comment_lines():
+            match = re.match(r'^.*;\s*(\w+(?:\s+\w+)*)\s*:(.*)$', l)
+            if match is not None:
+                m[match.group(1).replace(' ', '').lower()] = match.group(2)
+        self.config_map = m
+
+
+def main():
+    configuration = TestConfiguration()
+    cmd = [configuration.lfscc] + configuration.dep_graph.getPathsInOrder()
+    result = subprocess.Popen(cmd,
+                              stderr=subprocess.STDOUT,
+                              stdout=subprocess.PIPE)
+    code = result.wait()
+    if 0 != code:
+        stdout = result.stdout.read()
+        if stdout:
+            print(stdout.decode())
+    return code
+
+
+if __name__ == '__main__':
+    sys.exit(main())
diff --git a/proofs/signatures/th_lira_test.plf b/test/signatures/th_lira_test.plf
index 91d626bba..d1fbe59f4 100644
--- a/proofs/signatures/th_lira_test.plf
+++ b/test/signatures/th_lira_test.plf
@@ -1,4 +1,4 @@
-; Depends On: th_lira.plf
+; Deps: th_lira.plf
 ;; Proof (from predicates on linear polynomials) that the following imply bottom
 ;
 ; -x - 1/2 y + 2 >= 0