From 3203c9bf8ec818b287c8b4030bb4b71d48ede9f1 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 4 Feb 2010 19:01:55 +0000 Subject: [PATCH] test infrastructure updated for multiple-level regressions --- Makefile | 4 +- Makefile.subdir | 4 +- configure.ac | 4 ++ test/Makefile | 4 +- test/Makefile.am | 4 +- test/regress/Makefile | 4 +- test/regress/Makefile.am | 49 ++------------------ test/regress/regress0/Makefile | 8 ++++ test/regress/regress0/Makefile.am | 10 ++++ test/regress/regress1/Makefile | 8 ++++ test/regress/regress1/Makefile.am | 10 ++++ test/regress/regress2/Makefile | 8 ++++ test/regress/regress2/Makefile.am | 10 ++++ test/regress/regress3/Makefile | 8 ++++ test/regress/regress3/Makefile.am | 10 ++++ test/regress/run_regression | 77 +++++++++++++++++++++++++++++++ test/system/Makefile | 4 +- test/system/Makefile.am | 4 +- test/unit/Makefile | 4 +- test/unit/Makefile.am | 4 +- 20 files changed, 174 insertions(+), 64 deletions(-) create mode 100644 test/regress/regress0/Makefile create mode 100644 test/regress/regress0/Makefile.am create mode 100644 test/regress/regress1/Makefile create mode 100644 test/regress/regress1/Makefile.am create mode 100644 test/regress/regress2/Makefile create mode 100644 test/regress/regress2/Makefile.am create mode 100644 test/regress/regress3/Makefile create mode 100644 test/regress/regress3/Makefile.am create mode 100755 test/regress/run_regression diff --git a/Makefile b/Makefile index 061f3d8d1..7e0e0261b 100644 --- a/Makefile +++ b/Makefile @@ -15,5 +15,5 @@ all %: fi # synonyms for "check" -.PHONY: regress regress0 regress1 regress2 regress3 test -regress regress0 regress1 regress2 regress3 test: check +.PHONY: regress test +regress test: check diff --git a/Makefile.subdir b/Makefile.subdir index 1ac8357f6..5b151441e 100644 --- a/Makefile.subdir +++ b/Makefile.subdir @@ -33,5 +33,5 @@ check: fi # synonyms for "check" -.PHONY: regress regress0 regress1 regress2 regress3 test -regress regress0 regress1 regress2 regress3 test: check +.PHONY: regress test +regress test: check diff --git a/configure.ac b/configure.ac index 1c170dbe6..159f32a4e 100644 --- a/configure.ac +++ b/configure.ac @@ -443,6 +443,10 @@ AC_CONFIG_FILES([ src/theory/arith/Makefile test/Makefile test/regress/Makefile + test/regress/regress0/Makefile + test/regress/regress1/Makefile + test/regress/regress2/Makefile + test/regress/regress3/Makefile test/system/Makefile test/unit/Makefile ]) diff --git a/test/Makefile b/test/Makefile index fa1dcec3a..45659ae1e 100644 --- a/test/Makefile +++ b/test/Makefile @@ -4,5 +4,5 @@ srcdir = test include $(topdir)/Makefile.subdir # synonyms for "check" -.PHONY: regress regress0 regress1 regress2 regress3 test -regress regress0 regress1 regress2 regress3 test: check +.PHONY: regress test +regress test: check diff --git a/test/Makefile.am b/test/Makefile.am index 13f12edf7..575d07b77 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -1,5 +1,5 @@ SUBDIRS = unit system regress # synonyms for "check" -.PHONY: regress regress0 regress1 regress2 regress3 test -regress regress0 regress1 regress2 regress3 test: check +.PHONY: regress test +regress test: check diff --git a/test/regress/Makefile b/test/regress/Makefile index 06fe0f1fb..663fc1407 100644 --- a/test/regress/Makefile +++ b/test/regress/Makefile @@ -4,5 +4,5 @@ srcdir = test/regress include $(topdir)/Makefile.subdir # synonyms for "check" -.PHONY: regress regress0 regress1 regress2 regress3 test -regress regress0 regress1 regress2 regress3 test: check +.PHONY: test +test: check diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am index 819a892bd..bec1fce3e 100644 --- a/test/regress/Makefile.am +++ b/test/regress/Makefile.am @@ -1,48 +1,5 @@ -TESTS_ENVIRONMENT = @top_builddir@/../../bin/cvc4 -TESTS = \ - simple.cvc \ - simple.smt \ - hole6.cvc \ - hole7.cvc \ - hole8.cvc \ - hole9.cvc \ - hole10.cvc \ - wiki.cvc \ - test9.cvc \ - test11.cvc \ - bmc-ibm-1.smt \ - bmc-ibm-2.smt \ - bmc-ibm-3.smt \ - bmc-ibm-4.smt \ - bmc-ibm-5.smt \ - uf20-03.cvc \ - qwh.35.405.shuffled-as.sat03-1651.smt \ - C880mul.miter.shuffled-as.sat03-348.smt \ - instance_1151.smt \ - instance_1444.smt - -#Tests that currently do not work -FUTURETESTS = \ - logops.cvc \ - test12.cvc \ - bug1.cvc \ - boolean.cvc - -#Tests that take too long to be put in the default regress level -#TODO Make multiple regression levels. Some of which are off by default. -LONGTESTS = \ - friedman_n4_i5.smt \ - friedman_n6_i4.smt \ - bmc-galileo-8.smt \ - bmc-galileo-9.smt \ - bmc-ibm-6.smt \ - bmc-ibm-7.smt \ - bmc-ibm-10.smt \ - bmc-ibm-11.smt \ - bmc-ibm-12.smt \ - bmc-ibm-13.smt \ - comb2.shuffled-as.sat03-420.smt +SUBDIRS = regress0 regress1 regress2 regress3 # synonyms for "check" -.PHONY: regress regress0 regress1 regress2 regress3 test -regress regress0 regress1 regress2 regress3 test: check +.PHONY: regress test +regress test: check diff --git a/test/regress/regress0/Makefile b/test/regress/regress0/Makefile new file mode 100644 index 000000000..894759aa3 --- /dev/null +++ b/test/regress/regress0/Makefile @@ -0,0 +1,8 @@ +topdir = ../../.. +srcdir = test/regress/regress0 + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am new file mode 100644 index 000000000..b0caacf1b --- /dev/null +++ b/test/regress/regress0/Makefile.am @@ -0,0 +1,10 @@ +TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4 +TESTS = + +# synonyms for "check" +.PHONY: regress regress0 test +regress regress0 test: check + +# do nothing in this subdir +.PHONY: regress1 regress2 regress3 +regress1 regress2 regress3: diff --git a/test/regress/regress1/Makefile b/test/regress/regress1/Makefile new file mode 100644 index 000000000..b720980f1 --- /dev/null +++ b/test/regress/regress1/Makefile @@ -0,0 +1,8 @@ +topdir = ../../.. +srcdir = test/regress/regress1 + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am new file mode 100644 index 000000000..a99ed3f70 --- /dev/null +++ b/test/regress/regress1/Makefile.am @@ -0,0 +1,10 @@ +TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4 +TESTS = + +# synonyms for "check" +.PHONY: regress regress1 test +regress regress1 test: check + +# do nothing in this subdir +.PHONY: regress0 regress2 regress3 +regress0 regress2 regress3: diff --git a/test/regress/regress2/Makefile b/test/regress/regress2/Makefile new file mode 100644 index 000000000..5a9aa63be --- /dev/null +++ b/test/regress/regress2/Makefile @@ -0,0 +1,8 @@ +topdir = ../../.. +srcdir = test/regress/regress2 + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am new file mode 100644 index 000000000..72742f201 --- /dev/null +++ b/test/regress/regress2/Makefile.am @@ -0,0 +1,10 @@ +TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4 +TESTS = + +# synonyms for "check" +.PHONY: regress regress2 test +regress regress2 test: check + +# do nothing in this subdir +.PHONY: regress0 regress1 regress3 +regress0 regress1 regress3: diff --git a/test/regress/regress3/Makefile b/test/regress/regress3/Makefile new file mode 100644 index 000000000..223547305 --- /dev/null +++ b/test/regress/regress3/Makefile @@ -0,0 +1,8 @@ +topdir = ../../.. +srcdir = test/regress/regress3 + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am new file mode 100644 index 000000000..202bc553f --- /dev/null +++ b/test/regress/regress3/Makefile.am @@ -0,0 +1,10 @@ +TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4 +TESTS = + +# synonyms for "check" +.PHONY: regress regress3 test +regress regress3 test: check + +# do nothing in this subdir +.PHONY: regress0 regress1 regress2 +regress0 regress1 regress2: diff --git a/test/regress/run_regression b/test/regress/run_regression new file mode 100755 index 000000000..4cf9f07cf --- /dev/null +++ b/test/regress/run_regression @@ -0,0 +1,77 @@ +#!/bin/bash +# +# Morgan Deters +# for the CVC4 project +# +# usage: +# +# run_regression cvc4-binary [ benchmark.cvc | benchmark.smt ] +# +# 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 ]" >&2 + exit 1 +fi + +cvc4=$1 +benchmark=$2 + +function error { + echo "$prog: error: $*" + exit 1 +} + +if ! [ -x "$cvc4" ]; then + error "\`$cvc4' doesn't exist or isn't executable" >&2 +fi +if ! [ -r "$benchmark" ]; then + error "\`$benchmark' doesn't exist or isn't readable" >&2 +fi + +if expr "$benchmark" : '.*\.smt$' &>/dev/null; then + if grep '^ *:status *sat' &>/dev/null; then + expected_output=sat + expected_exit_status=10 + elif grep '^ *:status *unsat' &>/dev/null; then + expected_output=unsat + expected_exit_status=20 + else + error "cannot determine status of \`$benchmark'" + fi +elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then + expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'` + if [ -z "$expected_output" ]; then + error "cannot determine status of \`$benchmark'" + fi + expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,'` +else + error "benchmark \`$benchmark' must be *.cvc or *.smt" +fi + +expfile=`mktemp -t cvc4test.exp.XXXXXXXXXX` +outfile=`mktemp -t cvc4test.out.XXXXXXXXXX` +echo "$expected_output" >"$expfile" + +echo "$cvc4" --segv-nospin "$benchmark" +"$cvc4" --segv-nospin "$benchmark" | tee "$outfile" +exit_status=$? + +diffs=`diff -u "$expfile" "$outfile"` +rm -f "$expfile" +rm -f "$outfile" +if [ $? -ne 0 ]; then + echo "$prog: error: differences between expected and actual output" + echo "$diffs" + exit 1 +fi + +if [ -n "$expected_exit_status" ]; then + if [ $exit_status != "$expected_exit_status" ]; then + error "expected exit status \`$expected_exit_status' but got \`$exit_status'" + fi +fi + diff --git a/test/system/Makefile b/test/system/Makefile index c1dc3ef2f..2ca4091cb 100644 --- a/test/system/Makefile +++ b/test/system/Makefile @@ -4,5 +4,5 @@ srcdir = test/system include $(topdir)/Makefile.subdir # synonyms for "check" -.PHONY: regress regress0 regress1 regress2 regress3 test -regress regress0 regress1 regress2 regress3 test: check +.PHONY: regress test +regress test: check diff --git a/test/system/Makefile.am b/test/system/Makefile.am index 5e9cca17a..2aba75e1c 100644 --- a/test/system/Makefile.am +++ b/test/system/Makefile.am @@ -26,5 +26,5 @@ EXTRA_DIST = \ $(TESTS):: $(TEST_DEPS) # synonyms for "check" -.PHONY: regress regress0 regress1 regress2 regress3 test -regress regress0 regress1 regress2 regress3 test: check +.PHONY: regress test +regress test: check diff --git a/test/unit/Makefile b/test/unit/Makefile index b8a801378..94a9d1d9e 100644 --- a/test/unit/Makefile +++ b/test/unit/Makefile @@ -4,5 +4,5 @@ srcdir = test/unit include $(topdir)/Makefile.subdir # synonyms for "check" -.PHONY: regress regress0 regress1 regress2 regress3 test -regress regress0 regress1 regress2 regress3 test: check +.PHONY: regress test +regress test: check diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index eeed1f393..1908f909d 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -84,5 +84,5 @@ EXTRA_DIST = \ endif # synonyms for "check" -.PHONY: regress regress0 regress1 regress2 regress3 test -regress regress0 regress1 regress2 regress3 test: check +.PHONY: regress test +regress test: check -- 2.30.2