|
1 | 1 | import os
|
2 | 2 | import time
|
3 | 3 | import json
|
4 |
| -import shutil |
| 4 | +import utility |
5 | 5 |
|
6 | 6 |
|
7 | 7 | def __get_my_dir(): return os.path.dirname(os.path.realpath(__file__))
|
@@ -109,12 +109,44 @@ def run_program_slicing(
|
109 | 109 | timeout,
|
110 | 110 | verbosity
|
111 | 111 | ):
|
112 |
| - prof = {} |
| 112 | + prof = {"calling_slicer": []} |
113 | 113 | prof_start_time = time.time()
|
114 | 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")) |
| 115 | + with open(json_cfg_fname) as data_file: |
| 116 | + cfgs = json.load(data_file) |
| 117 | + |
| 118 | + result = [] |
| 119 | + for cfg in cfgs: |
| 120 | + src_plain_fname = os.path.splitext(os.path.basename(cfg["goto_binary_file"]))[0] |
| 121 | + src_idx_name = int(src_plain_fname[src_plain_fname.rfind("_")+1:]) |
| 122 | + dst_goto_program_fname = os.path.join(results_dir, "sliced_goto_program_" + str(src_idx_name) + ".gbf") |
| 123 | + |
| 124 | + command = ( |
| 125 | + get_goto_instrument_pathname() + " " + |
| 126 | + "--full-slice " + |
| 127 | + "--verbosity " + str(1) + " " + |
| 128 | + cfg["goto_binary_file"] + " " + |
| 129 | + "-o " + dst_goto_program_fname |
| 130 | + ) |
| 131 | + prof_calling_goto_instrument_start_time = time.time() |
| 132 | + print("Invoking 'goto-instrument' ...") |
| 133 | + with utility.PushCwd(results_dir) as cwd: |
| 134 | + if verbosity >= 9: |
| 135 | + print("CWD: " + cwd.get()) |
| 136 | + print("CMD: " + command) |
| 137 | + # TODO: Uncomment the next line when the slicer is functional! |
| 138 | + # os.system(command) |
| 139 | + prof["calling_slicer"].append({ |
| 140 | + "gbf_idx": src_idx_name, |
| 141 | + "duration": time.time() - prof_calling_goto_instrument_start_time |
| 142 | + }) |
| 143 | + |
| 144 | + result.append(cfg.copy()) |
| 145 | + # TODO: Uncomment the next line when the slicer is functional! |
| 146 | + # result[-1]["goto_binary_file"] = dst_goto_program_fname |
| 147 | + |
| 148 | + with open(os.path.join(results_dir, "sliced_goto_programs.json"), "w") as results_json: |
| 149 | + results_json.write(json.dumps(result, sort_keys=False, indent=4)) |
118 | 150 |
|
119 | 151 | prof["duration"] = time.time() - prof_start_time
|
120 | 152 | return prof
|
@@ -175,7 +207,7 @@ def run_search_for_error_traces(
|
175 | 207 | get_cbmc_pathname() + " " +
|
176 | 208 | cfg["goto_binary_file"] + " " +
|
177 | 209 | " --trace --lazy-methods --json-ui --unwind 10 " +
|
178 |
| - "--verbosity " + str(1) + " " |
| 210 | + "--verbosity " + str(verbosity) + " " |
179 | 211 | "> \"cbmc_results.json\""
|
180 | 212 | )
|
181 | 213 | prof["calling_cbmc"] = {}
|
|
0 commit comments