replace_symbolt must consider all non-lvalues

Literal constants are not the only ones: for example, address-of isn't an lvalue
either. Make is_lvalue globally available to accomplish this.

Author: tautschnig

src/goto-programs/builtin_functions.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/cprover_prefix.h>
+#include <util/expr_util.h>
 #include <util/pointer_offset_size.h>
 #include <util/rational.h>
 #include <util/rational_tools.h>
@@ -621,20 +622,6 @@ void goto_convertt::do_array_op(
   copy(array_op_statement, OTHER, dest);
 }
 
-bool is_lvalue(const exprt &expr)
-{
-  if(expr.id()==ID_index)
-    return is_lvalue(to_index_expr(expr).op0());
-  else if(expr.id()==ID_member)
-    return is_lvalue(to_member_expr(expr).op0());
-  else if(expr.id()==ID_dereference)
-    return true;
-  else if(expr.id()==ID_symbol)
-    return true;
-  else
-    return false;
-}
-
 exprt make_va_list(const exprt &expr)
 {
   // we first strip any typecast

src/util/expr_util.cpp

@@ -201,3 +201,18 @@ if_exprt lift_if(const exprt &src, std::size_t operand_number)
 
   return result;
 }
+
+/// returns true if the expression can be used as an lvalue
+bool is_lvalue(const exprt &expr)
+{
+  if(expr.id() == ID_index)
+    return is_lvalue(to_index_expr(expr).op0());
+  else if(expr.id() == ID_member)
+    return is_lvalue(to_member_expr(expr).op0());
+  else if(expr.id() == ID_dereference)
+    return true;
+  else if(expr.id() == ID_symbol)
+    return true;
+  else
+    return false;
+}

src/util/expr_util.h

@@ -72,4 +72,6 @@ bool has_subtype(const typet &, const irep_idt &id, const namespacet &);
 /// lift up an if_exprt one level
 if_exprt lift_if(const exprt &, std::size_t operand_number);
 
+bool is_lvalue(const exprt &);
+
 #endif // CPROVER_UTIL_EXPR_UTIL_H

src/util/replace_symbol.cpp

@@ -8,8 +8,9 @@ Author: Daniel Kroening, [email protected]
 
 #include "replace_symbol.h"
 
-#include "std_types.h"
+#include "expr_util.h"
 #include "std_expr.h"
+#include "std_types.h"
 
 replace_symbolt::replace_symbolt()
 {
@@ -80,7 +81,7 @@ bool replace_symbolt::replace(
     {
       const exprt &e=it->second;
 
-      if(!replace_with_const && e.is_constant())  // Would give non l-value.
+      if(!replace_with_const && !is_lvalue(e))
         return true;
 
       dest=e;

unit/util/replace_symbol.cpp

@@ -51,4 +51,10 @@ TEST_CASE("Lvalue only", "[core][util][optional]")
 
   REQUIRE(r.replace(binary) == true);
   REQUIRE(binary.op0() == address_of_exprt(s1));
+
+  address_of_exprt address_of(s1);
+  r.insert("b", address_of);
+
+  REQUIRE(r.replace(binary) == true);
+  REQUIRE(binary.op1() == address_of_exprt(s2));
 }