Merge pull request diffblue#549 from diffblue/bugfix_add_aliasing_between_DO_and_EVSes

SEC-633: Bugfix: added alias-computation between a DO and EVSes in the domain.

Author: owen-jones-diffblue

src/taint-analysis/taint_summary.cpp

@@ -520,14 +520,15 @@ numbered_lvalue_to_taint_mapt taint_algorithm_computing_summary_of_functiont::
 void taint_algorithm_computing_summary_of_functiont::assign(
   numbered_lvalue_to_taint_mapt &map,
   const taint_lvalue_numbert lvalue,
-  const taint_sett &taint)
+  const taint_sett &taint,
+  const bool allow_bottom_assignment)
 {
   TMPROF_BLOCK();
 
   const auto it = map.find(lvalue);
   if (it == map.end())
   {
-    if(!taint.is_bottom())
+    if(!taint.is_bottom() || allow_bottom_assignment)
       map.insert({ lvalue, taint });
   }
   else
@@ -919,6 +920,26 @@ taint_sett taint_algorithm_computing_summary_of_functiont::
       const auto input_it = input.find(lvalue_number);
       if(input_it != input.cend())
         result += input_it->second;
+      else
+      {
+        const exprt &alias_expr = numbering->at(lvalue_number);
+        if(alias_expr.id() == ID_dynamic_object)
+        {
+          const typet &alias_expr_type =
+            program->get_namespace().follow(alias_expr.type());
+          for(const auto &number_and_taint : a)
+          {
+            const exprt &expr = numbering->at(number_and_taint.first);
+            if(expr.id() == ID_external_value_set)
+            {
+              const typet &expr_type =
+                program->get_namespace().follow(expr.type());
+              if(alias_expr_type == expr_type)
+                result |= number_and_taint.second;
+            }
+          }
+        }
+      }
     }
   }
   return result;
@@ -943,7 +964,7 @@ void taint_algorithm_computing_summary_of_functiont::
     // Singular implies that lhs has exactly one element,
     // so we can access it directly
     for(const auto num : numbers_of_aliases)
-      assign(result, num, taint_from_rule);
+      assign(result, num, taint_from_rule, is_allowed_pure_assignment);
   }
   else
   {

src/taint-analysis/taint_summary.h

@@ -350,7 +350,8 @@ class taint_algorithm_computing_summary_of_functiont
   void assign(
     numbered_lvalue_to_taint_mapt &map,
     const taint_lvalue_numbert lvalue,
-    const taint_sett &taint);
+    const taint_sett &taint,
+    const bool allow_bottom_assignment = false);
 
   void maybe_assign(
     numbered_lvalue_to_taint_mapt &map,