Use sharing_mapt to store propagation map

goto-symex copies a state, which contains a propagation map, at each
branching point. The paths originating at that branch point typically
share most of the constants being propagated. Thus the copy is
unnecessarily expensive, and so is the merge at the next join point,
which will also result in one of the propagation maps to be destroyed.
With sharing_mapt, the copy has constant cost, and the cost of
destruction only depends on the size of the delta.

Author: tautschnig

src/goto-symex/goto_state.cpp

@@ -17,7 +17,10 @@ Author: Romain Brenguier, [email protected]
 /// 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";
   }
@@ -86,7 +89,11 @@ void goto_statet::apply_condition(
         increase_generation(
           l1_identifier, l1_lhs, previous_state.get_l2_name_provider());
 
-        propagation[l1_identifier] = rhs;
+        const auto propagation_entry = propagation.find(l1_identifier);
+        if(!propagation_entry.has_value())
+          propagation.insert(l1_identifier, rhs);
+        else if(propagation_entry->get() != rhs)
+          propagation.replace(l1_identifier, rhs);
 
         value_set.assign(l1_lhs, rhs, ns, true, false);
       }

src/goto-symex/goto_state.h

@@ -12,6 +12,8 @@ Author: Romain Brenguier, [email protected]
 #ifndef CPROVER_GOTO_SYMEX_GOTO_STATE_H
 #define CPROVER_GOTO_SYMEX_GOTO_STATE_H
 
+#include <util/sharing_map.h>
+
 #include <analyses/guard.h>
 #include <analyses/local_safe_pointers.h>
 #include <pointer-analysis/value_set.h>
@@ -54,7 +56,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/goto_symex_state.cpp

@@ -201,8 +201,14 @@ void goto_symex_statet::assignment(
   // for value propagation -- the RHS is L2
 
   if(!is_shared && record_value && goto_symex_is_constantt()(rhs))
-    propagation[l1_identifier] = rhs;
-  else
+  {
+    const auto propagation_entry = propagation.find(l1_identifier);
+    if(!propagation_entry.has_value())
+      propagation.insert(l1_identifier, rhs);
+    else if(propagation_entry->get() != rhs)
+      propagation.replace(l1_identifier, rhs);
+  }
+  else if(propagation.has_key(l1_identifier))
     propagation.erase(l1_identifier);
 
   {
@@ -289,8 +295,8 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
         // 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.has_value())
+          expr = *p_it; // already L2
         else
           ssa = set_indices<L2>(std::move(ssa), ns).get();
       }

src/goto-symex/symex_dead.cpp

@@ -36,7 +36,8 @@ void goto_symext::symex_dead(statet &state)
     // instance can no longer appear.
     if(state.value_set.values.has_key(l1_identifier))
       state.value_set.values.erase(l1_identifier);
-    state.propagation.erase(l1_identifier);
+    if(state.propagation.has_key(l1_identifier))
+      state.propagation.erase(l1_identifier);
     // Remove from the local L2 renaming map; this means any reads from the dead
     // identifier will use generation 0 (e.g. x!N@M#0, where N and M are
     // positive integers), which is never defined by any write, and will be

src/goto-symex/symex_goto.cpp

@@ -522,17 +522,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.has_value())
+      goto_state_rhs = *p_it;
     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.has_value())
+      dest_state_rhs = *p_it;
     else
       to_ssa_expr(dest_state_rhs).set_level_2(dest_count);
   }