Refactor lvalue-retainment in replace_symbolt into a separate class

Author: tautschnig

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 @@ class constant_propagator_domaint:public ai_domain_baset
   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/util/replace_symbol.cpp

@@ -27,9 +27,19 @@ void replace_symbolt::insert(
     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;
+
+  static_cast<exprt &>(s) = it->second;
+
+  return false;
+}
+
+bool replace_symbolt::replace(exprt &dest) const
 {
   bool result=true; // unchanged
 
@@ -49,14 +59,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 +76,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
   {
@@ -252,3 +248,85 @@ void unchecked_replace_symbolt::insert(
 {
   expr_map.emplace(old_expr.get_identifier(), new_expr);
 }
+
+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

@@ -28,22 +28,7 @@ class replace_symbolt
   void insert(const class symbol_exprt &old_expr,
               const exprt &new_expr);
 
-  /// \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
@@ -92,7 +77,8 @@ class replace_symbolt
 protected:
   expr_mapt expr_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;
 };
@@ -107,4 +93,42 @@ class unchecked_replace_symbolt : public replace_symbolt
   void insert(const symbol_exprt &old_expr, const exprt &new_expr);
 };
 
+/// 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

@@ -62,7 +62,7 @@ TEST_CASE("Lvalue only", "[core][util][replace_symbol]")
 
   constant_exprt c("some_value", typet("some_type"));
 
-  replace_symbolt r;
+  address_of_aware_replace_symbolt r;
   r.insert(s1, c);
 
   REQUIRE(r.replace(binary) == false);
@@ -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);
+}