bench 10.7 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 11
shopt -s nullglob

12
suffix=$1
Andrei Paskevich's avatar
Andrei Paskevich committed
13

Andrei Paskevich's avatar
Andrei Paskevich committed
14
# TODO: remove the hack about int.mlw once it has become builtin
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
15
goods () {
16
    pgm="bin/why3prove$suffix"
17
    ERROR=
18
    test -d $1 || exit 1
19
    rm -f bench_errors
Andrei Paskevich's avatar
Andrei Paskevich committed
20
    for f in $1/*.[wm][hl][yw] ; do
21
	printf "  $f... "
22
        opts="$2"
Andrei Paskevich's avatar
Andrei Paskevich committed
23
        if test $f = stdlib/int.mlw; then opts="$2 --type-only"; fi
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
24
	# running Why
25
	if ! $pgm $opts $f > /dev/null 2> bench_error; then
Andrei Paskevich's avatar
Andrei Paskevich committed
26 27
	    echo "FAILED!"
#            echo "env: WHY3DATA='$WHY3DATA'"
28
            echo "invocation: $pgm $opts $f" | tee -a bench_errors
29
            cat bench_error | tee -a bench_errors
30 31 32 33 34 35 36
            ERROR=yes
	elif test -s bench_error; then
            echo "warning!"
            cat bench_error
        else
	    echo "ok"
        fi
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
37
    done
38
    rm -f bench_error
39
    if test -n "$ERROR"; then
40
        echo "bench aborted due to the following errors:"
41 42
        cat bench_errors
        rm bench_errors
43 44
        exit 1
    fi
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
45 46 47
}

bads () {
48
    pgm="bin/why3prove$suffix"
49
    test -d $1 || exit 1
Andrei Paskevich's avatar
Andrei Paskevich committed
50
    for f in $1/*.[wm][hl][yw] ; do
51
	printf "  $f... "
52
	if $pgm $2 $f > /dev/null 2>&1; then
Andrei Paskevich's avatar
Andrei Paskevich committed
53 54 55
	    echo "SHOULD FAIL!"
#            echo "env: WHY3DATA='$WHY3DATA'"
            echo "invocation: $pgm $2 $f"
56
	    exit 1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
57
	fi
Andrei Paskevich's avatar
Andrei Paskevich committed
58
	echo "ok"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
59 60 61
    done
}

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
62
drivers () {
63
    pgm="bin/why3prove$suffix"
64
    test -d $1 || exit 1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
65
    for f in $1/*.drv; do
66
        if [[ $f == drivers/ocaml*.drv ]]; then continue; fi
67
        if [[ $f == drivers/c.drv ]]; then continue; fi
68
        if [[ $f == drivers/cakeml.drv ]]; then continue; fi
69
	printf "  $f... "
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
70
	# running Why
71
	if ! echo "theory Test goal G : 1=2 end" | $pgm -F whyml --driver $f - > /dev/null; then
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
72
	    echo "why FAILED"
73
            echo "theory Test goal G : 1=2 end" | $pgm -F whyml --driver $f -
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
74 75
	    exit 1
	fi
Andrei Paskevich's avatar
Andrei Paskevich committed
76
	echo "ok"
77 78 79
    done
}

80
valid_goals () {
81
    pgm="bin/why3prove$suffix"
82
    test -d $1 || exit 1
83
    for f in $1/*.mlw; do
84
	printf "  $f... "
85 86 87 88
        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
89
	    exit 1
Andrei Paskevich's avatar
Andrei Paskevich committed
90
       fi
91
       echo "ok"
92 93 94
    done
}

95
invalid_goals () {
96
    pgm="bin/why3prove$suffix"
97
    test -d $1 || exit 1
98
    for f in $1/*.mlw; do
99
	printf "  $f... "
100 101 102 103 104 105 106 107 108 109 110
	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
}

111 112
replay () {
    pgm="bin/why3replay$suffix"
113
    test -d $1 || exit 1
114 115
    for f in $1/*/; do
        printf "  $f... "
116
        if $pgm $2 $f > /dev/null 2> /dev/null; then
117 118 119
            echo "ok"
        else
            echo "replay test failed!"
120 121
            echo $pgm $2 $f
            $pgm $2 $f
122 123 124 125 126
            exit 1
        fi
    done
}

