bench/check-ce-bench

   1 #!/bin/bash
   2 set -euo pipefail
   3
   4
   5 ################################################################################
   6 # Global variables & utility functions
   7
   8 SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" &> /dev/null && pwd)"
   9 readonly SCRIPT_DIR
  10
  11 # Currently the script only works if it is run in this directory.
  12 # TODO Change this dirty workaround.
  13 cd "$SCRIPT_DIR/.."
  14
  15 # Suffix that is appened on the Why3 excecutable name
  16 SUFFIX=.opt
  17
  18 updateoracle=false
  19 removeoutfile=true
  20 debug=false
  21 files=""
  22 petiot=1
  23 failed=""
  24
  25 function usage() {
  26   cat <<EOF
  27 Usage: $(basename "$0") [OPTIONS...] <files>"
  28
  29 Run the check-ce tests on the given <files>.
  30 <files> must be given without the '.mlw' suffix.
  31 If <files> is empty, use all files from directory 'check-ce'.
  32
  33 Options:
  34   -h | -help | --help
  35     Prints this help text.
  36
  37   --update-oracle
  38     Update the oracles during the run of tests suite.
  39
  40   --keep-out-files
  41     Remove out files.
  42
  43   --suffix <s>
  44     The suffix <s> is appended on the Why3 executable name, e.g. '.opt'.
  45     Default: $SUFFIX
  46
  47   --debug
  48     Prints the why3 command used
  49 EOF
  50 }
  51
  52 ################################################################################
  53 # Parse options
  54
  55 while test $# != 0; do
  56   case "$1" in
  57     -h | -help | --help)
  58       usage
  59       exit 0
  60       ;;
  61     --update-oracle)
  62       updateoracle=true
  63       shift 1
  64       ;;
  65     --keep-out-files)
  66       removeoutfile=false
  67       shift 1
  68       ;;
  69     --suffix)
  70       SUFFIX="$2"
  71       shift 2
  72       ;;
  73     --debug)
  74       debug=true
  75       shift 1
  76       ;;
  77     "-"*)
  78       echo "unknown option: $1"
  79       usage
  80       exit 2
  81       ;;
  82     "petiot")
  83         files="$files "
  84         petiot=2
  85         shift 1
  86         ;;
  87     *)
  88         files="$files $1"
  89         if test "$petiot" = 1; then
  90             petiot=0
  91         fi
  92       shift 1
  93   esac
  94 done
  95
  96 # If files is empty, use all files from directory 'check-ce'.
  97 if test "$files" = "" ; then
  98   files="$SCRIPT_DIR/check-ce/*.mlw"
  99 fi
 100
 101 readonly SUFFIX
 102 readonly removeoutfile
 103 readonly updateoracle
 104 readonly files
 105 readonly petiot
 106
 107 # Path to the why3 binary
 108 WHY3_BIN="$SCRIPT_DIR"/../bin/why3"$SUFFIX"
 109 whydata=$("$WHY3_BIN" --print-datadir)
 110 whylib=$("$WHY3_BIN" --print-libdir)
 111 readonly WHY3_BIN
 112 readonly whydata
 113 readonly whylib
 114
 115
 116 colorize() {
 117   if command -v pygmentize &> /dev/null; then
 118     pygmentize -ldiff
 119   else
 120     cat
 121   fi
 122 }
 123
 124 remove_solver_details () {
 125    sed -e "s|$whydata|WHY3DATA|g" -e "s|$whylib|WHY3LIB|g" \
 126    | sed 's/ ([0-9.]\+\.[0-9]\+s, / (/' \
 127 #  | sed 's/ ([0-9.]\+\.[0-9]\+s, [0-9]\+ steps)\.$/\./' \
 128 #  | sed 's/Prover result is: \(Timeout\.\|Unknown (\(unknown\|incomplete\|unknown + \(incomplete\|interrupted\)\))\.\|Out of memory.\|Step limit exceeded\.\|Step limit exceeded ([^)]*)\.\)$/Prover result is: Unknown or time\/memory\/step limit./'
 129 }
 130
 131
 132 record_time () {
 133     elapsed=$(date +%s%N)
 134 }
 135
 136 # print elapsed time
 137 elapsed_time () {
 138     t=$(date +%s%N)
 139     d=$(expr $t - $elapsed)
 140 #    printf "d=${d}\n"
 141     l=$(expr length $d)
 142 #    printf "l=${l}\n"
 143     lmn=$(expr $l - 9 || true)
 144     if [ "$lmn" = "0" ] ; then
 145         d=0"$d"
 146         lmn=1
 147     fi
 148 #    printf "lmn=${lmn}\n"
 149     s=$(expr substr "${d}" 1 ${lmn} || true)
 150 #    printf "s=${s}\n"
 151     c=$(expr substr "${d}" ${lmn} 2 || true)
 152 #    printf "c=${c}\n"
 153     elapsed="$s"."$c"
 154 #    printf "${elapsed}\n"
 155 }
 156
 157
 158
 159
 160 # $1 = prover
 161 # $2 = dir
 162 # $3 = filename
 163 # $4 = true for WP, false for SP
 164 # $5 = steps
 165 # $6 = racsteps
 166 run () {
 167   file_path="$2/$3"
 168   debug_vc_sp=""
 169   if $4; then
 170     f="${file_path}_$1_WP"
 171     oracle_file="$2/oracles/$3_$1_WP.oracle"
 172     printf "${file_path},WP,$1... "
 173   else
 174     f="${file_path}_$1_SP"
 175     oracle_file="$2/oracles/$3_$1_SP.oracle"
 176     debug_vc_sp=",vc_sp"
 177     printf "${file_path},SP,$1... "
 178   fi
 179   steps=$5
 180   racsteps=$6
 181   if [ "$3" = "strings" ] && [[ $1 == CVC* ]] ; then
 182       prover="$1,strings+counterexamples"
 183   else
 184     prover="$1,counterexamples"
 185   fi
 186   # one may add reduction_cont_size,stack_trace, in
 187   # the debug flags below to test cont_invariant in reduction engine
 188   # (note that stack trace may be more detailed with bytecode)
 189   record_time
 190   cmd="$WHY3_BIN prove -a split_vc -P $prover \
 191       --stepslimit=$steps --timelimit=5 \
 192       --rac-steplimit=$racsteps --rac-timelimit=2 \
 193       --check-ce --rac-prover=$1 --ce-log-verbosity=5 \
 194       --library=$2 ${file_path}.mlw \
 195       --debug=check_ce:categorization${debug_vc_sp}"
 196   record_time
 197   if $debug; then echo $cmd ; fi
 198   ($cmd || true) 2>&1 \
 199     | remove_solver_details \
 200           > "$f.out"
 201   elapsed_time
 202   str_out=$(cat "$f.out")
 203   if [ -e "$oracle_file" ]; then
 204     str_oracle=$(cat "$oracle_file")
 205   else
 206     str_oracle=""
 207   fi
 208   if [ "$str_oracle" = "$str_out" ] ; then
 209     echo "OK (in ${elapsed}s)"
 210   else
 211     if $updateoracle; then
 212       echo "Updating oracle (in ${elapsed}s)"
 213       cp "$f.out" "${oracle_file}"
 214     else
 215       echo "FAILED"
 216       echo "diff is the following:"
 217             (diff -u "$oracle_file" "$f.out" \
 218         || [ $? -eq 1 ])|colorize
 219       failed="$failed$f\n"
 220     fi
 221   fi
 222   if $removeoutfile; then
 223     rm "$f.out"
 224   fi
 225 }
 226
 227
 228
 229 start=$(date +%s)
 230 for file in $files; do
 231   filedir="$(realpath --relative-to="$PWD" $(dirname $file))"
 232   filebase=`basename $file .mlw`
 233     printf "# Running provers on $filedir/$filebase.mlw\n";
 234     altergosteps=10000
 235     altergostepsrac=$altergosteps
 236     skipae=no
 237     skipcvc4=no
 238     cvc4steps=150000
 239     cvc4stepsrac=$cvc4steps
 240     cvc5steps=150000
 241     cvc5stepsrac=$cvc5steps
 242     z3steps=3000000
 243     z3stepsrac=$z3steps
 244     case "$filebase" in
 245       "640_no_loc_failure")
 246           z3steps=500000
 247           z3stepsrac=$z3steps
 248           ;;
 249       "657")
 250           z3steps=500000
 251           z3stepsrac=$z3steps
 252           ;;
 253       "668_projection")
 254           z3steps=500000
 255           z3stepsrac=$z3steps
 256           ;;
 257       "703_reduce_term")
 258           z3steps=500000
 259           z3stepsrac=$z3steps
 260           ;;
 261       "anonymous5")
 262           z3steps=500000
 263           z3stepsrac=$z3steps
 264           ;;
 265       "array_records_poly")
 266           skipae=yes
 267           skipcvc4=yes
 268           ;;
 269       "array_records_mono")
 270           z3stepsrac=100
 271           z3stepsrac=$z3steps
 272           skipae=yes
 273           ;;
 274       "array_mono")
 275           z3steps=100000
 276           z3stepsrac=$z3steps
 277           ;;
 278       "bv32")
 279           z3steps=500000
 280           z3stepsrac=$z3steps
 281           ;;
 282       "bv32_mono")
 283           z3steps=100000
 284           z3stepsrac=$z3steps
 285           ;;
 286       "bv32_toBig")
 287           z3steps=100000
 288           z3stepsrac=$z3steps
 289           ;;
 290       "floats")
 291           altergosteps=1000
 292           altergostepsrac=$altergosteps
 293           cvc5stepsrac=10000
 294           z3steps=100000
 295           z3stepsrac=10000
 296           ;;
 297       "int_overflow")
 298           z3steps=400000
 299           z3stepsrac=$z3steps
 300           ;;
 301       "jlamp0_mono")
 302           skipae=yes
 303           ;;
 304       "jlamp0_poly")
 305           skipae=yes
 306           ;;
 307       "loop_inv_int_mono")
 308           skipae=yes
 309           ;;
 310       "loop_inv_real")
 311           z3steps=1000000
 312           z3stepsrac=$z3steps
 313           ;;
 314       "map_of_algebraic")
 315           z3steps=50000
 316           z3stepsrac=$z3steps
 317           ;;
 318       "maps_mono")
 319           altergosteps=1000
 320           altergostepsrac=$altergosteps
 321           cvc5steps=5000
 322           cvc5stepsrac=$cvc5steps
 323           ;;
 324       "maps_poly")
 325           cvc5steps=15000
 326           cvc5stepsrac=$cvc5steps
 327           ;;
 328       "strings")
 329           z3steps=3000
 330           z3stepsrac=$z3steps
 331           ;;
 332       "test_result_ce_value2")
 333           skipae=yes
 334           ;;
 335       "threshold")
 336           z3steps=500000
 337           z3stepsrac=$z3steps
 338           ;;
 339       "while_mono")
 340           skipae=yes
 341           ;;
 342       *)
 343           ;;
 344     esac
 345     if [ "$skipae" = "yes" ] ; then
 346           echo "Skipping unreproducible run of Alt-Ergo 2.5.4 on $filedir/$filebase.mlw";
 347     else
 348       run Alt-Ergo,2.5.4 $filedir $filebase true  $altergosteps $altergostepsrac
 349       run Alt-Ergo,2.5.4 $filedir $filebase false  $altergosteps $altergostepsrac
 350     fi
 351     if [ "$skipcvc4" = "yes" ] ; then
 352           echo "Skipping unreproducible run of CVC4 1.8 on $filedir/$filebase.mlw";
 353     else
 354         run CVC4,1.8       $filedir $filebase true  $cvc4steps $cvc4stepsrac
 355         run CVC4,1.8       $filedir $filebase false $cvc4steps $cvc4stepsrac
 356     fi
 357     run CVC5,1.0.5     $filedir $filebase true  $cvc5steps $cvc5stepsrac
 358     run CVC5,1.0.5     $filedir $filebase false $cvc5steps $cvc5stepsrac
 359     run Z3,4.8.10      $filedir $filebase true  $z3steps $z3stepsrac
 360     run Z3,4.8.10      $filedir $filebase false $z3steps $z3stepsrac
 361   # fi
 362 done
 363
 364 if $updateoracle; then
 365   updatearg="--updateoracle"
 366 else
 367   updatearg=""
 368 fi
 369
 370 # Check the reproduction of the experiments by Petiot (2018).
 371 # $1 = prover
 372 # $2 = stepslimit
 373 petiot () {
 374 bench/check-ce/petiot2018/experiments.sh \
 375   --prover $1 --rac-prover $1 \
 376   --ce-prover $1,counterexamples --stepslimit $2 \
 377   $updatearg
 378 if [ $? = 1 ]; then failed="${failed}Petiot experiments with $1.\n"; fi
 379 }
 380
 381 if test "$petiot" -gt 0; then
 382     petiot Alt-Ergo,2.5.4  10000
 383     petiot Z3,4.8.10  500000
 384     petiot CVC4,1.8 10000
 385     petiot CVC5,1.0.5 10000
 386 fi
 387
 388 end=$(date +%s)
 389
 390 runtime=$((end-start))
 391 if [ "$failed" = "" ]; then
 392   echo "check-ce-bench: success (runtime = $runtime seconds)"
 393   exit 0
 394 else
 395   printf "\ncheck-ce-bench: failed for the following files (runtime = $runtime seconds)\n$failed\n"
 396   exit 1
 397 fi