Use sharing_mapt

Author: tautschnig

src/goto-symex/goto_symex_state.cpp

@@ -307,8 +307,8 @@ void goto_symex_statet::rename(
         // L1 identifiers are used for propagation!
         auto p_it = propagation.find(ssa.get_identifier());
 
-        if(p_it != propagation.end())
-          expr=p_it->second; // already L2
+        if(p_it.second)
+          expr = p_it.first; // already L2
         else
           set_l2_indices(ssa, ns);
       }
@@ -796,7 +796,10 @@ void goto_symex_statet::print_backtrace(std::ostream &out) const
 /// because there aren't any current callers.
 void goto_statet::output_propagation_map(std::ostream &out)
 {
-  for(const auto &name_value : propagation)
+  sharing_mapt<irep_idt, exprt>::viewt view;
+  propagation.get_view(view);
+
+  for(const auto &name_value : view)
   {
     out << name_value.first << " <- " << format(name_value.second) << "\n";
   }

src/goto-symex/goto_symex_state.h

@@ -15,11 +15,12 @@ Author: Daniel Kroening, [email protected]
 #include <memory>
 #include <unordered_set>
 
-#include <util/invariant.h>
 #include <util/guard.h>
-#include <util/std_expr.h>
-#include <util/ssa_expr.h>
+#include <util/invariant.h>
 #include <util/make_unique.h>
+#include <util/sharing_map.h>
+#include <util/ssa_expr.h>
+#include <util/std_expr.h>
 
 #include <pointer-analysis/value_set.h>
 #include <goto-programs/goto_function.h>
@@ -61,7 +62,7 @@ class goto_statet
   // "constants" can include symbols, but only in the context of an address-of
   // op (i.e. &x can be propagated), and an address-taken thing should only be
   // L1.
-  std::map<irep_idt, exprt> propagation;
+  sharing_mapt<irep_idt, exprt> propagation;
 
   void output_propagation_map(std::ostream &);
 

src/goto-symex/symex_goto.cpp

@@ -445,17 +445,17 @@ static void merge_names(
   {
     const auto p_it = goto_state.propagation.find(l1_identifier);
 
-    if(p_it != goto_state.propagation.end())
-      goto_state_rhs = p_it->second;
+    if(p_it.second)
+      goto_state_rhs = p_it.first;
     else
       to_ssa_expr(goto_state_rhs).set_level_2(goto_count);
   }
 
   {
     const auto p_it = dest_state.propagation.find(l1_identifier);
 
-    if(p_it != dest_state.propagation.end())
-      dest_state_rhs = p_it->second;
+    if(p_it.second)
+      dest_state_rhs = p_it.first;
     else
       to_ssa_expr(dest_state_rhs).set_level_2(dest_count);
   }

src/pointer-analysis/value_set.cpp

@@ -52,7 +52,7 @@ const value_sett::entryt *value_sett::find_entry(const value_sett::idt &id)
   const
 {
   auto found = values.find(id);
-  return found == values.end() ? nullptr : &found->second;
+  return !found.second ? nullptr : &found.first;
 }
 
 value_sett::entryt &value_sett::get_entry(const entryt &e, const typet &type)
@@ -64,10 +64,7 @@ value_sett::entryt &value_sett::get_entry(const entryt &e, const typet &type)
   else
     index=e.identifier;
 
-  std::pair<valuest::iterator, bool> r=
-    values.insert(std::pair<idt, entryt>(index, e));
-
-  return r.first->second;
+  return values.place(index, e).first;
 }
 
 bool value_sett::insert(
@@ -98,7 +95,10 @@ void value_sett::output(
   const namespacet &ns,
   std::ostream &out) const
 {
-  for(const auto &values_entry : values)
+  valuest::viewt view;
+  values.get_view(view);
+
+  for(const auto &values_entry : view)
   {
     irep_idt identifier, display_name;
 
@@ -205,6 +205,7 @@ bool value_sett::make_union(const value_sett::valuest &new_values)
 {
   bool result=false;
 
+#if 0
   valuest::iterator v_it=values.begin();
 
   for(valuest::const_iterator
@@ -236,6 +237,23 @@ bool value_sett::make_union(const value_sett::valuest &new_values)
     v_it++;
     it++;
   }
+#else
+  value_sett::valuest::delta_viewt delta_view;
+
+  new_values.get_delta_view(values, delta_view, false);
+
+  for(const auto &delta_entry : delta_view)
+  {
+    if(delta_entry.in_both)
+      result |= make_union(
+        values.at(delta_entry.k).object_map, delta_entry.m.object_map);
+    else
+    {
+      values.insert(delta_entry.k, delta_entry.m);
+      result = true;
+    }
+  }
+#endif
 
   return result;
 }

src/pointer-analysis/value_set.h

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/mp_arith.h>
 #include <util/reference_counting.h>
+#include <util/sharing_map.h>
 
 #include "object_numbering.h"
 #include "value_sets.h"
@@ -290,11 +291,11 @@ class value_sett
   ///
   /// The components of the ID are thus duplicated in the `valuest` key and in
   /// `entryt` fields.
-  #ifdef USE_DSTRING
-  typedef std::map<idt, entryt> valuest;
-  #else
+#ifdef USE_DSTRING
+  typedef sharing_mapt<idt, entryt> valuest;
+#else
   typedef std::unordered_map<idt, entryt, string_hash> valuest;
-  #endif
+#endif
 
   /// Gets values pointed to by `expr`, including following dereference
   /// operators (i.e. this is not a simple lookup in `valuest`).

src/pointer-analysis/value_set_analysis.cpp

@@ -41,7 +41,10 @@ void value_sets_to_xml(
     xmlt &i=dest.new_element("instruction");
     i.new_element()=::xml(location);
 
-    for(const auto &values_entry : value_set.values)
+    value_sett::valuest::viewt view;
+    value_set.values.get_view(view);
+
+    for(const auto &values_entry : view)
     {
       xmlt &var=i.new_element("variable");
       var.new_element("identifier").data=