bench 6.98 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"
Andrei Paskevich's avatar
Andrei Paskevich committed
14
    for f in $1/*.[wm][hl][yw] ; do
15
	printf "  $f... "
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
16
17
	# running Why
	if ! $pgm $2 $f > /dev/null 2>&1; then
Andrei Paskevich's avatar
Andrei Paskevich committed
18
19
	    echo "FAILED!"
#            echo "env: WHY3DATA='$WHY3DATA'"
20
21
            echo "invocation: $pgm $2 $f"
            echo "result:"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
22
23
24
	    $pgm $2 $f
	    exit 1
	fi
Andrei Paskevich's avatar
Andrei Paskevich committed
25
	echo "ok"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
26
27
28
29
    done
}

bads () {
30
    pgm="bin/why3prove$suffix"
Andrei Paskevich's avatar
Andrei Paskevich committed
31
    for f in $1/*.[wm][hl][yw] ; do
32
	printf "  $f... "
33
	if $pgm $2 $f > /dev/null 2>&1; then
Andrei Paskevich's avatar
Andrei Paskevich committed
34
35
36
	    echo "SHOULD FAIL!"
#            echo "env: WHY3DATA='$WHY3DATA'"
            echo "invocation: $pgm $2 $f"
37
	    exit 1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
38
	fi
Andrei Paskevich's avatar
Andrei Paskevich committed
39
	echo "ok"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
40
41
42
    done
}

Jean-Christophe Filliâtre's avatar
drivers    
Jean-Christophe Filliâtre committed
43
drivers () {
44
    pgm="bin/why3prove$suffix"
Jean-Christophe Filliâtre's avatar
drivers    
Jean-Christophe Filliâtre committed
45
    for f in $1/*.drv; do
46
        if [[ $f == drivers/ocaml*.drv ]]; then continue; fi
47
	printf "  $f... "
Jean-Christophe Filliâtre's avatar
drivers    
Jean-Christophe Filliâtre committed
48
	# running Why
49
	if ! echo "theory Test goal G : 1=2 end" | $pgm -F why --driver $f - > /dev/null 2>&1; then
Jean-Christophe Filliâtre's avatar
drivers    
Jean-Christophe Filliâtre committed
50
	    echo "why FAILED"
51
            echo "theory Test goal G : 1=2 end" | $pgm -F why --driver $f -
Jean-Christophe Filliâtre's avatar
drivers    
Jean-Christophe Filliâtre committed
52
53
	    exit 1
	fi
Andrei Paskevich's avatar
Andrei Paskevich committed
54
	echo "ok"
55
56
57
    done
}

58
valid_goals () {
59
    pgm="bin/why3prove$suffix"
60
    for f in $1/*.mlw; do
61
	printf "  "$f"... "
Andrei Paskevich's avatar
Andrei Paskevich committed
62
	if $pgm -t 10 -P alt-ergo $f | grep -q -v Valid; then
63
	    echo "valid test $f failed!"
Andrei Paskevich's avatar
Andrei Paskevich committed
64
65
	    echo "$pgm -P alt-ergo $f"
	    $pgm -t 10 -P alt-ergo $f
66
	    exit 1
67
       else
68
	    echo "ok"
Andrei Paskevich's avatar
Andrei Paskevich committed
69
       fi
70
71
72
    done
}

73
invalid_goals () {
74
    pgm="bin/why3prove$suffix"
75
    for f in $1/*.mlw; do
76
	printf "  "$f"... "
77
78
79
80
81
82
83
84
85
86
87
	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
}

88
execute () {
89
    pgm="bin/why3execute$suffix"
90
    printf "$1 $2... "
91
    if $pgm $1 $2 > /dev/null 2>&1; then
92
93
94
        echo "ok"
    else
        echo "execution test failed!"
95
96
        echo $pgm $1 $2
        $pgm $1 $2
97
98
99
100
        exit 1
    fi
}

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

151
list_stuff () {
152
    pgm="bin/why3$suffix"
MARCHE Claude's avatar
MARCHE Claude committed
153
    printf '%s ' "$1"
Andrei Paskevich's avatar
Andrei Paskevich committed
154
    if $pgm $1 > /dev/null 2>&1; then
155
156
157
158
159
160
161
162
        echo "ok"
    else
        echo "$pgm $1 FAIL"
        $pgm $1
        exit 1
    fi
}

163
164
165
166
echo "=== Checking invalid goals ==="
invalid_goals bench/invalid
echo ""

167
168
echo "=== Checking theories ==="
goods theories
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
169
170
echo ""

171
172
echo "=== Checking modules ==="
goods modules
173
goods modules/mach
Jean-Christophe Filliâtre's avatar
drivers    
Jean-Christophe Filliâtre committed
174
175
echo ""

176
177
178
179
echo "=== Checking drivers ==="
drivers drivers
echo ""

180
181
echo "=== Checking bad files ==="
goods bench/typing/bad --parse-only
Andrei Paskevich's avatar
Andrei Paskevich committed
182
goods bench/programs/bad-typing --parse-only
183
bads bench/typing/bad --type-only
Andrei Paskevich's avatar
Andrei Paskevich committed
184
bads bench/programs/bad-typing --type-only
MARCHE Claude's avatar
MARCHE Claude committed
185
bads examples/bad-bts
186
187
echo ""

188
189
echo "=== Checking good files ==="
goods bench/typing/good
Andrei Paskevich's avatar
Andrei Paskevich committed
190
goods bench/programs/good
191
192
193
194
195
goods examples/bts
goods examples/tests
goods examples/tests-provers
goods examples/check-builtin
goods examples/logic
Andrei Paskevich's avatar
Andrei Paskevich committed
196
197
goods examples
goods examples/foveoos11-cm
198
goods examples/WP_revisited
199
200
goods examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps"
goods examples/bitvectors "-L examples/bitvectors"
201
202
203
goods examples/in_progress
echo ""

204
echo "=== Checking execution ==="
MARCHE Claude's avatar
MARCHE Claude committed
205
206
execute examples/euler001.mlw Euler001.bench
execute examples/euler002.mlw Solve.bench
MARCHE Claude's avatar
MARCHE Claude committed
207
execute examples/fibonacci.mlw FibRecGhost.bench
MARCHE Claude's avatar
MARCHE Claude committed
208
execute examples/fibonacci.mlw FibonacciLogarithmic.bench
209
210
# fails: definition of psymbol eq not found
# execute examples/same_fringe.mlw SameFringe.bench
211
212
213
214
# fails: cannot evaluate condition a=b (how to do it?)
# execute examples/same_fringe.mlw --exec SameFringe.test5
# fails: "let" are cloned as "val"
# execute examples/same_fringe.mlw --exec Test.test1
MARCHE Claude's avatar
MARCHE Claude committed
215
execute examples/vstte12_combinators.mlw Combinators.test_SKK
MARCHE Claude's avatar
MARCHE Claude committed
216
217
execute examples/selection_sort.mlw SelectionSort.bench
execute examples/insertion_sort.mlw InsertionSort.bench
218
execute examples/quicksort.mlw Test.bench
219
execute examples/conjugate.mlw Test.bench
220
221
# fails: needs support for "val" without code (how to do it?)
# examples/vacid_0_sparse_array.mlw --exec Harness.bench
222
execute examples/knuth_prime_numbers.mlw PrimeNumbers.bench
MARCHE Claude's avatar
MARCHE Claude committed
223
execute examples/vstte10_max_sum.mlw TestCase.test_case
224
execute examples/verifythis_fm2012_LRS.mlw LCP_test.bench
225
226
execute examples/verifythis_fm2012_LRS.mlw SuffixSort_test.bench
execute examples/verifythis_fm2012_LRS.mlw SuffixArray_test.bench
227
execute examples/verifythis_fm2012_LRS.mlw LRS_test.bench
228
execute examples/verifythis_PrefixSumRec.mlw PrefixSumRec.bench
MARCHE Claude's avatar
MARCHE Claude committed
229
execute examples/vstte10_queens.mlw NQueens.test8
230
# fails: "Cannot decide condition of if: (not ((~)((<<)((~)(0), 8)) = 0))"
MARCHE Claude's avatar
MARCHE Claude committed
231
# examples/queens.mlw --exec  NQueensBits.test8
232
233
# fails: "let" are cloned as "val"
# examples/in_progress/residual.mlw --exec Test.test_astar
234
235
echo ""

MARCHE Claude's avatar
MARCHE Claude committed
236
echo "=== Extraction to Ocaml ==="
MARCHE Claude's avatar
MARCHE Claude committed
237
extract_and_run examples/euler001 euler001__*.ml 1000000
238
extract_and_run examples/gcd gcd__*.ml 6 15
MARCHE Claude's avatar
MARCHE Claude committed
239
extract_and_run examples/vstte10_max_sum vstte10_max_sum__*.ml
240
extract_and_run examples/vstte12_combinators vstte12_combinators__*.ml "((((K K) K) K) K)"
241
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
242
extract_and_run examples/defunctionalization defunctionalization__*.ml
MARCHE Claude's avatar
MARCHE Claude committed
243
244
echo ""

245
246
247
248
echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""

249
250
251
252
253
254
255
256
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 ""