Merge pull request diffblue#325 from diffblue/owen-jones-diffblue/taint-analysis-should-ignore-precise-external-value-sets

 Taint analysis should ignore precise EVSs

Author: owen-jones-diffblue

src/taint-analysis/taint_summary.cpp

@@ -81,7 +81,7 @@ void expand_external_objects(
   // TODO: figure out when an external reference made by the callee
   // is certain to be resolved here, so we can remove the external reference.
 
-  std::vector<unsigned> new_keys;
+  std::vector<taint_lvalue_numbert> new_keys;
   for(const auto& lval_number : lvalue_set)
   {
     const auto& lval=taint_object_numbering[lval_number];
@@ -117,42 +117,56 @@ static exprt transform_external_objects(const exprt& e)
     // uses it to mean
     // deref(any x field)
     auto evs_copy=to_external_value_set(get_underlying_object(e));
-    access_path_entry_exprt new_entry(
-      "."+
-      id2string(to_member_expr(e).get_component_name()),
-      "",
-      "",
-      typet());
-    evs_copy.extend_access_path(new_entry, external_value_set_typet::PER_FIELD);
-    evs_copy.label()=constant_exprt("external_objects",string_typet());
-    evs_copy.type()=e.type();
-    return evs_copy.as_non_initializer();
+    if(
+      evs_copy.get_external_value_set_type() !=
+      external_value_set_typet::PRECISE)
+    {
+      access_path_entry_exprt new_entry(
+        "."+
+        id2string(to_member_expr(e).get_component_name()),
+        "",
+        "",
+        typet());
+      evs_copy.extend_access_path(
+        new_entry,
+        external_value_set_typet::PER_FIELD);
+      evs_copy.label()=constant_exprt("external_objects", string_typet());
+      evs_copy.type()=e.type();
+      return evs_copy.as_non_initializer();
+    }
   }
   else if(e.id()==ID_external_value_set)
   {
     // Similarly, deref(any external), without a member operator, is assumed
     // to be an array access, and is rewritten to (any array)
     auto evs_copy=to_external_value_set(e);
-    access_path_entry_exprt new_entry("[]","","",typet());
-    evs_copy.extend_access_path(new_entry, external_value_set_typet::PER_FIELD);
-    evs_copy.label()=constant_exprt("external_objects",string_typet());
-    evs_copy.type()=e.type();
-    return evs_copy.as_non_initializer();
+    if(
+      evs_copy.get_external_value_set_type() !=
+      external_value_set_typet::PRECISE)
+    {
+      access_path_entry_exprt new_entry("[]", "", "", typet());
+      evs_copy.extend_access_path(
+        new_entry,
+        external_value_set_typet::PER_FIELD);
+      evs_copy.label()=constant_exprt("external_objects", string_typet());
+      evs_copy.type()=e.type();
+      return evs_copy.as_non_initializer();
+    }
   }
-  else
-    return e;
+
+  return e;
 }
 
 static void collect_lvsa_access_paths(
-  exprt const& querye_in,
+  exprt const& query_in,
   namespacet const& ns,
   local_value_set_analysist& lvsa,
   instruction_iteratort const& instit,
   std::set<exprt> &result)
 {
-  if(querye_in.id()==ID_side_effect)
+  if(query_in.id()==ID_side_effect)
   {
-    side_effect_exprt const see=to_side_effect_expr(querye_in);
+    side_effect_exprt const see=to_side_effect_expr(query_in);
     if(see.get_statement()==ID_nondet)
     {
       // TODO(marek-trtik): Add computation of a proper points-to set for NONDET
@@ -161,10 +175,10 @@ static void collect_lvsa_access_paths(
     }
   }
 
-  const exprt* querye=&querye_in;
-  while(querye->id()==ID_typecast)
-    querye=&querye->op0();
-  const exprt& e = *querye;
+  const exprt* query=&query_in;
+  while(query->id()==ID_typecast)
+    query=&query->op0();
+  const exprt& e = *query;
 
   if(e.id()==ID_symbol ||
      e.id()==ID_index ||
@@ -195,6 +209,14 @@ static void collect_lvsa_access_paths(
       }
       else if(get_underlying_object(transformed_object).id()=="NULL-object")
         continue;
+      else if(
+        get_underlying_object(transformed_object).id() ==
+          ID_external_value_set &&
+        to_external_value_set(get_underlying_object(transformed_object))
+            .get_external_value_set_type() == external_value_set_typet::PRECISE)
+      {
+        continue;
+      }
 
       result.insert(transformed_object);
     }
@@ -212,7 +234,7 @@ static void collect_lvsa_access_paths(
 }
 
 static void collect_lvsa_access_paths(
-  exprt const& querye_in,
+  exprt const& query_in,
   namespacet const& ns,
   local_value_set_analysist& lvsa,
   instruction_iteratort const& instit,
@@ -222,7 +244,7 @@ static void collect_lvsa_access_paths(
 {
   std::set<exprt> referees;
   collect_lvsa_access_paths(
-    querye_in,
+    query_in,
     ns,
     lvsa,
     instit,
@@ -256,7 +278,7 @@ static void collect_lvsa_alias_access_paths(
 }
 
 static void collect_lvsa_access_paths(
-  exprt const& querye_in,
+  exprt const& query_in,
   namespacet const& ns,
   lvalue_numbers_sett &result,
   local_value_set_analysist& lvsa,
@@ -266,7 +288,7 @@ static void collect_lvsa_access_paths(
   bool singular=false;
 
   collect_lvsa_access_paths(
-    querye_in,
+    query_in,
     ns,
     lvsa,
     instit,