replace_symbolt: Check type consistency

Author: tautschnig

src/goto-instrument/dump_c.cpp

@@ -923,7 +923,10 @@ void dump_ct::cleanup_harness(code_blockt &b)
   if(!ns.lookup("argv'", argv_sym))
   {
     symbol_exprt argv("argv", argv_sym->type);
-    replace.insert(argv_sym->symbol_expr(), argv);
+    // replace argc' by argc in the type of argv['] to maintain type consistency
+    // while replacing
+    replace(argv);
+    replace.insert(symbol_exprt(argv_sym->name, argv.type()), argv);
     code_declt d(argv);
     decls.add(d);
   }

src/util/replace_symbol.cpp

@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "replace_symbol.h"
 
+#include "invariant.h"
 #include "std_types.h"
 #include "std_expr.h"
 
@@ -23,6 +24,7 @@ void replace_symbolt::insert(
   const symbol_exprt &old_expr,
   const exprt &new_expr)
 {
+  PRECONDITION(old_expr.type() == new_expr.type());
   expr_map.insert(std::pair<irep_idt, exprt>(
     old_expr.get_identifier(), new_expr));
 }
@@ -34,6 +36,9 @@ bool replace_symbolt::replace_symbol_expr(symbol_exprt &s) const
   if(it == expr_map.end())
     return true;
 
+  DATA_INVARIANT(
+    s.type() == it->second.type(),
+    "type of symbol to be replaced should match");
   static_cast<exprt &>(s) = it->second;
 
   return false;
@@ -249,6 +254,18 @@ void unchecked_replace_symbolt::insert(
   expr_map.emplace(old_expr.get_identifier(), new_expr);
 }
 
+bool unchecked_replace_symbolt::replace_symbol_expr(symbol_exprt &s) const
+{
+  expr_mapt::const_iterator it = expr_map.find(s.get_identifier());
+
+  if(it == expr_map.end())
+    return true;
+
+  static_cast<exprt &>(s) = it->second;
+
+  return false;
+}
+
 bool address_of_aware_replace_symbolt::replace(exprt &dest) const
 {
   const exprt &const_dest(dest);

src/util/replace_symbol.h

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include <unordered_map>
 
 /// Replace expression or type symbols by an expression or type, respectively.
+/// The resolved type of the symbol must match the type of the replacement.
 class replace_symbolt
 {
 public:
@@ -91,6 +92,9 @@ class unchecked_replace_symbolt : public replace_symbolt
   }
 
   void insert(const symbol_exprt &old_expr, const exprt &new_expr);
+
+private:
+  bool replace_symbol_expr(symbol_exprt &dest) const override;
 };
 
 /// Replace symbols with constants while maintaining syntactically valid

unit/util/replace_symbol.cpp

@@ -23,7 +23,7 @@ TEST_CASE("Replace all symbols in expression", "[core][util][replace_symbol]")
   array_typet array_type(typet("sub-type"), s1);
   REQUIRE(array_type.size() == s1);
 
-  exprt other_expr("other");
+  exprt other_expr("other", typet("some_type"));
 
   replace_symbolt r;
   REQUIRE(r.empty());