Merge pull request diffblue#397 from diffblue/more_reduced_domain_size_and_improved_accuracy_for_undefined_functions

SEC-368: Improved accuracy when undefined functions are present and more reduced size of taint analysis domain

Author: marek-trtik

src/taint-analysis/taint_summary.cpp

@@ -429,7 +429,8 @@ bool taint_algorithm_computing_summary_of_functiont::
     const exprt &expr,
     const instruction_iteratort &it,
     local_value_set_analysist &lvsa,
-    lvalue_numbers_sett &result)
+    lvalue_numbers_sett &result,
+    const bool generate_fresh_evs)
 {
   TMPROF_BLOCK();
 
@@ -444,7 +445,7 @@ bool taint_algorithm_computing_summary_of_functiont::
     *numbering,
     raw_result,
     singular);
-  if(raw_result.empty())
+  if(generate_fresh_evs && raw_result.empty())
   {
     external_value_set_exprt new_lhs(
       query_expr.type(),
@@ -472,7 +473,7 @@ bool taint_algorithm_computing_summary_of_functiont::
       {
         if(
           !collect_lvsa_access_paths_extended(
-            member_expr->compound(), it, lvsa, result))
+            member_expr->compound(), it, lvsa, result, generate_fresh_evs))
         {
           singular = false;
         }
@@ -775,32 +776,21 @@ void taint_algorithm_computing_summary_of_functiont::initialise_domain(
     if(it->type==ASSIGN)
     {
       const code_assignt &asgn = to_code_assign(it->code);
-      collect_lvsa_access_paths_extended(asgn.lhs(), it, lvsa, environment);
-      collect_lvsa_access_paths_extended(asgn.lhs(), it, lvsa, written);
-      if(asgn.rhs().id()==ID_side_effect)
+      collect_lvsa_access_paths_extended(
+        asgn.lhs(), it, lvsa, environment, false);
+      collect_lvsa_access_paths_extended(
+        asgn.lhs(), it, lvsa, written, false);
+      if(asgn.rhs().id() != ID_side_effect)
       {
-        const side_effect_exprt see=to_side_effect_expr(asgn.rhs());
-        if(see.get_statement()==ID_nondet)
-        {
-          const auto replace_it=
-            program->get_NONDET_retvals_replacements().find(it);
-          if(replace_it != program->get_NONDET_retvals_replacements().cend())
-          {
-            collect_lvsa_access_paths_extended(
-              replace_it->second, it, lvsa, environment);
-          }
-          else
-          {
-            // This must be a NONDET assignment not relating to a stub function,
-            // for example initialising an input parameter in __CPROVER_start.
-          }
-        }
+        collect_lvsa_access_paths_extended(
+          asgn.rhs(), it, lvsa, environment, false);
       }
-      else
-        collect_lvsa_access_paths_extended(asgn.rhs(), it, lvsa, environment);
     }
     else if(it->type == ASSERT)
-      collect_lvsa_access_paths_extended(it->guard, it, lvsa, environment);
+    {
+      collect_lvsa_access_paths_extended(
+        it->guard, it, lvsa, environment, false);
+    }
     else if(it->type==FUNCTION_CALL)
     {
       const code_function_callt &fn_call = to_code_function_call(it->code);
@@ -809,8 +799,6 @@ void taint_algorithm_computing_summary_of_functiont::initialise_domain(
         // Can't handle call by pointer, etc
         continue;
       irep_idt callee_id = to_symbol_expr(callee_expr).get_identifier();
-      const auto &fn_type=
-        program->get_functions().function_map.at(callee_id).type;
 
       if(!database.contains(callee_id) || transition_rules->has_rule(callee_id))
       {
@@ -824,50 +812,15 @@ void taint_algorithm_computing_summary_of_functiont::initialise_domain(
         // In the future we could be more precise about exactly which arguments
         // are used in the rule.
         for(const auto &arg : fn_call.arguments())
-          collect_lvsa_access_paths_extended(arg, it, lvsa, environment);
+        {
+          collect_lvsa_access_paths_extended(
+            arg, it, lvsa, environment, false);
+        }
         if(!database.contains(callee_id))
           continue;
       }
 
       const std::shared_ptr<taint_summaryt> summary = database.at(callee_id);
-      for(const std::pair<taint_lvalue_numbert, taint_variablet>& input
-        : summary->input)
-      {
-        if(symbol_utilst(program->get_namespace())
-          .is_parameter(numbering->at(input.first)))
-        {
-          // Collect access paths for the corresponding actual argument:
-          parameter_matches_id match(
-            to_symbol_expr(numbering->at(input.first))
-              .get_identifier());
-          auto findit=std::find_if(
-            fn_type.parameters().begin(),
-            fn_type.parameters().end(),
-            match);
-          assert(findit!=fn_type.parameters().end() &&
-            "Parameter symbol doesn't match?");
-          const auto paramidx=
-            std::distance(fn_type.parameters().begin(), findit);
-          collect_lvsa_access_paths_extended(
-            fn_call.arguments()[paramidx], it, lvsa, environment);
-        }
-        else if(!symbol_utilst(program->get_namespace()).is_parameter(
-          numbering->at(input.first)) &&
-          !symbol_utilst(program->get_namespace())
-            .is_return_value_auxiliary(numbering->at(input.first)))
-        {
-          environment.insert(input.first);
-        }
-        if(numbering->at(input.first).id()==ID_external_value_set)
-        {
-          const auto& evse=to_external_value_set(
-            numbering->at(input.first));
-          if(evse.access_path_entries().size()==1)
-            numbering_map
-              ->get_object_numbers_by_field()[as_string(function_id)]
-              .insert({ evse.access_path_entries().back().label(), {} });
-        }
-      }
       for(const std::pair<taint_lvalue_numbert, taint_sett> &lvalue_taint:
           summary->output)
         written.insert(lvalue_taint.first);
@@ -1599,6 +1552,16 @@ void taint_algorithm_computing_summary_of_functiont::
   }
   summary.input = std::move(pruned_input);
 
+#ifndef NDEBUG  // Ignore the check below in a non-debug build.
+  {
+    taint_variable_sett input_vars;
+    for(const auto &input_var : summary.input)
+      input_vars.insert(input_var.second);
+    for(const auto &end_var : end_values_taint.get_vars())
+      INVARIANT(input_vars.count(end_var), "Out var must be present in input.");
+  }
+#endif
+
   const goto_functiont &func_ref =
     program->get_functions().function_map.at(fn_id);
   const code_typet &fn_type = to_code_type(func_ref.type);

src/taint-analysis/taint_summary.h

@@ -210,7 +210,8 @@ class taint_algorithm_computing_summary_of_functiont
     const exprt &expr,
     const instruction_iteratort &it,
     local_value_set_analysist &lvsa,
-    lvalue_numbers_sett &result);
+    lvalue_numbers_sett &result,
+    const bool generate_fresh_evs = true);
 
   numbered_lvalue_to_taint_mapt join(
     const numbered_lvalue_to_taint_mapt &a,