Clean up replace_symbolt interface

Add set(), with meaning similar to insert() but overwriting any existing value, and
an overload of erase() that takes an iterator. These allow the constant propagator to use
it more cleanly (though not entirely; it still needs get_expr_map() for some tasks such
as merging two replace_symbolt objects).

No behavioural change is intended here.

Author: smowton

src/analyses/constant_propagator.cpp

@@ -214,7 +214,7 @@ void constant_propagator_domaint::transform(
     const code_typet &type=to_code_type(symbol.type);
 
     for(const auto &param : type.parameters())
-      values.set_to_top(param.get_identifier());
+      values.set_to_top(symbol_exprt(param.get_identifier(), param.type()));
   }
 
   INVARIANT(from->is_goto() || !values.is_bottom,
@@ -334,9 +334,10 @@ bool constant_propagator_domaint::valuest::is_constant_address_of(
 }
 
 /// Do not call this when iterating over replace_const.expr_map!
-bool constant_propagator_domaint::valuest::set_to_top(const irep_idt &id)
+bool constant_propagator_domaint::valuest::set_to_top(
+  const symbol_exprt &symbol_expr)
 {
-  const auto n_erased = replace_const.erase(id);
+  const auto n_erased = replace_const.erase(symbol_expr.get_identifier());
 
   INVARIANT(n_erased==0 || !is_bottom, "bottom should have no elements at all");
 
@@ -360,7 +361,9 @@ void constant_propagator_domaint::valuest::set_dirty_to_top(
 
     if((!symbol.is_procedure_local() || dirty(id)) &&
        !symbol.type.get_bool(ID_C_constant))
-      it=expr_map.erase(it);
+    {
+      it = replace_const.erase(it);
+    }
     else
       it++;
   }
@@ -456,15 +459,15 @@ bool constant_propagator_domaint::valuest::merge(const valuest &src)
 
       if(expr!=src_expr)
       {
-        it=expr_map.erase(it);
+        it = replace_const.erase(it);
         changed=true;
       }
       else
         it++;
     }
     else
     {
-      it=expr_map.erase(it);
+      it = replace_const.erase(it);
       changed=true;
     }
   }
@@ -499,10 +502,11 @@ bool constant_propagator_domaint::valuest::meet(
     }
     else
     {
+      const typet &m_id_type = ns.lookup(m.first).type;
       DATA_INVARIANT(
-        base_type_eq(ns.lookup(m.first).type, m.second.type(), ns),
+        base_type_eq(m_id_type, m.second.type(), ns),
         "type of constant to be stored should match");
-      set_to(m.first, m.second);
+      set_to(symbol_exprt(m.first, m_id_type), m.second);
       changed=true;
     }
   }
@@ -558,7 +562,7 @@ bool constant_propagator_domaint::partial_evaluate_with_all_rounding_modes(
   {
     constant_propagator_domaint child(*this);
     child.values.set_to(
-      ID_cprover_rounding_mode_str,
+      symbol_exprt(ID_cprover_rounding_mode_str, integer_typet()),
       from_integer(rounding_modes[i], integer_typet()));
     exprt result = expr;
     if(child.replace_constants_and_simplify(result, ns))

src/analyses/constant_propagator.h

@@ -111,25 +111,13 @@ class constant_propagator_domaint:public ai_domain_baset
       return !is_bottom && replace_const.empty();
     }
 
-    // set single identifier
-
-    void set_to(const irep_idt &lhs, const exprt &rhs)
-    {
-      replace_const.get_expr_map()[lhs] = rhs;
-      is_bottom=false;
-    }
-
     void set_to(const symbol_exprt &lhs, const exprt &rhs)
     {
-      set_to(lhs.get_identifier(), rhs);
-    }
-
-    bool set_to_top(const symbol_exprt &expr)
-    {
-      return set_to_top(expr.get_identifier());
+      replace_const.set(lhs, rhs);
+      is_bottom=false;
     }
 
-    bool set_to_top(const irep_idt &id);
+    bool set_to_top(const symbol_exprt &expr);
 
     void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns);
 

src/util/replace_symbol.cpp

@@ -30,6 +30,13 @@ void replace_symbolt::insert(
     old_expr.get_identifier(), new_expr));
 }
 
+void replace_symbolt::set(const symbol_exprt &old_expr, const exprt &new_expr)
+{
+  PRECONDITION(old_expr.type() == new_expr.type());
+  expr_map[old_expr.get_identifier()] = new_expr;
+}
+
+
 bool replace_symbolt::replace_symbol_expr(symbol_exprt &s) const
 {
   expr_mapt::const_iterator it = expr_map.find(s.get_identifier());

src/util/replace_symbol.h

@@ -26,9 +26,15 @@ class replace_symbolt
 public:
   typedef std::unordered_map<irep_idt, exprt> expr_mapt;
 
+  /// Sets old_expr to be replaced by new_expr if we don't already have a
+  /// replacement; otherwise does nothing (i.e. std::map::insert-like
+  /// behaviour).
   void insert(const class symbol_exprt &old_expr,
               const exprt &new_expr);
 
+  /// Sets old_expr to be replaced by new_expr
+  void set(const class symbol_exprt &old_expr, const exprt &new_expr);
+
   virtual bool replace(exprt &dest) const;
   virtual bool replace(typet &dest) const;
 
@@ -57,6 +63,11 @@ class replace_symbolt
     return expr_map.erase(id);
   }
 
+  expr_mapt::iterator erase(expr_mapt::iterator it)
+  {
+    return expr_map.erase(it);
+  }
+
   bool replaces_symbol(const irep_idt &id) const
   {
     return expr_map.find(id) != expr_map.end();