Merge pull request #2723 from tautschnig/replace_symbol-cleanup

replace_symbolt refactoring and stricter type checking

regression/goto-instrument/constant-propagation2/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+int main()
+{
+  int i = 0;
+  int *p = &i;
+  assert(*p == 0);
+  return 0;
+}

regression/goto-instrument/constant-propagation2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--constant-propagator
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring

src/analyses/constant_propagator.h

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

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);
@@ -318,7 +324,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 ...
@@ -339,7 +346,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,11 +89,9 @@ 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())
       {
@@ -101,7 +99,7 @@ void concurrency_instrumentationt::instrument(exprt &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,7 +915,7 @@ 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);
   }
@@ -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->name, 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);
   }
@@ -931,7 +934,7 @@ void dump_ct::cleanup_harness(code_blockt &b)
   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
@@ -125,9 +130,9 @@ 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());
+      unchecked_replace_symbolt replace;
+      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/linking/linking_class.h

@@ -35,7 +35,7 @@ public:
   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/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.cpp

@@ -8,8 +8,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "replace_symbol.h"
 
-#include "std_types.h"
+#include "invariant.h"
 #include "std_expr.h"
+#include "std_types.h"
 
 replace_symbolt::replace_symbolt()
 {
@@ -23,13 +24,27 @@ 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));
 }
 
