From 9ce4c3153d42bc079470b7bd73bf131499b3fcbe Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 1 Jul 2020 08:44:21 -0700 Subject: [PATCH] Add testing infrastructure for LFSC signatures (#4678) 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 --- cmake/FindLFSC.cmake | 8 +- proofs/signatures/drat.plf | 2 +- proofs/signatures/er.plf | 2 +- proofs/signatures/lrat.plf | 2 +- proofs/signatures/smt.plf | 2 +- proofs/signatures/th_arrays.plf | 2 +- proofs/signatures/th_base.plf | 2 +- proofs/signatures/th_lira.plf | 2 +- proofs/signatures/th_real.plf | 2 +- test/CMakeLists.txt | 4 + test/signatures/CMakeLists.txt | 33 +++++ test/signatures/README.md | 32 +++++ {proofs => test}/signatures/drat_test.plf | 2 +- {proofs => test}/signatures/er_test.plf | 2 +- {proofs => test}/signatures/ex-mem.plf | 2 + {proofs => test}/signatures/ex_bv.plf | 2 + .../signatures/example-arrays.plf | 2 +- {proofs => test}/signatures/example-quant.plf | 2 +- {proofs => test}/signatures/example.plf | 2 +- {proofs => test}/signatures/lrat_test.plf | 1 + test/signatures/run_test.py | 123 ++++++++++++++++++ {proofs => test}/signatures/th_lira_test.plf | 2 +- 22 files changed, 216 insertions(+), 17 deletions(-) create mode 100644 test/signatures/CMakeLists.txt create mode 100644 test/signatures/README.md rename {proofs => test}/signatures/drat_test.plf (99%) rename {proofs => test}/signatures/er_test.plf (99%) rename {proofs => test}/signatures/ex-mem.plf (97%) rename {proofs => test}/signatures/ex_bv.plf (96%) rename {proofs => test}/signatures/example-arrays.plf (97%) rename {proofs => test}/signatures/example-quant.plf (96%) rename {proofs => test}/signatures/example.plf (97%) rename {proofs => test}/signatures/lrat_test.plf (99%) create mode 100755 test/signatures/run_test.py rename {proofs => test}/signatures/th_lira_test.plf (99%) 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 similarity index 99% rename from proofs/signatures/drat_test.plf rename to 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 similarity index 99% rename from proofs/signatures/er_test.plf rename to 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 similarity index 97% rename from proofs/signatures/ex-mem.plf rename to 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 similarity index 96% rename from proofs/signatures/ex_bv.plf rename to 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 similarity index 97% rename from proofs/signatures/example-arrays.plf rename to 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 similarity index 96% rename from proofs/signatures/example-quant.plf rename to 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 similarity index 97% rename from proofs/signatures/example.plf rename to 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 similarity index 99% rename from proofs/signatures/lrat_test.plf rename to 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 similarity index 99% rename from proofs/signatures/th_lira_test.plf rename to 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 -- 2.30.2