Implement l2_rename_rvalues(lvalue)

This renames the rvalue components of an lvalue expression to L2, such as the index of an array
expression or the offset involved in byte-extract operation. Lvalue components (e.g. symbols) are
left alone.

Author: smowton

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>
@@ -260,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