Merge pull request #3101 from smowton/smowton/cleanup/replace-symbol-interface

Clean up replace_symbolt interface

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();