test/regress/run_regression

   1 #!/bin/bash
   2 #
   3 # Morgan Deters <mdeters@cs.nyu.edu>
   4 # for the CVC4 project
   5 #
   6 # usage:
   7 #
   8 #     run_regression cvc4-binary [ --proof ] [ benchmark.cvc | benchmark.smt | benchmark.smt2 ]
   9 #
  10 # Runs benchmark and checks for correct exit status and output.
  11 #
  12
  13 prog=`basename "$0"`
  14
  15 if [ $# -lt 2 -o $# -gt 3 ]; then
  16   echo "usage: $prog cvc4-binary [ --proof ] [ benchmark.cvc | benchmark.smt | benchmark.smt2 ]" >&2
  17   exit 1
  18 fi
  19
  20 proof=no
  21 if [ $1 = --proof ]; then
  22   proof=yes
  23   shift
  24 fi
  25
  26 cvc4=$1
  27 benchmark=$2
  28
  29 function error {
  30   echo "$prog: error: $*"
  31   exit 1
  32 }
  33
  34 if ! [ -x "$cvc4" ]; then
  35   error "\`$cvc4' doesn't exist or isn't executable" >&2
  36 fi
  37 if ! [ -r "$benchmark" ]; then
  38   error "\`$benchmark' doesn't exist or isn't readable" >&2
  39 fi
  40
  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.
  45 declare -a tempfiles
  46 trap -- 'test ${#tempfiles[@]} -gt 0 && rm -f "${tempfiles[@]}"' EXIT
  47 function gettemp {
  48   local temp="`mktemp -t "$2"`"
  49   tempfiles[${#tempfiles[@]}]="$temp"
  50   eval "$1"="$temp"
  51 }
  52
  53 tmpbenchmark=
  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"
  63     fi
  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"
  77     fi
  78     benchmark=$tmpbenchmark
  79   elif grep '^ *:status  *sat' "$benchmark" &>/dev/null; then
  80     expected_proof=
  81     expected_output=sat
  82     expected_exit_status=10
  83     command_line=
  84   elif grep '^ *:status  *unsat' "$benchmark" &>/dev/null; then
  85     expected_proof=
  86     expected_output=unsat
  87     expected_exit_status=20
  88     command_line=
  89   else
  90     error "cannot determine status of \`$benchmark'"
  91   fi
  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"
 101     fi
 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"
 115     fi
 116     benchmark=$tmpbenchmark
 117   elif grep '^ *(set-info  *:status  *sat' "$benchmark" &>/dev/null; then
 118     expected_proof=
 119     expected_output=sat
 120     expected_exit_status=10
 121     command_line=
 122   elif grep '^ *(set-info  *:status  *unsat' "$benchmark" &>/dev/null; then
 123     expected_proof=
 124     expected_output=unsat
 125     expected_exit_status=20
 126     command_line=
 127   else
 128     error "cannot determine status of \`$benchmark'"
 129   fi
 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"
 137   fi
 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"
 142   fi
 143   command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
 144 else
 145   error "benchmark \`$benchmark' must be *.cvc or *.smt or *.smt2"
 146 fi
 147
 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
 153
 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"
 157   touch "$expoutfile"
 158 else
 159   echo "$expected_output" >"$expoutfile"
 160 fi
 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"
 164   touch "$experrfile"
 165 else
 166   echo "$expected_error" >"$experrfile"
 167 fi
 168
 169 cvc4dir=`dirname "$cvc4"`
 170 cvc4dirfull=`cd "$cvc4dir" && pwd`
 171 if [ -z "$cvc4dirfull" ]; then
 172   error "getting directory of \`$cvc4 !?"
 173 fi
 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"
 181
 182 diffs=`diff -u --strip-trailing-cr "$expoutfile" "$outfile"`
 183 diffexit=$?
 184 diffserr=`diff -u --strip-trailing-cr "$experrfile" "$errfile"`
 185 diffexiterr=$?
 186 exit_status=`cat "$exitstatusfile"`
 187
 188 exitcode=0
 189 if [ $diffexit -ne 0 ]; then
 190   echo "$prog: error: differences between expected and actual output on stdout"
 191   echo "$diffs"
 192   exitcode=1
 193 fi
 194 if [ $diffexiterr -ne 0 ]; then
 195   echo "$prog: error: differences between expected and actual output on stderr"
 196   echo "$diffserr"
 197   exitcode=1
 198 fi
 199
 200 if [ "$exit_status" != "$expected_exit_status" ]; then
 201   echo "$prog: error: expected exit status \`$expected_exit_status' but got \`$exit_status'"
 202   exitcode=1
 203 fi
 204
 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"
 211
 212   if [ ! -s "$outfile" ]; then
 213     echo "$prog: error: proof generation failed with empty output (stderr follows)"
 214     cat "$errfile"
 215     exitcode=1
 216   else
 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)"
 220       cat "$errfile"
 221       exitcode=1
 222     fi
 223   fi
 224 fi
 225
 226 exit $exitcode