Merge pull request diffblue#465 from diffblue/smowton/feature/csvsa-efficiency-improvement

SEC-495 CSVSA: don't store all domains or all values

Author: smowton

driver/analyser.py

@@ -56,7 +56,8 @@ def run_security_analyser(
         data_flow_insensitive_instrumentation,
         results_dir,
         temp_root_dir,
-        lazy_methods_context_sensitive
+        lazy_methods_context_sensitive,
+        verify_csvsa_sparse_domains
         ):
     prof = {}
     prof_start_time = time.time()
@@ -80,7 +81,8 @@ def run_security_analyser(
         "output-dir": "./",
         "temp-dir": temp_root_dir,
         "data-flow-insensitive-instrumentation": data_flow_insensitive_instrumentation,
-        "lazy-methods-context-sensitive": lazy_methods_context_sensitive
+        "lazy-methods-context-sensitive": lazy_methods_context_sensitive,
+        "verify-csvsa-sparse-domains": verify_csvsa_sparse_domains
     }
     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

@@ -150,6 +150,8 @@ def __parse_cmd_line():
                              "paths.")
     parser.add_argument("--lazy-methods-context-sensitive", action="store_true",
                         help="Use context-sensitive method loading in the first stage")
+    parser.add_argument("--verify-csvsa-sparse-domains", action="store_true",
+                        help="Verify CSVSA's sparse domains optimisation does not alter its output")
     return parser.parse_args()
 
 
@@ -200,7 +202,8 @@ def evaluate(cmdline, common_libraries):
             cmdline.data_flow_insensitive_instrumentation,
             cmdline.results_dir,
             os.path.abspath(os.path.join(cmdline.temp_dir,"GOTO-ANALYSER-TEMP")),
-            cmdline.lazy_methods_context_sensitive
+            cmdline.lazy_methods_context_sensitive,
+            cmdline.verify_csvsa_sparse_domains
             )
 
     instrumented_programs_json_path = \

regression/end_to_end/driver.py

@@ -123,6 +123,9 @@ def run_security_analyser_pipeline(
 
     if "SECURITY_REGRESSION_TESTS_USE_CSVSA" in os.environ and os.environ["SECURITY_REGRESSION_TESTS_USE_CSVSA"] != "0":
         cmdline.append("--lazy-methods-context-sensitive")
+        # Check that CSVSA's behaviour with and without sparse domains
+        # optimisation matches:
+        cmdline.append("--verify-csvsa-sparse-domains")
 
     pretty_cmdline = " ".join(quote_pathnames_in_command_line(cmdline))
 

src/driver/sec_driver_parse_options.cpp

@@ -135,6 +135,72 @@ static irep_idt get_cprover_start_main_callee(const goto_modelt &goto_model)
     .get_identifier();
 }
 
