examples/bench.sh

   1 #!/bin/sh
   2 # bench for why3
   3
   4 TMP=$PWD/why3bench.out
   5 TMPERR=$PWD/why3bench.err
   6 cd `dirname $0`
   7
   8 HTML=$PWD/why3bench.html
   9
  10 res=0
  11 export success=0
  12 export total=0
  13
  14 echo '<html>' > $HTML
  15 echo '<head><title>Why3 Bench</title></head>' >> $HTML
  16 echo '<body>' >> $HTML
  17 echo '<h1>Why3 bench</h1>' >> $HTML
  18
  19 run_dir () {
  20     echo '<h2>Directory '$1'</h2>' >> $HTML
  21     echo '<ul>' >> $HTML
  22     for f in `ls $1/*/why3session.xml`; do
  23         d=`dirname $f`
  24         b=`basename $d`
  25         echo -n "Benchmarking $d ... "
  26         ../bin/why3replay.opt -bench $REPLAYOPT $2 $d 2> $TMPERR > $TMP
  27         ret=$?
  28         if test "$ret" != "0"  ; then
  29             echo -n "FAILED (ret code=$ret):"
  30             out=`head -1 $TMP`
  31             if test -z "$out" ; then
  32                echo "standard error: (standard output empty)"
  33                cat $TMPERR
  34             else
  35                cat $TMP
  36             fi
  37             res=1
  38             echo '<li>'$d' failed' >> $HTML
  39         else
  40             echo "OK"
  41             success=`expr $success + 1`
  42             ../bin/why3session html $d 2> $TMPERR > $TMP
  43             echo '<li><a href="'$d/$b'.html">'$d'</a>' >> $HTML
  44         fi
  45         total=`expr $total + 1`
  46     done
  47     echo '</ul>' >> $HTML
  48 }
  49
  50 echo "=== Tests ==="
  51 run_dir tests
  52 run_dir tests-provers
  53 echo ""
  54
  55 echo "=== Check Builtin translation ==="
  56 run_dir check-builtin
  57 echo ""
  58
  59 echo "=== BTS ==="
  60 run_dir bts
  61 echo ""
  62
  63 echo "=== Logic ==="
  64 run_dir logic
  65 run_dir bitvectors "-I bitvectors"
  66 echo ""
  67
  68 echo "=== Programs ==="
  69 run_dir .
  70 run_dir foveoos11-cm
  71 run_dir WP_revisited
  72 run_dir vacid_0_binary_heaps "-I vacid_0_binary_heaps"
  73 echo ""
  74
  75 echo '</body></html>' >> $HTML
  76 echo "Summary: $success/$total"
  77 exit $res