bench 10.5 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
    rm -f bench_errors
Andrei Paskevich's avatar
Andrei Paskevich committed
19
    for f in $1/*.[wm][hl][yw] ; do
20
	printf "  $f... "
21
        opts="$2"
Andrei Paskevich's avatar
Andrei Paskevich committed
22
        if test $f = stdlib/int.mlw; then opts="$2 --type-only"; fi
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
23
	# running Why
24
	if ! $pgm $opts $f > /dev/null 2> bench_error; then
Andrei Paskevich's avatar
Andrei Paskevich committed
25 26
	    echo "FAILED!"
#            echo "env: WHY3DATA='$WHY3DATA'"
27
            echo "invocation: $pgm $opts $f" | tee -a bench_errors
28
            cat bench_error | tee -a bench_errors
29 30 31 32 33 34 35
            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
36
    done
37
    rm -f bench_error
38
    if test -n "$ERROR"; then
39
        echo "bench aborted due to the following errors:"
40 41
        cat bench_errors
        rm bench_errors
42 43
        exit 1
    fi
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
44 45 46
}

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

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

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

90
invalid_goals () {
91
    pgm="bin/why3prove$suffix"
92
    for f in $1/*.mlw; do
93
	printf "  $f... "
94 95 96 97 98 99 100 101 102 103 104
	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
}

105 106 107 108
replay () {
    pgm="bin/why3replay$suffix"
    for f in $1/*/; do
        printf "  $f... "
109
        if $pgm $2 $f > /dev/null 2> /dev/null; then
110 111 112
            echo "ok"
        else
            echo "replay test failed!"
113 114
            echo $pgm $2 $f
            $pgm $2 $f
115 116 117 118 119
            exit 1
        fi
    done
}

120
execute () {
121
    pgm="bin/why3execute$suffix"
122
    printf "  $1 $2... "
123
    if $pgm $1 $2 > /dev/null; then
124 125 126
        echo "ok"
    else
        echo "execution test failed!"
127 128
        echo $pgm $1 $2
        $pgm $1 $2
129 130 131 132
        exit 1
    fi
}

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

183 184 185 186 187 188 189 190 191 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
extract_and_test_wmp () {
    dir="examples/in_progress/multiprecision"
    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
}

222
list_stuff () {
223
    pgm="bin/why3$suffix"
224
    printf '  %s ' "$1"
225
    if $pgm $1 > /dev/null; then
226 227 228 229 230 231 232 233
        echo "ok"
    else
        echo "$pgm $1 FAIL"
        $pgm $1
        exit 1
    fi
}

234 235 236
echo "=== Checking stdlib ==="
goods stdlib
goods stdlib/mach
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
237 238
echo ""

239 240 241 242
echo "=== Checking drivers ==="
drivers drivers
echo ""

243 244
echo "=== Checking bad files ==="
goods bench/typing/bad --parse-only
Andrei Paskevich's avatar
Andrei Paskevich committed
245
goods bench/programs/bad-typing --parse-only
246
bads bench/typing/bad --type-only
Andrei Paskevich's avatar
Andrei Paskevich committed
247
bads bench/programs/bad-typing --type-only
248
goods bench/typing/x-bad --type-only
249 250
echo ""

251 252
echo "=== Checking good files ==="
goods bench/typing/good
253 254
goods bench/typing/x-good --parse-only
bads bench/typing/x-good --type-only
255
goods bench/programs/good
256
goods bench/ce
257 258 259 260 261 262 263 264 265 266 267
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"
268
goods examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_2016_matrix_multiplication"
269
goods examples/double_wp "-L examples/double_wp"
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
270
goods examples/ring_decision "-L examples/ring_decision"
271
goods examples/in_progress
272
goods examples/in_progress/multiprecision "-L examples/in_progress/multiprecision"
273 274
echo ""

275 276
echo "=== Checking replay (no prover) ==="
replay bench/replay
277
replay examples/stdlib --merging-only
278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293
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/to_port/verifythis_2016_matrix_multiplication "-L examples/to_port/verifythis_2016_matrix_multiplication --merging-only"
replay examples/double_wp "-L examples/double_wp --merging-only"
replay examples/ring_decision "-L examples/ring_decision --merging-only"
#replay examples/in_progress --merging-only
#replay examples/in_progress/multiprecision "-L examples/in_progress/multiprecision --merging-only"
294 295
echo ""

296 297 298 299 300 301 302 303
echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""

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

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

335

336
echo "=== Checking extraction to OCaml ==="
337
extract_and_run examples/euler001 euler001.ml 1000000
338
extract_and_run examples/gcd gcd.ml 6 15
339
extract_and_run examples/vstte10_max_sum vstte10_max_sum.ml
340 341
# needs to port
# extract_and_run examples/vstte12_combinators vstte12_combinators.ml "((((K K) K) K) K)"
342
extract_and_run examples/defunctionalization defunctionalization.ml
343
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
344 345
echo ""

346 347 348 349
echo "=== Checking extraction to C ==="
extract_and_test_wmp
echo ""

350 351 352 353 354 355 356 357
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 ""
358 359

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