Add tests for CSVSA's sparse-domains mode

This checks that CSVSA using the sparse-domains optimisation has the same outcome as without it
for all end-to-end tests.

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

@@ -694,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 & {
@@ -706,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)

src/pointer-analysis/context_sensitive_value_set_analysis.h

@@ -35,7 +35,7 @@ struct recursive_tag_edget
   {
     is_recursive_backedge = true;
   }
-  bool is_recursive()
+  bool is_recursive() const
   {
     return is_recursive_backedge;
   }
@@ -105,10 +105,15 @@ class context_sensitive_value_set_analysis_drivert : public messaget
   void fixedpoint();
 
 public:
+  const bool use_sparse_domains;
+
   context_sensitive_value_set_analysis_drivert(
     const symbol_tablet &symbol_table,
-    get_goto_programt get_goto_program)
-    : ns(symbol_table), get_goto_program(get_goto_program)
+    get_goto_programt get_goto_program,
+    bool use_sparse_domains)
+    : ns(symbol_table),
+      get_goto_program(get_goto_program),
+      use_sparse_domains(use_sparse_domains)
   {
     class_hierarchy(symbol_table);
   }
@@ -399,6 +404,15 @@ class csvsa_function_contextt :
              ID_virtual_function;
   }
 
+  static std::function<bool(locationt)> get_retain_domain_predicate(
+    const context_sensitive_value_set_analysis_drivert &driver)
+  {
+    if(driver.use_sparse_domains)
+      return csvsa_must_retain_domain;
+    else
+      return nullptr;
+  }
+
 public:
   /// Function context constructor
   /// \param ns: global namespace
@@ -419,7 +433,7 @@ class csvsa_function_contextt :
     context_sensitive_value_set_analysis_drivert &driver,
     context_indext parent,
     const locationt &parent_loc)
-    : csvsa_value_set_analysist(ns, csvsa_must_retain_domain),
+    : csvsa_value_set_analysist(ns, get_retain_domain_predicate(driver)),
       get_goto_program(get_goto_program),
       function_name(function_name),
       goto_program(get_goto_program(function_name)),
@@ -442,7 +456,7 @@ class csvsa_function_contextt :
     get_goto_programt get_goto_program,
     const irep_idt &function_name,
     context_sensitive_value_set_analysis_drivert &driver)
-    : csvsa_value_set_analysist(ns, csvsa_must_retain_domain),
+    : csvsa_value_set_analysist(ns, get_retain_domain_predicate(driver)),
       get_goto_program(get_goto_program),
       function_name(function_name),
       goto_program(get_goto_program(function_name)),
@@ -560,4 +574,11 @@ csvsa_load_and_analyze_functions(
   lazy_goto_modelt &lazy_model,
   message_handlert &msg);
 
+/// As `csvsa_load_and_analyze_functions`, except that CSVSA's sparse domains
+/// optimisation is disabled. Only useful for debugging purposes.
+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);
+
 #endif

src/taint-analysis/taint_config.cpp

@@ -233,7 +233,11 @@ void taint_build_cmdline_from_config(
     return;
 
   if(cfg.object["lazy-methods-context-sensitive"].is_true())
+  {
     cmdline.set("lazy-methods-context-sensitive");
+    if(cfg.object["verify-csvsa-sparse-domains"].is_true())
+      cmdline.set("verify-csvsa-sparse-domains");
+  }
   else
     cmdline.set("lazy-methods");