bench.sh 1.61 KB
Newer Older
1 2 3 4 5 6 7
#!/bin/sh
# bench for why3

TMP=$PWD/why3bench.out
TMPERR=$PWD/why3bench.err
cd `dirname $0`

8
HTML=$PWD/why3bench.html
9 10 11 12 13 14 15

res=0
export success=0
export total=0

echo '<html>' > $HTML
echo '<head><title>Why3 Bench</title></head>' >> $HTML
16 17
echo '<body>' >> $HTML
echo '<h1>Why3 bench</h1>' >> $HTML
18

19
run_dir () {
20 21
    echo '<h2>Directory '$1'</h2>' >> $HTML
    echo '<ul>' >> $HTML
22 23
    for f in `ls $1/*/why3session.xml`; do
        d=`dirname $f`
24
        b=`basename $d`
25
	echo -n "Benchmarking $d ... "
26
        ../bin/why3replay.opt -bench $REPLAYOPT $2 $d 2> $TMPERR > $TMP
27 28 29 30 31 32 33 34 35 36 37
        ret=$?
	if test "$ret" != "0"  ; then
	    echo -n "FAILED (ret code=$ret):"
            out=`head -1 $TMP`
            if test -z "$out" ; then
               echo "standard error: (standard output empty)"
               cat $TMPERR
            else
	       cat $TMP
            fi
	    res=1
38
            echo '<li>'$d' failed' >> $HTML
39
	else
40
	    echo "OK"
41
            success=`expr $success + 1`
42 43
            ../bin/why3session html $d 2> $TMPERR > $TMP
            echo '<li><a href="'$d/$b'.html">'$d'</a>' >> $HTML
44 45 46
	fi
        total=`expr $total + 1`
    done
47
    echo '</ul>' >> $HTML
48 49
}

50 51
echo "=== Tests ==="
run_dir tests
Andrei Paskevich's avatar
Andrei Paskevich committed
52
run_dir tests-provers
53 54
echo ""

Andrei Paskevich's avatar
Andrei Paskevich committed
55 56
echo "=== Check Builtin translation ==="
run_dir check-builtin
57
echo ""
58

Andrei Paskevich's avatar
Andrei Paskevich committed
59 60
echo "=== BTS ==="
run_dir bts
61
echo ""
62

Andrei Paskevich's avatar
Andrei Paskevich committed
63 64 65
echo "=== Logic ==="
run_dir logic
run_dir bitvectors "-I bitvectors"
66
echo ""
67

Andrei Paskevich's avatar
Andrei Paskevich committed
68 69 70
echo "=== Programs ==="
run_dir .
run_dir foveoos11-cm
71
run_dir WP_revisited
Andrei Paskevich's avatar
Andrei Paskevich committed
72
run_dir vacid_0_binary_heaps "-I vacid_0_binary_heaps"
73
echo ""
74

75
echo '</body></html>' >> $HTML
76 77
echo "Summary: $success/$total"
exit $res