bench 12.3 KB
Newer Older
1
#!/bin/bash
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
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
15
goods () {
16
    pgm="bin/why3prove$suffix"
17
    ERROR=
18
    test -d $1 || exit 1
19
    rm -f bench_errors
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
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
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
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
57
	fi
Andrei Paskevich's avatar
Andrei Paskevich committed
58
	echo "ok"
59 60 61
    done
}

62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81
warns () {
    pgm="bin/why3prove$suffix"
    test -d $1 || exit 1
    rm -f bench_errors
    for f in $1/*.[wm][hl][yw] ; do
	printf "  $f... "
	if ! $pgm $2 $f > /dev/null 2>bench_errors; then
            echo "FAILED!"
            echo "invocation: $pgm $2 $f"
            exit 1
        fi
        if ! test -s bench_errors; then
            echo "SHOULD HAVE A WARNING !"
            echo "invocation: $pgm $2 $f"
            exit 1
        fi
	echo "ok"
    done
}

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
82
drivers () {
83
    pgm="bin/why3prove$suffix"
84
    test -d $1 || exit 1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
85
    for f in $1/*.drv; do
86
        if [[ $f == drivers/ocaml*.drv ]]; then continue; fi
87
        if [[ $f == drivers/c.drv ]]; then continue; fi
88
        if [[ $f == drivers/cakeml.drv ]]; then continue; fi
89
	printf "  $f... "
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
90
	# running Why
91
	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
92
	    echo "why FAILED"
93
            echo "theory Test goal G : 1=2 end" | $pgm -F whyml --driver $f -
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
94 95
	    exit 1
	fi
Andrei Paskevich's avatar
Andrei Paskevich committed
96
	echo "ok"
97 98 99
    done
}

100
valid_goals () {
101
    bin/why3$suffix --list-provers | grep -q Alt-Ergo || return 0
102
    pgm="bin/why3prove$suffix"
103
    test -d $1 || exit 1
104
    for f in $1/*.mlw; do
105
	printf "  $f... "
106
        if ! $pgm -t 15 -P alt-ergo $2 $f > /dev/null 2>&1; then
107
            echo "FAILED!"
108 109
            echo "$pgm -t 15 -P alt-ergo $2 $f"
            $pgm -t 15 -P alt-ergo $2 $f
110
	    exit 1
Andrei Paskevich's avatar
Andrei Paskevich committed
111
       fi
112
       echo "ok"
113 114 115
    done
}

116
invalid_goals () {
117
    bin/why3$suffix --list-provers | grep -q Alt-Ergo || return 0
118
    pgm="bin/why3prove$suffix"
119
    test -d $1 || exit 1
120
    for f in $1/*.mlw; do
121
	printf "  $f... "
122 123 124 125 126 127 128 129 130 131 132
	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
}

133 134
replay () {
    pgm="bin/why3replay$suffix"
135
    test -d $1 || exit 1
136 137
    for f in $1/*/; do
        printf "  $f... "
138
        if $pgm $2 $f > /dev/null 2> /dev/null; then
139 140 141
            echo "ok"
        else
            echo "replay test failed!"
142 143
            echo $pgm $2 $f
            $pgm $2 $f
144 145 146 147 148
            exit 1
        fi
    done
}

149
execute () {
150
    pgm="bin/why3execute$suffix"
151
    printf "  $1 $2... "
152
    if $pgm $1 $2 > /dev/null; then
153 154 155
        echo "ok"
    else
        echo "execution test failed!"
156 157
        echo $pgm $1 $2
        $pgm $1 $2
158 159 160 161
        exit 1
    fi
}