-bool replace_symbolt::replace(
-  exprt &dest,
-  const bool replace_with_const) const
+bool 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;
+
+  DATA_INVARIANT(
+    s.type() == it->second.type(),
+    "type of symbol to be replaced should match");
+  static_cast<exprt &>(s) = it->second;
+
+  return false;
+}
+
+bool replace_symbolt::replace(exprt &dest) const
 {
   bool result=true; // unchanged
 
@@ -49,14 +64,14 @@ bool replace_symbolt::replace(
   {
     member_exprt &me=to_member_expr(dest);
 
-    if(!replace(me.struct_op(), replace_with_const)) // Could give non l-value.
+    if(!replace(me.struct_op()))
       result=false;
   }
   else if(dest.id()==ID_index)
   {
     index_exprt &ie=to_index_expr(dest);
 
-    if(!replace(ie.array(), replace_with_const)) // Could give non l-value.
+    if(!replace(ie.array()))
       result=false;
 
     if(!replace(ie.index()))
@@ -66,27 +81,13 @@ bool replace_symbolt::replace(
   {
     address_of_exprt &aoe=to_address_of_expr(dest);
 
-    if(!replace(aoe.object(), false))
+    if(!replace(aoe.object()))
       result=false;
   }
   else if(dest.id()==ID_symbol)
   {
-    const symbol_exprt &s=to_symbol_expr(dest);
-
-    expr_mapt::const_iterator it=
-      expr_map.find(s.get_identifier());
-
-    if(it!=expr_map.end())
-    {
-      const exprt &e=it->second;
-
-      if(!replace_with_const && e.is_constant())  // Would give non l-value.
-        return true;
-
-      dest=e;
-
+    if(!replace_symbol_expr(to_symbol_expr(dest)))
       return false;
-    }
   }
   else
   {
@@ -110,7 +111,7 @@ bool replace_symbolt::replace(
 
 bool replace_symbolt::have_to_replace(const exprt &dest) const
 {
-  if(expr_map.empty() && type_map.empty())
+  if(expr_map.empty())
     return false;
 
   // first look at type
@@ -186,17 +187,6 @@ bool replace_symbolt::replace(typet &dest) const
       if(!replace(*it))
         result=false;
   }
-  else if(dest.id() == ID_symbol_type)
-  {
-    type_mapt::const_iterator it =
-      type_map.find(to_symbol_type(dest).get_identifier());
-
-    if(it!=type_map.end())
-    {
-      dest=it->second;
-      result=false;
-    }
-  }
   else if(dest.id()==ID_array)
   {
     array_typet &array_type=to_array_type(dest);
@@ -209,7 +199,7 @@ bool replace_symbolt::replace(typet &dest) const
 
 bool replace_symbolt::have_to_replace(const typet &dest) const
 {
-  if(expr_map.empty() && type_map.empty())
+  if(expr_map.empty())
     return false;
 
   if(dest.has_subtype())
@@ -251,13 +241,109 @@ bool replace_symbolt::have_to_replace(const typet &dest) const
       if(have_to_replace(*it))
         return true;
   }
-  else if(dest.id() == ID_symbol_type)
-  {
-    const irep_idt &identifier = to_symbol_type(dest).get_identifier();
-    return type_map.find(identifier) != type_map.end();
-  }
   else if(dest.id()==ID_array)
     return have_to_replace(to_array_type(dest).size());
 
   return false;
 }
+
+void unchecked_replace_symbolt::insert(
+  const symbol_exprt &old_expr,
+  const exprt &new_expr)
+{
+  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);
+  if(!require_lvalue && const_dest.id() != ID_address_of)
+    return unchecked_replace_symbolt::replace(dest);
+
+  bool result = true; // unchanged
+
+  // first look at type
+  if(have_to_replace(const_dest.type()))
+  {
+    const set_require_lvalue_and_backupt backup(require_lvalue, false);
+    if(!unchecked_replace_symbolt::replace(dest.type()))
+      result = false;
+  }
+
+  // now do expression itself
+
+  if(!have_to_replace(dest))
+    return result;
+
+  if(dest.id() == ID_index)
+  {
+    index_exprt &ie = to_index_expr(dest);
+
+    // Could yield non l-value.
+    if(!replace(ie.array()))
+      result = false;
+
+    const set_require_lvalue_and_backupt backup(require_lvalue, false);
+    if(!replace(ie.index()))
+      result = false;
+  }
+  else if(dest.id() == ID_address_of)
+  {
+    address_of_exprt &aoe = to_address_of_expr(dest);
+
+    const set_require_lvalue_and_backupt backup(require_lvalue, true);
+    if(!replace(aoe.object()))
+      result = false;
+  }
+  else
+  {
+    if(!unchecked_replace_symbolt::replace(dest))
+      return false;
+  }
+
+  const set_require_lvalue_and_backupt backup(require_lvalue, false);
+
+  const typet &c_sizeof_type =
+    static_cast<const typet &>(dest.find(ID_C_c_sizeof_type));
+  if(c_sizeof_type.is_not_nil() && have_to_replace(c_sizeof_type))
+    result &= unchecked_replace_symbolt::replace(
+      static_cast<typet &>(dest.add(ID_C_c_sizeof_type)));
+
+  const typet &va_arg_type =
+    static_cast<const typet &>(dest.find(ID_C_va_arg_type));
+  if(va_arg_type.is_not_nil() && have_to_replace(va_arg_type))
+    result &= unchecked_replace_symbolt::replace(
+      static_cast<typet &>(dest.add(ID_C_va_arg_type)));
+
+  return result;
+}
+
+bool address_of_aware_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;
+
+  if(require_lvalue && e.is_constant()) // Would give non l-value.
+    return true;
+
+  static_cast<exprt &>(s) = e;
+
+  return false;
+}

src/util/replace_symbol.h

@@ -20,43 +20,16 @@ Author: Daniel Kroening, kroening@kroening.com
 #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:
   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));
-  }
-
-  /// \brief Replaces a symbol with a constant
-  /// If you are replacing symbols with constants in an l-value, you can
-  /// create something that is not an l-value.   For example if your
-  /// l-value is "a[i]" then substituting i for a constant results in an
-  /// l-value but substituting a for a constant (array) wouldn't.  This
-  /// only applies to the "top level" of the expression, for example, it
-  /// is OK to replace b with a constant array in a[b[0]].
-  ///
-  /// \param dest The expression in which to do the replacement
-  /// \param replace_with_const If false then it disables the rewrites that
-  /// could result in something that is not an l-value.
-  ///
-  virtual bool replace(
-    exprt &dest,
-    const bool replace_with_const=true) const;
-
+  virtual bool replace(exprt &dest) const;
   virtual bool replace(typet &dest) const;
 
   void operator()(exprt &dest) const
@@ -72,23 +45,21 @@ public:
   void clear()
   {
     expr_map.clear();
-    type_map.clear();
   }
 
   bool empty() const
   {
-    return expr_map.empty() && type_map.empty();
+    return expr_map.empty();
   }
 
   std::size_t erase(const irep_idt &id)
   {
-    return expr_map.erase(id) + type_map.erase(id);
+    return expr_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();
+    return expr_map.find(id) != expr_map.end();
   }
 
   replace_symbolt();
@@ -106,11 +77,62 @@ public:
 
 protected:
   expr_mapt expr_map;
-  type_mapt type_map;
 
-protected:
+  virtual bool replace_symbol_expr(symbol_exprt &dest) const;
+
   bool have_to_replace(const exprt &dest) const;
   bool have_to_replace(const typet &type) const;
 };
 
