Merge pull request #2720 from tautschnig/replace_symbol-cleanup1

replace_symbolt: hide {expr,type}_map

Author: tautschnig

src/analyses/constant_propagator.cpp

@@ -298,8 +298,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)
@@ -337,8 +336,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");
 
@@ -351,7 +349,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();)
@@ -377,19 +375,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';
   }
@@ -424,20 +422,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
@@ -484,12 +483,12 @@ bool constant_propagator_domaint::valuest::meet(
 
   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

@@ -105,7 +105,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;
     }
 
@@ -129,7 +129,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, kroening@kroening.com
 
 #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

@@ -26,7 +26,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);
@@ -37,8 +41,12 @@ 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.replace(array_type) == false);
   REQUIRE(array_type.size() == other_expr);
+
+  REQUIRE(r.erase("a") == 1);
+  REQUIRE(r.empty());
 }
 
 TEST_CASE("Lvalue only", "[core][util][replace_symbol]")