Symex: rename LHS rvalue components and simplify before symex_assign_rec

This was already happening in most cases (e.g. symex_dereference would apply field-sensitivity
before symex_assign_rec was entered), but the case of a statically non-constant but dynamically
constant array index or byte-extract offset would only be handled *after* symex_assign_rec, leading
to an asymmetry in which operations were combined into the ssa_exprt and which ones accumulated in
the expr_skeletont.

With this change the LHS expression is maximally renamed and simplified before symex_assign_rec is
entered, which means that any field-sensitive symbols on the LHS are fully constructed as early as
possible, and expr_skeletont only accumulates those member, index and byte-extract operations which
*cannot* be associated with an ssa_exprt. This means there is no need to undo with-operations or
try to simplify byte-extract operations in goto_symext::assign_from_non_struct_symbol, as this has
been taken care of already, and the l2_full_lhs can be constructed from the expression skeleton
trivially.

Author: smowton

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/symex_assign.cpp

@@ -362,16 +362,7 @@ void symex_assignt::assign_non_struct_symbol(
         ns)
       .get();
 
-  // Note the following two calls are specifically required for
-  // field-sensitivity. For example, with-expressions, which may have just been
-  // introduced by assign_struct_member, are transformed into member
-  // expressions on the LHS. If we add an option to disable field-sensitivity
-  // in the future these should be omitted.
-  assignmentt assignment = rewrite_with_to_field_symbols<use_update()>(
-    state,
-    shift_indexed_access_to_lhs<use_update()>(
-      state, {lhs, full_lhs, std::move(l2_rhs)}, ns, symex_config.simplify_opt),
-    ns);
+  assignmentt assignment{lhs, full_lhs, l2_rhs};
 
   if(symex_config.simplify_opt)
     assignment.rhs = simplify_expr(std::move(assignment.rhs), ns);
