Prepare for strict type checking in replace_symbolt

The derived class unchecked_replace_symbolt will not do any such type checking
and is to be used in all cases where types are expected to change or no type
checking can be performed.

Author: tautschnig

src/analyses/constant_propagator.h

@@ -71,7 +71,7 @@ class constant_propagator_domaint:public ai_domain_baset
   struct valuest
   {
     // maps variables to constants
-    replace_symbolt replace_const;
+    unchecked_replace_symbolt replace_const;
     bool is_bottom = true;
 
     bool merge(const valuest &src);

src/goto-instrument/code_contracts.cpp

@@ -185,7 +185,7 @@ void code_contractst::apply_contract(
     return;
 
   // replace formal parameters by arguments, replace return
-  replace_symbolt replace;
+  unchecked_replace_symbolt replace;
 
   // TODO: return value could be nil
   if(type.return_type()!=empty_typet())
@@ -303,7 +303,7 @@ void code_contractst::add_contract_check(
   // prepare function call including all declarations
   code_function_callt call;
   call.function()=ns.lookup(function).symbol_expr();
-  replace_symbolt replace;
+  unchecked_replace_symbolt replace;
 
   // decl ret
   if(gf.type.return_type()!=empty_typet())

src/goto-instrument/dump_c.cpp

@@ -908,7 +908,7 @@ void dump_ct::convert_global_variable(
 /// \param b: Code block to be cleaned
 void dump_ct::cleanup_harness(code_blockt &b)
 {
-  replace_symbolt replace;
+  unchecked_replace_symbolt replace;
   code_blockt decls;
 
   const symbolt *argc_sym=nullptr;

src/goto-instrument/model_argc_argv.cpp

@@ -125,7 +125,7 @@ bool model_argc_argv(
     {
       value = symbol_pair.second.value;
 
-      replace_symbolt replace;
+      unchecked_replace_symbolt replace;
       replace.insert("ARGC", ns.lookup("argc'").symbol_expr());
       replace.insert("ARGV", ns.lookup("argv'").symbol_expr());
       replace(value);

src/linking/linking_class.h

@@ -35,7 +35,7 @@ class linkingt:public typecheckt
   virtual void typecheck();
 
   rename_symbolt rename_symbol;
-  replace_symbolt object_type_updates;
+  unchecked_replace_symbolt object_type_updates;
 
 protected:
   bool needs_renaming_type(

src/solvers/smt2/smt2_solver.cpp

@@ -101,7 +101,7 @@ void smt2_solvert::expand_function_applications(exprt &expr)
                      app.arguments().size(),
                      "number of function parameters");
 
-      replace_symbolt replace_symbol;
+      unchecked_replace_symbolt replace_symbol;
 
       std::map<irep_idt, exprt> parameter_map;
       for(std::size_t i=0; i<f_type.domain().size(); i++)

src/util/replace_symbol.cpp

@@ -261,3 +261,33 @@ bool replace_symbolt::have_to_replace(const typet &dest) const
 
   return false;
 }
+
+unchecked_replace_symbolt &unchecked_replace_symbolt::operator=(
+  const unchecked_replace_symbolt &other)
+{
+  expr_map = other.expr_map;
+  type_map = other.type_map;
+
+  return *this;
+}
+
+void unchecked_replace_symbolt::insert(
+  const irep_idt &identifier,
+  const exprt &new_expr)
+{
+  expr_map.emplace(identifier, new_expr);
+}
+
+void unchecked_replace_symbolt::insert(
+  const symbol_exprt &old_expr,
+  const exprt &new_expr)
+{
+  insert(old_expr.get_identifier(), new_expr);
+}
+
+void unchecked_replace_symbolt::insert(
+  const irep_idt &identifier,
+  const typet &new_type)
+{
+  type_map.emplace(identifier, new_type);
+}

src/util/replace_symbol.h

@@ -113,4 +113,18 @@ class replace_symbolt
   bool have_to_replace(const typet &type) const;
 };
 
+class unchecked_replace_symbolt : public replace_symbolt
+{
+public:
+  unchecked_replace_symbolt()
+  {
+  }
+
+  unchecked_replace_symbolt &operator=(const unchecked_replace_symbolt &other);
+
+  void insert(const irep_idt &identifier, const exprt &new_expr);
+  void insert(const symbol_exprt &old_expr, const exprt &new_expr);
+  void insert(const irep_idt &identifier, const typet &new_type);
+};
+
 #endif // CPROVER_UTIL_REPLACE_SYMBOL_H

unit/util/replace_symbol.cpp

@@ -25,9 +25,8 @@ TEST_CASE("Replace all symbols in expression", "[core][util][replace_symbol]")
 
   exprt other_expr("other");
 
-  replace_symbolt r;
+  unchecked_replace_symbolt r;
   REQUIRE(r.empty());
-
   r.insert("a", other_expr);
   REQUIRE(r.replaces_symbol("a"));
   REQUIRE(r.get_expr_map().size() == 1);
@@ -62,7 +61,7 @@ TEST_CASE("Lvalue only", "[core][util][replace_symbol]")
 
   constant_exprt c("some_value", typet("some_type"));
 
-  replace_symbolt r;
+  unchecked_replace_symbolt r;
   r.insert("a", c);
 
   REQUIRE(r.replace(binary) == false);