Skip to content

Commit e577b8a

Browse files
SohrabiAlirSohrabiAlir
committed
visualization scripts
1 parent 1054e2c commit e577b8a

File tree

2 files changed

+248
-0
lines changed

2 files changed

+248
-0
lines changed

‎aazmaa.py‎

Lines changed: 179 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,179 @@
1+
import subprocess
2+
import time
3+
import os
4+
import seaborn as sns
5+
import matplotlib.pyplot as plt
6+
import numpy as np
7+
8+
9+
10+
TIMEOUT = 60 #seconds
11+
12+
13+
14+
15+
examples = """division-by-zero-3-35-beaten.btor2 division-by-zero-3-35.c
16+
cflobvdd-beaten.btor2 cflobvdd-multi-input-6.c return-from-loop-1-35-beaten.btor2
17+
cflobvdd-bit-inversion-2-beaten.btor2 cflobvdd-rotorized.btor2 return-from-loop-1-35-rotorized.btor2
18+
cflobvdd-bit-inversion-2-rotorized.btor2 cflobvdd.c return-from-loop-1-35.c
19+
cflobvdd-bit-inversion-2.c cflobvdd-multi-input-6-rotorized.btor2 simple-assignment-1-35-beaten.btor2
20+
cflobvdd-bit-inversion-3-beaten.btor2 division-by-zero-3-35-rotorized.btor2 simple-assignment-1-35-rotorized.btor2
21+
cflobvdd-bit-inversion-3-rotorized.btor2 recursive-fibonacci-1-10.c simple-assignment-1-35.c
22+
cflobvdd-bit-inversion-3.c invalid-memory-access-fail-2-35-beaten.btor2 simple-decreasing-loop-1-35-beaten.btor2
23+
cflobvdd-bit-inversion-4-beaten.btor2 invalid-memory-access-fail-2-35-rotorized.btor2 simple-decreasing-loop-1-35-rotorized.btor2
24+
cflobvdd-bit-inversion-4-rotorized.btor2 invalid-memory-access-fail-2-35.c simple-decreasing-loop-1-35.c
25+
cflobvdd-bit-inversion-4.c memory-access-fail-1-35-beaten.btor2 simple-if-else-1-35-beaten.btor2
26+
cflobvdd-bit-inversion-5-beaten.btor2 memory-access-fail-1-35-rotorized.btor2 simple-if-else-1-35-rotorized.btor2
27+
cflobvdd-bit-inversion-5-rotorized.btor2 memory-access-fail-1-35.c simple-if-else-1-35.c
28+
cflobvdd-bit-inversion-5.c nested-if-else-1-35-beaten.btor2 simple-if-else-reverse-1-35-beaten.btor2
29+
cflobvdd-bit-inversion-6-beaten.btor2 nested-if-else-1-35-rotorized.btor2 simple-if-else-reverse-1-35-rotorized.btor2
30+
cflobvdd-bit-inversion-6-rotorized.btor2 nested-if-else-1-35.c simple-if-else-reverse-1-35.c
31+
cflobvdd-bit-inversion-6.c nested-if-else-reverse-1-35-beaten.btor2 simple-if-without-else-1-35-beaten.btor2
32+
cflobvdd-multi-input-2-beaten.btor2 nested-if-else-reverse-1-35-rotorized.btor2 simple-if-without-else-1-35-rotorized.btor2
33+
cflobvdd-multi-input-2-rotorized.btor2 nested-if-else-reverse-1-35.c simple-if-without-else-1-35.c
34+
cflobvdd-multi-input-2.c nested-recursion-fail-1-35-beaten.btor2 simple-increasing-loop-1-35-beaten.btor2
35+
cflobvdd-multi-input-3-beaten.btor2 nested-recursion-fail-1-35-rotorized.btor2 simple-increasing-loop-1-35-rotorized.btor2
36+
cflobvdd-multi-input-3-rotorized.btor2 nested-recursion-fail-1-35.c simple-increasing-loop-1-35.c
37+
cflobvdd-multi-input-3.c recursive-ackermann-1-35-beaten.btor2 three-level-nested-loop-fail-1-35-beaten.btor2
38+
cflobvdd-multi-input-4-beaten.btor2 recursive-ackermann-1-35-rotorized.btor2 three-level-nested-loop-fail-1-35-rotorized.btor2
39+
cflobvdd-multi-input-4-rotorized.btor2 recursive-ackermann-1-35.c three-level-nested-loop-fail-1-35.c
40+
cflobvdd-multi-input-4.c recursive-factorial-fail-1-35-beaten.btor2 two-level-nested-loop-1-35-beaten.btor2
41+
cflobvdd-multi-input-5-beaten.btor2 recursive-factorial-fail-1-35-rotorized.btor2 two-level-nested-loop-1-35-rotorized.btor2
42+
cflobvdd-multi-input-5-rotorized.btor2 recursive-factorial-fail-1-35.c two-level-nested-loop-1-35.c
43+
cflobvdd-multi-input-5.c recursive-fibonacci-1-10-beaten.btor2
44+
cflobvdd-multi-input-6-beaten.btor2 recursive-fibonacci-1-10-rotorized.btor2""".split()
45+
neu_examples = []
46+
for i in range(len(examples)):
47+
if examples[i][-1] == 'c':
48+
neu_examples.append("examples/symbolic/"+examples[i])
49+
print(examples[i])
50+
examples = neu_examples
51+
52+
53+
result32 = subprocess.run(["./rotor", "-m32", "-c", "test.c", "-o", "test32.m", "-", "1", "-o", "test32.btor2"], capture_output=True, text=True)
54+
result64 = subprocess.run(["./rotor", "-m64", "-c", "test.c", "-o", "test64.m", "-", "1", "-o", "test64.btor2"], capture_output=True, text=True)
55+
size = os.path.getsize("test32.btor2")
56+
size2 = os.path.getsize("test64.btor2")
57+
58+
print(size)
59+
print(size2)
60+
61+
times32bit = []
62+
times64bit = []
63+
64+
sizes32bit = []
65+
sizes64bit = []
66+
67+
mems32bits = []
68+
mems64bits = []
69+
70+
71+
N = 2*len(examples)
72+
timedoutcnt32 = 0 # len(examples)
73+
timedoutcnt64 = 0 # len(examples)
74+
for examp in examples[:]:
75+
print(examp)
76+
examp2 = examp[:-2]
77+
result32 = subprocess.run(["./rotor", "-m32", "-c", f"{examp2}.c", "-o", f"{examp2}32.m", "-", "1", "-o", f"{examp2}32.btor2"], capture_output=True, text=True)
78+
result64 = subprocess.run(["./rotor", "-m64", "-c", f"{examp2}.c", "-o", f"{examp2}64.m", "-", "1", "-o", f"{examp2}64.btor2"], capture_output=True, text=True)
79+
80+
size32 = os.path.getsize(f"{examp2}32.btor2")
81+
size64 = os.path.getsize(f"{examp2}64.btor2")
82+
sizes32bit.append(size32)
83+
sizes64bit.append(size64)
84+
85+
86+
87+
print(examp[:-2])
88+
time1 = time.time()
89+
# cmnd = f"/usr/bin/time -v tools/bitme.py {examp2}32.btor2 -kmin 0 -kmax 120 -array 8 --unroll -propagate 8 --use-CFLOBVDD"
90+
cmnd = f"/usr/bin/time -v tools/bitme.py {examp2}32.btor2 -kmin 0 -kmax 120 -array 8 --unroll -propagate 8 --use-CFLOBVDD --check-termination"
91+
print(cmnd)
92+
try:
93+
bitme32 = subprocess.run(cmnd.split(), capture_output=True, text=True, timeout=TIMEOUT)
94+
# mem32 = int(bitme32.stderr.replace('\t', "").split('\n')[9][36:])
95+
print("RRRrrrRRrRrrrRRRrrRrrrrRr@$3RWEfFDfrf3#$FE3f\nRRrrrRRrRrrrRRRrrRrrrrRr@$3RWEfFDfrf3#\nRRrrrRRrRrrrRRRrrRrrrrRr@$3RWEfFDfrf3#\nRRrrrRRrRrrrRRRrrRrrrrRr@$3RWEfFDfrf3#\nRRrrrRRrRrrrRRRrrRrrrrRr@$3RWEfFDfrf3#\nRRrrrRRrRrrrRRRrrRrrrrRr@$3RWEfFDfrf3#\n")
96+
except subprocess.TimeoutExpired:
97+
print("timedout")
98+
timedoutcnt32 += 1
99+
except:
100+
print("Rsldkjvnsdlfkjsdfklj\nRRsldkjvnsdlfkjsdfklj\nrsldkjvnsdlfkjsdfklj\nrsldkjvnsdlfkjsdfklj\nrsldkjvnsdlfkjsdfklj\nRsldkjvnsdlfkjsdfklj\nRsldkjvnsdlfkjsdfklj\nrsldkjvnsdlfkjsdfklj\nRsldkjvnsdlfkjsdfklj\nrrsldkjvnsdlfkjsdfklj\nrRsldkjvnsdlfkjsdfklj\nRRrsldkjvnsdlfkjsdfklj\nrsldkjvnsdlfkjsdfklj\nRrrsldkjvnsdlfkjsdfklj\nrsldkjvnsdlfkjsdfklj\nrRr")
101+
102+
time2 = time.time()
103+
# cmnd = f"/usr/bin/time -v tools/bitme.py {examp2}64.btor2 -kmin 0 -kmax 120 -array 8 --unroll -propagate 8 --use-CFLOBVDD"
104+
cmnd = f"/usr/bin/time -v tools/bitme.py {examp2}64.btor2 -kmin 0 -kmax 120 -array 8 --unroll -propagate 8 --use-CFLOBVDD --check-termination"
105+
try:
106+
bitme64 = subprocess.run(cmnd.split(), capture_output=True, text=True, timeout=TIMEOUT)
107+
# mem64 = int(bitme32.stderr.replace('\t', "").split('\n')[9][36:])
108+
print("RRRrrrRRrRrrrRRRrrRrrrrRr@$3RWEfFDfrf3#$FE3f\nRRrrrRRrRrrrRRRrrRrrrrRr@$3RWEfFDfrf3#\nRRrrrRRrRrrrRRRrrRrrrrRr@$3RWEfFDfrf3#\nRRrrrRRrRrrrRRRrrRrrrrRr@$3RWEfFDfrf3#\nRRrrrRRrRrrrRRRrrRrrrrRr@$3RWEfFDfrf3#\nRRrrrRRrRrrrRRRrrRrrrrRr@$3RWEfFDfrf3#\n")
109+
except subprocess.TimeoutExpired:
110+
print("timedout")
111+
timedoutcnt64 += 1
112+
except:
113+
print("Rsldkjvnsdlfkjsdfklj\nRRsldkjvnsdlfkjsdfklj\nrsldkjvnsdlfkjsdfklj\nrsldkjvnsdlfkjsdfklj\nrsldkjvnsdlfkjsdfklj\nRsldkjvnsdlfkjsdfklj\nRsldkjvnsdlfkjsdfklj\nrsldkjvnsdlfkjsdfklj\nRsldkjvnsdlfkjsdfklj\nrrsldkjvnsdlfkjsdfklj\nrRsldkjvnsdlfkjsdfklj\nRRrsldkjvnsdlfkjsdfklj\nrsldkjvnsdlfkjsdfklj\nRrrsldkjvnsdlfkjsdfklj\nrsldkjvnsdlfkjsdfklj\nrRr")
114+
time3 = time.time()
115+
116+
117+
118+
print("32bit size:", size32)
119+
print("64bit size:", size64)
120+
print()
121+
print("32bit time:", time2-time1)
122+
print("64bit time:", time3-time2)
123+
print()
124+
print()
125+
times32bit.append(time2-time1)
126+
times64bit.append(time3-time2)
127+
128+
129+
130+
131+
exp_samples3 = np.random.exponential(scale=1.6, size=30)
132+
exp_samples = np.random.normal(scale=1.0, size=30)
133+
x = np.linspace(0, 10, 100)
134+
135+
fig, axs = plt.subplots(1, 4, figsize=(12, 4)) # 1 row, 3 columns
136+
137+
axs[0].bar(["successful", "timedout32", "timedout64"], [N - timedoutcnt32 - timedoutcnt64, timedoutcnt32, timedoutcnt64], color=["forestgreen", "firebrick", "darkorange"])
138+
axs[0].set_title("Timedout experiments")
139+
140+
141+
sns.violinplot(data=[sizes32bit, sizes64bit], ax=axs[1], split=True)
142+
axs[1].set_xticks([0, 1])
143+
axs[1].set_xticklabels(["32-bit", "64-bit"])
144+
axs[1].set_title("model size")
145+
146+
147+
sns.violinplot(data=[times32bit, times64bit], ax=axs[2], split=True)
148+
axs[2].set_xticks([0, 1])
149+
axs[2].set_xticklabels(["32-bit", "64-bit"])
150+
axs[2].set_title("bitme time consumption")
151+
152+
153+
sns.violinplot(data=[exp_samples, exp_samples3], ax=axs[3], split=True)
154+
axs[3].set_xticks([0, 1])
155+
axs[3].set_xticklabels(["32-bit", "64-bit"])
156+
axs[3].set_title("bitme memory consumption")
157+
158+
159+
160+
161+
162+
163+
plt.tight_layout()
164+
plt.savefig("plot.png")
165+
166+
167+
168+
169+
170+
171+
172+
173+
"""
174+
175+
tools/bitme.py examples/symbolic/division-by-zero-3-35-beaten.btor2 -kmin 0 -kmax 120 -array 8 --unroll -propagate 8 --use-CFLOBVDD
176+
tools/bitme.py examples/symbolic/division-by-zero-3-35.btor2 -kmin 0 -kmax 120 -array 8 --unroll -propagate 8 --use-CFLOBVDD
177+
tools/bitme.py examples/symbolic/recursive-fibonacci-1-1032.btor2 -kmin 0 -kmax 120 -array 8 --unroll -propagate 8 --use-CFLOBVDD
178+
179+
"""

