bench 7.31 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
suffix=$1
Andrei Paskevich's avatar
Andrei Paskevich committed
11

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
12
goods () {
13
    pgm="bin/why3prove$suffix"
14
    ERROR=
Andrei Paskevich's avatar
Andrei Paskevich committed
15
    for f in $1/*.[wm][hl][yw] ; do
Andrei Paskevich's avatar
Andrei Paskevich committed
16
	echo -n "  $f... "
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
17
	# running Why
18
	if ! $pgm $2 $f > /dev/null 2> bench_error; then
Andrei Paskevich's avatar
Andrei Paskevich committed
19
20
	    echo "FAILED!"
#            echo "env: WHY3DATA='$WHY3DATA'"
21
            echo "invocation: $pgm $2 $f"
22
23
24
25
26
27
28
29
            cat bench_error
            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
30
    done
31
32
33
34
    rm bench_error
    if test -n "$ERROR"; then
        exit 1
    fi
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
35
36
37
}

bads () {
38
    pgm="bin/why3prove$suffix"
Andrei Paskevich's avatar
Andrei Paskevich committed
39
40
    for f in $1/*.[wm][hl][yw] ; do
	echo -n "  $f... "
41
	if $pgm $2 $f > /dev/null 2>&1; then
Andrei Paskevich's avatar
Andrei Paskevich committed
42
43
44
	    echo "SHOULD FAIL!"
#            echo "env: WHY3DATA='$WHY3DATA'"
            echo "invocation: $pgm $2 $f"
45
	    exit 1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
46
	fi
Andrei Paskevich's avatar
Andrei Paskevich committed
47
	echo "ok"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
48
49
50
    done
}

Jean-Christophe Filliâtre's avatar
drivers    
Jean-Christophe Filliâtre committed
51
drivers () {
52
    pgm="bin/why3prove$suffix"
Jean-Christophe Filliâtre's avatar
drivers    
Jean-Christophe Filliâtre committed
53
    for f in $1/*.drv; do
54
        if [[ $f == drivers/ocaml*.drv ]]; then continue; fi
55
        if [[ $f == drivers/c.drv ]]; then continue; fi
Andrei Paskevich's avatar
Andrei Paskevich committed
56
	echo -n "  $f... "
Jean-Christophe Filliâtre's avatar
drivers    
Jean-Christophe Filliâtre committed
57
	# running Why
58
	if ! echo "theory Test goal G : 1=2 end" | $pgm -F whyml --driver $f - > /dev/null; then
Jean-Christophe Filliâtre's avatar
drivers    
Jean-Christophe Filliâtre committed
59
	    echo "why FAILED"
60
            echo "theory Test goal G : 1=2 end" | $pgm -F whyml --driver $f -
Jean-Christophe Filliâtre's avatar
drivers    
Jean-Christophe Filliâtre committed
61
62
	    exit 1
	fi
Andrei Paskevich's avatar
Andrei Paskevich committed
63
	echo "ok"
64
65
66
    done
}

67
valid_goals () {
68
    pgm="bin/why3prove$suffix"
69
70
    for f in $1/*.mlw; do
	echo -n "  "$f"... "
Andrei Paskevich's avatar
Andrei Paskevich committed
71
	if $pgm -t 10 -P alt-ergo $f | grep -q -v Valid; then
72
	    echo "valid test $f failed!"
Andrei Paskevich's avatar
Andrei Paskevich committed
73
74
	    echo "$pgm -P alt-ergo $f"
	    $pgm -t 10 -P alt-ergo $f
75
	    exit 1
76
       else
77
	    echo "ok"
Andrei Paskevich's avatar
Andrei Paskevich committed
78
       fi
79
80
81
    done
}

82
invalid_goals () {
83
    pgm="bin/why3prove$suffix"
84
85
86
87
88
89
90
91
92
93
94
95
96
    for f in $1/*.mlw; do
	echo -n "  "$f"... "
	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
}

97
execute () {
98
    pgm="bin/why3execute$suffix"
99
    echo -n "$1 $2... "
100
    if $pgm $1 $2 > /dev/null; then
101
102
103
        echo "ok"
    else
        echo "execution test failed!"
104
105
        echo $pgm $1 $2
        $pgm $1 $2
106
107
108
109
        exit 1
    fi
}

MARCHE Claude's avatar
MARCHE Claude committed
110
extract_and_run () {
111
112
113
114
115
116
    dir=$1
    shift
    prg=$1
    shift
    echo -n "$dir... "
    rm -f $dir/$prg
MARCHE Claude's avatar
MARCHE Claude committed
117
    echo -n "clean... "
118
    if BENCH=yes make -C $dir clean > /dev/null; then
MARCHE Claude's avatar
MARCHE Claude committed
119
        echo -n "extract... "
120
        if BENCH=yes make -C $dir extract > /dev/null; then
MARCHE Claude's avatar
MARCHE Claude committed
121
            echo -n "compile... "
122
            if BENCH=yes make -C $dir > /dev/null; then
MARCHE Claude's avatar
MARCHE Claude committed
123
                echo -n "execute... "
124
                if $dir/main.opt "$@" > /dev/null; then
MARCHE Claude's avatar
MARCHE Claude committed
125
                    echo -n "doc... "
126
                    if BENCH=yes make -C $dir doc > /dev/null; then
MARCHE Claude's avatar
MARCHE Claude committed
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
                        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
MARCHE Claude's avatar
MARCHE Claude committed
146
        else
MARCHE Claude's avatar
MARCHE Claude committed
147
148
149
            echo "extract failed!"
            echo BENCH=yes make -C $dir extract
            BENCH=yes make -C $dir extract
MARCHE Claude's avatar
MARCHE Claude committed
150
151
            exit 1
        fi
MARCHE Claude's avatar
MARCHE Claude committed
152
    else
MARCHE Claude's avatar
MARCHE Claude committed
153
154
155
        echo "clean failed!"
        echo BENCH=yes make -C $dir clean
        BENCH=yes make -C $dir clean
MARCHE Claude's avatar
MARCHE Claude committed
156
157
158
159
        exit 1
    fi
}

160
list_stuff () {
161
    pgm="bin/why3$suffix"
162
    echo -n "$1 "
163
    if $pgm $1 > /dev/null; then
164
165
166
167
168
169
170
171
        echo "ok"
    else
        echo "$pgm $1 FAIL"
        $pgm $1
        exit 1
    fi
}

172
echo "=== Checking theories ==="
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
173
goods theories --type-only # FIXME remove --type-only
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
174
175
echo ""

176
echo "=== Checking modules ==="
177
178
goods modules
goods modules/mach
Jean-Christophe Filliâtre's avatar
drivers    
Jean-Christophe Filliâtre committed
179
180
echo ""

181
182
183
184
echo "=== Checking drivers ==="
drivers drivers
echo ""

185
186
echo "=== Checking bad files ==="
goods bench/typing/bad --parse-only
Andrei Paskevich's avatar
Andrei Paskevich committed
187
goods bench/programs/bad-typing --parse-only
188
bads bench/typing/bad --type-only
Andrei Paskevich's avatar
Andrei Paskevich committed
189
bads bench/programs/bad-typing --type-only
190
191
echo ""

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
echo "=== Checking good files ==="
goods bench/typing/good
goods bench/programs/good
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"
goods examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_2016_matrix_multiplication"
goods examples/double_wp "-L examples/double_wp"
goods examples/in_progress
echo ""

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

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

219
echo "=== Checking execution ==="
MARCHE Claude's avatar
MARCHE Claude committed
220
221
execute examples/euler001.mlw Euler001.bench
execute examples/euler002.mlw Solve.bench
MARCHE Claude's avatar
MARCHE Claude committed
222
execute examples/fibonacci.mlw FibRecGhost.bench
MARCHE Claude's avatar
MARCHE Claude committed
223
execute examples/fibonacci.mlw FibonacciLogarithmic.bench
224
# fails: cannot execute Cany
225
# execute examples/same_fringe.mlw SameFringe.bench
226
# fails: cannot evaluate condition a=b (how to do it?)
227
228
# execute examples/same_fringe.mlw SameFringe.test5
execute examples/same_fringe.mlw Test.test1
MARCHE Claude's avatar
MARCHE Claude committed
229
execute examples/vstte12_combinators.mlw Combinators.test_SKK
MARCHE Claude's avatar
MARCHE Claude committed
230
231
execute examples/selection_sort.mlw SelectionSort.bench
execute examples/insertion_sort.mlw InsertionSort.bench
232
execute examples/quicksort.mlw Test.bench
233
execute examples/conjugate.mlw Test.bench
234
# fails: needs support for "val" without code (how to do it?)
235
# examples/vacid_0_sparse_array.mlw Harness.bench
236
execute examples/knuth_prime_numbers.mlw PrimeNumbers.bench
MARCHE Claude's avatar
MARCHE Claude committed
237
execute examples/vstte10_max_sum.mlw TestCase.test_case
238
execute examples/verifythis_fm2012_LRS.mlw LCP_test.bench
239
240
execute examples/verifythis_fm2012_LRS.mlw SuffixSort_test.bench
execute examples/verifythis_fm2012_LRS.mlw SuffixArray_test.bench
241
execute examples/verifythis_fm2012_LRS.mlw LRS_test.bench
242
execute examples/verifythis_PrefixSumRec.mlw PrefixSumRec.bench
MARCHE Claude's avatar
MARCHE Claude committed
243
execute examples/vstte10_queens.mlw NQueens.test8
244
# fails: "Cannot decide condition of if: (not ((~)((<<)((~)(0), 8)) = 0))"
245
246
247
# examples/queens.mlw NQueensBits.test8
# fails: cannot find definition of routine eq
# examples/residual.mlw Test.test_astar
248
249
echo ""

250

251
echo "=== Checking extraction to OCaml ==="
252
253
extract_and_run examples/euler001 euler001.ml 1000000
extract_and_run examples/gcd gcd.ml 6 15
254
255
256
extract_and_run examples/vstte10_max_sum vstte10_max_sum.ml
extract_and_run examples/vstte12_combinators vstte12_combinators.ml "((((K K) K) K) K)"
extract_and_run examples/defunctionalization defunctionalization.ml
257
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
258
259
echo ""

260
261
262
263
264
265
266
267
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 ""