1
1
import os
2
2
import time
3
3
import json
4
+ import shutil
4
5
5
6
6
7
def __get_my_dir (): return os .path .dirname (os .path .realpath (__file__ ))
7
8
8
9
9
- def get_possible_analyser_binary_pathnames ():
10
- result = []
11
- for rdir in ["./" , "../src/driver" ]:
12
- fname = os .path .abspath (os .path .join (__get_my_dir (), rdir , "security-analyzer" ))
13
- result .append (fname )
14
- return result
10
+ def get_security_analyser_pathname ():
11
+ return os .path .abspath (os .path .join (__get_my_dir (), "../src/driver/security-analyzer" ))
15
12
13
+ def get_goto_instrument_pathname ():
14
+ return os .path .abspath (os .path .join (__get_my_dir (), "../cbmc/src/goto-instrument/goto-instrument" ))
16
15
17
- def get_analyser_binary_pathname ():
18
- for fname in get_possible_analyser_binary_pathnames ():
19
- if os .path .exists (fname ) and os .path .isfile (fname ):
20
- return fname
21
- return None
16
+ def get_cbmc_pathname ():
17
+ return os .path .abspath (os .path .join (__get_my_dir (), "../cbmc/src/cbmc/cbmc" ))
22
18
19
+ def get_symex_pathname ():
20
+ return os .path .abspath (os .path .join (__get_my_dir (), "../cbmc/src/symex/symex" ))
23
21
24
- def run_analyser (
22
+
23
+ def run_security_analyser (
25
24
root_jar ,
26
25
transition_rules_file_pathname ,
27
26
timeout ,
@@ -33,23 +32,23 @@ def run_analyser(
33
32
results_dir ,
34
33
temp_root_dir
35
34
):
36
- prof = { "duration" : time .time () }
35
+ prof = {}
36
+ prof_start_time = time .time ()
37
+
37
38
if not os .path .exists (results_dir ):
38
39
os .makedirs (results_dir )
39
40
40
41
# Building the program JSON file (the list of all JARs application consists of) for the security analyser
41
42
program_json_fname = os .path .abspath (os .path .join (results_dir , "program.json" ))
42
43
print ("Building the program JSON file (the list of all JARs application consists of) for the 'goto-analyser': "
43
44
+ program_json_fname )
44
- program_json_file = open (program_json_fname ,"w" )
45
- program_jars_list = [ os .path .relpath (root_jar ,results_dir ) ]
46
- program_json_file .write (json .dumps (program_jars_list ,sort_keys = True ,indent = 4 ))
47
- program_json_file .close ()
45
+ with open (program_json_fname ,"w" ) as program_json_file :
46
+ program_jars_list = [ os .path .relpath (root_jar ,results_dir ) ]
47
+ program_json_file .write (json .dumps (program_jars_list ,sort_keys = True ,indent = 4 ))
48
48
49
49
# Building the root config file for the security analyser
50
50
root_config_json_fname = os .path .abspath (os .path .join (results_dir , "config.json" ))
51
51
print ("Building the root config JSON file for 'goto-analyser': " + root_config_json_fname )
52
- root_config_json_file = open (root_config_json_fname ,"w" )
53
52
root_config_json = {
54
53
"program" : "./program.json" ,
55
54
"rules" : os .path .relpath (transition_rules_file_pathname ,results_dir ),
@@ -77,27 +76,142 @@ def run_analyser(
77
76
root_config_json ["dump_html_program" ] = True
78
77
else :
79
78
root_config_json ["dump_html_program" ] = False
80
- root_config_json_file . write ( json . dumps ( root_config_json , sort_keys = True , indent = 4 ))
81
- root_config_json_file .close ( )
79
+ with open ( root_config_json_fname , "w" ) as root_config_json_file :
80
+ root_config_json_file .write ( json . dumps ( root_config_json , sort_keys = True , indent = 4 ) )
82
81
83
82
if not os .path .exists (results_dir ):
84
83
os .makedirs (results_dir )
85
84
86
85
old_cwd = os .getcwd ()
87
86
os .chdir (results_dir )
88
87
command = (
89
- get_analyser_binary_pathname () + " "
88
+ get_security_analyser_pathname () + " "
90
89
+ "'./" + os .path .relpath (root_jar ,results_dir ) + "' "
91
90
"--security-scanner '" + os .path .relpath (root_config_json_fname ,results_dir ) + "' "
92
91
)
93
- prof ["calling_goto_analyser" ] = { "duration" : time .time () }
94
- print ("Invoking 'security_analyser' ..." )
92
+ prof ["calling_goto_analyser" ] = {}
93
+ prof_calling_goto_analyser_start_time = time .time ()
94
+ print ("Invoking 'security-analyser' ..." )
95
95
if verbosity >= 9 :
96
96
print ("CWD: " + results_dir )
97
97
print ("CMD: " + command )
98
98
os .system (command )
99
- prof ["calling_goto_analyser" ]["duration" ] = time .time () - prof [ "calling_goto_analyser" ][ "duration" ]
99
+ prof ["calling_goto_analyser" ]["duration" ] = time .time () - prof_calling_goto_analyser_start_time
100
100
os .chdir (old_cwd )
101
- prof ["duration" ] = time .time () - prof ["duration" ]
101
+ prof ["duration" ] = time .time () - prof_start_time
102
+
103
+ return prof
104
+
105
+
106
+ def run_program_slicing (
107
+ json_cfg_fname ,
108
+ results_dir ,
109
+ timeout ,
110
+ verbosity
111
+ ):
112
+ prof = {}
113
+ prof_start_time = time .time ()
102
114
115
+ # TODO: once the slicer in "goto-instrument" tool is available, then provide proper implementation here!
116
+ # Until then we assume the slicing removes nothing from the instrumented program.
117
+ shutil .copyfile (json_cfg_fname , os .path .join (os .path .dirname (json_cfg_fname ),"sliced_goto_programs.json" ))
118
+
119
+ prof ["duration" ] = time .time () - prof_start_time
103
120
return prof
121
+
122
+
123
+ def append_cbmc_error_trace_if_it_is_relevant (trace , trace_id , results_dir , cfg , traces_list ):
124
+ """A trace is relevant, if it ends at a sink."""
125
+ was_trace_saved = False
126
+ last_rec = trace [- 1 ]
127
+ if "sourceLocation" in last_rec :
128
+ loc = last_rec ["sourceLocation" ]
129
+ for sink in cfg ["sinks" ]:
130
+ if loc ["file" ] == sink ["file" ] and \
131
+ loc ["function" ] == sink ["function" ] and \
132
+ loc ["line" ] == str (sink ["line" ]):
133
+ trace_fname = os .path .join (results_dir , "error_trace_" + str (trace_id ) + ".json" )
134
+ with open (trace_fname , "w" ) as trace_file :
135
+ trace_file .write (json .dumps (trace , sort_keys = False , indent = 4 ))
136
+ was_trace_saved = True
137
+
138
+ found = False
139
+ for rec in traces_list :
140
+ if rec ["file" ] == sink ["file" ] and \
141
+ rec ["function" ] == sink ["function" ] and \
142
+ rec ["line" ] == sink ["line" ] and \
143
+ rec ["goto_binary_file" ] == cfg ["goto_binary_file" ]:
144
+ rec ["error_traces" ].append (trace_fname )
145
+ if found == False :
146
+ rec = sink
147
+ rec ["goto_binary_file" ] = cfg ["goto_binary_file" ]
148
+ rec ["error_traces" ] = [trace_fname ]
149
+ traces_list .append (rec )
150
+ break
151
+ return was_trace_saved
152
+
153
+
154
+ def run_search_for_error_traces (
155
+ json_cfg_fname ,
156
+ results_dir ,
157
+ timeout ,
158
+ verbosity
159
+ ):
160
+ prof = {}
161
+ prof_start_time = time .time ()
162
+ if not os .path .exists (results_dir ):
163
+ os .makedirs (results_dir )
164
+
165
+ trace_id = 0
166
+ traces_list = []
167
+
168
+ with open (json_cfg_fname ) as data_file :
169
+ cfgs = json .load (data_file )
170
+ for cfg in cfgs :
171
+ old_cwd = os .getcwd ()
172
+ os .chdir (results_dir )
173
+ command = (
174
+ get_cbmc_pathname () + " " +
175
+ cfg ["goto_binary_file" ] + " " +
176
+ " --trace --lazy-methods --json-ui --unwind 10 " +
177
+ "--verbosity " + str (1 ) + " "
178
+ "> \" cbmc_results.json\" "
179
+ )
180
+ prof ["calling_cbmc" ] = {}
181
+ prof_calling_cbmc_start_time = time .time ()
182
+ print ("Invoking 'cbmc' ..." )
183
+ if verbosity >= 9 :
184
+ print ("CWD: " + results_dir )
185
+ print ("CMD: " + command )
186
+ os .system (command )
187
+ prof ["calling_cbmc" ]["duration" ] = time .time () - prof_calling_cbmc_start_time
188
+ os .chdir (old_cwd )
189
+
190
+ with open (os .path .join (results_dir ,"cbmc_results.json" )) as data_file :
191
+ cbmc_results = json .load (data_file )
192
+ for outer_element in cbmc_results :
193
+ if "result" in outer_element :
194
+ for inner_element in outer_element ["result" ]:
195
+ if "trace" in inner_element and len (inner_element ["trace" ]) > 0 :
196
+ trace = inner_element ["trace" ]
197
+ was_trace_saved = append_cbmc_error_trace_if_it_is_relevant (
198
+ trace ,
199
+ trace_id ,
200
+ results_dir ,
201
+ cfg ,
202
+ traces_list
203
+ )
204
+ if was_trace_saved :
205
+ trace_id += 1
206
+
207
+ with open (os .path .join (results_dir , "error_traces.json" ), "w" ) as traces_file :
208
+ traces_file .write (json .dumps (traces_list , sort_keys = True , indent = 4 ))
209
+
210
+ prof ["duration" ] = time .time () - prof_start_time
211
+ return prof
212
+
213
+
214
+
215
+
216
+ if __name__ == "__main__" :
217
+ pass
0 commit comments