127
execute () {
128
    pgm="bin/why3execute$suffix"
129
    printf "  $1 $2... "
130
    if $pgm $1 $2 > /dev/null; then
131 132 133
        echo "ok"
    else
        echo "execution test failed!"
134 135
        echo $pgm $1 $2
        $pgm $1 $2
136 137 138 139
        exit 1
    fi
}

MARCHE Claude's avatar
MARCHE Claude committed
140
extract_and_run () {
141 142 143 144
    dir=$1
    shift
    prg=$1
    shift
145
    printf "  $dir... "
146
    rm -f $dir/$prg
147
    printf "clean... "
148
    if BENCH=yes make -C $dir clean > /dev/null; then
149
        printf "extract... "
150
        if BENCH=yes make -C $dir extract > /dev/null; then
151
            printf "compile... "
152
            if BENCH=yes make -C $dir > /dev/null; then
153
                printf "execute... "
154
                if $dir/main.opt "$@" > /dev/null; then
155
                    printf "doc... "
156
                    if BENCH=yes make -C $dir doc > /dev/null; then
157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175
                        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
176
        else
177 178 179
            echo "extract failed!"
            echo BENCH=yes make -C $dir extract
            BENCH=yes make -C $dir extract
180 181
            exit 1
        fi
MARCHE Claude's avatar
MARCHE Claude committed
182
    else
183 184 185
        echo "clean failed!"
        echo BENCH=yes make -C $dir clean
        BENCH=yes make -C $dir clean
MARCHE Claude's avatar
MARCHE Claude committed
186 187 188 189
        exit 1
    fi
}

190
extract_and_test_wmp () {
191
    dir=$1
192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228
    shift
    printf "  $dir... "
    printf "clean... "
    if BENCH=yes make -C $dir clean > /dev/null; then
        printf "extract... "
        if BENCH=yes make -C $dir extract > /dev/null; then
            printf "compile... "
            if BENCH=yes make -C $dir bench-tests > /dev/null; then
                printf "execute... "
                if $dir/build/bench-tests > /dev/null; then
                    echo "ok"
                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
        else
            echo "extract failed!"
            echo BENCH=yes make -C $dir extract
            BENCH=yes make -C $dir extract
            exit 1
        fi
    else
        echo "clean failed!"
        echo BENCH=yes make -C $dir clean
        BENCH=yes make -C $dir clean
        exit 1
    fi
}

229
list_stuff () {
230
    pgm="bin/why3$suffix"
231
    printf '  %s ' "$1"
232
    if $pgm $1 > /dev/null; then
233 234 235 236 237 238 239 240
        echo "ok"
    else
        echo "$pgm $1 FAIL"
        $pgm $1
        exit 1
    fi
}

241 242 243
echo "=== Checking stdlib ==="
goods stdlib
goods stdlib/mach
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
244 245
echo ""

246 247 248 249
echo "=== Checking drivers ==="
drivers drivers
echo ""

250 251
echo "=== Checking bad files ==="
goods bench/typing/bad --parse-only
Andrei Paskevich's avatar
Andrei Paskevich committed
252
goods bench/programs/bad-typing --parse-only
253
bads bench/typing/bad --type-only
Andrei Paskevich's avatar
Andrei Paskevich committed
254
bads bench/programs/bad-typing --type-only
255
goods bench/typing/x-bad --type-only
256 257
echo ""

258 259
echo "=== Checking good files ==="
goods bench/typing/good
260 261
goods bench/typing/x-good --parse-only
bads bench/typing/x-good --type-only
262
goods bench/programs/good
263
goods bench/ce
264 265 266 267 268 269 270 271 272 273 274
goods examples/bts
goods examples/tests
goods examples/tests-provers
goods examples/check-builtin
goods examples/logic
goods examples
goods examples/foveoos11-cm
goods examples/WP_revisited
goods examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps"
goods examples/bitvectors "-L examples/bitvectors"
goods examples/avl "-L examples/avl"
275
goods examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_2016_matrix_multiplication"
276
goods examples/double_wp "-L examples/double_wp"
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
277
goods examples/ring_decision "-L examples/ring_decision"
278
goods examples/multiprecision "-L examples/multiprecision"
279 280 281
goods examples/in_progress
echo ""

