3 # Morgan Deters <mdeters@cs.nyu.edu>
8 # run_regression cvc4-binary [ --proof ] [ benchmark.cvc | benchmark.smt | benchmark.smt2 ]
10 # Runs benchmark and checks for correct exit status and output.
15 if [ $# -lt 2 -o $# -gt 3 ]; then
16 echo "usage: $prog cvc4-binary [ --proof ] [ benchmark.cvc | benchmark.smt | benchmark.smt2 ]" >&2
21 if [ $1 = --proof ]; then
30 echo "$prog: error: $*"
34 if ! [ -x "$cvc4" ]; then
35 error
"\`$cvc4' doesn't exist or isn't executable" >&2
37 if ! [ -r "$benchmark" ]; then
38 error
"\`$benchmark' doesn't exist or isn't readable" >&2
41 # gettemp() and its associated tempfiles[] array are intended to never
42 # allow a temporary file to leak---the trap ensures that when this script
43 # exits, whether via a regular exit or an -INT or other signal, the
44 # temp files are deleted.
46 trap -- 'test ${#tempfiles[@]} -gt 0 && rm -f "${tempfiles[@]}"' EXIT
48 local temp
="`mktemp -t "$2"`"
49 tempfiles
[${#tempfiles[@]}]="$temp"
54 if expr "$benchmark" : '.*\.smt$' &>/dev
/null
; then
55 if test -e "$benchmark.expect"; then
56 expected_proof
=`grep -q '^% PROOF' "$benchmark.expect" && echo yes`
57 expected_output
=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'`
58 expected_error
=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'`
59 expected_exit_status
=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
60 command_line
=`grep '^% COMMAND-LINE: ' "$benchmark.expect" | sed 's,^% COMMAND-LINE: ,,'`
61 if [ -z "$expected_exit_status" ]; then
62 error
"cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
64 elif grep -q '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark"; then
65 expected_proof
=`grep -q '^% PROOF' "$benchmark" && echo yes`
66 expected_output
=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'`
67 expected_error
=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
68 expected_exit_status
=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
69 command_line
=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
70 # old mktemp from coreutils 7.x is broken, can't do XXXX in the middle
71 # this frustrates our auto-language-detection, so add explicit --lang
72 gettemp tmpbenchmark cvc4_benchmark.smt.$$.XXXXXXXXXX
73 command_line
="${command_line:+$command_line }--lang=smt"
74 grep -v '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" >"$tmpbenchmark"
75 if [ -z "$expected_exit_status" ]; then
76 error
"cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
78 benchmark
=$tmpbenchmark
79 elif grep '^ *:status *sat' "$benchmark" &>/dev
/null
; then
82 expected_exit_status
=10
84 elif grep '^ *:status *unsat' "$benchmark" &>/dev
/null
; then
87 expected_exit_status
=20
90 error
"cannot determine status of \`$benchmark'"
92 elif expr "$benchmark" : '.*\.smt2$' &>/dev
/null
; then
93 if test -e "$benchmark.expect"; then
94 expected_proof
=`grep -q '^% PROOF' "$benchmark.expect" && echo yes`
95 expected_output
=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'`
96 expected_error
=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'`
97 expected_exit_status
=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
98 command_line
=`grep '^% COMMAND-LINE: ' "$benchmark.expect" | sed 's,^% COMMAND-LINE: ,,'`
99 if [ -z "$expected_exit_status" ]; then
100 error
"cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
102 elif grep -q '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark"; then
103 expected_proof
=`grep -q '^% PROOF' "$benchmark" && echo yes`
104 expected_output
=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'`
105 expected_error
=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
106 expected_exit_status
=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
107 command_line
=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
108 # old mktemp from coreutils 7.x is broken, can't do XXXX in the middle
109 # this frustrates our auto-language-detection, so add explicit --lang
110 gettemp tmpbenchmark cvc4_benchmark.smt2.$$.XXXXXXXXXX
111 command_line
="${command_line:+$command_line }--lang=smt2"
112 grep -v '^% \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" >"$tmpbenchmark"
113 if [ -z "$expected_exit_status" ]; then
114 error
"cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
116 benchmark
=$tmpbenchmark
117 elif grep '^ *(set-info *:status *sat' "$benchmark" &>/dev
/null
; then
120 expected_exit_status
=10
122 elif grep '^ *(set-info *:status *unsat' "$benchmark" &>/dev
/null
; then
124 expected_output
=unsat
125 expected_exit_status
=20
128 error
"cannot determine status of \`$benchmark'"
130 elif expr "$benchmark" : '.*\.cvc$' &>/dev
/null
; then
131 expected_proof
=`grep -q '^% PROOF' "$benchmark" && echo yes`
132 expected_output
=$
(grep '^% EXPECT: ' "$benchmark")
133 expected_error
=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
134 if [ -z "$expected_output" -a -z "$expected_error" ]; then
135 error
"cannot determine expected output of \`$benchmark': " \
136 "please use \`% EXPECT:' and/or \`% EXPECT-ERROR:' gestures"
138 expected_output
=$
(echo "$expected_output" | perl
-pe 's,^% EXPECT: ,,;s,\r,,')
139 expected_exit_status
=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
140 if [ -z "$expected_exit_status" ]; then
141 error
"cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
143 command_line
=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
145 error
"benchmark \`$benchmark' must be *.cvc or *.smt or *.smt2"
148 gettemp expoutfile cvc4_expect_stdout.$$.XXXXXXXXXX
149 gettemp experrfile cvc4_expect_stderr.$$.XXXXXXXXXX
150 gettemp outfile cvc4_stdout.$$.XXXXXXXXXX
151 gettemp errfile cvc4_stderr.$$.XXXXXXXXXX
152 gettemp exitstatusfile cvc4_exitstatus.$$.XXXXXXXXXX
154 if [ -z "$expected_output" ]; then
155 # in case expected stdout output is empty, make sure we don't differ
156 # by a newline, which we would if we echo "" >"$expoutfile"
159 echo "$expected_output" >"$expoutfile"
161 if [ -z "$expected_error" ]; then
162 # in case expected stderr output is empty, make sure we don't differ
163 # by a newline, which we would if we echo "" >"$experrfile"
166 echo "$expected_error" >"$experrfile"
169 cvc4dir
=`dirname "$cvc4"`
170 cvc4dirfull
=`cd "$cvc4dir" && pwd`
171 if [ -z "$cvc4dirfull" ]; then
172 error
"getting directory of \`$cvc4 !?"
174 cvc4base
=`basename "$cvc4"`
175 cvc4full
="$cvc4dirfull/$cvc4base"
176 echo running
$cvc4full $CVC4_REGRESSION_ARGS $command_line --segv-nospin `basename "$benchmark"` [from working dir
`dirname "$benchmark"`]
177 ( cd `dirname "$benchmark"`;
178 "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --segv-nospin `basename "$benchmark"`;
179 echo $?
>"$exitstatusfile"
180 ) > "$outfile" 2> "$errfile"
182 diffs
=`diff -u --strip-trailing-cr "$expoutfile" "$outfile"`
184 diffserr
=`diff -u --strip-trailing-cr "$experrfile" "$errfile"`
186 exit_status
=`cat "$exitstatusfile"`
189 if [ $diffexit -ne 0 ]; then
190 echo "$prog: error: differences between expected and actual output on stdout"
194 if [ $diffexiterr -ne 0 ]; then
195 echo "$prog: error: differences between expected and actual output on stderr"
200 if [ "$exit_status" != "$expected_exit_status" ]; then
201 echo "$prog: error: expected exit status \`$expected_exit_status' but got \`$exit_status'"
205 if [ "$proof" = yes -a "$expected_proof" = yes ]; then
206 echo running
$cvc4full $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$benchmark"` [from working dir
`dirname "$benchmark"`]
207 ( cd `dirname "$benchmark"`;
208 "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$benchmark"`;
209 echo $?
>"$exitstatusfile"
210 ) > "$outfile" 2> "$errfile"
212 if [ ! -s "$outfile" ]; then
213 echo "$prog: error: proof generation failed with empty output (stderr follows)"
217 echo running
$LFSC "$outfile" [from working dir
`dirname "$benchmark"`]
218 if ! $LFSC "$outfile" &> "$errfile"; then
219 echo "$prog: error: proof checker failed (output follows)"