bench 7.07 KB
Newer Older
1
#!/bin/bash
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
2 3 4

# auto bench for why

MARCHE Claude's avatar
MARCHE Claude committed
5 6 7
# Useless in this script ?
# export WHY3LIB=lib
# export WHY3DATA=.
Andrei Paskevich's avatar
Andrei Paskevich committed
8
# export WHY3LOADPATH=theories
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
9

10
suffix=$1
Andrei Paskevich's avatar
Andrei Paskevich committed
11

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
12
goods () {
13
    pgm="bin/why3prove$suffix"
Andrei Paskevich's avatar
Andrei Paskevich committed
14 15
    for f in $1/*.[wm][hl][yw] ; do
	echo -n "  $f... "
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
16 17
	# running Why
	if ! $pgm $2 $f > /dev/null 2>&1; then
Andrei Paskevich's avatar
Andrei Paskevich committed
18 19
	    echo "FAILED!"
#            echo "env: WHY3DATA='$WHY3DATA'"
20 21
            echo "invocation: $pgm $2 $f"
            echo "result:"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
22 23 24
	    $pgm $2 $f
	    exit 1
	fi
Andrei Paskevich's avatar
Andrei Paskevich committed
25
	echo "ok"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
26 27 28 29
    done
}

bads () {
30
    pgm="bin/why3prove$suffix"
Andrei Paskevich's avatar
Andrei Paskevich committed
31 32
    for f in $1/*.[wm][hl][yw] ; do
	echo -n "  $f... "
33
	if $pgm $2 $f > /dev/null 2>&1; then
Andrei Paskevich's avatar
Andrei Paskevich committed
34 35 36
	    echo "SHOULD FAIL!"
#            echo "env: WHY3DATA='$WHY3DATA'"
            echo "invocation: $pgm $2 $f"
37
	    exit 1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
38
	fi
Andrei Paskevich's avatar
Andrei Paskevich committed
39
	echo "ok"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
40 41 42
    done
}

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
43
drivers () {
44
    pgm="bin/why3prove$suffix"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
45
    for f in $1/*.drv; do
46
        if [[ $f == drivers/ocaml*.drv ]]; then continue; fi
Andrei Paskevich's avatar
Andrei Paskevich committed
47
	echo -n "  $f... "
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
48
	# running Why
49
	if ! echo "theory Test goal G : 1=2 end" | $pgm -F why --driver $f - > /dev/null 2>&1; then
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
50
	    echo "why FAILED"
51
            echo "theory Test goal G : 1=2 end" | $pgm -F why --driver $f -
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
52 53
	    exit 1
	fi
Andrei Paskevich's avatar
Andrei Paskevich committed
54
	echo "ok"
55 56 57
    done
}

58
valid_goals () {
59
    pgm="bin/why3prove$suffix"
60 61
    for f in $1/*.mlw; do
	echo -n "  "$f"... "
62 63 64 65
        if ! $pgm -t 15 -P alt-ergo $f > /dev/null 2>&1; then
            echo "FAILED!"
            echo "$pgm -t 15 -P alt-ergo $f"
            $pgm -t 15 -P alt-ergo $f
66
	    exit 1
Andrei Paskevich's avatar
Andrei Paskevich committed
67
       fi
68
       echo "ok"
69 70 71
    done
}

72
invalid_goals () {
73
    pgm="bin/why3prove$suffix"
74 75 76 77 78 79 80 81 82 83 84 85 86
    for f in $1/*.mlw; do
	echo -n "  "$f"... "
	if $pgm -t 3 -P alt-ergo $f | grep -q Valid; then
	    echo "invalid test $f failed!"
	    echo "$pgm -P alt-ergo $f"
	    $pgm -t 3 -P alt-ergo $f
	    exit 1
        else
	    echo "ok"
       fi
    done
}

87
execute () {
88
    pgm="bin/why3execute$suffix"
89
    echo -n "  $1 $2... "
90
    if $pgm $1 $2 > /dev/null 2>&1; then
91 92 93
        echo "ok"
    else
        echo "execution test failed!"
94 95
        echo $pgm $1 $2
        $pgm $1 $2
96 97 98 99
        exit 1
    fi
}

MARCHE Claude's avatar
MARCHE Claude committed
100
extract_and_run () {
101 102 103 104
    dir=$1
    shift
    prg=$1
    shift
105
    echo -n "  $dir... "
106
    rm -f $dir/$prg
107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135
    echo -n "clean... "
    if BENCH=yes make -C $dir clean > /dev/null 2>&1; then
        echo -n "extract... "
        if BENCH=yes make -C $dir extract > /dev/null 2>&1; then
            echo -n "compile... "
            if BENCH=yes make -C $dir > /dev/null 2>&1; then
                echo -n "execute... "
                if $dir/main.opt "$@" > /dev/null 2>&1; then
                    echo -n "doc... "
                    if BENCH=yes make -C $dir doc > /dev/null 2>&1; then
                        echo "ok"
                    else
                        echo "documentation failed!"
                        echo BENCH=yes make -C $dir doc
                        BENCH=yes make -C $dir doc
                        exit 1
                    fi
                else
                    echo "execution failed!"
                    echo $dir/main.opt "$@"
                    $dir/main.opt "$@"
                    exit 1
                fi
            else
                echo "compilation failed!"
                echo BENCH=yes make -C $dir
                BENCH=yes make -C $dir
                exit 1
            fi
136
        else
137 138 139
            echo "extract failed!"
            echo BENCH=yes make -C $dir extract
            BENCH=yes make -C $dir extract
140 141
            exit 1
        fi
MARCHE Claude's avatar
MARCHE Claude committed
142
    else
143 144 145
        echo "clean failed!"
        echo BENCH=yes make -C $dir clean
        BENCH=yes make -C $dir clean
MARCHE Claude's avatar
MARCHE Claude committed
146 147 148 149
        exit 1
    fi
}

150
list_stuff () {
151
    pgm="bin/why3$suffix"
152
    echo -n "  $1 "
Andrei Paskevich's avatar
Andrei Paskevich committed
153
    if $pgm $1 > /dev/null 2>&1; then
154 155 156 157 158 159 160 161
        echo "ok"
    else
        echo "$pgm $1 FAIL"
        $pgm $1
        exit 1
    fi
}

162 163 164 165
echo "=== Checking invalid goals ==="
invalid_goals bench/invalid
echo ""

166 167
echo "=== Checking theories ==="
goods theories
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
168 169
echo ""

170 171
echo "=== Checking modules ==="
goods modules
172
goods modules/mach
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
173 174
echo ""

175 176 177 178
echo "=== Checking drivers ==="
drivers drivers
echo ""

179 180
echo "=== Checking bad files ==="
goods bench/typing/bad --parse-only
Andrei Paskevich's avatar
Andrei Paskevich committed
181
goods bench/programs/bad-typing --parse-only
182
bads bench/typing/bad --type-only
Andrei Paskevich's avatar
Andrei Paskevich committed
183
bads bench/programs/bad-typing --type-only
MARCHE Claude's avatar
MARCHE Claude committed
184
bads examples/bad-bts
185 186
echo ""

187 188
echo "=== Checking good files ==="
goods bench/typing/good
Andrei Paskevich's avatar
Andrei Paskevich committed
189
goods bench/programs/good
190 191 192 193 194
goods examples/bts
goods examples/tests
goods examples/tests-provers
goods examples/check-builtin
goods examples/logic
Andrei Paskevich's avatar
Andrei Paskevich committed
195 196
goods examples
goods examples/foveoos11-cm
197
goods examples/WP_revisited
198 199
goods examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps"
goods examples/bitvectors "-L examples/bitvectors"
200 201 202
goods examples/in_progress
echo ""

203
echo "=== Checking execution ==="
MARCHE Claude's avatar
MARCHE Claude committed
204 205
execute examples/euler001.mlw Euler001.bench
execute examples/euler002.mlw Solve.bench
MARCHE Claude's avatar
MARCHE Claude committed
206
execute examples/fibonacci.mlw FibRecGhost.bench
MARCHE Claude's avatar
MARCHE Claude committed
207
execute examples/fibonacci.mlw FibonacciLogarithmic.bench
208 209
# fails: definition of psymbol eq not found
# execute examples/same_fringe.mlw SameFringe.bench
210 211 212 213
# fails: cannot evaluate condition a=b (how to do it?)
# execute examples/same_fringe.mlw --exec SameFringe.test5
# fails: "let" are cloned as "val"
# execute examples/same_fringe.mlw --exec Test.test1
MARCHE Claude's avatar
MARCHE Claude committed
214
execute examples/vstte12_combinators.mlw Combinators.test_SKK
MARCHE Claude's avatar
MARCHE Claude committed
215 216
execute examples/selection_sort.mlw SelectionSort.bench
execute examples/insertion_sort.mlw InsertionSort.bench
217
execute examples/quicksort.mlw Test.bench
218
execute examples/conjugate.mlw Test.bench
219 220
# fails: needs support for "val" without code (how to do it?)
# examples/vacid_0_sparse_array.mlw --exec Harness.bench
221
execute examples/knuth_prime_numbers.mlw PrimeNumbers.bench
MARCHE Claude's avatar
MARCHE Claude committed
222
execute examples/vstte10_max_sum.mlw TestCase.test_case
223
execute examples/verifythis_fm2012_LRS.mlw LCP_test.bench
224 225
execute examples/verifythis_fm2012_LRS.mlw SuffixSort_test.bench
execute examples/verifythis_fm2012_LRS.mlw SuffixArray_test.bench
226
execute examples/verifythis_fm2012_LRS.mlw LRS_test.bench
227
execute examples/verifythis_PrefixSumRec.mlw PrefixSumRec.bench
MARCHE Claude's avatar
MARCHE Claude committed
228
execute examples/vstte10_queens.mlw NQueens.test8
229
# fails: "Cannot decide condition of if: (not ((~)((<<)((~)(0), 8)) = 0))"
MARCHE Claude's avatar
MARCHE Claude committed
230
# examples/queens.mlw --exec  NQueensBits.test8
231 232
# fails: "let" are cloned as "val"
# examples/in_progress/residual.mlw --exec Test.test_astar
233 234
echo ""

MARCHE Claude's avatar
MARCHE Claude committed
235
echo "=== Extraction to Ocaml ==="
MARCHE Claude's avatar
MARCHE Claude committed
236
extract_and_run examples/euler001 euler001__*.ml 1000000
237
extract_and_run examples/gcd gcd__*.ml 6 15
MARCHE Claude's avatar
MARCHE Claude committed
238
extract_and_run examples/vstte10_max_sum vstte10_max_sum__*.ml
239
extract_and_run examples/vstte12_combinators vstte12_combinators__*.ml "((((K K) K) K) K)"
240
extract_and_run examples/sudoku sudoku__*.ml 2,0,9,0,0,0,0,1,0,0,0,0,0,6,0,0,0,0,0,5,3,8,0,2,7,0,0,3,0,0,0,0,0,0,0,0,0,0,0,0,7,5,0,0,3,0,4,1,2,0,8,9,0,0,0,0,4,0,9,0,0,2,0,8,0,0,0,0,1,0,0,5,0,0,0,0,0,0,0,7,6
241
extract_and_run examples/defunctionalization defunctionalization__*.ml
MARCHE Claude's avatar
MARCHE Claude committed
242 243
echo ""

244 245 246 247
echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""

248 249 250 251 252 253 254 255
echo "=== Checking --list-* ==="
list_stuff --list-transforms
list_stuff --list-printers
list_stuff --list-provers
list_stuff --list-formats
list_stuff --list-metas
list_stuff --list-debug-flags
echo ""
256 257 258

echo "=== Checking realizations ==="
exec bench/check_realizations.sh