Don't create unneeded entries for precise EVSs

Previously we would create an entry with the precise EVS on the left
and also on the right, which mirrors what we do for per field EVSs. Now
we only make an entry for a precise EVS if something is actually written
to it.

Author: Owen Jones

src/pointer-analysis/local_value_set.cpp

@@ -41,11 +41,10 @@ void local_value_sett::make_union_adjusting_evs_types(
 }
 
 std::pair<value_sett::valuest::iterator, bool>
-local_value_sett::init_external_value_set(const external_value_set_exprt &evse)
+local_value_sett::init_per_field_external_value_set(
+  const external_value_set_exprt &evse)
 {
   PRECONDITION(!evse.access_path_entries().empty());
-  bool per_field_evs =
-    evse.get_external_value_set_type() == external_value_set_typet::PER_FIELD;
   const auto &apback=evse.access_path_entries().back();
   std::string basename=evse.get_access_path_basename(apback.declared_on_type());
   std::string access_path_suffix=evse.get_access_path_suffix();
@@ -56,15 +55,30 @@ local_value_sett::init_external_value_set(const external_value_set_exprt &evse)
   auto insert_result=values.insert(std::make_pair(irep_idt(entryname), entry));
 
   if(insert_result.second)
-  {
-    const external_value_set_exprt &evs_to_insert =
-      per_field_evs ? evse.as_initializer() : evse;
-    insert(insert_result.first->second.object_map, evs_to_insert);
-  }
+    insert(insert_result.first->second.object_map, evse.as_initializer());
 
   return insert_result;
 }
 
+void local_value_sett::init_precise_external_value_set(
+  const external_value_set_exprt &evse,
+  object_mapt &dest)
+{
+  PRECONDITION(!evse.access_path_entries().empty());
+  const auto &apback = evse.access_path_entries().back();
+  std::string basename =
+    evse.get_access_path_basename(apback.declared_on_type());
+  std::string access_path_suffix = evse.get_access_path_suffix();
+  std::string entryname = basename + access_path_suffix;
+
+  const irep_idt key(entryname);
+
+  if(values.count(key))
+    make_union(dest, values.at(key).object_map);
+  else
+    insert(dest, evse);
+}
+
 /// Builds a version of expr suitable for alias-comparison
 /// \param expr: The expression to be converted to the alias-uniform structure
 /// \return expr without information which is irrelevant to alias-comparison
@@ -290,9 +304,8 @@ void local_value_sett::get_value_set_rec(
 
         // TODO: figure out how to do this sort of on-demand-insert
         // without such ugly const hacking:
-        auto insert_result=
-          (const_cast<local_value_sett *>(this))->
-            init_external_value_set(new_ext_set);
+        auto insert_result = (const_cast<local_value_sett *>(this))
+                               ->init_per_field_external_value_set(new_ext_set);
 
         make_union(dest, insert_result.first->second.object_map);
       }
@@ -317,11 +330,8 @@ void local_value_sett::get_value_set_rec(
 
           // TODO: figure out how to do this sort of on-demand-insert
           // without such ugly const hacking:
-          auto insert_result=
-            (const_cast<local_value_sett *>(this))->
-              init_external_value_set(new_ext_set);
-
-          make_union(dest, insert_result.first->second.object_map);
+          (const_cast<local_value_sett *>(this))
+            ->init_precise_external_value_set(new_ext_set, dest);
         }
       }
     }

src/pointer-analysis/local_value_set.h

@@ -58,8 +58,13 @@ class local_value_sett:public value_sett
   /// \param evse: external value set whose entry to create
   /// \return a la `std::map::insert`, a pair of an iterator pointing to the
   ///   relevant entry and a boolean indicating if it is new.
-  std::pair<valuest::iterator, bool> init_external_value_set(
-    const external_value_set_exprt& evse);
+  std::pair<valuest::iterator, bool>
+  init_per_field_external_value_set(const external_value_set_exprt &evse);
+
+  /// TODO
+  void init_precise_external_value_set(
+    const external_value_set_exprt &evse,
+    object_mapt &dest);
 
   // For all the overrides below, see the base type for parameter-level docs
   // as their meanings are unchanged.