-
Notifications
You must be signed in to change notification settings - Fork 0
/
utility.py
180 lines (129 loc) · 4.28 KB
/
utility.py
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
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
import os
import subprocess
import constant
def telegram_notification(message: str):
"""
Send a message to a Telegram chat using the Telegram API.
:param message: The message to send.
:return: None
"""
API_KEY = constant.TL_API_KEY
CHAT_ID = constant.TL_CHAT_ID
_message = '%20'.join(message.split())
cmd = f'curl -s "https://api.telegram.org/bot{API_KEY}/sendMessage?chat_id={CHAT_ID}&text={_message}"'
subprocess.call(cmd, shell=True)
def generate_instance(tool_path: str, file_path: str, unwind: int, rounds: int) -> tuple:
"""
Generate the instance to be solved by cbmc with lazycseq.
:param tool_path: The path of tool 'lazycseq'.
:param file_path: The path of the file to be solved.
:param unwind: The number of times the loop must be unwinded.
:param rounds: The number of rounds to be executed.
:return: The stdout and the stderr of the execution.
"""
os.chdir(tool_path)
cmd = f'\
./lazycseq.py \
-i {file_path} \
--unwind {unwind} \
--rounds {rounds} \
--seq \
'
process = subprocess.Popen(
cmd.split(),
stdout=subprocess.PIPE,
stderr=subprocess.PIPE
)
process.wait()
_output, _error = process.communicate()
return _output.decode('utf-8'), _error.decode('utf-8')
def run_cbmc(tool_path: str, file_path: str, unwind: int, object_bits: int) -> tuple:
"""
Run cbmc on the instance generated by lazycseq.
:param file_path: The path of the file to be solved.
:param unwind: The number of times the loop must be unwinded.
:param object_bits: The number of bits of the object.
:return: The stdout and the stderr of the execution.
"""
os.chdir(tool_path)
cmd = f'\
./cbmc \
{file_path} \
--unwind {unwind} \
--stop-on-fail \
--object-bits {object_bits} \
--trace \
'
process = subprocess.Popen(
cmd.split(),
stdout=subprocess.PIPE,
stderr=subprocess.PIPE
)
_output, _error = process.communicate()
return _output.decode('utf-8'), _error.decode('utf-8')
def get_solution(file_path: str) -> list:
"""
Get the solution from the log file of cbmc (we find variable 'var_to_get').
:param file_path: The path of the file to be solved.
:return: The solution
"""
_solution = list()
try:
log_file = open(file_path, 'r')
lines = log_file.readlines()
log_file.close()
except IOError as e:
print(f'File {file_path} not found')
print(f'Error: {e}')
if lines[-2] == 'VERIFICATION SUCCESSFUL':
print('VERIFICATION SUCCESSFUL')
return []
for line in lines:
if 'var_to_get' in line:
line = line.replace(' ', '')
line = line.replace('l', '')
line = line.replace('var_to_get[', '')
line = line.replace(']', '')
line = line.replace(line[line.find('('):], '')
line = line.split('=')
try:
index = int(line[0])
value = int(line[1])
except ValueError:
index = -1
value = -1
if len(_solution) < index + 1:
_solution.append(value)
else:
_solution[index] = value
return _solution
def move(_from: str, _to: str) -> None:
"""
Move a file from a path to another.
:param _from: The path of the file to move.
:param _to: The path where to move the file.
:return: None
"""
os.system(f'mv {_from} {_to}')
def copy(_from: str, _to: str) -> None:
"""
Copy a file from a path to another.
:param _from: The path of the file to copy.
:param _to: The path where to copy the file.
:return: None
"""
os.system(f'cp {_from} {_to}')
def create_folder(folder_path: str) -> None:
"""
Create a folder.
:param folder_path: The path of the folder to create.
:return: None
"""
os.mkdir(folder_path)
def purge_folder(folder_path: str) -> None:
"""
Delete all the files in a folder.
:param folder_path: The path of the folder to purge.
:return: None
"""
os.system(f'rm -rf {folder_path}/*')