‎dasti.py‎

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
import subprocess
2+
import time
3+
import os
4+
import seaborn as sns
5+
import matplotlib.pyplot as plt
6+
import numpy as np
7+
8+
LEVEL = 8
9+
SWITCH = 8
10+
FORK = 8
11+
12+
TIMEOUT = 200
13+
14+
MODEL_PATH = "cflobvdd64.btor2"
15+
16+
17+
18+
times = np.zeros((SWITCH, FORK))
19+
for i in range(0, SWITCH, 2):
20+
for j in range(0, FORK, 2):
21+
try:
22+
cmnd = f"tools/bitme.py {MODEL_PATH} -array 9 -kmin 0 --check-termination --unroll -propagate 8 --use-CFLOBVDD {j} {i} {LEVEL}"
23+
strt_time = time.time()
24+
bitme = subprocess.run(cmnd.split(), capture_output=True, text=True, timeout=TIMEOUT)
25+
end_time = time.time()
26+
elapsed_time = end_time-strt_time
27+
print()
28+
print(cmnd, " : ", elapsed_time)
29+
times[i, j] = elapsed_time
30+
except:
31+
print(f"error for fork={j} and switch={i}")
32+
times[i, j] = 0
33+
34+
35+
36+
sns.heatmap(times, annot=True, fmt=".2f", cmap="Blues", vmin=0)
37+
#plt.colorbar(label="Value")
38+
plt.title("Rutime based on switch and fork heights (s)")
39+
plt.xlabel("Fork Height")
40+
plt.ylabel("Switch Height")
41+
plt.tight_layout()
42+
plt.savefig("plot.png")
43+
44+
45+
46+
47+
48+
49+
50+
51+
52+
53+
54+
55+
56+
57+
58+
59+
60+
61+
62+
63+
64+
65+
"""
66+
./rotor -m64 -c examples/symbolic/cflobvdd.c -o cflobvdd64.m - 1 -o cflobvdd64.btor2
67+
68+
tools/bitme.py cflobvdd64.btor2 -array 9 -kmin 0 --check-termination --unroll -propagate 8 --use-CFLOBVDD 0 1 7
69+
"""

0 commit comments

Comments
 (0)