bench 11.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
}

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
    pgm="bin/why3prove$suffix"
102
    test -d $1 || exit 1
103
    for f in $1/*.mlw; do
104
	printf "  $f... "
105
        if ! $pgm -t 15 -P alt-ergo $2 $f > /dev/null 2>&1; then
106
            echo "FAILED!"
107 108
            echo "$pgm -t 15 -P alt-ergo $2 $f"
            $pgm -t 15 -P alt-ergo $2 $f
109
	    exit 1
Andrei Paskevich's avatar
Andrei Paskevich committed
110
       fi
111
       echo "ok"
112 113 114
    done
}

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

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

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

MARCHE Claude's avatar
MARCHE Claude committed
160
extract_and_run () {
161 162 163 164
    dir=$1
    shift
    prg=$1
    shift
165
    printf "  $dir... "
166
    rm -f $dir/$prg
167
    printf "clean... "
168
    if BENCH=yes make -C $dir clean > /dev/null; then
169
        printf "extract... "
170
        if BENCH=yes make -C $dir extract > /dev/null; then
171
            printf "compile... "
172
            if BENCH=yes make -C $dir > /dev/null; then
173
                printf "execute... "
174
                if $dir/main.opt "$@" > /dev/null; then
175
                    printf "doc... "
176
                    if BENCH=yes make -C $dir doc > /dev/null; then
177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195
                        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
196
        else
197 198 199
            echo "extract failed!"
            echo BENCH=yes make -C $dir extract
            BENCH=yes make -C $dir extract
200 201
            exit 1
        fi
MARCHE Claude's avatar
MARCHE Claude committed
202
    else
203 204 205
        echo "clean failed!"
        echo BENCH=yes make -C $dir clean
        BENCH=yes make -C $dir clean
MARCHE Claude's avatar
MARCHE Claude committed
206 207 208 209
        exit 1
    fi
}

210
extract_and_test_wmp () {
211
    dir=$1
212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248
    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
}

249
list_stuff () {
250
    pgm="bin/why3$suffix"
251
    printf '  %s ' "$1"
252
    if $pgm $1 > /dev/null; then
253 254 255 256 257 258 259 260
        echo "ok"
    else
        echo "$pgm $1 FAIL"
        $pgm $1
        exit 1
    fi
}

261 262 263
echo "=== Checking stdlib ==="
goods stdlib
goods stdlib/mach
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
264 265
echo ""

266 267 268 269
echo "=== Checking drivers ==="
drivers drivers
echo ""

270 271
echo "=== Checking bad files ==="
goods bench/typing/bad --parse-only
Andrei Paskevich's avatar
Andrei Paskevich committed
272
goods bench/programs/bad-typing --parse-only
273
goods bench/programs/warn-typing --parse-only
274
bads bench/typing/bad --type-only
Andrei Paskevich's avatar
Andrei Paskevich committed
275
bads bench/programs/bad-typing --type-only
276
warns bench/programs/warn-typing --type-only
277
goods bench/typing/x-bad --type-only
278 279
echo ""

280 281
echo "=== Checking good files ==="
goods bench/typing/good
282 283
goods bench/typing/x-good --parse-only
bads bench/typing/x-good --type-only
284
goods bench/programs/good
285
goods bench/ce
286
goods src/trywhy3/examples "--debug ignore_missing_diverges"
287 288 289 290 291 292 293 294 295 296 297
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"
298
goods examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_2016_matrix_multiplication"
299
goods examples/double_wp "-L examples/double_wp"
300
goods examples/in_progress/ring_decision "-L examples/in_progress/ring_decision"
301
goods examples/multiprecision "-L examples/multiprecision"
302
goods examples/prover "-L examples/prover --debug ignore_unused_vars"
303 304 305
goods examples/in_progress
echo ""

306 307
echo "=== Checking replay (no prover) ==="
replay bench/replay
308
replay examples/stdlib --merging-only
309 310 311 312 313 314 315 316 317 318 319
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"
320
replay examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_2016_matrix_multiplication --merging-only"
321
replay examples/double_wp "-L examples/double_wp --merging-only"
322
replay examples/in_progress/ring_decision "-L examples/in_progress/ring_decision --merging-only"
323
replay examples/multiprecision "-L examples/multiprecision --merging-only"
324
replay examples/prover "-L examples/prover --merging-only --debug ignore_unused_vars"
325 326
#replay examples/in_progress --merging-only
#replay examples/in_progress/multiprecision "-L examples/in_progress/multiprecision --merging-only"
327 328
echo ""

329 330 331 332
echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""

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

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

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

372

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

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

388 389 390 391 392 393 394 395
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 ""
396 397

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