162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181
extract () {
    pgm="bin/why3extract$suffix"
    dir=$1
    shift
    for f in $dir/*.mlw; do
        printf "  $f... "
        if ($pgm $@ $f -o bench_test.ml && ocaml -noinit bench_test.ml) > /dev/null 2> /dev/null; then
            echo "ok"
        else
            echo "extract test failed!"
            echo $pgm $@ $f
            $pgm $@ $f -o bench_test.ml
            ocaml -noinit bench_test.ml
            rm -f bench_test.ml
            exit 1
        fi
    done
    rm -f bench_test.ml
}

182
extract_and_run () {
183 184 185 186
    dir=$1
    shift
    prg=$1
    shift
187
    printf "  $dir... "
188
    rm -f $dir/$prg
189
    printf "clean... "
190
    if BENCH=yes make -C $dir clean > /dev/null; then
191
        printf "extract... "
192
        if BENCH=yes make -C $dir extract > /dev/null; then
193
            printf "compile... "
194
            if BENCH=yes make -C $dir > /dev/null; then
195
                printf "execute... "
196
                if $dir/main.opt "$@" > /dev/null; then
197
                    printf "doc... "
198
                    if BENCH=yes make -C $dir doc > /dev/null; then
199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217
                        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
218
        else
219 220 221
            echo "extract failed!"
            echo BENCH=yes make -C $dir extract
            BENCH=yes make -C $dir extract
222 223
            exit 1
        fi
224
    else
225 226 227
        echo "clean failed!"
        echo BENCH=yes make -C $dir clean
        BENCH=yes make -C $dir clean
228 229 230 231
        exit 1
    fi
}

232
extract_and_test_wmp () {
233
    dir=$1
234 235 236 237 238 239 240 241 242 243 244 245 246
    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!"
247 248
                    echo $dir/build/bench-tests
                    $dir/build/bench-tests
249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270
                    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
}

271
list_stuff () {
272
    pgm="bin/why3$suffix"
273
    printf '  %s ' "$1"
274
    if $pgm $1 > /dev/null; then
275 276 277 278 279 280 281 282
        echo "ok"
    else
        echo "$pgm $1 FAIL"
        $pgm $1
        exit 1
    fi
}

283 284 285
echo "=== Checking stdlib ==="
goods stdlib
goods stdlib/mach
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
286 287
echo ""

288 289 290 291
echo "=== Checking drivers ==="
drivers drivers
echo ""

292 293
echo "=== Checking bad files ==="
goods bench/typing/bad --parse-only
Andrei Paskevich's avatar
Andrei Paskevich committed
294
goods bench/programs/bad-typing --parse-only
295
goods bench/programs/warn-typing --parse-only
296
bads bench/typing/bad --type-only
297
bads bench/programs/bad-typing --type-only
298
warns bench/programs/warn-typing --type-only
299
goods bench/typing/x-bad --type-only
300 301
echo ""

302 303
echo "=== Checking good files ==="
goods bench/typing/good
304 305
goods bench/typing/x-good --parse-only
bads bench/typing/x-good --type-only
306
goods bench/programs/good
307
goods bench/ce
308
goods src/trywhy3/examples "--debug ignore_missing_diverges"
309 310 311 312 313 314 315 316 317 318 319
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"
320
goods examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_2016_matrix_multiplication"
321
goods examples/double_wp "-L examples/double_wp"
322
goods examples/in_progress/ring_decision "-L examples/in_progress/ring_decision"
323
goods examples/multiprecision "-L examples/multiprecision"
324
goods examples/prover "-L examples/prover --debug ignore_unused_vars"
325 326 327 328 329 330 331
goods examples/in_progress
echo ""

echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""

332 333 334 335
echo "=== Checking splitted valid goals ==="
valid_goals bench/valid/split_vc "-a split_vc"
echo ""

336 337 338 339
echo "=== Checking invalid goals ==="
invalid_goals bench/invalid
echo ""

340
echo "=== Checking execution ==="
MARCHE Claude's avatar
MARCHE Claude committed
341 342
execute examples/euler001.mlw Euler001.bench
execute examples/euler002.mlw Solve.bench
MARCHE Claude's avatar
MARCHE Claude committed
343
execute examples/fibonacci.mlw FibRecGhost.bench
MARCHE Claude's avatar
MARCHE Claude committed
344
execute examples/fibonacci.mlw FibonacciLogarithmic.bench
345
# fails: cannot execute Cany
346
# execute examples/same_fringe.mlw SameFringe.bench
347
# fails: cannot evaluate condition a=b (how to do it?)
348 349
# execute examples/same_fringe.mlw SameFringe.test5
execute examples/same_fringe.mlw Test.test1
350
execute examples/vstte12_combinators.mlw Combinators.test_SKK
MARCHE Claude's avatar
MARCHE Claude committed
351 352
execute examples/selection_sort.mlw SelectionSort.bench
execute examples/insertion_sort.mlw InsertionSort.bench
353
execute examples/quicksort.mlw Test.bench
354
execute examples/conjugate.mlw Test.bench
355
# fails: needs support for "val" without code (how to do it?)
356
# examples/vacid_0_sparse_array.mlw Harness.bench
Guillaume Melquiond's avatar
Guillaume Melquiond committed
357
execute examples/knuth_prime_numbers.mlw PrimeNumbers.bench
MARCHE Claude's avatar
MARCHE Claude committed
358
execute examples/vstte10_max_sum.mlw TestCase.test_case
359
execute examples/verifythis_fm2012_LRS.mlw LCP_test.bench
360 361
execute examples/verifythis_fm2012_LRS.mlw SuffixSort_test.bench
execute examples/verifythis_fm2012_LRS.mlw SuffixArray_test.bench
362
execute examples/verifythis_fm2012_LRS.mlw LRS_test.bench
MARCHE Claude's avatar
MARCHE Claude committed
363
execute examples/verifythis_PrefixSumRec.mlw PrefixSumRec.bench
MARCHE Claude's avatar
MARCHE Claude committed
364
execute examples/vstte10_queens.mlw NQueens.test8
365
# fails: "Cannot decide condition of if: (not ((~)((<<)((~)(0), 8)) = 0))"
366 367 368
# examples/queens.mlw NQueensBits.test8
# fails: cannot find definition of routine eq
# examples/residual.mlw Test.test_astar
369 370
echo ""

371
echo "=== Checking extraction to OCaml ==="
372
extract bench/extraction -D ocaml64
373
extract_and_run examples/euler001 euler001.ml 1000000
374
extract_and_run examples/gcd gcd.ml 6 15
375
extract_and_run examples/vstte10_max_sum vstte10_max_sum.ml
376 377
# needs to port
# extract_and_run examples/vstte12_combinators vstte12_combinators.ml "((((K K) K) K) K)"
378
extract_and_run examples/defunctionalization defunctionalization.ml
379
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
380 381
echo ""

382
echo "=== Checking extraction to C ==="
383 384
extract_and_test_wmp examples/in_progress/multiprecision
extract_and_test_wmp examples/multiprecision
385 386
echo ""

387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409
echo "=== Checking replay (no prover) ==="
replay bench/replay
replay examples/stdlib --merging-only
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"
replay examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_2016_matrix_multiplication --merging-only"
replay examples/double_wp "-L examples/double_wp --merging-only"
replay examples/in_progress/ring_decision "-L examples/in_progress/ring_decision --merging-only"
replay examples/multiprecision "-L examples/multiprecision --merging-only"
replay examples/prover "-L examples/prover --merging-only --debug ignore_unused_vars"
#replay examples/in_progress --merging-only
#replay examples/in_progress/multiprecision "-L examples/in_progress/multiprecision --merging-only"
echo ""

410 411 412 413 414 415 416 417
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 ""
418 419

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