282 283
echo "=== Checking replay (no prover) ==="
replay bench/replay
284
replay examples/stdlib --merging-only
285 286 287 288 289 290 291 292 293 294 295
replay examples/bts --merging-only
replay examples/tests --merging-only
replay examples/tests-provers --merging-only
replay examples/check-builtin --merging-only
replay examples/logic --merging-only
replay examples --merging-only
replay examples/foveoos11-cm --merging-only
replay examples/WP_revisited --merging-only
replay examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps --merging-only"
replay examples/bitvectors "-L examples/bitvectors --merging-only"
replay examples/avl "-L examples/avl --merging-only"
296
replay examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_2016_matrix_multiplication --merging-only"
297 298
replay examples/double_wp "-L examples/double_wp --merging-only"
replay examples/ring_decision "-L examples/ring_decision --merging-only"
299
replay examples/multiprecision "-L examples/multiprecision --merging-only"
300 301
#replay examples/in_progress --merging-only
#replay examples/in_progress/multiprecision "-L examples/in_progress/multiprecision --merging-only"
302 303
echo ""

304 305 306 307 308 309 310 311
echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""

echo "=== Checking invalid goals ==="
invalid_goals bench/invalid
echo ""

312
echo "=== Checking execution ==="
MARCHE Claude's avatar
MARCHE Claude committed
313 314
execute examples/euler001.mlw Euler001.bench
execute examples/euler002.mlw Solve.bench
MARCHE Claude's avatar
MARCHE Claude committed
315
execute examples/fibonacci.mlw FibRecGhost.bench
MARCHE Claude's avatar
MARCHE Claude committed
316
execute examples/fibonacci.mlw FibonacciLogarithmic.bench
317
# fails: cannot execute Cany
318
# execute examples/same_fringe.mlw SameFringe.bench
319
# fails: cannot evaluate condition a=b (how to do it?)
320 321
# execute examples/same_fringe.mlw SameFringe.test5
execute examples/same_fringe.mlw Test.test1
322
execute examples/vstte12_combinators.mlw Combinators.test_SKK
MARCHE Claude's avatar
MARCHE Claude committed
323 324
execute examples/selection_sort.mlw SelectionSort.bench
execute examples/insertion_sort.mlw InsertionSort.bench
325
execute examples/quicksort.mlw Test.bench
326
execute examples/conjugate.mlw Test.bench
327
# fails: needs support for "val" without code (how to do it?)
328
# examples/vacid_0_sparse_array.mlw Harness.bench
Guillaume Melquiond's avatar
Guillaume Melquiond committed
329
execute examples/knuth_prime_numbers.mlw PrimeNumbers.bench
MARCHE Claude's avatar
MARCHE Claude committed
330
execute examples/vstte10_max_sum.mlw TestCase.test_case
331
execute examples/verifythis_fm2012_LRS.mlw LCP_test.bench
332 333
execute examples/verifythis_fm2012_LRS.mlw SuffixSort_test.bench
execute examples/verifythis_fm2012_LRS.mlw SuffixArray_test.bench
334
execute examples/verifythis_fm2012_LRS.mlw LRS_test.bench
MARCHE Claude's avatar
MARCHE Claude committed
335
execute examples/verifythis_PrefixSumRec.mlw PrefixSumRec.bench
MARCHE Claude's avatar
MARCHE Claude committed
336
execute examples/vstte10_queens.mlw NQueens.test8
337
# fails: "Cannot decide condition of if: (not ((~)((<<)((~)(0), 8)) = 0))"
338 339 340
# examples/queens.mlw NQueensBits.test8
# fails: cannot find definition of routine eq
# examples/residual.mlw Test.test_astar
341 342
echo ""

343

344
echo "=== Checking extraction to OCaml ==="
345
extract_and_run examples/euler001 euler001.ml 1000000
346
extract_and_run examples/gcd gcd.ml 6 15
347
extract_and_run examples/vstte10_max_sum vstte10_max_sum.ml
348 349
# needs to port
# extract_and_run examples/vstte12_combinators vstte12_combinators.ml "((((K K) K) K) K)"
350
extract_and_run examples/defunctionalization defunctionalization.ml
351
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
352 353
echo ""

354
echo "=== Checking extraction to C ==="
355 356
extract_and_test_wmp examples/in_progress/multiprecision
extract_and_test_wmp examples/multiprecision
357 358
echo ""

359 360 361 362 363 364 365 366
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 ""
367 368

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