This repository was archived by the owner on Jan 28, 2022. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathtest.zsh
executable file
·103 lines (83 loc) · 4.5 KB
/
test.zsh
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
#!/usr/bin/env zsh
# Runs end-to-end workflow tests.
set -ex
function num_constraints() {
cat C | head -n 1 | awk '{ print $3 }'
}
stack run -- circom ./test/Code/Circom/bitify4.circom --setup
stack run -- circom ./test/Code/Circom/bitify4.circom -i ./test/Code/Circom/bitify4.in --prove
stack run -- verify
stack run -- c outer ./test/Code/C/fn_call.c --setup
stack run -- c outer ./test/Code/C/fn_call.c --prove -i <(echo x 1; echo y 3)
stack run -- verify
stack run -- c bar ./test/Code/C/struct_inout.c --setup
stack run -- c bar ./test/Code/C/struct_inout.c --prove -i <(echo p.x 1; echo p.y 4;)
stack run -- verify
C_no_overflow=True stack run -- c outer ./test/Code/C/fn_call.c --setup
C_no_overflow=True stack run -- c outer ./test/Code/C/fn_call.c --prove -i <(echo x 1; echo y 3)
stack run -- verify
stack run -- c outer ./test/Code/C/fn_call.c --check --setup
stack run -- c-check-prove outer ./test/Code/C/fn_call.c
stack run -- verify
stack run -- c bar ./test/Code/C/struct_inout.c --check --setup
stack run -- c-check-prove bar ./test/Code/C/struct_inout.c
stack run -- verify
C_c_sv=True stack run -- c main ./test/Code/C/sv/assume.c --check --setup
C_c_sv=True stack run -- c-check-prove main ./test/Code/C/sv/assume.c
stack run -- verify
stack run -- c sum ./test/Code/C/array_8.c --setup
stack run -- c sum ./test/Code/C/array_8.c --prove -i ./test/Code/C/inputs/array_8_sum.in
stack run -- verify
stack run -- c struct_sum ./test/Code/C/array_8.c --setup
stack run -- c struct_sum ./test/Code/C/array_8.c --prove -i ./test/Code/C/inputs/array_8_struct_sum.in
stack run -- verify
C_pequin_io=True C_no_overflow=True stack run -- c compute ./test/Code/C/pequin/mm_flat.c --setup
C_pequin_io=True C_no_overflow=True stack run -- c compute ./test/Code/C/pequin/mm_flat.c --prove -i ./test/Code/C/pequin/inputs/mm_flat.i
stack run -- verify
[[ $(num_constraints) = 125 ]]
C_smt_benes_thresh=1 C_pequin_io=True stack run -- c compute ./test/Code/C/pequin/ptrchase_8_8.c --setup
C_smt_benes_thresh=1 C_pequin_io=True stack run -- c compute ./test/Code/C/pequin/ptrchase_8_8.c --prove -i ./test/Code/C/pequin/inputs/ptrchase_8_8.i
stack run -- verify
C_smt_opts=cfee,ee,mem C_smt_check_opts=True stack run -- c flex test/Code/C/benes_arrays.c --setup
C_smt_opts=cfee,ee,mem C_smt_check_opts=True stack run -- c flex test/Code/C/benes_arrays.c --prove -i <(echo x 1; echo y 1)
stack run -- verify
C_smt_opts=cfee,ee,mem C_smt_check_opts=True stack run -- c flex test/Code/C/benes_arrays.c --setup
C_smt_opts=cfee,ee,mem C_smt_check_opts=True stack run -- c flex test/Code/C/benes_arrays.c --prove -i <(echo x 0; echo y 0)
stack run -- verify
C_smt_benes_thresh=1 C_smt_opts=cfee,ee,mem C_smt_check_opts=True stack run -- c flex test/Code/C/benes_arrays.c --setup
C_smt_benes_thresh=1 C_smt_opts=cfee,ee,mem C_smt_check_opts=True stack run -- c flex test/Code/C/benes_arrays.c --prove -i <(echo x 1; echo y 1)
stack run -- verify
stack run -- zokrates main test/Code/Zokrates/sum.zok --setup
stack run -- zokrates main test/Code/Zokrates/sum.zok --prove -i test/Code/Zokrates/inputs/sum.i
# 32-bit OpenSSL bug, found naively
C_c_sv=True stack run -- c mult test/Code/C/openssl_bug.c --check --setup
C_c_sv=True stack run -- c mult test/Code/C/openssl_bug.c --check --solve | tee out
cat out | egrep '\w+ [[:digit:]]+' > out2
mv out2 out
C_c_sv=True stack run -- c mult test/Code/C/openssl_bug.c --check --prove -i out
stack run -- verify
rm out
# 32-bit OpenSSL bug, found with an assumption
C_c_sv=True stack run -- c mult test/Code/C/openssl_bug.c --check --setup
C_c_sv=True stack run -- c mult test/Code/C/openssl_assume.c --check --solve | tee out
cat out | egrep '\w+ [[:digit:]]+' > out2
mv out2 out
C_c_sv=True stack run -- c mult test/Code/C/openssl_bug.c --check --prove -i out
stack run -- verify
rm out
# 64-bit OpenSSL bug, found with an assumption
C_c_sv=True stack run -- c mult test/Code/C/openssl_big_bug.c --check --setup
C_c_sv=True stack run -- c mult test/Code/C/openssl_big_assume.c --check --solve | tee out
cat out | egrep '\w+ [[:digit:]]+' > out2
mv out2 out
C_c_sv=True stack run -- c mult test/Code/C/openssl_big_bug.c --check --prove -i out
stack run -- verify
rm out
# 32-bit OpenSSL bug, found with a weaker assumption
C_c_sv=True stack run -- c mult test/Code/C/openssl_bug.c --check --setup
C_c_sv=True stack run -- c mult test/Code/C/openssl_weak_assume.c --check --solve | tee out
cat out | egrep '\w+ [[:digit:]]+' > out2
mv out2 out
C_c_sv=True stack run -- c mult test/Code/C/openssl_bug.c --check --prove -i out
stack run -- verify
rm out