Rename LHS rvalues up front

src/goto-symex/expr_skeleton.cpp

@@ -52,51 +52,3 @@ expr_skeletont expr_skeletont::compose(expr_skeletont other) const
 {
   return expr_skeletont(apply(other.skeleton));
 }
-
-/// In the expression corresponding to a skeleton returns a pointer to the
-/// deepest subexpression before we encounter nil.
-static exprt *deepest_not_nil(exprt &e)
-{
-  exprt *ptr = &e;
-  while(!ptr->op0().is_nil())
-    ptr = &ptr->op0();
-  return ptr;
-}
-
-optionalt<expr_skeletont>
-expr_skeletont::clear_innermost_index_expr(expr_skeletont skeleton)
-{
-  exprt *to_update = deepest_not_nil(skeleton.skeleton);
-  if(index_exprt *index_expr = expr_try_dynamic_cast<index_exprt>(*to_update))
-  {
-    index_expr->make_nil();
-    return expr_skeletont{std::move(skeleton)};
-  }
-  return {};
-}
-
-optionalt<expr_skeletont>
-expr_skeletont::clear_innermost_member_expr(expr_skeletont skeleton)
-{
-  exprt *to_update = deepest_not_nil(skeleton.skeleton);
-  if(member_exprt *member = expr_try_dynamic_cast<member_exprt>(*to_update))
-  {
-    member->make_nil();
-    return expr_skeletont{std::move(skeleton)};
-  }
-  return {};
-}
-
-optionalt<expr_skeletont>
-expr_skeletont::clear_innermost_byte_extract_expr(expr_skeletont skeleton)
-{
-  exprt *to_update = deepest_not_nil(skeleton.skeleton);
-  if(
-    to_update->id() != ID_byte_extract_big_endian &&
-    to_update->id() != ID_byte_extract_little_endian)
-  {
-    return {};
-  }
-  to_update->make_nil();
-  return expr_skeletont{std::move(skeleton.skeleton)};
-}

src/goto-symex/expr_skeleton.h

@@ -43,24 +43,6 @@ class expr_skeletont final
   /// `array2[index]`.
   static expr_skeletont remove_op0(exprt e);
 
-  /// If the deepest subexpression in the skeleton is a member expression,
-  /// replace it with a nil expression and return the obtained skeleton.
-  static optionalt<expr_skeletont>
-  clear_innermost_index_expr(expr_skeletont skeleton);
-
-  /// If the deepest subexpression in the skeleton is a member expression,
-  /// replace it with a nil expression and return the obtained skeleton.
-  static optionalt<expr_skeletont>
-  clear_innermost_member_expr(expr_skeletont skeleton);
-
-  /// If the deepest subexpression in the skeleton is a byte-extract expression,
-  /// replace it with a nil expression and return the obtained skeleton.
-  /// For instance, for `(byte_extract(☐, 2, int)).field[index]`
-  /// `☐.field[index]` is returned, while for `byte_extract(☐.field, 2, int)`
-  /// an empty optional is returned.
-  static optionalt<expr_skeletont>
-  clear_innermost_byte_extract_expr(expr_skeletont skeleton);
-
 private:
   /// In \c skeleton, nil_exprt is used to mark the sub expression to be
   /// substituted. The nil_exprt always appears recursively following the first

src/goto-symex/goto_symex.cpp

@@ -41,6 +41,13 @@ void goto_symext::symex_assign(statet &state, const code_assignt &code)
               << messaget::eom;
     });
 
