Avoid using replace_symbolt::insert(irep_idt, exprt)

All such cases will have a symbol_exprt in the vicinity and thus use
insert(symbol_exprt, exprt) instead.

Author: tautschnig

src/goto-instrument/code_contracts.cpp

@@ -189,7 +189,10 @@ void code_contractst::apply_contract(
 
   // TODO: return value could be nil
   if(type.return_type()!=empty_typet())
-    replace.insert("__CPROVER_return_value", call.lhs());
+  {
+    symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type());
+    replace.insert(ret_val, call.lhs());
+  }
 
   // formal parameters
   code_function_callt::argumentst::const_iterator a_it=
@@ -200,7 +203,10 @@ void code_contractst::apply_contract(
       a_it!=call.arguments().end();
       ++p_it, ++a_it)
     if(!p_it->get_identifier().empty())
-      replace.insert(p_it->get_identifier(), *a_it);
+    {
+      symbol_exprt p(p_it->get_identifier(), p_it->type());
+      replace.insert(p, *a_it);
+    }
 
   replace(requires);
   replace(ensures);
@@ -319,7 +325,8 @@ void code_contractst::add_contract_check(
 
     call.lhs()=r;
 
-    replace.insert("__CPROVER_return_value", r);
+    symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type());
+    replace.insert(ret_val, r);
   }
 
   // decl parameter1 ...
@@ -340,7 +347,10 @@ void code_contractst::add_contract_check(
     call.arguments().push_back(p);
 
     if(!p_it->get_identifier().empty())
-      replace.insert(p_it->get_identifier(), p);
+    {
+      symbol_exprt cur_p(p_it->get_identifier(), p_it->type());
+      replace.insert(cur_p, p);
+    }
   }
 
   // assume(requires)

src/goto-instrument/concurrency.cpp

@@ -89,19 +89,17 @@ void concurrency_instrumentationt::instrument(exprt &expr)
   {
     if(s_it->id()==ID_symbol)
     {
-      const irep_idt identifier=
-        to_symbol_expr(*s_it).get_identifier();
+      const symbol_exprt &s = to_symbol_expr(*s_it);
 
-      shared_varst::const_iterator
-        v_it=shared_vars.find(identifier);
+      shared_varst::const_iterator v_it = shared_vars.find(s.get_identifier());
 
       if(v_it!=shared_vars.end())
       {
         index_exprt new_expr;
         // new_expr.array()=symbol_expr();
         // new_expr.index()=symbol_expr();
 
-        replace_symbol.insert(identifier, new_expr);
+        replace_symbol.insert(s, new_expr);
       }
     }
   }

src/goto-instrument/dump_c.cpp

@@ -915,23 +915,23 @@ void dump_ct::cleanup_harness(code_blockt &b)
   if(!ns.lookup("argc'", argc_sym))
   {
     symbol_exprt argc("argc", argc_sym->type);
-    replace.insert(argc_sym->name, argc);
+    replace.insert(argc_sym->symbol_expr(), argc);
     code_declt d(argc);
     decls.add(d);
   }
   const symbolt *argv_sym=nullptr;
   if(!ns.lookup("argv'", argv_sym))
   {
     symbol_exprt argv("argv", argv_sym->type);
-    replace.insert(argv_sym->name, argv);
+    replace.insert(argv_sym->symbol_expr(), argv);
     code_declt d(argv);
     decls.add(d);
   }
   const symbolt *return_sym=nullptr;
   if(!ns.lookup("return'", return_sym))
   {
     symbol_exprt return_value("return_value", return_sym->type);
-    replace.insert(return_sym->name, return_value);
+    replace.insert(return_sym->symbol_expr(), return_value);
     code_declt d(return_value);
     decls.add(d);
   }

src/goto-instrument/model_argc_argv.cpp

@@ -74,6 +74,11 @@ bool model_argc_argv(
     return false;
   }
 
+  const symbolt &argc_primed = ns.lookup("argc'");
+  symbol_exprt ARGC("ARGC", argc_primed.type);
+  const symbolt &argv_primed = ns.lookup("argv'");
+  symbol_exprt ARGV("ARGV", argv_primed.type);
+
   // set the size of ARGV storage to 4096, which matches the minimum
   // guaranteed by POSIX (_POSIX_ARG_MAX):
   // http://pubs.opengroup.org/onlinepubs/009695399/basedefs/limits.h.html
@@ -126,8 +131,8 @@ bool model_argc_argv(
       value = symbol_pair.second.value;
 
       replace_symbolt replace;
-      replace.insert("ARGC", ns.lookup("argc'").symbol_expr());
-      replace.insert("ARGV", ns.lookup("argv'").symbol_expr());
+      replace.insert(ARGC, ns.lookup("argc'").symbol_expr());
+      replace.insert(ARGV, ns.lookup("argv'").symbol_expr());
       replace(value);
     }
     else if(

src/linking/linking.cpp

@@ -993,7 +993,8 @@ void linkingt::duplicate_object_symbol(
     else if(set_to_new)
       old_symbol.type=new_symbol.type;
 
-    object_type_updates.insert(old_symbol.name, old_symbol.symbol_expr());
+    object_type_updates.insert(
+      old_symbol.symbol_expr(), old_symbol.symbol_expr());
   }
 
   // care about initializers

src/solvers/flattening/flatten_byte_operators.cpp

@@ -79,7 +79,7 @@ static exprt unpack_rec(
     {
       index_exprt index(src, from_integer(i, index_type()));
       replace_symbolt replace;
-      replace.insert(ID_C_incomplete, index);
+      replace.insert(dummy, index);
 
       for(const auto &op : sub.operands())
       {

src/solvers/smt2/smt2_solver.cpp

@@ -106,10 +106,9 @@ void smt2_solvert::expand_function_applications(exprt &expr)
       std::map<irep_idt, exprt> parameter_map;
       for(std::size_t i=0; i<f_type.domain().size(); i++)
       {
-        const irep_idt p_identifier=
-          f_type.domain()[i].get_identifier();
-
-        replace_symbol.insert(p_identifier, app.arguments()[i]);
+        const auto &var = f_type.domain()[i];
+        const symbol_exprt s(var.get_identifier(), var.type());
+        replace_symbol.insert(s, app.arguments()[i]);
       }
 
       exprt body=f.definition;

src/util/replace_symbol.h

@@ -26,12 +26,6 @@ class replace_symbolt
   typedef std::unordered_map<irep_idt, exprt> expr_mapt;
   typedef std::unordered_map<irep_idt, typet> type_mapt;
 
-  void insert(const irep_idt &identifier,
-                     const exprt &expr)
-  {
-    expr_map.insert(std::pair<irep_idt, exprt>(identifier, expr));
-  }
-
   void insert(const class symbol_exprt &old_expr,
               const exprt &new_expr);
 

unit/util/replace_symbol.cpp

@@ -28,7 +28,7 @@ TEST_CASE("Replace all symbols in expression", "[core][util][replace_symbol]")
   replace_symbolt r;
   REQUIRE(r.empty());
 
-  r.insert("a", other_expr);
+  r.insert(s1, other_expr);
   REQUIRE(r.replaces_symbol("a"));
   REQUIRE(r.get_expr_map().size() == 1);
 
@@ -63,7 +63,7 @@ TEST_CASE("Lvalue only", "[core][util][replace_symbol]")
   constant_exprt c("some_value", typet("some_type"));
 
   replace_symbolt r;
-  r.insert("a", c);
+  r.insert(s1, c);
 
   REQUIRE(r.replace(binary) == false);
   REQUIRE(binary.op0() == address_of_exprt(s1));