bench 9.24 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... "
Andrei Paskevich's avatar
Andrei Paskevich committed
80
	if $pgm -t 10 -P alt-ergo $f | grep -q -v Valid; then
81
	    echo "valid test $f failed!"
Andrei Paskevich's avatar
Andrei Paskevich committed
82 83
	    echo "$pgm -P alt-ergo $f"
	    $pgm -t 10 -P alt-ergo $f
84
	    exit 1
85
       else
86
	    echo "ok"
Andrei Paskevich's avatar
Andrei Paskevich committed
87
       fi
88 89 90
    done
}

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

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

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

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

184
list_stuff () {
185
    pgm="bin/why3$suffix"
186
    printf '  %s ' "$1"
187
    if $pgm $1 > /dev/null; then
188 189 190 191 192 193 194 195
        echo "ok"
    else
        echo "$pgm $1 FAIL"
        $pgm $1
        exit 1
    fi
}

196 197 198
echo "=== Checking stdlib ==="
goods stdlib
goods stdlib/mach
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
199 200
echo ""

201 202 203 204
echo "=== Checking drivers ==="
drivers drivers
echo ""

205 206
echo "=== Checking bad files ==="
goods bench/typing/bad --parse-only
Andrei Paskevich's avatar
Andrei Paskevich committed
207
goods bench/programs/bad-typing --parse-only
208
bads bench/typing/bad --type-only
Andrei Paskevich's avatar
Andrei Paskevich committed
209
bads bench/programs/bad-typing --type-only
210
goods bench/typing/x-bad --type-only
211 212
echo ""

213 214
echo "=== Checking good files ==="
goods bench/typing/good
215 216
goods bench/typing/x-good --parse-only
bads bench/typing/x-good --type-only
217
goods bench/programs/good
218
goods bench/ce
219 220 221 222 223 224 225 226 227 228 229
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"
230
goods examples/to_port/verifythis_2016_matrix_multiplication "-L examples/to_port/verifythis_2016_matrix_multiplication"
231
goods examples/double_wp "-L examples/double_wp"
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
232
goods examples/ring_decision "-L examples/ring_decision"
233
goods examples/in_progress
234
goods examples/in_progress/multiprecision "-L examples/in_progress/multiprecision"
235 236
echo ""

237 238
echo "=== Checking replay (no prover) ==="
replay bench/replay
239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254
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"
255 256
echo ""

257 258 259 260 261 262 263 264
echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""

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

265
echo "=== Checking execution ==="
MARCHE Claude's avatar
MARCHE Claude committed
266 267
execute examples/euler001.mlw Euler001.bench
execute examples/euler002.mlw Solve.bench
MARCHE Claude's avatar
MARCHE Claude committed
268
execute examples/fibonacci.mlw FibRecGhost.bench
MARCHE Claude's avatar
MARCHE Claude committed
269
execute examples/fibonacci.mlw FibonacciLogarithmic.bench
270
# fails: cannot execute Cany
271
# execute examples/same_fringe.mlw SameFringe.bench
272
# fails: cannot evaluate condition a=b (how to do it?)
273 274
# execute examples/same_fringe.mlw SameFringe.test5
execute examples/same_fringe.mlw Test.test1
275
execute examples/vstte12_combinators.mlw Combinators.test_SKK
MARCHE Claude's avatar
MARCHE Claude committed
276 277
execute examples/selection_sort.mlw SelectionSort.bench
execute examples/insertion_sort.mlw InsertionSort.bench
278
execute examples/quicksort.mlw Test.bench
279
execute examples/conjugate.mlw Test.bench
280
# fails: needs support for "val" without code (how to do it?)
281
# examples/vacid_0_sparse_array.mlw Harness.bench
Guillaume Melquiond's avatar
Guillaume Melquiond committed
282
execute examples/knuth_prime_numbers.mlw PrimeNumbers.bench
MARCHE Claude's avatar
MARCHE Claude committed
283
execute examples/vstte10_max_sum.mlw TestCase.test_case
284
execute examples/verifythis_fm2012_LRS.mlw LCP_test.bench
285 286
execute examples/verifythis_fm2012_LRS.mlw SuffixSort_test.bench
execute examples/verifythis_fm2012_LRS.mlw SuffixArray_test.bench
287
execute examples/verifythis_fm2012_LRS.mlw LRS_test.bench
MARCHE Claude's avatar
MARCHE Claude committed
288
execute examples/verifythis_PrefixSumRec.mlw PrefixSumRec.bench
MARCHE Claude's avatar
MARCHE Claude committed
289
execute examples/vstte10_queens.mlw NQueens.test8
290
# fails: "Cannot decide condition of if: (not ((~)((<<)((~)(0), 8)) = 0))"
291 292 293
# examples/queens.mlw NQueensBits.test8
# fails: cannot find definition of routine eq
# examples/residual.mlw Test.test_astar
294 295
echo ""

296

297
echo "=== Checking extraction to OCaml ==="
298
extract_and_run examples/euler001 euler001.ml 1000000
299
extract_and_run examples/gcd gcd.ml 6 15
300
extract_and_run examples/vstte10_max_sum vstte10_max_sum.ml
301 302
# needs to port
# extract_and_run examples/vstte12_combinators vstte12_combinators.ml "((((K K) K) K) K)"
303
extract_and_run examples/defunctionalization defunctionalization.ml
304
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
305 306
echo ""

307 308 309 310 311 312 313 314
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 ""
315 316

echo "=== Checking realizations ==="
Guillaume Melquiond's avatar
Guillaume Melquiond committed
317 318
echo "temporarily disabled"
#exec bench/check_realizations.sh