+class csvsa_graph_mismatcht : public std::logic_error
+{
+public:
+  explicit csvsa_graph_mismatcht(const std::string &s) : logic_error(s)
+  {
+  }
+};
+
+static void check_csvsa_graphs_equal(
+  const context_sensitive_value_set_analysis_drivert &analysis_a,
+  const context_sensitive_value_set_analysis_drivert &analysis_b)
+{
+  const auto &graph_a = analysis_a.get_context_graph();
+  const auto &graph_b = analysis_b.get_context_graph();
+
+  if(graph_a.size() != graph_b.size())
+  {
+    throw csvsa_graph_mismatcht(
+      "Different function context count: " + std::to_string(graph_a.size()) +
+      " vs. " + std::to_string(graph_b.size()));
+  }
+
+  for(std::size_t node_idx = 0; node_idx < graph_a.size(); ++node_idx)
+  {
+    const csvsa_context_graph_nodet &node_a = graph_a[node_idx];
+    const csvsa_context_graph_nodet &node_b = graph_b[node_idx];
+    const irep_idt &function_a = node_a.context->function();
+    const irep_idt &function_b = node_b.context->function();
+
+    if(function_a != function_b)
+    {
+      throw csvsa_graph_mismatcht(
+        "Node " + std::to_string(node_idx) + " refers to functions " +
+        id2string(function_a) + " vs. " + id2string(function_b));
+    }
+
+    if(node_a.out.size() != node_b.out.size())
+    {
+      throw csvsa_graph_mismatcht(
+        "Node " + std::to_string(node_idx) + " has " +
+        std::to_string(node_a.out.size()) + " vs. " +
+        std::to_string(node_b.out.size()) + " successors");
+    }
+
+    for(auto out_iter_a = node_a.out.begin(), out_iter_b = node_b.out.begin();
+        out_iter_a != node_a.out.end();
+        ++out_iter_a, ++out_iter_b)
+    {
+      if(out_iter_a->first != out_iter_b->first)
+      {
+        throw csvsa_graph_mismatcht(
+          "Node " + std::to_string(node_idx) + " has differing children: " +
+          "at least node " + std::to_string(out_iter_a->first) + " vs. " +
+          std::to_string(out_iter_b->first));
+      }
+
+      if(out_iter_a->second.is_recursive() != out_iter_b->second.is_recursive())
+      {
+        throw csvsa_graph_mismatcht(
+          "Node " + std::to_string(node_idx) + " has an outgoing edge that "
+          "disagrees regarding whether the edge is recursive");
+      }
+    }
+  }
+}
+
 /// invoke main modules
 int sec_driver_parse_optionst::doit()
 {
@@ -189,6 +255,25 @@ int sec_driver_parse_optionst::doit()
 
       return CPROVER_EXIT_SUCCESS;
     }
+
+    if(cmdline.isset("verify-csvsa-sparse-domains"))
+    {
+      auto csvsa_without_sparse_domains =
+        csvsa_load_and_analyze_functions_without_sparse_domains(
+          lazy_goto_model, get_message_handler());
+
+      try
+      {
+        check_csvsa_graphs_equal(
+          *csvsa_analysis, *csvsa_without_sparse_domains);
+      }
+      catch(const csvsa_graph_mismatcht &difference)
+      {
+        error() << "CSVSA results with and without sparse domains mismatch: "
+                << difference.what() << messaget::eom;
+        return CPROVER_EXIT_INTERNAL_ERROR;
+      }
+    }
   }
   else
     lazy_goto_model.load_all_functions();
@@ -630,6 +715,9 @@ void sec_driver_parse_optionst::help()
     "                                  their virtual callsites\n"
     " --show-csvsa-value-sets          print CSVSA's value sets (possible pointer\n" // NOLINT (*)
     "                                  targets) and exit.\n"
+    " --verify-csvsa-sparse-domains    after CSVSA completes, re-run it with\n"
+    "                                  sparse domains disabled and verify the\n"
+    "                                  results are the same.\n"
     "\n"
     "Java Bytecode frontend options:\n"
     " --classpath dir/jar              set the classpath\n"

src/driver/sec_driver_parse_options.h

@@ -49,6 +49,7 @@ class optionst;
   "(rebuild-taint-cache)" \
   "(lazy-methods-context-sensitive)" \
   "(show-csvsa-value-sets)" \
+  "(verify-csvsa-sparse-domains)" \
   "(java-assume-inputs-non-null)" \
   "(java-max-input-array-length):" \
   "(string-max-input-length):" \

src/pointer-analysis/context_sensitive_value_set_analysis.cpp

