Skip to content

Commit

Permalink
Kani optimisation blog post (#41)
Browse files Browse the repository at this point in the history
Co-authored-by: Celina Val <[email protected]>
Co-authored-by: Remi Delmas <[email protected]>
Co-authored-by: Adrian Palacios <[email protected]>
Co-authored-by: Zyad Hassan <[email protected]>
  • Loading branch information
4 people authored Aug 3, 2023
1 parent 910255c commit 59bc1c5
Show file tree
Hide file tree
Showing 19 changed files with 715 additions and 0 deletions.
373 changes: 373 additions & 0 deletions _posts/2023-08-03-turbocharging-rust-code-verification.md

Large diffs are not rendered by default.

Binary file added assets/images/cadical.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
12 changes: 12 additions & 0 deletions assets/images/field-sens-plots/sat-time.gnuplot
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
set term pngcairo size 400, 400
set output 'sat-time.png'
set logscale xy
set xlabel 'no field-sens'
set ylabel 'field-sens'
set xrange [0:1000]
set yrange [0:1000]
set size ratio 1
set title 'SAT solving time (s)'
plot 'sat-time.txt' using 2:1 with points pt 7 ps 1 lc rgb 'blue' notitle, \
x with line lt 1 lc rgb 'black' notitle

Binary file added assets/images/field-sens-plots/sat-time.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
56 changes: 56 additions & 0 deletions assets/images/field-sens-plots/sat-time.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,56 @@
1,24 900,0
7,77 900,0
6,77 900,0
10,75 17,2
0,53 0,6
0,01 0,0
0,00 0,0
0,00 0,0
0,01 900,0
0,00 900,0
0,00 13,5
0,00 51,5
0,00 0,0
0,00 0,0
0,00 0,0
0,00 0,0
0,00 0,0
0,28 0,5
0,07 0,1
0,42 0,6
0,00 0,0
4,62 5,5
31,02 35,5
12,39 31,0
0,30 0,4
0,11 0,1
0,79 1,2
0,80 0,6
0,76 1,6
0,01 0,0
0,20 0,2
0,00 0,0
0,98 1,3
4,52 6,4
0,58 0,9
13,62 9,4
127,14 115,4
50,37 54,8
0,07 0,0
417,46 436,3
103,72 74,6
1,63 1,4
1,09 4,6
1,34 2,9
0,50 1,8
2,26 8,4
0,12 0,2
0,68 2,8
1,31 1,4
14,66 15,7
343,37 364,5
0,41 0,6
42,62 45,1
0,43 86,6
0,57 119,5
0,02 0,0
12 changes: 12 additions & 0 deletions assets/images/field-sens-plots/symex-steps.gnuplot
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
set term pngcairo size 400, 400
set output 'symex-steps.png'
set logscale xy
set xlabel 'no field-sens'
set ylabel 'field-sens'
set xrange [900:1000000]
set yrange [900:1000000]
set size ratio 1
set title 'Symex steps'
plot 'symex-steps.txt' using 2:1 with points pt 7 ps 1 lc rgb 'blue' notitle, \
x with line lt 1 lc rgb 'black' notitle

Binary file added assets/images/field-sens-plots/symex-steps.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
56 changes: 56 additions & 0 deletions assets/images/field-sens-plots/symex-steps.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,56 @@
14288 66140
34219 98807
33957 98545
72521 82618
29853 28810
5250 5250
3728 3728
5774 7473
7502 10488
1765 359975
998 34009
1025 66040
2589 3482
2542 3435
2597 3490
2542 3435
2597 3490
2625 3517
2589 3482
2625 3517
2589 3482
7498 8367
11742 12587
33658 97749
21959 21934
6633 7401
31436 30426
18084 18147
9058 10749
6834 7760
4185 5062
1696 1934
6604 7298
24385 22663
4717 5451
3265 4132
4763 5667
74536 75450
2597 3490
94250 95166
43824 44741
3510 4397
22518 19546
22262 19328
21211 18515
21053 18383
2325 3242
21819 19031
13771 11636
11025 12214
98691 91330
22242 20489
3710 4603
4841 17279
11239 38095
5966 5957
12 changes: 12 additions & 0 deletions assets/images/field-sens-plots/symex-time.gnuplot
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
set term pngcairo size 400, 400
set output 'symex-time.png'
set logscale xy
set xlabel 'no field-sens'
set ylabel 'field-sens'
set xrange [1:100]
set yrange [1:100]
set size ratio 1
set title 'Symex time (s)'
plot 'symex-time.txt' using 2:1 with points pt 7 ps 1 lc rgb 'blue' notitle, \
x with line lt 1 lc rgb 'black' notitle

Binary file added assets/images/field-sens-plots/symex-time.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
56 changes: 56 additions & 0 deletions assets/images/field-sens-plots/symex-time.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,56 @@
2,27 10,33
6,15 16,72
6,14 16,71
18,75 14,58
6,52 4,60
0,56 0,57
0,65 0,58
0,85 0,96
1,22 1,39
0,61 41,94
0,12 3,67
0,14 7,37
0,40 0,34
0,40 0,33
0,40 0,34
0,40 0,33
0,40 0,33
0,40 0,33
0,40 0,33
0,40 0,33
0,40 0,33
1,02 0,89
1,67 1,47
7,16 21,32
3,53 2,83
1,14 0,94
5,65 4,21
3,33 2,55
1,26 1,14
0,91 0,83
0,65 0,53
0,18 0,17
0,91 0,69
4,30 2,69
0,74 0,56
0,57 0,49
0,61 0,54
12,10 11,11
0,46 0,36
15,96 13,16
5,77 5,09
0,56 0,42
5,14 2,61
5,12 2,62
4,51 2,35
5,15 2,57
0,38 0,32
4,74 2,48
3,75 1,57
2,49 1,77
48,59 25,68
4,23 2,97
0,52 0,44
0,71 2,56
2,02 6,67
0,82 0,80
12 changes: 12 additions & 0 deletions assets/images/field-sens-plots/total-time.gnuplot
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
set term pngcairo size 400, 400
set output 'total-time.png'
set logscale xy
set xlabel 'no field-sens'
set ylabel 'field-sens'
set xrange [1:1000]
set yrange [1:1000]
set size ratio 1
set title 'Total time (s)'
plot 'total-time.txt' using 2:1 with points pt 7 ps 1 lc rgb 'blue' notitle, \
x with line lt 1 lc rgb 'black' notitle

Binary file added assets/images/field-sens-plots/total-time.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
57 changes: 57 additions & 0 deletions assets/images/field-sens-plots/total-time.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,57 @@
5,14 900,0
19,87 900,0
16,65 900,0
42,94 43,83
12,06 9,41
0,92 0,93
0,95 0,86
2,13 2,43
2,67 900,0
0,89 900,0
0,21 20,33
0,24 66,72
0,69 0,68
0,65 0,62
0,65 0,63
0,65 0,62
0,65 0,63
0,98 1,15
0,75 0,75
1,11 1,33
0,69 0,67
7,90 8,90
36,83 41,29
26,03 66,29
21,04 19,59
4,38 4,25
53,53 48,89
17,95 16,40
3,87 4,88
2,65 2,62
1,55 1,46
0,36 0,38
3,85 3,89
20,20 19,38
2,59 2,75
14,76 10,48
129,32 117,62
77,71 81,54
0,87 0,82
459,59 474,06
126,45 92,84
2,76 2,49
14,37 13,66
14,06 11,64
10,82 8,76
18,15 19,27
1,08 1,15
12,50 11,21
7,59 5,17
19,33 19,50
497,46 463,27
10,98 7,09
44,53 47,06
1,79 97,24
4,02 142,38
2,21 2,18

12 changes: 12 additions & 0 deletions assets/images/field-sens-plots/vccs.gnuplot
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
set term pngcairo size 400, 400
set output 'vccs.png'
set logscale xy
set xlabel 'no field-sens'
set ylabel 'field-sens'
set xrange [10:10000]
set yrange [10:10000]
set size ratio 1
set title 'Number of VCCs'
plot 'vccs.txt' using 2:1 with points pt 7 ps 1 lc rgb 'blue' notitle, \
x with line lt 1 lc rgb 'black' notitle

Binary file added assets/images/field-sens-plots/vccs.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
57 changes: 57 additions & 0 deletions assets/images/field-sens-plots/vccs.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,57 @@
683 4978
1982 7677
1966 7661
5967 6477
2703 2713
403 403
299 299
281 410
458 668
92 66399
10 6002
10 11939
73 143
68 138
70 140
68 138
70 140
79 149
73 143
79 149
73 143
379 449
874 944
2902 9145
730 800
319 389
1684 1754
925 995
466 585
253 332
153 223
42 50
184 254
1013 1102
158 228
196 266
160 230
7285 7483
77 147
10788 10864
5018 5097
83 153
752 849
718 815
657 754
659 756
88 158
690 787
395 484
674 744
8224 8299
950 1020
197 267
408 1519
909 3076
358 358

Binary file added assets/images/kani-high-level.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added assets/images/kissat.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.

0 comments on commit 59bc1c5

Please sign in to comment.