bench/infer-bench

   1 #!/bin/bash
   2
   3 has_infer=`sed -n -e 's/INFERLIB *= *\([^ ]\+\)/\1/p' share/Makefile.config`
   4
   5 if test -z "$has_infer"; then
   6     echo "Inference of loop invariants not enabled!"
   7     exit 3
   8 fi
   9
  10 updateoracle=false
  11 forceupdateoracle=false
  12 files=""
  13 dirs=""
  14 success=true
  15 why3prove="bin/why3 prove"
  16 why3libs=""
  17
  18 if test $# = 0; then
  19   printf "no files provided\n"
  20   exit 2
  21 fi
  22
  23 while test $# != 0; do
  24   case "$1" in
  25     "-update-oracle")
  26         updateoracle=true;;
  27     "-force-update-oracle")
  28         forceupdateoracle=true;;
  29     -L=?*)
  30         why3libs="$why3libs ${1#*=}";;
  31     "-"*)
  32         printf "unknown option: %s\n" "$1"
  33         printf "usage: infer-bench [-update-oracle] <file>\n"
  34         printf "  if <file> is a directory, it runs on all the *.mlw files\n"
  35         exit 2;;
  36     *)
  37       if [ -d "$1" ]; then
  38         dirs="$dirs $1"
  39       else
  40         if [ -f "$1" ]; then
  41           files="$files $1"
  42         else
  43           echo "File not found: $1"
  44           exit 2
  45         fi
  46       fi
  47   esac
  48   shift
  49 done
  50
  51 if test -n "$why3libs"; then
  52    why3libs="-L $why3libs"
  53 fi
  54
  55 for d in $dirs; do
  56   d=$(echo $d | sed 's:/*$::') #remove trailling slashs
  57   mlw="$(ls $d/*.mlw 2> /dev/null)"
  58   files="$files $mlw"
  59 done
  60
  61 failed=""
  62
  63 # $1 = file
  64 run () {
  65   printf "running for $1"
  66   file_base="$(basename $1)"
  67   file_dir="$(dirname $1)"
  68   out_file="$file_dir/${file_base%.*}.out"
  69   oracle_file="$file_dir/infer-oracles/${file_base%.*}.oracle"
  70   $why3prove $1 -t 1 -P alt-ergo --debug=print-inferred-invs $why3libs > "$out_file" 2>&1
  71   str_out=$(sed 's/[0-9]\+\.[0-9]\+s//g' $out_file | sed 's/[0-9]\+ steps//g')
  72   str_oracle=$(sed 's/[0-9]\+\.[0-9]\+s//g' $oracle_file | sed 's/[0-9]\+ steps//g')
  73   if [ "$str_oracle" = "$str_out" ] ; then
  74     printf " - ok\n"
  75   else
  76     printf "\n"
  77     if $updateoracle; then
  78       echo "Updating oracle for $file_base"
  79       cp "$out_file" "$oracle_file"
  80     else
  81       echo "FAILED!"
  82       echo "diff is the following:"
  83       echo "$f"
  84       diff <(echo "$str_oracle") <(echo "$str_out")
  85       failed="$failed\n$1"
  86       success=false
  87     fi
  88   fi
  89   if $forceupdateoracle; then
  90     echo "Forcing update oracle for $file_base"
  91     cp "$out_file" "$oracle_file"
  92   fi
  93   rm "$out_file"
  94 }
  95
  96 for file in $files; do
  97     run $file
  98 done
  99
 100 if $success; then
 101     echo "Infer bench: success"
 102     exit 0
 103 else
 104     echo "Infer bench: failed"
 105     printf "$failed\n"
 106     exit 1
 107 fi