@@ -92,7 +92,7 @@ def run_security_analyser(config_json_file, cmdline):
92
92
93
93
94
94
def run_program_slicing (
95
- cfgs ,
95
+ cfg ,
96
96
results_dir ,
97
97
timeout ,
98
98
verbosity ,
@@ -101,59 +101,48 @@ def run_program_slicing(
101
101
prof = {"calling_slicer" : []}
102
102
prof_start_time = time .time ()
103
103
104
- result = []
105
- for cfg in cfgs :
106
- src_plain_fname = os .path .splitext (os .path .basename (cfg ["goto_binary_file" ]))[0 ]
107
- src_idx_name = int (src_plain_fname [src_plain_fname .rfind ("_" )+ 1 :])
108
- dst_goto_program_fname = os .path .join (results_dir , "sliced_goto_program_" + str (src_idx_name ) + ".gbf" )
109
- dst_goto_stats_fname = os .path .join (results_dir , "sliced_goto_program_" + str (src_idx_name ) + ".stats.json" )
104
+ dst_goto_program_fname = os .path .join (results_dir , "sliced_goto_program.gbf" )
105
+ dst_goto_stats_fname = os .path .join (results_dir , "sliced_goto_program.stats.json" )
110
106
107
+ command = (
108
+ get_goto_instrument_pathname () + " " +
109
+ "--reachability-slice " +
110
+ # "--full-slice " +
111
+ "--verbosity " + str (verbosity ) + " " +
112
+ cfg ["goto_binary_file" ] + " " +
113
+ dst_goto_program_fname + " " +
114
+ "--save-code-statistics " + dst_goto_stats_fname
115
+ )
116
+ prof_calling_goto_instrument_start_time = time .time ()
117
+ print ("Invoking 'goto-instrument' ..." )
118
+ with utility .PushCwd (results_dir ) as cwd :
119
+ if verbosity >= 9 :
120
+ print ("CWD: " + cwd .get ())
121
+ print ("CMD: " + command )
122
+ os .system (command )
123
+ #shutil.copy(cfg["goto_binary_file"], dst_goto_program_fname)
124
+
125
+ prof ["calling_slicer" ].append ({
126
+ "duration" : time .time () - prof_calling_goto_instrument_start_time
127
+ })
128
+
129
+ result = cfg .copy ()
130
+ result ["goto_binary_file" ] = dst_goto_program_fname
131
+
132
+ if dump_html_slice :
111
133
command = (
112
- get_goto_instrument_pathname () + " " +
113
- "--reachability-slice " +
114
- # "--full-slice " +
115
- "--verbosity " + str (verbosity ) + " " +
116
- cfg ["goto_binary_file" ] + " " +
134
+ get_security_analyser_pathname () + " " +
117
135
dst_goto_program_fname + " " +
118
- "--save-code-statistics " + dst_goto_stats_fname
136
+ "--dump-html-program " +
137
+ "'" + os .path .join (results_dir , "SLICED_PROGRAM_IN_HTML" ) + "'"
119
138
)
120
- prof_calling_goto_instrument_start_time = time .time ()
121
- print ("Invoking 'goto-instrument' ..." )
122
139
with utility .PushCwd (results_dir ) as cwd :
123
140
if verbosity >= 9 :
124
141
print ("CWD: " + cwd .get ())
125
142
print ("CMD: " + command )
126
143
os .system (command )
127
- #shutil.copy(cfg["goto_binary_file"], dst_goto_program_fname)
128
-
129
- prof ["calling_slicer" ].append ({
130
- "gbf_idx" : src_idx_name ,
131
- "duration" : time .time () - prof_calling_goto_instrument_start_time
132
- })
133
-
134
- result .append (cfg .copy ())
135
- result [- 1 ]["goto_binary_file" ] = dst_goto_program_fname
136
-
137
- if dump_html_slice :
138
- command = (
139
- get_security_analyser_pathname () + " " +
140
- dst_goto_program_fname + " " +
141
- "--dump-html-program " +
142
- "'" +
143
- os .path .join (
144
- results_dir ,
145
- "HTML_dump_of_sliced_GOTO_programs" ,
146
- os .path .splitext (os .path .basename (dst_goto_program_fname ))[0 ]
147
- ) +
148
- "'"
149
- )
150
- with utility .PushCwd (results_dir ) as cwd :
151
- if verbosity >= 9 :
152
- print ("CWD: " + cwd .get ())
153
- print ("CMD: " + command )
154
- os .system (command )
155
144
156
- with open (os .path .join (results_dir , "sliced_goto_programs .json" ), "w" ) as results_json :
145
+ with open (os .path .join (results_dir , "sliced_goto_program .json" ), "w" ) as results_json :
157
146
results_json .write (json .dumps (result , sort_keys = False , indent = 4 ))
158
147
159
148
prof ["duration" ] = time .time () - prof_start_time
@@ -207,44 +196,43 @@ def run_search_for_error_traces(
207
196
traces_list = []
208
197
209
198
with open (json_cfg_fname ) as data_file :
210
- cfgs = json .load (data_file )
211
- for cfg in cfgs :
212
- old_cwd = os .getcwd ()
213
- os .chdir (results_dir )
214
- # verbosity must be at least 4 for error traces to get printed!
215
- command = (
216
- get_jbmc_pathname () + " " +
217
- cfg ["goto_binary_file" ] + " " +
218
- " --trace --trace-json-extended --no-refine-strings --json-ui --unwind 10 " +
219
- "--verbosity " + str (max (verbosity , 4 )) + " "
220
- "> \" jbmc_results.json\" "
221
- )
222
- prof ["calling_jbmc" ] = {}
223
- prof_calling_jbmc_start_time = time .time ()
224
- print ("Invoking 'jbmc' ..." )
225
- if verbosity >= 9 :
226
- print ("CWD: " + results_dir )
227
- print ("CMD: " + command )
228
- os .system (command )
229
- prof ["calling_jbmc" ]["duration" ] = time .time () - prof_calling_jbmc_start_time
230
- os .chdir (old_cwd )
231
-
232
- with open (os .path .join (results_dir ,"jbmc_results.json" )) as data_file :
233
- jbmc_results = json .load (data_file )
234
- for outer_element in jbmc_results :
235
- if "result" in outer_element :
236
- for inner_element in outer_element ["result" ]:
237
- if "trace" in inner_element and len (inner_element ["trace" ]) > 0 :
238
- trace = inner_element ["trace" ]
239
- was_trace_saved = append_jbmc_error_trace_if_it_is_relevant (
240
- trace ,
241
- trace_id ,
242
- results_dir ,
243
- cfg ,
244
- traces_list
245
- )
246
- if was_trace_saved :
247
- trace_id += 1
199
+ cfg = json .load (data_file )
200
+ old_cwd = os .getcwd ()
201
+ os .chdir (results_dir )
202
+ # verbosity must be at least 4 for error traces to get printed!
203
+ command = (
204
+ get_jbmc_pathname () + " " +
205
+ cfg ["goto_binary_file" ] + " " +
206
+ " --trace --trace-json-extended --no-refine-strings --json-ui --unwind 10 " +
207
+ "--verbosity " + str (max (verbosity , 4 )) + " "
208
+ "> \" jbmc_results.json\" "
209
+ )
210
+ prof ["calling_jbmc" ] = {}
211
+ prof_calling_jbmc_start_time = time .time ()
212
+ print ("Invoking 'jbmc' ..." )
213
+ if verbosity >= 9 :
214
+ print ("CWD: " + results_dir )
215
+ print ("CMD: " + command )
216
+ os .system (command )
217
+ prof ["calling_jbmc" ]["duration" ] = time .time () - prof_calling_jbmc_start_time
218
+ os .chdir (old_cwd )
219
+
220
+ with open (os .path .join (results_dir ,"jbmc_results.json" )) as data_file :
221
+ jbmc_results = json .load (data_file )
222
+ for outer_element in jbmc_results :
223
+ if "result" in outer_element :
224
+ for inner_element in outer_element ["result" ]:
225
+ if "trace" in inner_element and len (inner_element ["trace" ]) > 0 :
226
+ trace = inner_element ["trace" ]
227
+ was_trace_saved = append_jbmc_error_trace_if_it_is_relevant (
228
+ trace ,
229
+ trace_id ,
230
+ results_dir ,
231
+ cfg ,
232
+ traces_list
233
+ )
234
+ if was_trace_saved :
235
+ trace_id += 1
248
236
249
237
with open (os .path .join (results_dir , "error_traces.json" ), "w" ) as traces_file :
250
238
traces_file .write (json .dumps (traces_list , sort_keys = True , indent = 4 ))
0 commit comments