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           altergosteps=1000
 259           altergostepsrac=$altergosteps
 260           z3steps=500000
 261           z3stepsrac=$z3steps
 262           ;;
 263       "algebraic_types_mono")
 264           altergosteps=1000
 265           altergostepsrac=$altergosteps
 266           ;;
 267       "algebraic_types_poly")
 268           skipae=yes
 269           altergosteps=1000
 270           altergostepsrac=$altergosteps
 271           ;;
 272       "anonymous3")
 273           altergosteps=1000
 274           altergostepsrac=$altergosteps
 275           ;;
 276       "anonymous5")
 277           z3steps=500000
 278           z3stepsrac=$z3steps
 279           ;;
 280       "array_records_poly")
 281           skipae=yes
 282           skipcvc4=yes
 283           ;;
 284       "array_records_mono")
 285           z3stepsrac=100
 286           z3stepsrac=$z3steps
 287           skipae=yes
 288           ;;
 289       "array_mono")
 290           skipae=yes
 291           z3steps=100000
 292           z3stepsrac=$z3steps
 293           ;;
 294       "bv32")
 295           z3steps=500000
 296           z3stepsrac=$z3steps
 297           ;;
 298       "bv32_mono")
 299           z3steps=100000
 300           z3stepsrac=$z3steps
 301           ;;
 302       "bv32_toBig")
 303           z3steps=100000
 304           z3stepsrac=$z3steps
 305           ;;
 306       "falseCE")
 307           skipae=yes
 308           altergosteps=7500
 309           altergostepsrac=$altergosteps
 310           ;;
 311       "floats")
 312           skipae=yes
 313           altergosteps=1000
 314           altergostepsrac=$altergosteps
 315           cvc5stepsrac=10000
 316           z3steps=100000
 317           z3stepsrac=10000
 318           ;;
 319       "int_overflow")
 320           skipae=yes
 321           z3steps=400000
 322           z3stepsrac=$z3steps
 323           ;;
 324       "jlamp0_mono")
 325           skipae=yes
 326           ;;
 327       "jlamp0_poly")
 328           skipae=yes
 329           ;;
 330       "lists")
 331           skipae=yes
 332           altergosteps=1000
 333           altergostepsrac=$altergosteps
 334           ;;
 335       "loop_inv_int_mono")
 336           skipae=yes
 337           ;;
 338       "loop_inv_real")
 339           z3steps=1000000
 340           z3stepsrac=$z3steps
 341           ;;
 342       "map_of_algebraic")
 343           z3steps=50000
 344           z3stepsrac=$z3steps
 345           ;;
 346       "maps_mono")
 347           altergosteps=1000
 348           altergostepsrac=$altergosteps
 349           cvc5steps=5000
 350           cvc5stepsrac=$cvc5steps
 351           ;;
 352       "maps_poly")
 353           cvc5steps=15000
 354           cvc5stepsrac=$cvc5steps
 355           ;;
 356       "strings")
 357           z3steps=3000
 358           z3stepsrac=$z3steps
 359           ;;
 360       "test_result_ce_value2")
 361           skipae=yes
 362           ;;
 363       "threshold")
 364           z3steps=500000
 365           z3stepsrac=$z3steps
 366           ;;
 367       "while_mono")
 368           skipae=yes
 369           ;;
 370       *)
 371           ;;
 372     esac
 373     if [ "$skipae" = "yes" ] ; then
 374           echo "Skipping unreproducible run of Alt-Ergo 2.6.0 on $filedir/$filebase.mlw";
 375     else
 376       run Alt-Ergo,2.6.0 $filedir $filebase true  $altergosteps $altergostepsrac
 377       run Alt-Ergo,2.6.0 $filedir $filebase false  $altergosteps $altergostepsrac
 378     fi
 379     if [ "$skipcvc4" = "yes" ] ; then
 380           echo "Skipping unreproducible run of CVC4 1.8 on $filedir/$filebase.mlw";
 381     else
 382         run CVC4,1.8       $filedir $filebase true  $cvc4steps $cvc4stepsrac
 383         run CVC4,1.8       $filedir $filebase false $cvc4steps $cvc4stepsrac
 384     fi
 385     run CVC5,1.0.5     $filedir $filebase true  $cvc5steps $cvc5stepsrac
 386     run CVC5,1.0.5     $filedir $filebase false $cvc5steps $cvc5stepsrac
 387     run Z3,4.8.10      $filedir $filebase true  $z3steps $z3stepsrac
 388     run Z3,4.8.10      $filedir $filebase false $z3steps $z3stepsrac
 389   # fi
 390 done
 391
 392 if $updateoracle; then
 393   updatearg="--updateoracle"
 394 else
 395   updatearg=""
 396 fi
 397
 398 # Check the reproduction of the experiments by Petiot (2018).
 399 # $1 = prover
 400 # $2 = stepslimit
 401 petiot () {
 402 bench/check-ce/petiot2018/experiments.sh \
 403   --prover $1 --rac-prover $1 \
 404   --ce-prover $1,counterexamples --stepslimit $2 \
 405   $updatearg
 406 if [ $? = 1 ]; then failed="${failed}Petiot experiments with $1.\n"; fi
 407 }
 408
 409 if test "$petiot" -gt 0; then
 410     petiot Alt-Ergo,2.6.0  10000
 411     petiot Z3,4.8.10  500000
 412     petiot CVC4,1.8 10000
 413     petiot CVC5,1.0.5 10000
 414 fi
 415
 416 end=$(date +%s)
 417
 418 runtime=$((end-start))
 419 if [ "$failed" = "" ]; then
 420   echo "check-ce-bench: success (runtime = $runtime seconds)"
 421   exit 0
 422 else
 423   printf "\ncheck-ce-bench: failed for the following files (runtime = $runtime seconds)\n$failed\n"
 424   exit 1
 425 fi