replace_symbolt: hide {expr,type}_map

Values should only be added via insert. Add expr_map access functions as some
code still does access the expr_map.

Author: tautschnig

src/analyses/constant_propagator.cpp

@@ -292,8 +292,7 @@ bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const
     return false;
 
   if(expr.id()==ID_symbol)
-    if(replace_const.expr_map.find(to_symbol_expr(expr).get_identifier())==
-       replace_const.expr_map.end())
+    if(!replace_const.replaces_symbol(to_symbol_expr(expr).get_identifier()))
       return false;
 
   if(expr.id()==ID_index)
@@ -331,8 +330,7 @@ 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)
 {
-  replace_symbolt::expr_mapt::size_type n_erased=
-    replace_const.expr_map.erase(id);
+  const auto n_erased = replace_const.erase(id);
 
   INVARIANT(n_erased==0 || !is_bottom, "bottom should have no elements at all");
 
@@ -345,7 +343,7 @@ void constant_propagator_domaint::valuest::set_dirty_to_top(
   const namespacet &ns)
 {
   typedef replace_symbolt::expr_mapt expr_mapt;
-  expr_mapt &expr_map=replace_const.expr_map;
+  expr_mapt &expr_map = replace_const.get_expr_map();
 
   for(expr_mapt::iterator it=expr_map.begin();
       it!=expr_map.end();)
@@ -371,19 +369,19 @@ void constant_propagator_domaint::valuest::output(
   if(is_bottom)
   {
     out << "  bottom\n";
-    DATA_INVARIANT(replace_const.expr_map.empty(),
+    DATA_INVARIANT(is_empty(),
                    "If the domain is bottom, the map must be empty");
     return;
   }
 
   INVARIANT(!is_bottom, "Have handled bottom");
-  if(replace_const.expr_map.empty())
+  if(is_empty())
   {
     out << "top\n";
     return;
   }
 
-  for(const auto &p : replace_const.expr_map)
+  for(const auto &p : replace_const.get_expr_map())
   {
     out << ' ' << p.first << "=" << from_expr(ns, p.first, p.second) << '\n';
   }
@@ -418,20 +416,21 @@ bool constant_propagator_domaint::valuest::merge(const valuest &src)
 
   bool changed=false;
 
-  replace_symbolt::expr_mapt &expr_map=replace_const.expr_map;
-  const replace_symbolt::expr_mapt &src_expr_map=src.replace_const.expr_map;
-
   // handle top
-  if(src_expr_map.empty())
+  if(src.is_empty())
   {
     // change if it was not top
-    changed=!expr_map.empty();
+    changed = !is_empty();
 
     set_to_top();
 
     return changed;
   }
 
+  replace_symbolt::expr_mapt &expr_map = replace_const.get_expr_map();
+  const replace_symbolt::expr_mapt &src_expr_map =
+    src.replace_const.get_expr_map();
+
   // remove those that are
   // - different in src
   // - do not exist in src
@@ -476,12 +475,12 @@ bool constant_propagator_domaint::valuest::meet(const valuest &src)
 
   bool changed=false;
 
-  for(const auto &m : src.replace_const.expr_map)
+  for(const auto &m : src.replace_const.get_expr_map())
   {
-    replace_symbolt::expr_mapt::iterator
-      c_it=replace_const.expr_map.find(m.first);
+    replace_symbolt::expr_mapt::const_iterator c_it =
+      replace_const.get_expr_map().find(m.first);
 
-    if(c_it!=replace_const.expr_map.end())
+    if(c_it != replace_const.get_expr_map().end())
     {
       if(c_it->second!=m.second)
       {

src/analyses/constant_propagator.h

@@ -108,7 +108,7 @@ class constant_propagator_domaint:public ai_domain_baset
 
     void set_to(const irep_idt &lhs, const exprt &rhs)
     {
-      replace_const.expr_map[lhs]=rhs;
+      replace_const.get_expr_map()[lhs] = rhs;
       is_bottom=false;
     }
 
@@ -132,7 +132,7 @@ class constant_propagator_domaint:public ai_domain_baset
 
     bool is_empty() const
     {
-      return replace_const.expr_map.empty();
+      return replace_const.empty();
     }
 
     void output(std::ostream &out, const namespacet &ns) const;

src/goto-programs/link_goto_model.cpp

@@ -140,7 +140,7 @@ static bool link_functions(
       rename_symbols_in_function(dest_it->second, final_id, macro_application);
     }
 
-  if(!object_type_updates.expr_map.empty())
+  if(!object_type_updates.empty())
   {
     Forall_goto_functions(dest_it, dest_functions)
       Forall_goto_program_instructions(iit, dest_it->second.body)

src/util/replace_symbol.h

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <unordered_map>
 
+/// Replace expression or type symbols by an expression or type, respectively.
 class replace_symbolt
 {
 public:
@@ -79,9 +80,31 @@ class replace_symbolt
     return expr_map.empty() && type_map.empty();
   }
 
+  std::size_t erase(const irep_idt &id)
+  {
+    return expr_map.erase(id) + type_map.erase(id);
+  }
+
+  bool replaces_symbol(const irep_idt &id) const
+  {
+    return expr_map.find(id) != expr_map.end() ||
+           type_map.find(id) != type_map.end();
+  }
+
   replace_symbolt();
   virtual ~replace_symbolt();
 
+  const expr_mapt &get_expr_map() const
+  {
+    return expr_map;
+  }
+
+  expr_mapt &get_expr_map()
+  {
+    return expr_map;
+  }
+
+protected:
   expr_mapt expr_map;
   type_mapt type_map;
 

unit/util/replace_symbol.cpp

@@ -23,7 +23,11 @@ TEST_CASE("Replace all symbols in expression", "[core][util][replace_symbol]")
   exprt other_expr("other");
 
   replace_symbolt r;
+  REQUIRE(r.empty());
+
   r.insert("a", other_expr);
+  REQUIRE(r.replaces_symbol("a"));
+  REQUIRE(r.get_expr_map().size() == 1);
 
   REQUIRE(r.replace(binary) == false);
   REQUIRE(binary.op0() == other_expr);
@@ -33,6 +37,9 @@ TEST_CASE("Replace all symbols in expression", "[core][util][replace_symbol]")
 
   REQUIRE(r.replace(s2) == true);
   REQUIRE(s2 == symbol_exprt("b", typet("some_type")));
+
+  REQUIRE(r.erase("a") == 1);
+  REQUIRE(r.empty());
 }
 
 TEST_CASE("Lvalue only", "[core][util][optional]")