1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
|
#!/bin/bash
#
# Morgan Deters <mdeters@cs.nyu.edu>
# 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' "$benchmark" &>/dev/null; then
expected_output=SAT
expected_exit_status=10
elif grep '^ *:status *unsat' "$benchmark" &>/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: ,,'`
expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
if [ -z "$expected_output" -a -z "$expected_error" ]; then
error "cannot determine expected output of \`$benchmark': " \
"please use \`% EXPECT:' and/or \`% EXPECT-ERROR:' gestures"
fi
expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,'`
if [ -z "$expected_exit_status" ]; then
error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
fi
else
error "benchmark \`$benchmark' must be *.cvc or *.smt"
fi
expoutfile=`mktemp -t cvc4_expect_stdout.XXXXXXXXXX`
experrfile=`mktemp -t cvc4_expect_stderr.XXXXXXXXXX`
outfile=`mktemp -t cvc4_stdout.XXXXXXXXXX`
errfile=`mktemp -t cvc4_stderr.XXXXXXXXXX`
exitstatusfile=`mktemp -t cvc4_exitstatus.XXXXXXXXXX`
if [ -z "$expected_output" ]; then
# in case expected stdout output is empty, make sure we don't differ
# by a newline, which we would if we echo "" >"$expoutfile"
touch "$expoutfile"
else
echo "$expected_output" >"$expoutfile"
fi
if [ -z "$expected_error" ]; then
# in case expected stderr output is empty, make sure we don't differ
# by a newline, which we would if we echo "" >"$experrfile"
touch "$experrfile"
else
echo "$expected_error" >"$experrfile"
fi
cvc4dir=`dirname "$cvc4"`
cvc4dirfull=`cd "$cvc4dir" && pwd`
if [ -z "$cvc4dirfull" ]; then
error "getting directory of \`$cvc4 !?"
fi
cvc4base=`basename "$cvc4"`
cvc4full="$cvc4dirfull/$cvc4base"
( cd `dirname "$benchmark"`;
"$cvc4full" --segv-nospin `basename "$benchmark"`;
echo $? >"$exitstatusfile"
) > "$outfile" 2> "$errfile"
diffs=`diff -u "$expoutfile" "$outfile"`
diffexit=$?
diffserr=`diff -u "$experrfile" "$errfile"`
diffexiterr=$?
exit_status=`cat "$exitstatusfile"`
rm -f "$expoutfile"
rm -f "$experrfile"
rm -f "$outfile"
rm -f "$errfile"
rm -f "$exitstatusfile"
exitcode=0
if [ $diffexit -ne 0 ]; then
echo "$prog: error: differences between expected and actual output on stdout"
echo "$diffs"
exitcode=1
fi
if [ $diffexiterr -ne 0 ]; then
echo "$prog: error: differences between expected and actual output on stderr"
echo "$diffserr"
exitcode=1
fi
if [ "$exit_status" != "$expected_exit_status" ]; then
echo "$prog: error: expected exit status \`$expected_exit_status' but got \`$exit_status'"
exitcode=1
fi
exit $exitcode
|
