Reducing the size of domain of the taint analysis.

Instead of propagating all EVSes and DO introduced in both this function
and callees (transitively), we add them into the domain of the current
function on demand. So, the values get to the domain at the locations,
where they are first used.

This is solved so that we keep EVSes and DOs only in the input map
of the summary and we later use it in cases when the a queried object
is not yet in the domain element of the current location.

Author: marek-trtik

src/taint-analysis/taint_summary.cpp

@@ -836,8 +836,6 @@ void taint_algorithm_computing_summary_of_functiont::initialise_domain(
     }
   }
 
-  numbered_lvalue_to_taint_mapt entry_map;
-  numbered_lvalue_to_taint_mapt others_map;
   for(const auto  lvaluenum : environment)
   {
     const taint_lvaluet &lvalue=numbering->at(lvaluenum);
@@ -852,18 +850,15 @@ void taint_algorithm_computing_summary_of_functiont::initialise_domain(
     {
       taint_variablet v = taint_variablet::fresh();
       caller_summary.input.insert({ lvaluenum, v });
-      entry_map.insert({lvaluenum, taint_sett::from_variable(v) });
-      others_map.insert({lvaluenum, taint_sett() });
     }
   }
 
-  caller_summary.domain.insert(
-    { function.body.instructions.cbegin(), entry_map });
-  for(auto  it = std::next(function.body.instructions.cbegin());
+  numbered_lvalue_to_taint_mapt initial_map;
+  for(auto it = function.body.instructions.cbegin();
       it != function.body.instructions.cend();
       ++it)
   {
-    caller_summary.domain.insert({ it, others_map });
+    caller_summary.domain.insert({ it, initial_map });
   }
 
   // Now that all maps have been created, replace those with a unique
@@ -913,6 +908,7 @@ void taint_algorithm_computing_summary_of_functiont::initialise_domain(
 void taint_algorithm_computing_summary_of_functiont::handle_assignment(
   const code_assignt& asgn,
   numbered_lvalue_to_taint_mapt const&  a,
+  const taint_summary_inputt &input,
   numbered_lvalue_to_taint_mapt& result,
   instruction_iteratort const& Iit,
   local_value_set_analysist &lvsa)
@@ -931,30 +927,16 @@ void taint_algorithm_computing_summary_of_functiont::handle_assignment(
       handle_assignment(
         member_assign,
         a,
+        input,
         result,
         Iit,
         lvsa);
     }
     return;
   }
 
-  taint_sett taint;
-  {
-    lvalue_numbers_sett rhs;
-    collect_lvsa_access_paths(
-      asgn.rhs(),
-      program->get_namespace(),
-      rhs,
-      lvsa,
-      Iit,
-      *numbering);
-    for(const auto &lvalue : rhs)
-    {
-      const auto it=a.find(lvalue);
-      if(it!=a.cend())
-        taint|=it->second;
-    }
-  }
+  taint_sett taint = compute_taint_of_aliased_numbers_of_lvalue(
+    asgn.rhs(), Iit, lvsa, input, a);
 
   lvalue_numbers_sett lhs;
   bool singular=false;
@@ -987,6 +969,7 @@ taint_sett taint_algorithm_computing_summary_of_functiont::
     const taint_lvaluet &lvalue,
     const instruction_iteratort &Iit,
     local_value_set_analysist &lvsa,
+    const taint_summary_inputt &input,
     const numbered_lvalue_to_taint_mapt &a)
 {
   TMPROF_BLOCK();
@@ -1005,6 +988,12 @@ taint_sett taint_algorithm_computing_summary_of_functiont::
     auto it=a.find(lvalue_number);
     if(it!=a.cend())
       result |= it->second;
+    else
+    {
+      const auto input_it = input.find(lvalue_number);
+      if(input_it != input.cend())
+        result += input_it->second;
+    }
   }
   return result;
 }
@@ -1059,6 +1048,7 @@ numbered_lvalue_to_taint_mapt taint_algorithm_computing_summary_of_functiont::
     const numbered_lvalue_to_taint_mapt &a,
     const instruction_iteratort &Iit,
     const irep_idt &caller_ident,
+    const taint_summary_inputt &input,
     taint_summaryt::dbt &database,
     local_value_set_analysist &lvsa,
     taint_transition_propertiest &transition_properties)
@@ -1089,7 +1079,7 @@ numbered_lvalue_to_taint_mapt taint_algorithm_computing_summary_of_functiont::
           {
             taint_sett taint =
               compute_taint_of_aliased_numbers_of_lvalue(
-                replace_it->second, Iit, lvsa, a);
+                replace_it->second, Iit, lvsa, input, a);
 
             lvalue_numbers_sett numbers_of_aliases;
             collect_lvsa_access_paths(
@@ -1140,7 +1130,7 @@ numbered_lvalue_to_taint_mapt taint_algorithm_computing_summary_of_functiont::
           }
         }
       }
-      handle_assignment(asgn, a, result, Iit, lvsa);
+      handle_assignment(asgn, a, input, result, Iit, lvsa);
     }
     break;
   case FUNCTION_CALL:
@@ -1230,6 +1220,7 @@ numbered_lvalue_to_taint_mapt taint_algorithm_computing_summary_of_functiont::
                         propagation_rule.get_input_location().arg_index),
                       Iit,
                       lvsa,
+                      input,
                       a))
                 : propagation_rule.apply();
 
@@ -1362,13 +1353,15 @@ numbered_lvalue_to_taint_mapt taint_algorithm_computing_summary_of_functiont::
                       sink_rule.get_input_location().arg_index),
                     Iit,
                     lvsa,
+                    input,
                     a)
                 : taint_sett{},
               compute_taint_of_aliased_numbers_of_lvalue(
                 fn_call.arguments().at(
                   sink_rule.get_sink_target_location().arg_index),
                 Iit,
                 lvsa,
+                input,
                 a),
               sink_conditions);
 
@@ -1449,6 +1442,7 @@ numbered_lvalue_to_taint_mapt taint_algorithm_computing_summary_of_functiont::
       handle_assignment(
         fake_assignment,
         a,
+        input,
         result,
         Iit,
         lvsa);
@@ -1708,6 +1702,7 @@ void taint_algorithm_computing_summary_of_functiont::
         src_value,
         src_instr_it,
         function_id,
+        summary->input,
         database,
         lvsa,
         summary->transition_props);

src/taint-analysis/taint_summary.h

@@ -254,6 +254,7 @@ class taint_algorithm_computing_summary_of_functiont
   void handle_assignment(
     const code_assignt& asgn,
     numbered_lvalue_to_taint_mapt const&  a,
+    const taint_summary_inputt &input,
     numbered_lvalue_to_taint_mapt& result,
     instruction_iteratort const& Iit,
     local_value_set_analysist &lvsa);
@@ -262,6 +263,7 @@ class taint_algorithm_computing_summary_of_functiont
     const taint_lvaluet &lvalue,
     const instruction_iteratort &Iit,
     local_value_set_analysist &lvsa,
+    const taint_summary_inputt &input,
     const numbered_lvalue_to_taint_mapt &a);
 
   void apply_taint_to_aliased_numbers_of_lvalue(
@@ -276,6 +278,7 @@ class taint_algorithm_computing_summary_of_functiont
     const numbered_lvalue_to_taint_mapt &a,
     const instruction_iteratort &Iit,
     const irep_idt &caller_ident,
+    const taint_summary_inputt &input,
     taint_summaryt::dbt &database,
     local_value_set_analysist &lvsa,
     taint_transition_propertiest &transition_properties);