Merge pull request diffblue#347 from diffblue/owen-jones-diffblue/per-test-turn-off-precise-access-paths

Add functionality to turn off precise access paths for individual tests

Author: owen-jones-diffblue

driver/analyser.py

@@ -52,6 +52,7 @@ def run_security_analyser(
         dump_html_slice,
         dump_html_program,
         verbosity,
+        do_not_use_precise_access_paths,
         data_flow_insensitive_instrumentation,
         results_dir,
         temp_root_dir
@@ -70,29 +71,15 @@ def run_security_analyser(
         "rules": transition_rules_file_pathname,
         "timeout": timeout,
         "verbosity": verbosity,
+        "dump_html_summaries": dump_html_summaries,
+        "dump_html_statistics": dump_html_statistics,
+        "dump_html_slice": dump_html_slice,
+        "dump_html_program": dump_html_program,
+        "do_not_use_precise_access_paths": do_not_use_precise_access_paths,
         "output-dir": "./",
         "temp-dir": temp_root_dir,
         "data-flow-insensitive-instrumentation": data_flow_insensitive_instrumentation
     }
-    if dump_html_summaries:
-        root_config_json["dump_html_summaries"] = True
-    else:
-        root_config_json["dump_html_summaries"] = False
-
-    if dump_html_statistics:
-        root_config_json["dump_html_statistics"] = True
-    else:
-        root_config_json["dump_html_statistics"] = False
-
-    if dump_html_slice:
-        root_config_json["dump_html_slice"] = True
-    else:
-        root_config_json["dump_html_slice"] = False
-
-    if dump_html_program:
-        root_config_json["dump_html_program"] = True
-    else:
-        root_config_json["dump_html_program"] = False
     with open(root_config_json_fname, "w") as root_config_json_file:
         root_config_json_file.write(json.dumps(root_config_json, sort_keys=True, indent=4))
 

driver/run.py

@@ -134,6 +134,9 @@ def __parse_cmd_line():
                              "of this data-flow insensitive instrumentation is that it allows more aggressive program "
                              "slicing and so smaller programs for CBMC to analyse, i.e. considerably faster analysis. "
                              "The disadvantage is that some of the generated error traces might be false positives.")
+    parser.add_argument("--do-not-use-precise-access-paths", action="store_true",
+                        help="Call security-analyzer with a command line argument which turns off precise access "
+                             "paths.")
     return parser.parse_args()
 
 
@@ -177,6 +180,7 @@ def evaluate(cmdline, common_libraries):
             cmdline.dump_html_slice,
             cmdline.dump_html_program,
             cmdline.verbosity,
+            cmdline.do_not_use_precise_access_paths,
             cmdline.data_flow_insensitive_instrumentation,
             cmdline.results_dir,
             os.path.abspath(os.path.join(cmdline.temp_dir,"GOTO-ANALYSER-TEMP"))

regression/end_to_end/taint_over_list_models/test_taint_over_list_models.py

@@ -20,6 +20,6 @@ def test_taint_over_list_models():
         "build",
         "rules.json",
         os.path.realpath(os.path.dirname(__file__)),
-        ["--use-models-library"])
+        ["--use-models-library", "--do-not-use-precise-access-paths"])
     assert traces.count_traces() == 1
     assert traces.trace_exists("java::Main.main:()V", 14)

src/taint-analysis/taint_config.cpp

@@ -22,6 +22,7 @@ taint_configt::taint_configt(const std::string &cfg_fname)
   , dump_html_statistics(false)
   , dump_html_slice(false)
   , dump_html_program(false)
+  , do_not_use_precise_access_paths(false)
   , data_flow_insensitive_instrumentation(false)
 {
 }
@@ -177,6 +178,7 @@ bool taint_configt::load(message_handlert &handler)
   dump_html_statistics=cfg["dump_html_statistics"].is_true();
   dump_html_slice=cfg["dump_html_slice"].is_true();
   dump_html_program=cfg["dump_html_program"].is_true();
+  do_not_use_precise_access_paths=cfg["do_not_use_precise_access_paths"].is_true();
   data_flow_insensitive_instrumentation=
     cfg["data-flow-insensitive-instrumentation"].is_true();
 

src/taint-analysis/taint_config.h

@@ -95,6 +95,11 @@ class taint_configt
     return dump_html_program;
   }
 
+  bool is_do_not_precise_access_paths_enabled() const
+  {
+    return do_not_use_precise_access_paths;
+  }
+
   bool use_data_flow_insensitive_instrumentation() const
   {
     return data_flow_insensitive_instrumentation;
@@ -120,6 +125,7 @@ class taint_configt
   bool dump_html_statistics;
   bool dump_html_slice;
   bool dump_html_program;
+  bool do_not_use_precise_access_paths;
   bool data_flow_insensitive_instrumentation;
 };
 

src/taint-analysis/taint_security_scanner.cpp

@@ -118,6 +118,9 @@ bool taint_do_security_scan(
 
     statistics.begin_loading_taint_summaries_database();
 
+    local_value_sett::do_not_use_precise_access_paths =
+      config.is_do_not_precise_access_paths_enabled();
+
     boost::filesystem::path summaries_root(
       config.get_taint_summaries_root_directory());