Security analyser drivers: cbmc -> jbmc

smowton · smowton · commit 6b3e1443ec78 · 2017-10-20T17:51:08.000+01:00
diff --git a/benchmarks/TRAINING/diffblue/taint_traces_01_evaluator.json b/benchmarks/TRAINING/diffblue/taint_traces_01_evaluator.json
@@ -17,7 +17,7 @@
                     {
                         "error_traces":
                             {
-                                "cbmc":
+                                "jbmc":
                                     [
                                         "search_for_error_traces/error_trace_0.json"
                                     ],
diff --git a/benchmarks/TRAINING/diffblue/taint_traces_04_evaluator.json b/benchmarks/TRAINING/diffblue/taint_traces_04_evaluator.json
@@ -16,7 +16,7 @@
                 [
                     {
                         "error_traces": {
-                            "cbmc": [
+                            "jbmc": [
                                 "search_for_error_traces/error_trace_0.json"
                             ], 
                             "symex": []
@@ -28,7 +28,7 @@
                     }, 
                     {
                         "error_traces": {
-                            "cbmc": [
+                            "jbmc": [
                                 "search_for_error_traces/error_trace_1.json"
                             ], 
                             "symex": []
@@ -40,7 +40,7 @@
                     }, 
                     {
                         "error_traces": {
-                            "cbmc": [
+                            "jbmc": [
                                 "search_for_error_traces/error_trace_2.json"
                             ], 
                             "symex": []
diff --git a/benchmarks/TRAINING/diffblue/taint_traces_05_evaluator.json b/benchmarks/TRAINING/diffblue/taint_traces_05_evaluator.json
@@ -16,7 +16,7 @@
                 [
                     {
                         "error_traces": {
-                            "cbmc": [
+                            "jbmc": [
                                 "search_for_error_traces/error_trace_0.json"
                             ], 
                             "symex": []
diff --git a/benchmarks/TRAINING/diffblue/taint_traces_06_evaluator.json b/benchmarks/TRAINING/diffblue/taint_traces_06_evaluator.json
@@ -16,7 +16,7 @@
                 [
                     {
                         "error_traces": {
-                            "cbmc": [
+                            "jbmc": [
                                 "search_for_error_traces/error_trace_0.json"
                             ], 
                             "symex": []
@@ -28,7 +28,7 @@
                     }, 
                     {
                         "error_traces": {
-                            "cbmc": [
+                            "jbmc": [
                                 "search_for_error_traces/error_trace_1.json"
                             ], 
                             "symex": []
diff --git a/benchmarks/TRAINING/diffblue/taint_traces_07_evaluator.json b/benchmarks/TRAINING/diffblue/taint_traces_07_evaluator.json
@@ -16,7 +16,7 @@
                 [
                     {
                         "error_traces": {
-                            "cbmc": [
+                            "jbmc": [
                                 "search_for_error_traces/error_trace_0.json"
                             ], 
                             "symex": []
diff --git a/benchmarks/evaluator.py b/benchmarks/evaluator.py
@@ -119,7 +119,7 @@ def __compare_computed_and_expected_results(error_traces, record):
         file_line = expected_loc_traces["file"] + "', line " + str(expected_loc_traces["line"])
         if not loc_traces:
             return "There are missing error traces for the sink location '" + file_line + "."
-        if len(expected_loc_traces["error_traces"]["cbmc"]) != len(loc_traces["error_traces"]["cbmc"]):
+        if len(expected_loc_traces["error_traces"]["jbmc"]) != len(loc_traces["error_traces"]["jbmc"]):
             return "Wrong number of CBMC generated error traces for the sink location '" + file_line + "."
         if len(expected_loc_traces["error_traces"]["symex"]) != len(loc_traces["error_traces"]["symex"]):
             return "Wrong number of SYMEX generated error traces for the sink location '" + file_line + "."
@@ -212,7 +212,7 @@ def __main():
             print("PASSED:\"" + benchmark["sources-dir"] + "\"")
         return 0    # success (for Travis)
     except Exception as e:
-        print("ERROR: " + str(e))
+        print("ERROR: " + repr(e))
         return 1    # failure (for Travis)
     except:
         print("ERROR: Unknown exception was raised.")
diff --git a/driver/analyser.py b/driver/analyser.py
@@ -34,8 +34,8 @@ def get_goto_instrument_pathname():
     return os.path.abspath(os.path.join(_tools_binary_dir, "goto-instrument"))
 
 
-def get_cbmc_pathname():
-    return os.path.abspath(os.path.join(_tools_binary_dir, "cbmc"))
+def get_jbmc_pathname():
+    return os.path.abspath(os.path.join(_tools_binary_dir, "jbmc"))
 
 
 def get_symex_pathname():
@@ -167,7 +167,7 @@ def run_program_slicing(
     return prof
 
 
-def append_cbmc_error_trace_if_it_is_relevant(trace, trace_id, results_dir, cfg, traces_list):
+def append_jbmc_error_trace_if_it_is_relevant(trace, trace_id, results_dir, cfg, traces_list):
     """A trace is relevant, if it ends at a sink."""
     was_trace_saved = False
     last_rec = trace[-1]
@@ -188,12 +188,12 @@ def append_cbmc_error_trace_if_it_is_relevant(trace, trace_id, results_dir, cfg,
                        rec["function"] == sink["function"] and \
                        rec["line"] == sink["line"] and \
                        rec["goto_binary_file"] == cfg["goto_binary_file"]:
-                        rec["error_traces"]["cbmc"].append(trace_fname)
+                        rec["error_traces"]["jbmc"].append(trace_fname)
                         found = True
                 if found == False:
                     rec = sink.copy()
                     rec["goto_binary_file"] = cfg["goto_binary_file"]
-                    rec["error_traces"] = { "cbmc": [trace_fname], "symex": [] }
+                    rec["error_traces"] = { "jbmc": [trace_fname], "symex": [] }
                     traces_list.append(rec)
                 break
     return was_trace_saved
@@ -220,30 +220,30 @@ def run_search_for_error_traces(
         os.chdir(results_dir)
         # verbosity must be at least 4 for error traces to get printed!
         command = (
-            get_cbmc_pathname() + " " +
+            get_jbmc_pathname() + " " +
             cfg["goto_binary_file"] + " " +
             " --trace --lazy-methods --json-ui --unwind 10 " +
             "--verbosity " + str(max(verbosity, 4)) + " "
-            "> \"cbmc_results.json\""
+            "> \"jbmc_results.json\""
             )
-        prof["calling_cbmc"] = {}
-        prof_calling_cbmc_start_time = time.time()
-        print("Invoking 'cbmc' ...")
+        prof["calling_jbmc"] = {}
+        prof_calling_jbmc_start_time = time.time()
+        print("Invoking 'jbmc' ...")
         if verbosity >= 9:
             print("CWD: " + results_dir)
             print("CMD: " + command)
         os.system(command)
-        prof["calling_cbmc"]["duration"] = time.time() - prof_calling_cbmc_start_time
+        prof["calling_jbmc"]["duration"] = time.time() - prof_calling_jbmc_start_time
         os.chdir(old_cwd)
 
-        with open(os.path.join(results_dir,"cbmc_results.json")) as data_file:
-            cbmc_results = json.load(data_file)
-        for outer_element in cbmc_results:
+        with open(os.path.join(results_dir,"jbmc_results.json")) as data_file:
+            jbmc_results = json.load(data_file)
+        for outer_element in jbmc_results:
             if "result" in outer_element:
                 for inner_element in outer_element["result"]:
                     if "trace" in inner_element and len(inner_element["trace"]) > 0:
                         trace=inner_element["trace"]
-                        was_trace_saved = append_cbmc_error_trace_if_it_is_relevant(
+                        was_trace_saved = append_jbmc_error_trace_if_it_is_relevant(
                                                 trace,
                                                 trace_id,
                                                 results_dir,
diff --git a/driver/presentation.py b/driver/presentation.py
@@ -401,13 +401,13 @@ def build_HTML_interface_to_error_traces(root_dir,sub_dir,ofile):
         ofile.write("  <tr>\n")
         ofile.write("    <td>" + traces_group["file"] + "</td>\n")
         ofile.write("    <td>" + str(traces_group["line"]) + "</td>\n")
-        if len(traces_group["error_traces"]["cbmc"]) > 0:
-            ofile.write("    <td align=\"center\"><a href=\"./" + sub_dir + "/error_traces_cbmc_" + str(group_idx) +
+        if len(traces_group["error_traces"]["jbmc"]) > 0:
+            ofile.write("    <td align=\"center\"><a href=\"./" + sub_dir + "/error_traces_jbmc_" + str(group_idx) +
                         ".html\">here</a></td>\n")
-            with open(os.path.join(full_sub_dir,"error_traces_cbmc_" + str(group_idx) + ".html"),"w") as group_ofile:
+            with open(os.path.join(full_sub_dir,"error_traces_jbmc_" + str(group_idx) + ".html"),"w") as group_ofile:
                 build_HTML_interface_to_group_of_error_traces(
                         traces_group["error_traces"],
-                        "cbmc",
+                        "jbmc",
                         traces_group["file"],
                         traces_group["line"],
                         group_ofile)
@@ -707,7 +707,7 @@ def build_HTML_interface_to_results_and_statistics(
 
 
         ofile.write("<h3>Phase 5: Search for error-traces in sliced programs</h3>\n")
-        ofile.write("<p>It is performed by tools 'cbmc' and 'symex'.</p>\n")
+        ofile.write("<p>It is performed by tools 'jbmc' and 'symex'.</p>\n")
 
         if num_slicing_tasks == 0:
             ofile.write("<p>There are no error traces, because there was no slicing task generated.</p>\n")
diff --git a/driver/run.py b/driver/run.py
@@ -222,9 +222,9 @@ def __main():
               analyser.get_goto_instrument_pathname() + "'. " +
               analyser.get_missing_binary_error_message())
         return
-    if not os.path.exists(analyser.get_cbmc_pathname()):
-        print("ERROR: Cannot find 'cbmc' executable file at '" +
-              analyser.get_cbmc_pathname() + "'. " +
+    if not os.path.exists(analyser.get_jbmc_pathname()):
+        print("ERROR: Cannot find 'jbmc' executable file at '" +
+              analyser.get_jbmc_pathname() + "'. " +
               analyser.get_missing_binary_error_message())
         return
 

Original file line number	Diff line number	Diff line change
`@@ -17,7 +17,7 @@`
`17`	`17`	`{`
`18`	`18`	`"error_traces":`
`19`	`19`	`{`
`20`		`- "cbmc":`
	`20`	`+ "jbmc":`
`21`	`21`	`[`
`22`	`22`	`"search_for_error_traces/error_trace_0.json"`
`23`	`23`	`],`
Original file line number	Diff line number	Diff line change
`@@ -16,7 +16,7 @@`
`16`	`16`	`[`
`17`	`17`	`{`
`18`	`18`	`"error_traces": {`
`19`		`- "cbmc": [`
	`19`	`+ "jbmc": [`
`20`	`20`	`"search_for_error_traces/error_trace_0.json"`
`21`	`21`	`],`
`22`	`22`	`"symex": []`