+  // rvalues present within the lhs (for example, "some_array[this_rvalue]" or
+  // "byte_extract <type> from an_lvalue offset this_rvalue") can affect whether
+  // we use field-sensitive symbols or not, so L2-rename them up front:
+  lhs = state.l2_rename_rvalues(lhs, ns);
+  do_simplify(lhs);
+  lhs = state.field_sensitivity.apply(ns, state, std::move(lhs), true);
+
   if(rhs.id() == ID_side_effect)
   {
     const side_effect_exprt &side_effect_expr = to_side_effect_expr(rhs);

src/goto-symex/goto_symex_state.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/as_const.h>
 #include <util/base_exceptions.h>
+#include <util/byte_operators.h>
 #include <util/exception_utils.h>
 #include <util/expr_util.h>
 #include <util/format.h>
@@ -48,90 +49,6 @@ goto_symex_statet::goto_symex_statet(
 
 goto_symex_statet::~goto_symex_statet()=default;
 
-/// Check that \p expr is correctly renamed to level 2 and return true in case
-/// an error is detected.
-static bool check_renaming(const exprt &expr);
-
-static bool check_renaming(const typet &type)
-{
-  if(type.id()==ID_array)
-    return check_renaming(to_array_type(type).size());
-  else if(type.id() == ID_struct || type.id() == ID_union)
-  {
-    for(const auto &c : to_struct_union_type(type).components())
-      if(check_renaming(c.type()))
-        return true;
-  }
-  else if(type.has_subtype())
-    return check_renaming(to_type_with_subtype(type).subtype());
-
-  return false;
-}
-
-static bool check_renaming_l1(const exprt &expr)
-{
-  if(check_renaming(expr.type()))
-    return true;
-
-  if(expr.id()==ID_symbol)
-  {
-    const auto &type = expr.type();
-    if(!expr.get_bool(ID_C_SSA_symbol))
-      return type.id() != ID_code && type.id() != ID_mathematical_function;
-    if(!to_ssa_expr(expr).get_level_2().empty())
-      return true;
-    if(to_ssa_expr(expr).get_original_expr().type() != type)
-      return true;
-  }
-  else
-  {
-    forall_operands(it, expr)
-      if(check_renaming_l1(*it))
-        return true;
-  }
-
-  return false;
-}
-
-static bool check_renaming(const exprt &expr)
-{
-  if(check_renaming(expr.type()))
-    return true;
-
-  if(
-    expr.id() == ID_address_of &&
-    to_address_of_expr(expr).object().id() == ID_symbol)
-  {
-    return check_renaming_l1(to_address_of_expr(expr).object());
-  }
-  else if(
-    expr.id() == ID_address_of &&
-    to_address_of_expr(expr).object().id() == ID_index)
-  {
-    const auto index_expr = to_index_expr(to_address_of_expr(expr).object());
-    return check_renaming_l1(index_expr.array()) ||
-           check_renaming(index_expr.index());
-  }
-  else if(expr.id()==ID_symbol)
-  {
-    const auto &type = expr.type();
-    if(!expr.get_bool(ID_C_SSA_symbol))
-      return type.id() != ID_code && type.id() != ID_mathematical_function;
-    if(to_ssa_expr(expr).get_level_2().empty())
-      return true;
-    if(to_ssa_expr(expr).get_original_expr().type() != type)
-      return true;
-  }
-  else
-  {
-    forall_operands(it, expr)
-      if(check_renaming(*it))
-        return true;
-  }
-
-  return false;
-}
-
 template <>
 renamedt<ssa_exprt, L0>
 goto_symex_statet::set_indices<L0>(ssa_exprt ssa_expr, const namespacet &ns)
@@ -344,6 +261,73 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
   }
 }
 
+exprt goto_symex_statet::l2_rename_rvalues(exprt lvalue, const namespacet &ns)
+{
+  rename(lvalue.type(), irep_idt(), ns);
+
+  if(lvalue.id() == ID_symbol)
+  {
+    // Nothing to do
+  }
+  else if(is_read_only_object(lvalue))
+  {
+    // Ignore apparent writes to 'NULL-object' and similar read-only objects
+  }
+  else if(lvalue.id() == ID_typecast)
+  {
+    auto &typecast_lvalue = to_typecast_expr(lvalue);
+    typecast_lvalue.op() = l2_rename_rvalues(typecast_lvalue.op(), ns);
+  }
+  else if(lvalue.id() == ID_member)
+  {
+    auto &member_lvalue = to_member_expr(lvalue);
+    member_lvalue.compound() = l2_rename_rvalues(member_lvalue.compound(), ns);
+  }
+  else if(lvalue.id() == ID_index)
+  {
+    // The index is an rvalue:
+    auto &index_lvalue = to_index_expr(lvalue);
+    index_lvalue.array() = l2_rename_rvalues(index_lvalue.array(), ns);
+    index_lvalue.index() = rename(index_lvalue.index(), ns).get();
+  }
+  else if(
+    lvalue.id() == ID_byte_extract_little_endian ||
+    lvalue.id() == ID_byte_extract_big_endian)
+  {
+    // The offset is an rvalue:
+    auto &byte_extract_lvalue = to_byte_extract_expr(lvalue);
+    byte_extract_lvalue.op() = l2_rename_rvalues(byte_extract_lvalue.op(), ns);
+    byte_extract_lvalue.offset() = rename(byte_extract_lvalue.offset(), ns);
+  }
+  else if(lvalue.id() == ID_if)
+  {
+    // The condition is an rvalue:
+    auto &if_lvalue = to_if_expr(lvalue);
+    if_lvalue.cond() = rename(if_lvalue.cond(), ns);
+    if(!if_lvalue.cond().is_false())
+      if_lvalue.true_case() = l2_rename_rvalues(if_lvalue.true_case(), ns);
+    if(!if_lvalue.cond().is_true())
+      if_lvalue.false_case() = l2_rename_rvalues(if_lvalue.false_case(), ns);
+  }
+  else if(lvalue.id() == ID_complex_real)
+  {
+    auto &complex_real_lvalue = to_complex_real_expr(lvalue);
+    complex_real_lvalue.op() = l2_rename_rvalues(complex_real_lvalue.op(), ns);
+  }
+  else if(lvalue.id() == ID_complex_imag)
+  {
+    auto &complex_imag_lvalue = to_complex_imag_expr(lvalue);
+    complex_imag_lvalue.op() = l2_rename_rvalues(complex_imag_lvalue.op(), ns);
+  }
+  else
+  {
+    throw unsupported_operation_exceptiont(
+      "l2_rename_rvalues case `" + lvalue.id_string() + "' not handled");
+  }
+
+  return lvalue;
+}
+
 template renamedt<exprt, L1>
 goto_symex_statet::rename<L1>(exprt expr, const namespacet &ns);
 

