Extension of the Python driver script w.r.t. calling of the slicer.

Once the slicer is functional, it can be enabled by uncommenting 2 lines in the script. The code was tested with the functional slicer in Lucas'es local branch (There is PR to CBMC repo; not merged yet).

Author: marek-trtik

security-scanner/analyser.py

@@ -109,12 +109,46 @@ def run_program_slicing(
         timeout,
         verbosity
         ):
-    prof = {}
+    prof = { "calling_goto_instrument": [] }
     prof_start_time = time.time()
 
-    # TODO: once the slicer in "goto-instrument" tool is available, then provide proper implementation here!
-    #       Until then we assume the slicing removes nothing from the instrumented program.
-    shutil.copyfile(json_cfg_fname, os.path.join(os.path.dirname(json_cfg_fname),"sliced_goto_programs.json"))
+    with open(json_cfg_fname) as data_file:
+        cfgs = json.load(data_file)
+
+    result = []
+    for cfg in cfgs:
+        src_plain_fname = os.path.splitext(os.path.basename(cfg["goto_binary_file"]))[0]
+        src_idx_name = int(src_plain_fname[src_plain_fname.rfind("_")+1:])
+        dst_goto_program_fname = os.path.join(results_dir, "sliced_goto_program_" + str(src_idx_name) + ".gbf")
+
+        old_cwd = os.getcwd()
+        os.chdir(results_dir)
+        command = (
+            get_goto_instrument_pathname() + " " +
+            "--full-slice " +
+            "--verbosity " + str(1) + " " +
+            cfg["goto_binary_file"] + " " +
+            "-o " + dst_goto_program_fname
+            )
+        prof_calling_goto_instrument_start_time = time.time()
+        print("Invoking 'goto-instrument' ...")
+        if verbosity >= 9:
+            print("CWD: " + results_dir)
+            print("CMD: " + command)
+        # TODO: Uncomment the next line when the slicer is functional!
+        # os.system(command)
+        prof["calling_goto_instrument"].append({
+            "gbf_idx": src_idx_name,
+            "duration": time.time() - prof_calling_goto_instrument_start_time
+            })
+        os.chdir(old_cwd)
+
+        result.append(cfg.copy())
+        # TODO: Uncomment the next line when the slicer is functional!
+        # result[-1]["goto_binary_file"] = dst_goto_program_fname
+
+    with open(os.path.join(results_dir, "sliced_goto_programs.json"), "w") as results_json:
+        results_json.write(json.dumps(result, sort_keys=False, indent=4))
 
     prof["duration"] = time.time() - prof_start_time
     return prof