Use sharing_mapt for abstract environment

Author: hannes-steffenhagen-diffblue

src/analyses/variable-sensitivity/abstract_enviroment.cpp

@@ -52,14 +52,14 @@ abstract_object_pointert abstract_environmentt::eval(
   if(simplified_id==ID_symbol)
   {
     const symbol_exprt &symbol(to_symbol_expr(simplified_expr));
-    const auto &symbol_entry=map.find(symbol);
-    if(symbol_entry==map.cend())
+    const auto &symbol_entry=map.const_find(symbol);
+    if(!symbol_entry.second)
     {
       return abstract_object_factory(simplified_expr.type(), ns, true);
     }
     else
     {
-      abstract_object_pointert found_symbol_value=symbol_entry->second;
+      abstract_object_pointert found_symbol_value=symbol_entry.first;
       return found_symbol_value;
     }
   }
@@ -191,7 +191,7 @@ bool abstract_environmentt::assign(
   {
     INVARIANT(s.id()==ID_symbol, "Have a symbol or a stack");
     const symbol_exprt &symbol_expr(to_symbol_expr(s));
-    if(map.find(symbol_expr)==map.end())
+    if(!map.has_key(symbol_expr))
     {
       lhs_value=abstract_object_factory(
         symbol_expr.type(), ns, true, false);
@@ -483,9 +483,9 @@ bool abstract_environmentt::merge(const abstract_environmentt &env)
     // For each element in the intersection of map and env.map merge
     // If the result of the merge is top, remove from the map
     bool modified=false;
-    for(const auto &entry : env.map)
+    for(const auto &entry : env.map.get_view())
     {
-      if(map.find(entry.first)!=map.end())
+      if(map.has_key(entry.first))
       {
         bool object_modified=false;
         abstract_object_pointert new_object=
@@ -626,10 +626,10 @@ void abstract_environmentt::output(
 {
   out << "{\n";
 
-  for(const auto &entry : map)
+  for(const auto &entry : map.get_view())
   {
     out << entry.first.get_identifier()
-        << " (" << ") -> ";
+        << " () -> ";
     entry.second->output(out, ai, ns);
     out << "\n";
   }
@@ -650,9 +650,9 @@ Function: abstract_environmentt::verify
 
 bool abstract_environmentt::verify() const
 {
-  for(const auto &entry : map)
+  for(const auto &entry : map.get_view())
   {
-    if(!entry.second)
+    if(entry.second == nullptr)
     {
       return false;
     }
@@ -712,21 +712,21 @@ std::vector<symbol_exprt> abstract_environmentt::modified_symbols(
 {
   // Find all symbols who have different write locations in each map
   std::vector<symbol_exprt> symbols_diff;
-  for (const auto &entry : first.map)
+  for (const auto &entry : first.map.get_view())
   {
-    const auto &second_entry = second.map.find(entry.first);
-    if (second_entry != second.map.end())
+    const auto second_entry = second.map.const_find(entry.first);
+    if (second_entry.second)
     {
-      if(second_entry->second->has_been_modified(entry.second))
+      if(second_entry.first->has_been_modified(entry.second))
         symbols_diff.push_back(entry.first);
     }
   }
 
   // Add any symbols that are only in the second map
-  for(const auto &entry : second.map)
+  for(const auto &entry : second.map.get_view())
   {
-    const auto &second_entry = first.map.find(entry.first);
-    if (second_entry==first.map.end())
+    const auto &second_entry = first.map.const_find(entry.first);
+    if (!second_entry.second)
     {
       symbols_diff.push_back(entry.first);
     }

src/analyses/variable-sensitivity/abstract_enviroment.h

@@ -18,6 +18,7 @@
 #include <util/std_expr.h>
 #include <util/message.h>
 #include <analyses/variable-sensitivity/abstract_object.h>
+#include <util/sharing_map.h>
 
 class abstract_environmentt
 {
@@ -80,7 +81,7 @@ class abstract_environmentt
     const exprt &e, const namespacet &ns) const;
 
   typedef symbol_exprt map_keyt;
-  std::map<map_keyt, abstract_object_pointert> map;
+  sharing_mapt<map_keyt, abstract_object_pointert> map;
 
 private:
   abstract_object_pointert abstract_object_factory(

src/util/sharing_map.h

@@ -128,6 +128,11 @@ class sharing_mapt
 
   const_find_type find(const key_type &k) const;
 
+  const_find_type const_find(const key_type &k) const
+  {
+    return find(k);
+  }
+
   mapped_type &at(
     const key_type &k,
     const tvt &key_exists=tvt::unknown());
@@ -197,6 +202,12 @@ class sharing_mapt
   typedef std::vector<delta_view_itemt> delta_viewt;
 
   void get_view(viewt &view) const;
+  viewt get_view() const
+  {
+    viewt result;
+    get_view(result);
+    return result;
+  }
 
   void get_delta_view(
     const self_type &other,

src/util/std_expr.h

@@ -135,6 +135,16 @@ class symbol_exprt:public exprt
   }
 };
 
+namespace std {
+  template<> struct hash<::symbol_exprt>
+  {
+    size_t operator()(const ::symbol_exprt& sym)
+    {
+      return irep_id_hash()(sym.get_identifier());
+    }
+  };
+}
+
 /*! \brief Expression to hold a symbol (variable)
 */
 class decorated_symbol_exprt:public symbol_exprt