Merge pull request diffblue#324 from diffblue/owen-jones-diffblue/strong-writes-precise-evs

SEC-200: Use strong writes on precise EVSs except for arrays

Author: owen-jones-diffblue

src/pointer-analysis/external_value_set_expr.h

@@ -295,6 +295,17 @@ class external_value_set_exprt:public exprt
     }
   }
 
+  bool can_make_strong_write_to_precise_external_value_set() const
+  {
+    PRECONDITION(
+      get_external_value_set_type() == external_value_set_typet::PRECISE);
+    for(const auto &entry : access_path_entries())
+      if(entry.label() == "[]")
+        return false;
+
+    return true;
+  }
+
   static const typet &get_precise_evs_irep_id()
   {
     static typet precise_evs("precise_evs");

src/pointer-analysis/local_value_set.cpp

@@ -625,7 +625,23 @@ void local_value_sett::assign_rec(
 
         auto &lhs_entry=insert_result.first->second;
 
-        make_union(lhs_entry.object_map, values_rhs);
+        const bool weak_write =
+          add_to_sets ||
+          !new_ext_set.can_make_strong_write_to_precise_external_value_set();
+
+        if(weak_write)
+        {
+          /// If we are doing a weak write, but this precise EVS did not
+          /// already exist in the domain, we also put a copy of the precise
+          /// EVS with is_initializer set to true in its value-set to
+          /// represent that it might have its original value
+          if(insert_result.second)
+            insert(lhs_entry.object_map, new_ext_set.as_initializer());
+
+          make_union(lhs_entry.object_map, values_rhs);
+        }
+        else
+          lhs_entry.object_map = values_rhs;
       }
     }
   }

src/pointer-analysis/local_value_set_analysis.cpp

@@ -445,10 +445,10 @@ void local_value_set_analysist::transform_function_stub(
     }
     else if(has_prefix(lhs_fieldname.base_name, precise_evs_prefix))
     {
+      const external_value_set_exprt &precise_evs =
+        to_external_value_set(lhs_fieldname.structured_lhs);
       const external_value_set_exprt::access_path_entriest
-        &access_path_entries =
-          to_external_value_set(lhs_fieldname.structured_lhs)
-            .access_path_entries();
+        &access_path_entries = precise_evs.access_path_entries();
       const exprt precise_access_path_expr = get_expr_from_root_object(
         lhs_fieldname.base_name.substr(precise_evs_prefix.size()),
         access_path_entries,
@@ -457,8 +457,14 @@ void local_value_set_analysist::transform_function_stub(
         ns,
         *this);
 
-      /// Weak write - can we do strong writes?
-      bool add_to_sets=true;
+      std::string objkey = lhs_fieldname.base_name + lhs_fieldname.field_name;
+      auto it = valuesets.values.find(objkey);
+      const bool singular = it == valuesets.values.end() ||
+                            it->second.object_map.read().size() == 1;
+      bool add_to_sets =
+        !singular ||
+        !precise_evs.can_make_strong_write_to_precise_external_value_set();
+
       auto demoted_rhs_values=pre_call_rhs_value_sets.at(assignment.second);
       valuesets.demote_initializers(demoted_rhs_values);
       valuesets.assign_valueset(