Skip to content

Commit c9cf09f

Browse files
Popax21Popax21
committed
Recollect CFLOBVDD data
1 parent 698b212 commit c9cf09f

6 files changed

+75
-61
lines changed

‎tools/bitme/analyzor.py‎

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -97,7 +97,6 @@ class BitmeConfig:
9797

9898
class BitmeBVDDMode(enum.StrEnum):
9999
BVDD = enum.auto()
100-
ROABVDD = enum.auto()
101100
CFLOBVDD = enum.auto()
102101

103102
def __repr__(self) -> str:
@@ -127,9 +126,8 @@ def __str__(self) -> str:
127126

128127
def run_bitme(config: BitmeConfig, model: Path) -> BitmeResult:
129128
BVDD_FLAGS = {
130-
BitmeBVDDMode.BVDD: "--use-BVDD",
131-
BitmeBVDDMode.ROABVDD: "--use-ROABVDD",
132-
BitmeBVDDMode.CFLOBVDD: "--use-CFLOBVDD",
129+
BitmeBVDDMode.BVDD: ["--use-BVDD"],
130+
BitmeBVDDMode.CFLOBVDD: ["--use-CFLOBVDD", "1", "1"],
133131
}
134132
SATSOLVER_FLAGS = {
135133
BitmeSatSolver.NONE: "", # - default mode
@@ -140,12 +138,13 @@ def run_bitme(config: BitmeConfig, model: Path) -> BitmeResult:
140138
args = [
141139
BITME,
142140
"-analyzor",
143-
BVDD_FLAGS[config.bvdd_mode],
141+
*BVDD_FLAGS[config.bvdd_mode],
144142
SATSOLVER_FLAGS[config.satsolver],
145143
"-propagate",
146144
str(config.max_propagate_bits),
147145
"-array",
148146
str(config.max_array_flatten_bits),
147+
"--unroll",
149148
model,
150149
]
151150

‎tools/bitme/bitme-data-bCFLOBVDD-sZ3-p8-a0-v3.csv‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ cflobvdd-bit-inversion-5.c,,,,,
2020
cflobvdd-bit-inversion-3.c,,,,,
2121
invalid-memory-access-fail-2-35.c,,,,,
2222
cflobvdd-multi-input-4.c,,,,,
23+
cflobvdd.c,,,,,
2324
nested-if-else-1-35.c,,,,,
2425
recursive-fibonacci-1-10.c,,,,,
2526
nested-if-else-reverse-1-35.c,,,,,

‎tools/bitme/bitme-data-bCFLOBVDD-sZ3-p8-a4-v3.csv‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,17 +9,18 @@ simple-if-without-else-1-35.c,,,,,
99
cflobvdd-multi-input-3.c,,,,,
1010
three-level-nested-loop-fail-1-35.c,,,,,
1111
simple-increasing-loop-1-35.c,,,,,
12-
memory-access-fail-1-35.c,56.811555999999996,596232.0,core-0-load-seg-fault,66,0000
12+
memory-access-fail-1-35.c,59.07674333333333,629469.3333333334,core-0-load-seg-fault,66,0000
1313
cflobvdd-multi-input-5.c,,,,,
1414
simple-if-else-reverse-1-35.c,,,,,
1515
simple-assignment-1-35.c,,,,,
16-
division-by-zero-3-35.c,65.40773166666666,650962.6666666666,core-0-division-by-zero,76,3000
16+
division-by-zero-3-35.c,77.77768,689685.3333333334,core-0-division-by-zero,76,3000
1717
cflobvdd-bit-inversion-2.c,,,,,
1818
cflobvdd-multi-input-6.c,,,,,
1919
cflobvdd-bit-inversion-5.c,,,,,
2020
cflobvdd-bit-inversion-3.c,,,,,
2121
invalid-memory-access-fail-2-35.c,,,,,
2222
cflobvdd-multi-input-4.c,,,,,
23+
cflobvdd.c,20.266515666666667,360506.6666666667,core-0-load-seg-fault,31,0000
2324
nested-if-else-1-35.c,,,,,
2425
recursive-fibonacci-1-10.c,,,,,
2526
nested-if-else-reverse-1-35.c,,,,,

‎tools/bitme/bitme-data-bCFLOBVDD-sZ3-p8-a8-v3.csv‎

Lines changed: 27 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -1,29 +1,30 @@
11
sample,runtime_secs,memory_usage_kb,bad_state,bad_step,bad_input
2-
cflobvdd-bit-inversion-6.c,136.675578,1631666.6666666667,core-0-bad-exit-code,156,3300
3-
recursive-factorial-fail-1-35.c,180.39272866666667,2291024.0,core-0-bad-exit-code,398,3100
4-
simple-if-else-1-35.c,25.663527000000002,546769.3333333334,core-0-bad-exit-code,107,3100
5-
recursive-ackermann-1-35.c,96.03411433333333,1246892.0,core-0-bad-exit-code,270,3100
2+
cflobvdd-bit-inversion-6.c,89.77713566666667,1215088.0,core-0-bad-exit-code,156,3300
3+
recursive-factorial-fail-1-35.c,280.4160656666666,2117337.3333333335,core-0-bad-exit-code,398,3100
4+
simple-if-else-1-35.c,18.42349833333333,550885.3333333334,core-0-bad-exit-code,107,3100
5+
recursive-ackermann-1-35.c,92.924829,1140165.3333333333,core-0-bad-exit-code,270,3100
66
nested-recursion-fail-1-35.c,,,,,
7-
two-level-nested-loop-1-35.c,57.120737,901484.0,core-0-bad-exit-code,189,3100
8-
simple-if-without-else-1-35.c,11.661524,515832.0,core-0-bad-exit-code,106,3100
9-
cflobvdd-multi-input-3.c,31.656125666666668,709040.0,core-0-bad-exit-code,188,3000
10-
three-level-nested-loop-fail-1-35.c,237.12627999999998,2537349.3333333335,core-0-bad-exit-code,393,3100
11-
simple-increasing-loop-1-35.c,68.72782533333333,1005293.3333333334,core-0-bad-exit-code,269,3100
7+
two-level-nested-loop-1-35.c,46.869052,852714.6666666666,core-0-bad-exit-code,189,3100
8+
simple-if-without-else-1-35.c,10.701304333333333,523945.3333333333,core-0-bad-exit-code,106,3100
9+
cflobvdd-multi-input-3.c,26.010532666666666,684921.3333333334,core-0-bad-exit-code,188,3000
10+
three-level-nested-loop-fail-1-35.c,175.525881,2136977.3333333335,core-0-bad-exit-code,393,3100
11+
simple-increasing-loop-1-35.c,55.94645833333333,942506.6666666666,core-0-bad-exit-code,269,3100
1212
memory-access-fail-1-35.c,,,,,
13-
cflobvdd-multi-input-5.c,61.321812333333334,919009.3333333334,core-0-bad-exit-code,262,3000
14-
simple-if-else-reverse-1-35.c,25.473632666666663,546241.3333333334,core-0-bad-exit-code,105,3100
15-
simple-assignment-1-35.c,9.434983666666668,495156.0,core-0-bad-exit-code,91,3d00
16-
division-by-zero-3-35.c,7.100455333333334,470256.0,core-0-division-by-zero,76,3000
17-
cflobvdd-bit-inversion-2.c,20.788877666666664,614125.3333333334,core-0-bad-exit-code,118,3200
18-
cflobvdd-multi-input-6.c,86.58188533333333,1069529.3333333333,core-0-bad-exit-code,299,3000
19-
cflobvdd-bit-inversion-5.c,115.47487466666666,1370476.0,core-0-bad-exit-code,149,3300
20-
cflobvdd-bit-inversion-3.c,50.757531666666665,828698.6666666666,core-0-bad-exit-code,135,3300
21-
invalid-memory-access-fail-2-35.c,8.807429,486254.6666666667,core-0-store-invalid-address,79,3000
22-
cflobvdd-multi-input-4.c,38.51964866666666,771340.0,core-0-bad-exit-code,225,3000
23-
nested-if-else-1-35.c,27.174953333333335,576190.6666666666,core-0-bad-exit-code,113,3100
24-
recursive-fibonacci-1-10.c,145.40920733333334,1584076.0,core-0-bad-exit-code,230,3100
25-
nested-if-else-reverse-1-35.c,27.230138999999998,577086.6666666666,core-0-bad-exit-code,112,3100
26-
cflobvdd-bit-inversion-4.c,80.22934233333332,1075553.3333333333,core-0-bad-exit-code,142,3300
27-
return-from-loop-1-35.c,10.660293666666666,512733.3333333333,core-0-bad-exit-code,95,3000
28-
cflobvdd-multi-input-2.c,22.21864633333333,627497.3333333334,core-0-bad-exit-code,151,3000
29-
simple-decreasing-loop-1-35.c,58.208945,937422.6666666666,core-0-bad-exit-code,243,3100
13+
cflobvdd-multi-input-5.c,45.66959133333334,837054.6666666666,core-0-bad-exit-code,262,3000
14+
simple-if-else-reverse-1-35.c,18.558165,549608.0,core-0-bad-exit-code,105,3100
15+
simple-assignment-1-35.c,8.815695,505114.6666666667,core-0-bad-exit-code,91,0000
16+
division-by-zero-3-35.c,7.484001666666667,481781.3333333333,core-0-division-by-zero,76,3000
17+
cflobvdd-bit-inversion-2.c,17.873525666666666,599718.6666666666,core-0-bad-exit-code,118,3200
18+
cflobvdd-multi-input-6.c,60.76104899999999,941889.3333333334,core-0-bad-exit-code,299,3000
19+
cflobvdd-bit-inversion-5.c,76.14159866666667,1075160.0,core-0-bad-exit-code,149,3300
20+
cflobvdd-bit-inversion-3.c,37.374147,747396.0,core-0-bad-exit-code,135,3300
21+
invalid-memory-access-fail-2-35.c,8.751950666666668,496956.0,core-0-store-invalid-address,79,3000
22+
cflobvdd-multi-input-4.c,31.43896033333333,735842.6666666666,core-0-bad-exit-code,225,3000
23+
cflobvdd.c,4.456448,452724.0,core-0-load-seg-fault,31,0000
24+
nested-if-else-1-35.c,20.569998,574909.3333333334,core-0-bad-exit-code,113,3100
25+
recursive-fibonacci-1-10.c,148.57188666666664,1426705.3333333333,core-0-bad-exit-code,230,3100
26+
nested-if-else-reverse-1-35.c,20.336954666666667,575484.0,core-0-bad-exit-code,112,3100
27+
cflobvdd-bit-inversion-4.c,53.841184999999996,893476.0,core-0-bad-exit-code,142,3300
28+
return-from-loop-1-35.c,10.448643333333333,518068.0,core-0-bad-exit-code,95,3000
29+
cflobvdd-multi-input-2.c,18.269352666666666,609582.6666666666,core-0-bad-exit-code,151,3000
30+
simple-decreasing-loop-1-35.c,47.107724,874725.3333333334,core-0-bad-exit-code,243,3100

‎tools/bitme/bitme-data-rotor3-bCFLOBVDD-sZ3-p8-a8-v3.csv‎

Lines changed: 13 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,30 @@
11
sample,runtime_secs,memory_usage_kb,bad_state,bad_step,bad_input
2+
cflobvdd-bit-inversion-6.c,,,,,
23
recursive-factorial-fail-1-35.c,,,,,
34
simple-if-else-1-35.c,,,,,
45
recursive-ackermann-1-35.c,,,,,
56
nested-recursion-fail-1-35.c,,,,,
67
two-level-nested-loop-1-35.c,,,,,
78
simple-if-without-else-1-35.c,,,,,
9+
cflobvdd-multi-input-3.c,,,,,
810
three-level-nested-loop-fail-1-35.c,,,,,
911
simple-increasing-loop-1-35.c,,,,,
10-
memory-access-fail-1-35.c,125.29732233333334,1053076.0,core-0-load-seg-fault,66,0000
12+
memory-access-fail-1-35.c,152.046311,1169325.3333333333,core-0-load-seg-fault,66,0000
13+
cflobvdd-multi-input-5.c,,,,,
1114
simple-if-else-reverse-1-35.c,,,,,
1215
simple-assignment-1-35.c,,,,,
13-
division-by-zero-3-35.c,215.877805,946357.3333333334,core-0-division-by-zero,76,3000
16+
division-by-zero-3-35.c,251.52737433333334,1040502.6666666666,core-0-division-by-zero,76,3000
17+
cflobvdd-bit-inversion-2.c,,,,,
18+
cflobvdd-multi-input-6.c,,,,,
19+
cflobvdd-bit-inversion-5.c,,,,,
20+
cflobvdd-bit-inversion-3.c,,,,,
1421
invalid-memory-access-fail-2-35.c,,,,,
22+
cflobvdd-multi-input-4.c,,,,,
23+
cflobvdd.c,1.191449,96673.33333333333,core-0-load-seg-fault,31,0000
1524
nested-if-else-1-35.c,,,,,
1625
recursive-fibonacci-1-10.c,,,,,
1726
nested-if-else-reverse-1-35.c,,,,,
27+
cflobvdd-bit-inversion-4.c,,,,,
1828
return-from-loop-1-35.c,,,,,
29+
cflobvdd-multi-input-2.c,,,,,
1930
simple-decreasing-loop-1-35.c,,,,,

‎tools/bitme/bitme-data-rotorF-bCFLOBVDD-sZ3-p8-a8-v3.csv‎

Lines changed: 27 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -1,29 +1,30 @@
11
sample,runtime_secs,memory_usage_kb,bad_state,bad_step,bad_input
2-
cflobvdd-bit-inversion-6.c,163.4977736666667,2791708.0,core-0-bad-exit-code,156,3300
3-
recursive-factorial-fail-1-35.c,228.172944,3642778.6666666665,core-0-bad-exit-code,398,3100
4-
simple-if-else-1-35.c,39.36912233333333,1631289.3333333333,core-0-bad-exit-code,107,3100
5-
recursive-ackermann-1-35.c,129.564624,2463370.6666666665,core-0-bad-exit-code,270,3100
2+
cflobvdd-bit-inversion-6.c,114.53559766666667,2468944.0,core-0-bad-exit-code,156,3300
3+
recursive-factorial-fail-1-35.c,355.32029200000005,3601496.0,core-0-bad-exit-code,398,3100
4+
simple-if-else-1-35.c,34.41878766666667,1740628.0,core-0-bad-exit-code,107,3100
5+
recursive-ackermann-1-35.c,127.89718433333333,2451828.0,core-0-bad-exit-code,270,3100
66
nested-recursion-fail-1-35.c,,,,,
7-
two-level-nested-loop-1-35.c,80.49442033333334,2050281.3333333333,core-0-bad-exit-code,189,3100
8-
simple-if-without-else-1-35.c,23.84578833333333,1599070.6666666667,core-0-bad-exit-code,106,3100
9-
cflobvdd-multi-input-3.c,49.30454433333333,1821325.3333333333,core-0-bad-exit-code,188,3000
10-
three-level-nested-loop-fail-1-35.c,286.88438233333335,3880297.3333333335,core-0-bad-exit-code,393,3100
11-
simple-increasing-loop-1-35.c,97.76852566666666,2179533.3333333335,core-0-bad-exit-code,269,3100
7+
two-level-nested-loop-1-35.c,69.628269,2100552.0,core-0-bad-exit-code,189,3100
8+
simple-if-without-else-1-35.c,24.945095,1714229.3333333333,core-0-bad-exit-code,106,3100
9+
cflobvdd-multi-input-3.c,43.56015633333333,1898690.6666666667,core-0-bad-exit-code,188,3000
10+
three-level-nested-loop-fail-1-35.c,218.43486666666664,3553552.0,core-0-bad-exit-code,393,3100
11+
simple-increasing-loop-1-35.c,81.06128433333333,2211438.6666666665,core-0-bad-exit-code,269,3100
1212
memory-access-fail-1-35.c,,,,,
13-
cflobvdd-multi-input-5.c,84.619428,2054240.0,core-0-bad-exit-code,262,3000
14-
simple-if-else-reverse-1-35.c,39.962160000000004,1632456.0,core-0-bad-exit-code,105,3100
15-
simple-assignment-1-35.c,21.033970333333333,1573628.0,core-0-bad-exit-code,91,3d00
16-
division-by-zero-3-35.c,17.936584,1541018.6666666667,core-0-division-by-zero,76,3000
17-
cflobvdd-bit-inversion-2.c,36.09325533333333,1710198.6666666667,core-0-bad-exit-code,118,3200
18-
cflobvdd-multi-input-6.c,110.75834566666667,2222032.0,core-0-bad-exit-code,299,3000
19-
cflobvdd-bit-inversion-5.c,141.233536,2516793.3333333335,core-0-bad-exit-code,149,3300
20-
cflobvdd-bit-inversion-3.c,69.84890833333334,1942273.3333333333,core-0-bad-exit-code,135,3300
21-
invalid-memory-access-fail-2-35.c,19.153799000000003,1561438.6666666667,core-0-store-invalid-address,79,3000
22-
cflobvdd-multi-input-4.c,57.01791666666667,1893974.6666666667,core-0-bad-exit-code,225,3000
23-
nested-if-else-1-35.c,41.27282266666666,1667102.6666666667,core-0-bad-exit-code,113,3100
24-
recursive-fibonacci-1-10.c,180.47943766666666,2811878.6666666665,core-0-bad-exit-code,230,3100
25-
nested-if-else-reverse-1-35.c,41.571618666666666,1668290.6666666667,core-0-bad-exit-code,112,3100
26-
cflobvdd-bit-inversion-4.c,99.65657599999999,2200625.3333333335,core-0-bad-exit-code,142,3300
27-
return-from-loop-1-35.c,21.80108733333333,1591505.3333333333,core-0-bad-exit-code,95,3000
28-
cflobvdd-multi-input-2.c,35.94242566666667,1720592.0,core-0-bad-exit-code,151,3000
29-
simple-decreasing-loop-1-35.c,80.97381233333333,2103022.6666666665,core-0-bad-exit-code,243,3100
13+
cflobvdd-multi-input-5.c,66.399492,2071848.0,core-0-bad-exit-code,262,3000
14+
simple-if-else-reverse-1-35.c,34.85539966666667,1742253.3333333333,core-0-bad-exit-code,105,3100
15+
simple-assignment-1-35.c,22.911271666666664,1691949.3333333333,core-0-bad-exit-code,91,0000
16+
division-by-zero-3-35.c,20.086863333333334,1661417.3333333333,core-0-division-by-zero,76,3000
17+
cflobvdd-bit-inversion-2.c,34.01658,1800288.0,core-0-bad-exit-code,118,3200
18+
cflobvdd-multi-input-6.c,82.885678,2191560.0,core-0-bad-exit-code,299,3000
19+
cflobvdd-bit-inversion-5.c,97.10815266666667,2317980.0,core-0-bad-exit-code,149,3300
20+
cflobvdd-bit-inversion-3.c,54.99990333333333,1962034.6666666667,core-0-bad-exit-code,135,3300
21+
invalid-memory-access-fail-2-35.c,21.570083666666665,1680410.6666666667,core-0-store-invalid-address,79,3000
22+
cflobvdd-multi-input-4.c,49.138906999999996,1959148.0,core-0-bad-exit-code,225,3000
23+
cflobvdd.c,16.823034333333336,1625468.0,core-0-load-seg-fault,31,0000
24+
nested-if-else-1-35.c,34.996094,1771606.6666666667,core-0-bad-exit-code,113,3100
25+
recursive-fibonacci-1-10.c,183.22004266666667,2762964.0,core-0-bad-exit-code,230,3100
26+
nested-if-else-reverse-1-35.c,34.95552933333334,1772397.3333333333,core-0-bad-exit-code,112,3100
27+
cflobvdd-bit-inversion-4.c,72.03915500000001,2119656.0,core-0-bad-exit-code,142,3300
28+
return-from-loop-1-35.c,23.454661333333334,1706497.3333333333,core-0-bad-exit-code,95,3000
29+
cflobvdd-multi-input-2.c,32.413563,1810541.3333333333,core-0-bad-exit-code,151,3000
30+
simple-decreasing-loop-1-35.c,67.91053766666667,2135821.3333333335,core-0-bad-exit-code,243,3100

0 commit comments

Comments
 (0)