Merge pull request diffblue#321 from diffblue/owen-jones-diffblue/fix-evs-initializer-status

SEC-193: Various fix-ups for EVSs in LVSA (version 2)

Author: owen-jones-diffblue

regression/LVSA/lvsa_driver.py

@@ -101,8 +101,11 @@ def check_contains_per_field_evs(self, expected_number=1, is_initializer=False,
             matches = [x for x in matches if x.label.endswith(label)]
         assert expected_number == len(matches)
 
-    def check_contains_precise_evs(self, expected_number=1, access_path=None, label_suffix=None):
+    def check_contains_precise_evs(self, expected_number=1, is_initializer=False, access_path=None, label_suffix=None):
         matches = [x for x in self.external_value_sets if x.evs_type == EvsType.precise]
+        if is_initializer is not None:
+            # Expect True or False
+            matches = [x for x in matches if x.is_initializer == is_initializer]
         if access_path is not None:
             # Expect an array of strings, e.g. ['.a', '.b']
             matches = [x for x in matches if x.access_path_entries == access_path]

src/pointer-analysis/external_value_set_expr.h

@@ -128,6 +128,11 @@ class external_value_set_exprt:public exprt
     return get_bool(ID_is_initializer);
   }
 
+  void set_initializer()
+  {
+    set(ID_is_initializer, ID_1);
+  }
+
   void set_non_initializer()
   {
     set(ID_is_initializer, ID_0);
@@ -212,7 +217,7 @@ class external_value_set_exprt:public exprt
     }
   }
 
-  /// Add a new entry to the access path
+  /// Add a new entry to the access path, and set as not an initializer
   /// \param newentry: the entry to add to the access path
   /// \param evs_type: which external_value_set_type we want *this to become.
   ///   A root object can become per field or precise. The other two must
@@ -226,6 +231,8 @@ class external_value_set_exprt:public exprt
   {
     PRECONDITION(evs_type!=external_value_set_typet::ROOT_OBJECT);
     set_external_value_set_type(evs_type);
+    set_non_initializer();
+
     switch(evs_type)
     {
     case external_value_set_typet::PER_FIELD:
@@ -250,9 +257,6 @@ class external_value_set_exprt:public exprt
         if(entry==newentry)
           return true;
 
-      /// Precise EVSs always have is_initializer=false
-      set_non_initializer();
-
       if(access_path_entries().empty())
         label()=constant_exprt(
           PRECISE_EVS_PREFIX+id2string(label().get_value()), string_typet());
@@ -267,6 +271,18 @@ class external_value_set_exprt:public exprt
     return false;
   }
 
+  external_value_set_exprt as_initializer() const
+  {
+    if(is_initializer())
+      return *this;
+    else
+    {
+      external_value_set_exprt copy = *this;
+      copy.set_initializer();
+      return copy;
+    }
+  }
+
   external_value_set_exprt as_non_initializer() const
   {
     if(!is_initializer())
@@ -278,6 +294,12 @@ class external_value_set_exprt:public exprt
       return copy;
     }
   }
+
+  static const typet &get_precise_evs_irep_id()
+  {
+    static typet precise_evs("precise_evs");
+    return precise_evs;
+  }
 };
 
 inline external_value_set_exprt &to_external_value_set(exprt &e)

src/pointer-analysis/local_value_set.cpp

@@ -40,25 +40,6 @@ 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)
-{
-  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;
-
-  entryt entry(basename, access_path_suffix, apback.declared_on_type(), evse);
-
-  auto insert_result=values.insert(std::make_pair(irep_idt(entryname), entry));
-
-  if(insert_result.second)
-    insert(insert_result.first->second.object_map, evse);
-
-  return insert_result;
-}
-
 /// 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
@@ -282,11 +263,27 @@ void local_value_sett::get_value_set_rec(
           new_entry, external_value_set_typet::PER_FIELD);
         new_ext_set.type()=field_type.subtype();
 
-        // 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);
+        std::string basename =
+          new_ext_set.get_access_path_basename(declared_on_type);
+        std::string entryname = basename + access_path_suffix;
+
+        entryt entry(
+          basename, access_path_suffix, declared_on_type, new_ext_set);
+
+        /// If there is already an entry for this EVS then find it, otherwise
+        /// create a new entry for it
+        /// 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))
+            ->values.insert(std::make_pair(irep_idt(entryname), entry));
+
+        /// If we've just created a new entry then populate the object map
+        /// with an initializer EVS
+        if(insert_result.second)
+          insert(
+            insert_result.first->second.object_map,
+            new_ext_set.as_initializer());
 
         make_union(dest, insert_result.first->second.object_map);
       }
@@ -309,13 +306,21 @@ void local_value_sett::get_value_set_rec(
         {
           new_ext_set.type()=field_type.subtype();
 
-          // 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);
+          declared_on_type =
+            external_value_set_exprt::get_precise_evs_irep_id();
+          std::string basename =
+            new_ext_set.get_access_path_basename(declared_on_type);
+          access_path_suffix = new_ext_set.get_access_path_suffix();
+          std::string entryname = basename + access_path_suffix;
+
+          const auto it = values.find(entryname);
+
+          /// If an entry already exists then use the values in the object
+          /// map, otherwise do not create an entry and use the EVS
+          if(it != values.end())
+            make_union(dest, it->second.object_map);
+          else
+            insert(dest, new_ext_set);
         }
       }
     }
@@ -582,7 +587,7 @@ void local_value_sett::assign_rec(
       if(insert_result.second && field_type.id()==ID_pointer)
       {
         new_ext_set.type()=field_type.subtype();
-        insert(lhs_entry.object_map, new_ext_set);
+        insert(lhs_entry.object_map, new_ext_set.as_initializer());
       }
 
       make_union(lhs_entry.object_map, values_rhs);
@@ -608,7 +613,10 @@ void local_value_sett::assign_rec(
         std::string entryname=basename+access_path_suffix;
 
         entryt entry(
-          basename, access_path_suffix, declared_on_type, new_ext_set);
+          basename,
+          access_path_suffix,
+          external_value_set_exprt::get_precise_evs_irep_id(),
+          new_ext_set);
 
         auto insert_result=const_cast<valuest &>(values).
           insert(std::make_pair(irep_idt(entryname), entry));

src/pointer-analysis/local_value_set.h

@@ -50,17 +50,6 @@ class local_value_sett:public value_sett
     const object_mapt &src,
     const typet&) const;
 
-  /// Gets or creates a value-set entry corresponding to an external value set
-  /// expression, which initially contains the EVS itself. For example, given
-  /// EVS(A.x), representing all `x` fields of objects of type `A`, this would
-  /// create an entry `external_objects.A.x <- EVS(A.x)` if it didn't already
-  /// exist and return an iterator pointing to it.
-  /// \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);
-
   // For all the overrides below, see the base type for parameter-level docs
   // as their meanings are unchanged.
 

src/pointer-analysis/local_value_set_analysis.cpp

@@ -88,7 +88,7 @@ void local_value_set_analysist::initialize(const goto_programt &fun)
         extsym.type().subtype(),
         constant_exprt(extsym_name, string_typet()),
         default_mode_for_new_evs,
-        true);
+        false);
       local_value_sett::entryt extsym_entry_blank(
         id2string(extsym_name), "", typet(), extsym_var);
       auto &extsym_entry = initial_state.get_entry(