@@ -387,8 +378,15 @@ void symex_assignt::assign_non_struct_symbol(
                              .get();
 
   state.record_events.push(false);
-  const exprt l2_full_lhs =
-    state.rename(assignment.original_lhs_skeleton.apply(l2_lhs), ns).get();
+  // Note any other symbols mentioned in the skeleton are rvalues -- for example
+  // array indices -- and were renamed to L2 at the start of
+  // goto_symext::symex_assign.
+  const exprt l2_full_lhs = assignment.original_lhs_skeleton.apply(l2_lhs);
+  if(symex_config.run_validation_checks)
+  {
+    INVARIANT(
+      !check_renaming(l2_full_lhs), "l2_full_lhs should be renamed to L2");
+  }
   state.record_events.pop();
 
   auto current_assignment_type =
@@ -552,23 +550,14 @@ void symex_assignt::assign_if(
   exprt::operandst &guard)
 {
   // we have (c?a:b)=e;
-  exprt renamed_guard = state.rename(lhs.cond(), ns).get();
-  if(symex_config.simplify_opt)
-    renamed_guard = simplify_expr(std::move(renamed_guard), ns);
 
-  if(!renamed_guard.is_false())
-  {
-    guard.push_back(renamed_guard);
-    assign_rec(lhs.true_case(), full_lhs, rhs, guard);
-    guard.pop_back();
-  }
+  guard.push_back(lhs.cond());
+  assign_rec(lhs.true_case(), full_lhs, rhs, guard);
+  guard.pop_back();
 
-  if(!renamed_guard.is_true())
-  {
-    guard.push_back(not_exprt(renamed_guard));
-    assign_rec(lhs.false_case(), full_lhs, rhs, guard);
-    guard.pop_back();
-  }
+  guard.push_back(not_exprt(lhs.cond()));
+  assign_rec(lhs.false_case(), full_lhs, rhs, guard);
+  guard.pop_back();
 }
 
 void symex_assignt::assign_byte_extract(

unit/goto-symex/symex_assign.cpp

@@ -219,33 +219,66 @@ SCENARIO(
                     symex_config,
                     target_equation}
         .assign_symbol(struct1_ssa, skeleton, rhs, guard);
-      THEN("An equation is added to the target")
+      THEN("Two equations are added to the target")
       {
-        REQUIRE(target_equation.SSA_steps.size() == 1);
-        SSA_stept step = target_equation.SSA_steps.back();
-        THEN("LHS is `struct1!0#2..field1`")
+        REQUIRE(target_equation.SSA_steps.size() == 2);
+        SSA_stept assign_step = target_equation.SSA_steps.front();
+        SSA_stept expand_step = target_equation.SSA_steps.back();
+        THEN("Assign step LHS is `struct1!0#1`")
         {
-          REQUIRE(step.ssa_lhs.get_identifier() == "struct1!0#1..field1");
+          REQUIRE(assign_step.ssa_lhs.get_identifier() == "struct1!0#1");
         }
-        THEN("Original full LHS is `struct1.field1`")
+        THEN("Assign step original full LHS is `struct1.field1`")
         {
           REQUIRE(
-            step.original_full_lhs ==
+            assign_step.original_full_lhs ==
             member_exprt{struct1_sym, "field1", int_type});
         }
-        THEN("SSA full LHS is `struct1!0#1..field1`")
+        THEN("Assign step SSA full LHS is `struct1!0#1`")
         {
           const auto as_symbol =
-            expr_try_dynamic_cast<symbol_exprt>(step.ssa_lhs);
+            expr_try_dynamic_cast<symbol_exprt>(assign_step.ssa_lhs);
           REQUIRE(as_symbol);
-          REQUIRE(as_symbol->get_identifier() == "struct1!0#1..field1");
+          REQUIRE(as_symbol->get_identifier() == "struct1!0#1");
+        }
+        THEN("Assign step RHS is { struct1!0#0..field1 } with field1 = 234")
+        {
+          ssa_exprt struct1_v0_field1{
+            member_exprt{struct1_sym, "field1", int_type}};
+          struct1_v0_field1.set_level_0(0);
+          struct1_v0_field1.set_level_2(0);
+          struct_exprt struct_expr(struct_type);
+          struct_expr.add_to_operands(struct1_v0_field1);
+          with_exprt struct1_v0_with_field_set = rhs;
+          struct1_v0_with_field_set.old() = struct_expr;
+          REQUIRE(assign_step.ssa_rhs == struct1_v0_with_field_set);
         }
-        THEN("RHS is 234")
+        THEN("Expand step LHS is `struct1!0#2..field1`")
         {
-          const auto as_constant =
-            expr_try_dynamic_cast<constant_exprt>(step.ssa_rhs);
-          REQUIRE(as_constant);
-          REQUIRE(numeric_cast_v<mp_integer>(*as_constant) == 234);
+          REQUIRE(
+            expand_step.ssa_lhs.get_identifier() == "struct1!0#2..field1");
+        }
+        THEN("Expand step original full LHS is `struct1.field1`")
+        {
+          REQUIRE(
+            expand_step.original_full_lhs ==
+            member_exprt{struct1_sym, "field1", int_type});
+        }
+        THEN("Expand step SSA full LHS is `struct1!0#2..field1`")
+        {
+          const auto as_symbol =
+            expr_try_dynamic_cast<symbol_exprt>(expand_step.ssa_lhs);
+          REQUIRE(as_symbol);
+          REQUIRE(as_symbol->get_identifier() == "struct1!0#2..field1");
+        }
+        THEN("Expand step RHS is struct1!0#1.field1")
+        {
+          ssa_exprt struct1_v1{struct1_sym};
+          struct1_v1.set_level_0(0);
+          struct1_v1.set_level_2(1);
+          REQUIRE(
+            expand_step.ssa_rhs ==
+            member_exprt{struct1_v1, "field1", int_type});
         }
       }
     }