replace_symbolt: Check type consistency

Author: tautschnig

src/goto-instrument/concurrency.cpp

@@ -80,7 +80,8 @@ void concurrency_instrumentationt::instrument(exprt &expr)
 
   find_symbols(expr, symbols);
 
-  replace_symbolt replace_symbol;
+  const namespacet ns(symbol_table);
+  replace_symbolt replace_symbol(ns);
 
   for(std::set<exprt>::const_iterator
       s_it=symbols.begin();

src/goto-programs/instrument_preconditions.cpp

@@ -71,7 +71,7 @@ replace_symbolt actuals_replace_map(
   const auto &parameters=code_type.parameters();
   const auto &arguments=call.arguments();
 
-  replace_symbolt result;
+  replace_symbolt result(ns);
   std::size_t count=0;
   for(const auto &p : parameters)
   {

src/solvers/flattening/flatten_byte_operators.cpp

@@ -15,6 +15,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/pointer_offset_size.h>
 #include <util/replace_symbol.h>
 #include <util/simplify_expr.h>
+#include <util/symbol.h>
+#include <util/symbol_table.h>
 
 #include "flatten_byte_extract_exceptions.h"
 
@@ -72,13 +74,20 @@ static exprt unpack_rec(
     // all array members will have the same structure; do this just
     // once and then replace the dummy symbol by a suitable index
     // expression in the loop below
-    symbol_exprt dummy(ID_C_incomplete, subtype);
+    symbolt dummy_sym;
+    dummy_sym.name = ID_C_incomplete;
+    dummy_sym.type = subtype;
+    const symbol_exprt dummy = dummy_sym.symbol_expr();
+    symbol_tablet st;
+    st.add(dummy_sym);
+    namespacet dummy_ns(st);
+
     exprt sub=unpack_rec(dummy, little_endian, max_bytes, ns, true);
 
     for(mp_integer i=0; i<num_elements; ++i)
     {
       index_exprt index(src, from_integer(i, index_type()));
-      replace_symbolt replace;
+      replace_symbolt replace(dummy_ns);
       replace.insert(ID_C_incomplete, index);
 
       for(const auto &op : sub.operands())

src/util/replace_symbol.cpp

@@ -8,23 +8,54 @@ Author: Daniel Kroening, [email protected]
 
 #include "replace_symbol.h"
 
+#include "base_type.h"
+#include "invariant.h"
+#include "namespace.h"
 #include "std_types.h"
 #include "std_expr.h"
+#include "symbol.h"
 
-replace_symbolt::replace_symbolt()
+replace_symbolt::~replace_symbolt()
 {
 }
 
-replace_symbolt::~replace_symbolt()
+replace_symbolt &replace_symbolt::operator=(const replace_symbolt &other)
+{
+  PRECONDITION(&ns.get_symbol_table() == &other.ns.get_symbol_table());
+
+  expr_map = other.expr_map;
+  type_map = other.type_map;
+
+  return *this;
+}
+
+void replace_symbolt::insert(
+  const irep_idt &identifier,
+  const exprt &new_expr)
 {
+  const symbolt &symbol = ns.lookup(identifier);
+  PRECONDITION(!symbol.is_type);
+  PRECONDITION(base_type_eq(ns.lookup(identifier).type, new_expr.type(), ns));
+
+  expr_map.emplace(identifier, new_expr);
 }
 
 void replace_symbolt::insert(
   const symbol_exprt &old_expr,
   const exprt &new_expr)
 {
-  expr_map.insert(std::pair<irep_idt, exprt>(
-    old_expr.get_identifier(), new_expr));
+  insert(old_expr.get_identifier(), new_expr);
+}
+
+void replace_symbolt::insert(
+  const irep_idt &identifier,
+  const typet &new_type)
+{
+  const symbolt &symbol = ns.lookup(identifier);
+  PRECONDITION(symbol.is_type);
+  PRECONDITION(base_type_eq(ns.lookup(identifier).type, new_type, ns));
+
+  type_map.emplace(identifier, new_type);
 }
 
 bool replace_symbolt::replace_symbol_expr(symbol_exprt &s) const
@@ -34,6 +65,9 @@ bool replace_symbolt::replace_symbol_expr(symbol_exprt &s) const
   if(it == expr_map.end())
     return true;
 
+  DATA_INVARIANT(
+    base_type_eq(s.type(), it->second.type(), ns),
+    "type of symbol to be replaced should match");
   static_cast<exprt &>(s) = it->second;
 
   return false;
@@ -288,6 +322,30 @@ void unchecked_replace_symbolt::insert(
   type_map.emplace(identifier, new_type);
 }
 
+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;
+
+  const exprt &e = it->second;
+
+  static_cast<exprt &>(s) = e;
+#if 0
+  if(ignore_type_change || dest.type() == e.type())
+    dest = e;
+  else
+  {
+    typet type = dest.type();
+    dest = e;
+    dest.make_typecast(type);
+  }
+#endif
+
+  return false;
+}
+
 bool address_of_aware_replace_symbolt::replace(exprt &dest) const
 {
   const exprt &const_dest(dest);

src/util/replace_symbol.h

@@ -15,32 +15,25 @@ Author: Daniel Kroening, [email protected]
 // false: replaced something
 //
 
+#include <unordered_map>
+
 #include "expr.h"
+#include "namespace.h"
+#include "symbol_table.h"
 
-#include <unordered_map>
+class symbol_exprt;
 
 /// 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:
   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);
-
-  void insert(const irep_idt &identifier,
-                     const typet &type)
-  {
-    type_map.insert(std::pair<irep_idt, typet>(identifier, type));
-  }
-
+  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);
 
   virtual bool replace(exprt &dest) const;
   virtual bool replace(typet &dest) const;
@@ -77,7 +70,11 @@ class replace_symbolt
            type_map.find(id) != type_map.end();
   }
 
-  replace_symbolt();
+  explicit replace_symbolt(const namespacet &ns)
+    : ns(ns)
+  {
+  }
+
   virtual ~replace_symbolt();
 
   const expr_mapt &get_expr_map() const
@@ -90,7 +87,10 @@ class replace_symbolt
     return expr_map;
   }
 
+  replace_symbolt &operator=(const replace_symbolt &other);
+
 protected:
+  const namespacet &ns;
   expr_mapt expr_map;
   type_mapt type_map;
 
@@ -104,6 +104,7 @@ class unchecked_replace_symbolt : public replace_symbolt
 {
 public:
   unchecked_replace_symbolt()
+    : replace_symbolt(dummy_ns), dummy_ns(symbol_table)
   {
   }
 
@@ -112,6 +113,12 @@ class unchecked_replace_symbolt : public replace_symbolt
   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);
+
+private:
+  const symbol_tablet symbol_table;
+  const namespacet dummy_ns;
+
+  bool replace_symbol_expr(symbol_exprt &dest) const override;
 };
 
 /// Replace symbols with constants while maintaining syntactically valid

unit/util/replace_symbol.cpp

@@ -13,8 +13,19 @@
 
 TEST_CASE("Replace all symbols in expression", "[core][util][replace_symbol]")
 {
-  symbol_exprt s1("a", typet("some_type"));
-  symbol_exprt s2("b", typet("some_type"));
+  symbol_tablet symbol_table;
+
+  symbolt sym_a;
+  sym_a.name = "a";
+  sym_a.type = typet("some_type");
+  symbol_exprt s1 = sym_a.symbol_expr();
+  symbol_table.add(sym_a);
+
+  symbolt sym_b;
+  sym_b.name = "b";
+  sym_b.type = typet("some_type");
+  symbol_exprt s2 = sym_b.symbol_expr();
+  symbol_table.add(sym_b);
 
   exprt binary("binary", typet("some_type"));
   binary.copy_to_operands(s1);
@@ -23,9 +34,10 @@ 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"));
 
-  unchecked_replace_symbolt r;
+  namespacet ns(symbol_table);
+  replace_symbolt r(ns);
   REQUIRE(r.empty());
   r.insert("a", other_expr);
   REQUIRE(r.replaces_symbol("a"));