@@ -62,11 +62,13 @@ void csvsa_function_contextt::csvsa_visit(locationt l)
   {
     // Function returns are special-- if anything changed,
     // queue all of this context's callsites' successors:
-    const auto &end_state = (*this)[l];
-    std::unique_ptr<const value_set_domaint> end_state_without_locals;
+    auto &end_state = (*this)[l];
+    end_state.set_seen();
+
+    std::unique_ptr<const domaint> end_state_without_locals;
     for(const auto &caller : callers)
     {
-      const value_set_domaint *export_state;
+      const domaint *export_state;
       // Remove locals only on an edge that leaves a recursive part
       // of the program:
       if(recursive_status == RECURSIVE_CHILD)
@@ -120,7 +122,7 @@ void csvsa_function_contextt::csvsa_visit(locationt l)
 
 void csvsa_function_contextt::merge_call_return_state(
   locationt call_loc,
-  const value_set_domaint &callee_state)
+  const domaint &callee_state)
 {
   value_sett callee_values = callee_state.value_set;
 
@@ -203,9 +205,12 @@ bool csvsa_function_contextt::assign_formal_parameters(
     if(param_id.empty())
       continue;
     auto findit = entry_state_vs.values.find(param_id);
+    bool should_track_parameter = csvsa_should_track_value(param);
     INVARIANT(
-      findit != entry_state_vs.values.end(),
-      "all parameters should have been assigned to by now");
+      (findit != entry_state_vs.values.end()) == should_track_parameter,
+      "(only) pointer-typed parameters should have been assigned to by now");
+    if(!should_track_parameter)
+      continue;
     if(findit->second.object_map.read().size() != *sizes_before_iter)
       return true;
     ++sizes_before_iter;
@@ -266,14 +271,14 @@ void csvsa_function_contextt::read_function_arguments(
   }
 }
 
-std::unique_ptr<const value_set_domaint>
-csvsa_function_contextt::cleanup_locals(const value_set_domaint &last_state)
+std::unique_ptr<const csvsa_function_contextt::domaint>
+csvsa_function_contextt::cleanup_locals(const domaint &last_state)
 {
   // Remove local variables, formal parameters etc from this function's
   // final state.
   // Shouldn't do this if this is a recursive function, as our locals
   // will inherit values via a (mutually) recursive call:
-  std::unique_ptr<value_set_domaint> tmp_state(static_cast<value_set_domaint *>(
+  std::unique_ptr<domaint> tmp_state(static_cast<domaint *>(
     make_temporary_state(last_state).release()));
   std::vector<irep_idt> to_erase;
   for(const auto &kv : last_state.value_set.values)
@@ -689,10 +694,11 @@ void csvsa_function_contextt::print_tree(
   }
 }
 
-std::unique_ptr<context_sensitive_value_set_analysis_drivert>
+static std::unique_ptr<context_sensitive_value_set_analysis_drivert>
 csvsa_load_and_analyze_functions(
   lazy_goto_modelt &lazy_model,
-  message_handlert &msg)
+  message_handlert &msg,
+  bool use_sparse_domains)
 {
   get_goto_programt get_function_from_lazy_model =
     [&lazy_model](const irep_idt &name) -> const goto_programt & {
@@ -701,14 +707,32 @@ csvsa_load_and_analyze_functions(
 
   std::unique_ptr<context_sensitive_value_set_analysis_drivert> driver =
     util_make_unique<context_sensitive_value_set_analysis_drivert>(
-      lazy_model.symbol_table, get_function_from_lazy_model);
+      lazy_model.symbol_table,
+      get_function_from_lazy_model,
+      use_sparse_domains);
   driver->set_message_handler(msg);
 
   (*driver)(goto_functionst::entry_point());
 
   return driver;
 }
 
+std::unique_ptr<context_sensitive_value_set_analysis_drivert>
+csvsa_load_and_analyze_functions(
+  lazy_goto_modelt &lazy_model,
+  message_handlert &msg)
+{
+  return csvsa_load_and_analyze_functions(lazy_model, msg, true);
+}
+
+std::unique_ptr<context_sensitive_value_set_analysis_drivert>
+csvsa_load_and_analyze_functions_without_sparse_domains(
+  lazy_goto_modelt &lazy_model,
+  message_handlert &msg)
+{
+  return csvsa_load_and_analyze_functions(lazy_model, msg, false);
+}
+
 bool context_sensitive_value_set_analysis_drivert
   ::compare_working_set_entriest::operator()(
   const working_set_entryt &a, const working_set_entryt &b)