From b695ce10f294b2469434656fb2c5dc8e6d701c5d Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 28 Oct 2011 22:08:55 +0000 Subject: [PATCH] proof regressions --- configure.ac | 20 ++++++++++++- test/regress/regress0/Makefile.am | 5 ++++ test/regress/regress0/boolean.cvc | 1 + test/regress/regress0/hole6.cvc | 1 + test/regress/regress0/wiki.05.cvc | 1 + test/regress/run_regression | 50 ++++++++++++++++++++++++++----- 6 files changed, 70 insertions(+), 8 deletions(-) diff --git a/configure.ac b/configure.ac index 922f65416..729544391 100644 --- a/configure.ac +++ b/configure.ac @@ -478,7 +478,6 @@ if test "$enable_proof" = yes; then CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROOF" fi - AC_MSG_CHECKING([whether to optimize libcvc4]) AC_ARG_ENABLE([optimized], @@ -722,6 +721,24 @@ if test "$CVC4_CONFIGURE_IN_BUILDS" = yes -a -n "$CXXTEST"; then esac fi +AC_ARG_VAR(LFSC, [path to LFSC proof checker]) +AC_ARG_VAR(LFSCARGS, [arguments to pass to LFSC proof checker]) +if test -z "$LFSC"; then + AC_CHECK_PROGS(LFSC, lfsc, [], []) +else + AC_CHECK_PROG(LFSC, "$LFSC", [], []) +fi +AM_CONDITIONAL([PROOF_REGRESSIONS], [test -n "$LFSC" -a "$enable_proof" = yes]) +if test -z "$LFSC"; then + support_proof_tests='no, lfsc proof checker unavailable' +elif test "$enable_proof" = yes; then + support_proof_tests='yes, proof regression tests enabled' +else + support_proof_tests='no, proof generation disabled for this build' +fi +AC_SUBST([LFSC]) +AC_SUBST([LFSCARGS]) + CXXTESTGEN= AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH]) if test -z "$CXXTESTGEN"; then @@ -1061,6 +1078,7 @@ Dumping : $enable_dumping Muzzle : $enable_muzzle Unit tests : $support_unit_tests +Proof tests : $support_proof_tests gcov support : $enable_coverage gprof support: $enable_profiling CUDD : $cvc4cudd diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 948731057..3a4583805 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,6 +1,11 @@ SUBDIRS = . arith precedence uf uflra bv arrays datatypes lemmas push-pop preprocess +if PROOF_REGRESSIONS +TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/cvc4 +else TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4 +endif + MAKEFLAGS = -k # These are run for all build profiles. diff --git a/test/regress/regress0/boolean.cvc b/test/regress/regress0/boolean.cvc index fe3450c27..d6f428bdb 100644 --- a/test/regress/regress0/boolean.cvc +++ b/test/regress/regress0/boolean.cvc @@ -805,3 +805,4 @@ a288 : BOOLEAN = ENDIF; QUERY a288; % EXIT: 20 +% PROOF diff --git a/test/regress/regress0/hole6.cvc b/test/regress/regress0/hole6.cvc index 64231aaf5..31204a6c1 100644 --- a/test/regress/regress0/hole6.cvc +++ b/test/regress/regress0/hole6.cvc @@ -178,3 +178,4 @@ ASSERT x_42 OR x_41 OR x_40 OR x_39 OR x_38 OR x_37; QUERY FALSE; % EXIT: 20 +% PROOF diff --git a/test/regress/regress0/wiki.05.cvc b/test/regress/regress0/wiki.05.cvc index 9469a9902..1aedcbe2b 100644 --- a/test/regress/regress0/wiki.05.cvc +++ b/test/regress/regress0/wiki.05.cvc @@ -3,3 +3,4 @@ a, b, c : BOOLEAN; % EXPECT: valid QUERY a OR (a AND b) <=> a; % EXIT: 20 +% PROOF diff --git a/test/regress/run_regression b/test/regress/run_regression index 28bb5cb42..b836b39f6 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -5,18 +5,24 @@ # # usage: # -# run_regression cvc4-binary [ benchmark.cvc | benchmark.smt | benchmark.smt2 ] +# run_regression cvc4-binary [ --proof ] [ benchmark.cvc | benchmark.smt | benchmark.smt2 ] # # Runs benchmark and checks for correct exit status and output. # prog=`basename "$0"` -if [ $# != 2 ]; then - echo "usage: $prog cvc4-binary [ benchmark.cvc | benchmark.smt | benchmark.smt2 ]" >&2 +if [ $# -lt 2 -o $# -gt 3 ]; then + echo "usage: $prog cvc4-binary [ --proof ] [ benchmark.cvc | benchmark.smt | benchmark.smt2 ]" >&2 exit 1 fi +proof=no +if [ $1 = --proof ]; then + proof=yes + shift +fi + cvc4=$1 benchmark=$2 @@ -47,6 +53,7 @@ function gettemp { tmpbenchmark= if expr "$benchmark" : '.*\.smt$' &>/dev/null; then if test -e "$benchmark.expect"; then + expected_proof=`grep -q '^% PROOF' "$benchmark.expect" && echo yes` expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'` @@ -54,7 +61,8 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then if [ -z "$expected_exit_status" ]; then error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture" fi - elif grep -q '^% \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark"; then + elif grep -q '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark"; then + expected_proof=`grep -q '^% PROOF' "$benchmark" && echo yes` expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'` @@ -63,16 +71,18 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then # this frustrates our auto-language-detection, so add explicit --lang gettemp tmpbenchmark cvc4_benchmark.smt.$$.XXXXXXXXXX command_line="${command_line:+$command_line }--lang=smt" - grep -v '^% \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" >"$tmpbenchmark" + grep -v '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" >"$tmpbenchmark" if [ -z "$expected_exit_status" ]; then error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture" fi benchmark=$tmpbenchmark elif grep '^ *:status *sat' "$benchmark" &>/dev/null; then + expected_proof= expected_output=sat expected_exit_status=10 command_line= elif grep '^ *:status *unsat' "$benchmark" &>/dev/null; then + expected_proof= expected_output=unsat expected_exit_status=20 command_line= @@ -81,6 +91,7 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then fi elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then if test -e "$benchmark.expect"; then + expected_proof=`grep -q '^% PROOF' "$benchmark.expect" && echo yes` expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'` @@ -88,7 +99,8 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then if [ -z "$expected_exit_status" ]; then error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture" fi - elif grep -q '^% \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark"; then + elif grep -q '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark"; then + expected_proof=`grep -q '^% PROOF' "$benchmark" && echo yes` expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'` @@ -103,10 +115,12 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then fi benchmark=$tmpbenchmark elif grep '^ *(set-info *:status *sat' "$benchmark" &>/dev/null; then + expected_proof= expected_output=sat expected_exit_status=10 command_line= elif grep '^ *(set-info *:status *unsat' "$benchmark" &>/dev/null; then + expected_proof= expected_output=unsat expected_exit_status=20 command_line= @@ -114,6 +128,7 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then error "cannot determine status of \`$benchmark'" fi elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then + expected_proof=`grep -q '^% PROOF' "$benchmark" && echo yes` expected_output=$(grep '^% EXPECT: ' "$benchmark") expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` if [ -z "$expected_output" -a -z "$expected_error" ]; then @@ -183,8 +198,29 @@ if [ $diffexiterr -ne 0 ]; then fi if [ "$exit_status" != "$expected_exit_status" ]; then - echo "$prog: error: expected exit status \`$expected_exit_status' but got \`$exit_status'" + echo "$prog: error: expected exit status \`$expected_exit_status' but got \`$exit_status'" exitcode=1 fi +if [ "$proof" = yes -a "$expected_proof" = yes ]; then + echo running $cvc4full $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$benchmark"` [from working dir `dirname "$benchmark"`] + ( cd `dirname "$benchmark"`; + "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$benchmark"`; + echo $? >"$exitstatusfile" + ) > "$outfile" 2> "$errfile" + + if [ ! -s "$outfile" ]; then + echo "$prog: error: proof generation failed with empty output (stderr follows)" + cat "$errfile" + exitcode=1 + else + echo running $LFSC "$outfile" [from working dir `dirname "$benchmark"`] + if ! $LFSC "$outfile" &> "$errfile"; then + echo "$prog: error: proof checker failed (output follows)" + cat "$errfile" + exitcode=1 + fi + fi +fi + exit $exitcode -- 2.30.2