+class unchecked_replace_symbolt : public replace_symbolt
+{
+public:
+  unchecked_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
+/// expressions.
+/// If you are replacing symbols with constants in an l-value, you can
+/// create something that is not an l-value.   For example if your
+/// l-value is "a[i]" then substituting i for a constant results in an
+/// l-value but substituting a for a constant (array) wouldn't.  This
+/// only applies to the "top level" of the expression, for example, it
+/// is OK to replace b with a constant array in a[b[0]].
+class address_of_aware_replace_symbolt : public unchecked_replace_symbolt
+{
+public:
+  bool replace(exprt &dest) const override;
+
+private:
+  mutable bool require_lvalue = false;
+
+  class set_require_lvalue_and_backupt
+  {
+  public:
+    set_require_lvalue_and_backupt(bool &require_lvalue, const bool value)
+      : require_lvalue(require_lvalue), prev_value(require_lvalue)
+    {
+      require_lvalue = value;
+    }
+
+    ~set_require_lvalue_and_backupt()
+    {
+      require_lvalue = prev_value;
+    }
+
+  private:
+    bool &require_lvalue;
+    bool prev_value;
+  };
+
+  bool replace_symbol_expr(symbol_exprt &dest) const override;
+};
+
 #endif // CPROVER_UTIL_REPLACE_SYMBOL_H

unit/util/replace_symbol.cpp

@@ -23,12 +23,12 @@ 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());
 
-  r.insert("a", other_expr);
+  r.insert(s1, other_expr);
   REQUIRE(r.replaces_symbol("a"));
   REQUIRE(r.get_expr_map().size() == 1);
 
@@ -62,8 +62,8 @@ TEST_CASE("Lvalue only", "[core][util][replace_symbol]")
 
   constant_exprt c("some_value", typet("some_type"));
 
-  replace_symbolt r;
-  r.insert("a", c);
+  address_of_aware_replace_symbolt r;
+  r.insert(s1, c);
 
   REQUIRE(r.replace(binary) == false);
   REQUIRE(binary.op0() == address_of_exprt(s1));
@@ -72,3 +72,27 @@ TEST_CASE("Lvalue only", "[core][util][replace_symbol]")
   REQUIRE(to_array_type(index_expr.array().type()).size() == c);
   REQUIRE(index_expr.index() == c);
 }
+
+TEST_CASE("Replace always", "[core][util][replace_symbol]")
+{
+  symbol_exprt s1("a", typet("some_type"));
+  array_typet array_type(typet("some_type"), s1);
+  symbol_exprt array("b", array_type);
+  index_exprt index(array, s1);
+
+  exprt binary("binary", typet("some_type"));
+  binary.copy_to_operands(address_of_exprt(s1));
+  binary.copy_to_operands(address_of_exprt(index));
+
+  constant_exprt c("some_value", typet("some_type"));
+
+  unchecked_replace_symbolt r;
+  r.insert(s1, c);
+
+  REQUIRE(r.replace(binary) == false);
+  REQUIRE(binary.op0() == address_of_exprt(c));
+  const index_exprt &index_expr =
+    to_index_expr(to_address_of_expr(binary.op1()).object());
+  REQUIRE(to_array_type(index_expr.array().type()).size() == c);
+  REQUIRE(index_expr.index() == c);
+}