src/goto-symex/goto_symex_state.h

@@ -107,6 +107,8 @@ class goto_symex_statet final : public goto_statet
   template <levelt level = L2>
   void rename(typet &type, const irep_idt &l1_identifier, const namespacet &ns);
 
+  exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns);
+
   /// \return lhs renamed to level 2
   renamedt<ssa_exprt, L2> assignment(
     ssa_exprt lhs,    // L0/L1
@@ -239,6 +241,14 @@ class goto_symex_statet final : public goto_statet
     return fresh_l2_name_provider;
   }
 
+  /// Returns true if \p lvalue is a read-only object, such as the null object
+  static bool is_read_only_object(const exprt &lvalue)
+  {
+    return lvalue.id() == ID_string_constant || lvalue.id() == ID_null_object ||
+           lvalue.id() == "zero_string" || lvalue.id() == "is_zero_string" ||
+           lvalue.id() == "zero_string_length";
+  }
+
 private:
   std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider;
 

src/goto-symex/renaming_level.cpp

@@ -205,3 +205,83 @@ typet get_original_name(typet type)
   }
   return type;
 }
+
+bool check_renaming(const typet &type)
+{
+  if(type.id() == ID_array)
+    return check_renaming(to_array_type(type).size());
+  else if(type.id() == ID_struct || type.id() == ID_union)
+  {
+    for(const auto &c : to_struct_union_type(type).components())
+      if(check_renaming(c.type()))
+        return true;
+  }
+  else if(type.has_subtype())
+    return check_renaming(to_type_with_subtype(type).subtype());
+
+  return false;
+}
+
+bool check_renaming_l1(const exprt &expr)
+{
+  if(check_renaming(expr.type()))
+    return true;
+
+  if(expr.id() == ID_symbol)
+  {
+    const auto &type = expr.type();
+    if(!expr.get_bool(ID_C_SSA_symbol))
+      return type.id() != ID_code && type.id() != ID_mathematical_function;
+    if(!to_ssa_expr(expr).get_level_2().empty())
+      return true;
+    if(to_ssa_expr(expr).get_original_expr().type() != type)
+      return true;
+  }
+  else
+  {
+    forall_operands(it, expr)
+      if(check_renaming_l1(*it))
+        return true;
+  }
+
+  return false;
+}
+
+bool check_renaming(const exprt &expr)
+{
+  if(check_renaming(expr.type()))
+    return true;
+
+  if(
+    expr.id() == ID_address_of &&
+    to_address_of_expr(expr).object().id() == ID_symbol)
+  {
+    return check_renaming_l1(to_address_of_expr(expr).object());
+  }
+  else if(
+    expr.id() == ID_address_of &&
+    to_address_of_expr(expr).object().id() == ID_index)
+  {
+    const auto index_expr = to_index_expr(to_address_of_expr(expr).object());
+    return check_renaming_l1(index_expr.array()) ||
+           check_renaming(index_expr.index());
+  }
+  else if(expr.id() == ID_symbol)
+  {
+    const auto &type = expr.type();
+    if(!expr.get_bool(ID_C_SSA_symbol))
+      return type.id() != ID_code && type.id() != ID_mathematical_function;
+    if(to_ssa_expr(expr).get_level_2().empty())
+      return true;
+    if(to_ssa_expr(expr).get_original_expr().type() != type)
+      return true;
+  }
+  else
+  {
+    forall_operands(it, expr)
+      if(check_renaming(*it))
+        return true;
+  }
+
+  return false;
+}

src/goto-symex/renaming_level.h

@@ -103,4 +103,16 @@ exprt get_original_name(exprt expr);
 /// Undo all levels of renaming
 typet get_original_name(typet type);
 
+/// Check that \p expr is correctly renamed to level 2 and return true in case
+/// an error is detected.
+bool check_renaming(const exprt &expr);
+
+/// Check that \p expr is correctly renamed to level 1 and return true in case
+/// an error is detected.
+bool check_renaming_l1(const exprt &expr);
+
+/// Check that \p type is correctly renamed to level 2 and return true in case
+/// an error is detected.
+bool check_renaming(const typet &type);
+
 #endif // CPROVER_GOTO_SYMEX_RENAMING_LEVEL_H