Field-sensitive level-2 SSA renaming

Struct member and array index expressions are replaced by new SSA
symbols such that updates to individual fields of structs or arrays do
not affect the SSA index of the remaining object. This enables more
fine-grained constant propagation, which should be particularly
beneficial to Java (where structs/classes prevail).

jbmc/regression/jbmc-generics/constant_propagation/test.desc

@@ -3,8 +3,10 @@ Test.class
 --function Test.main --show-vcc
 ^EXIT=0$
 ^SIGNAL=0$
-^\{-\d+\} symex_dynamic::dynamic_object1#3 = \{ \{ \{ "java::GenericSub" \}, NULL, 0 \} \}$
-^\{-\d+\} symex_dynamic::dynamic_object1#4 = \{ \{ \{ "java::GenericSub" \}, NULL, 5 \} \}$
+^\{-\d+\} symex_dynamic::dynamic_object1#2 = \{ \{ \{ "java::GenericSub" \}, NULL, 0 \} \}$
+^\{-\d+\} symex_dynamic::dynamic_object1#2\.@Generic\.@java.lang.Object\.@class_identifier = "java::GenericSub"$
+^\{-\d+\} symex_dynamic::dynamic_object1#2\.@Generic\.key = NULL$
+^\{-\d+\} symex_dynamic::dynamic_object1#3\.@Generic\.x = 5$
 --
 byte_extract_(big|little)_endian
 --

jbmc/regression/jbmc-strings/ClassName/test.desc

@@ -4,5 +4,3 @@ test.class
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-\[java::test\.main:\(\)V\.assertion\.1\] line 5 assertion at file test\.java line 5 function java::test\.main:\(\)V bytecode-index 8: SUCCESS$
-\[java::test\.main:\(\)V\.assertion\.2\] line 6 assertion at file test\.java line 6 function java::test\.main:\(\)V bytecode-index 19: SUCCESS$

regression/cbmc-concurrency/norace_struct1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG pthread
+CORE pthread
 main.c
 
 ^EXIT=0$

regression/cbmc-concurrency/struct_and_array1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/Array_Propagation1/main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+
+struct S
+{
+  int a;
+};
+
+int main()
+{
+  struct S s;
+  s.a = 1;
+
+  assert(s.a == 1);
+
+  int A[1];
+  A[0] = 1;
+
+  assert(A[0] == 1);
+
+  return 0;
+}

regression/cbmc/Array_Propagation1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+(Starting CEGAR Loop|VCC\(s\), 0 remaining after simplification$)
+--
+^warning: ignoring

regression/cbmc/Struct_Propagation1/main.c

@@ -0,0 +1,34 @@
+struct S
+{
+  int v;
+  struct Inner
+  {
+    int x;
+  } inner;
+};
+
+struct S works;
+
+int main()
+{
+  struct S fails;
+
+  works.v = 2;
+  fails.v = 2;
+
+  while(works.v > 0)
+    --(works.v);
+
+  while(fails.v > 0)
+    --(fails.v);
+
+  __CPROVER_assert(works.inner.x == 0, "");
+
+  _Bool b;
+  if(b)
+  {
+    struct S s = {42, {42}};
+  }
+
+  return 0;
+}

regression/cbmc/Struct_Propagation1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--unwind 5
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+(Starting CEGAR Loop|VCC\(s\), 0 remaining after simplification$)
+--
+^warning: ignoring

regression/cbmc/variable-access-to-constant-array/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+THOROUGH broken-smt-backend
 main.c
 
 ^EXIT=10$
@@ -6,5 +6,10 @@ main.c
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
+--
 This test actually passes when using the SMT2 back-end, but takes 68 seconds to
 do so.
+
+Field-sensitive encoding of array accesses for an array of 2^16 elements is very
+expensive. We might consider some bounds up to which we actually do field
+expansion.

regression/goto-harness/nondet_elements_longer_lists/test.desc

@@ -1,8 +1,6 @@
 CORE
 main.c
 --harness-type call-function --max-nondet-tree-depth 4 --min-null-tree-depth 1 --function test_function
-\[test_function.unwind.\d+\] line \d+ unwinding assertion loop 0: SUCCESS
-\[test_function.unwind.\d+\] line \d+ unwinding assertion loop 1: SUCCESS
 \[test_function.assertion.\d+\] line \d+ assertion list_walker->datum == \+\+i: SUCCESS
 ^EXIT=0$
 ^SIGNAL=0$

regression/goto-harness/nondet_elements_longer_lists_global/test.desc

@@ -1,8 +1,6 @@
 CORE
 main.c
 --harness-type call-function --max-nondet-tree-depth 4 --min-null-tree-depth 1 --function test_function --nondet-globals
-\[test_function.unwind.\d+\] line \d+ unwinding assertion loop 0: SUCCESS
-\[test_function.unwind.\d+\] line \d+ unwinding assertion loop 1: SUCCESS
 \[test_function.assertion.\d+\] line \d+ assertion list_walker->datum == \+\+i: SUCCESS
 ^EXIT=0$
 ^SIGNAL=0$

src/goto-symex/Makefile

@@ -1,5 +1,6 @@
 SRC = auto_objects.cpp \
       build_goto_trace.cpp \
+      field_sensitivity.cpp \
       goto_state.cpp \
       goto_symex.cpp \
       goto_symex_state.cpp \

src/goto-symex/field_sensitivity.cpp

@@ -0,0 +1,255 @@
+/*******************************************************************\
+
+Module: Field-sensitive SSA
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#include "field_sensitivity.h"
+
+#include <util/arith_tools.h>
+#include <util/c_types.h>
+#include <util/simplify_expr.h>
+#include <util/std_expr.h>
+
+#include "goto_symex_state.h"
+#include "symex_target.h"
+
+void field_sensitivityt::apply(const namespacet &ns, exprt &expr, bool write)
+  const
+{
+  if(!run_apply)
+    return;
+
+  if(expr.id() != ID_address_of)
+  {
+    Forall_operands(it, expr)
+      apply(ns, *it, write);
+  }
+
+  if(expr.id() == ID_symbol && expr.get_bool(ID_C_SSA_symbol) && !write)
+  {
+    expr = get_fields(ns, to_ssa_expr(expr));
+  }
+  else if(
+    !write && expr.id() == ID_member &&
+    to_member_expr(expr).struct_op().id() == ID_struct)
+  {
+    simplify(expr, ns);
+  }
+  else if(
+    !write && expr.id() == ID_index &&
+    to_index_expr(expr).array().id() == ID_array)
+  {
+    simplify(expr, ns);
+  }
+  else if(expr.id() == ID_member)
+  {
+    // turn a member-of-an-SSA-expression into a single SSA expression, thus
+    // encoding the member as an individual symbol rather than only the full
+    // struct
+    member_exprt &member = to_member_expr(expr);
+
+    if(
+      member.struct_op().id() == ID_symbol &&
+      member.struct_op().get_bool(ID_C_SSA_symbol) &&
+      (member.struct_op().type().id() == ID_struct ||
+       member.struct_op().type().id() == ID_struct_tag))
+    {
+      // place the entire member expression, not just the struct operand, in an
+      // SSA expression
+      ssa_exprt tmp = to_ssa_expr(member.struct_op());
+      member.struct_op() = tmp.get_original_expr();
+      tmp.set_expression(member);
+
+      expr.swap(tmp);
+    }
+  }
+  else if(expr.id() == ID_index)
+  {
+    // turn a index-of-an-SSA-expression into a single SSA expression, thus
+    // encoding the index access into an array as an individual symbol rather
+    // than only the full array
+    index_exprt &index = to_index_expr(expr);
+    simplify(index.index(), ns);
+
+    if(
+      index.array().id() == ID_symbol &&
+      index.array().get_bool(ID_C_SSA_symbol) &&
+      index.array().type().id() == ID_array &&
+      index.index().id() == ID_constant)
+    {
+      // place the entire index expression, not just the array operand, in an
+      // SSA expression
+      ssa_exprt tmp = to_ssa_expr(index.array());
+      index.array() = tmp.get_original_expr();
+      tmp.set_expression(index);
+
+      expr.swap(tmp);
+    }
+  }
+}
+
+exprt field_sensitivityt::get_fields(
+  const namespacet &ns,
+  const ssa_exprt &ssa_expr)
+{
+  if(ssa_expr.type().id() == ID_struct || ssa_expr.type().id() == ID_struct_tag)
+  {
+    const struct_typet &type = to_struct_type(ns.follow(ssa_expr.type()));
+    const struct_union_typet::componentst &components = type.components();
+
+    struct_exprt result(ssa_expr.type());
+    result.reserve_operands(components.size());
+
+    const exprt &struct_op = ssa_expr.get_original_expr();
+
+    for(const auto &comp : components)
+    {
+      const member_exprt member(struct_op, comp.get_name(), comp.type());
+      ssa_exprt tmp = ssa_expr;
+      tmp.set_expression(member);
+      result.copy_to_operands(get_fields(ns, tmp));
+    }
+
+    return std::move(result);
+  }
+  else if(
+    ssa_expr.type().id() == ID_array &&
+    to_array_type(ssa_expr.type()).size().id() == ID_constant)
+  {
+    const array_typet &type = to_array_type(ssa_expr.type());
+    const std::size_t array_size =
+      numeric_cast_v<std::size_t>(to_constant_expr(type.size()));
+
+    array_exprt result(type);
+    result.reserve_operands(array_size);
+
+    const exprt &array = ssa_expr.get_original_expr();
+
+    for(std::size_t i = 0; i < array_size; ++i)
+    {
+      const index_exprt index(array, from_integer(i, index_type()));
+      ssa_exprt tmp = ssa_expr;
+      tmp.set_expression(index);
+      result.copy_to_operands(get_fields(ns, tmp));
+    }
+
+    return std::move(result);
+  }
+  else
+    return ssa_expr;
+}
+
+void field_sensitivityt::field_assignments(
+  const namespacet &ns,
+  goto_symex_statet &state,
+  const exprt &lhs,
+  symex_targett &target)
+{
+  exprt lhs_fs = lhs;
+  apply(ns, lhs_fs, false);
+
+  bool run_apply_bak = run_apply;
+  run_apply = false;
+  field_assignments_rec(ns, state, lhs_fs, lhs, target);
+  run_apply = run_apply_bak;
+}
+
+/// Assign to the individual fields \p lhs_fs of a non-expanded symbol \p lhs.
+/// This is required whenever prior steps have updated the full object rather
+/// than individual fields, e.g., in case of assignments to an array at an
+/// unknown index.
+/// \param ns: a namespace to resolve type symbols/tag types
+/// \param state: symbolic execution state
+/// \param lhs_fs: expanded symbol
+/// \param lhs: non-expanded symbol
+/// \param target: symbolic execution equation store
+void field_sensitivityt::field_assignments_rec(
+  const namespacet &ns,
+  goto_symex_statet &state,
+  const exprt &lhs_fs,
+  const exprt &lhs,
+  symex_targett &target)
+{
+  if(lhs == lhs_fs)
+    return;
+  else if(lhs_fs.id() == ID_symbol && lhs_fs.get_bool(ID_C_SSA_symbol))
+  {
+    exprt ssa_rhs = state.rename(lhs, ns).get();
+    simplify(ssa_rhs, ns);
+
+    ssa_exprt ssa_lhs = to_ssa_expr(lhs_fs);
+    state.assignment(ssa_lhs, ssa_rhs, ns, true, true);
+
+    // do the assignment
+    target.assignment(
+      state.guard.as_expr(),
+      ssa_lhs,
+      ssa_lhs,
+      ssa_lhs.get_original_expr(),
+      ssa_rhs,
+      state.source,
+      symex_targett::assignment_typet::STATE);
+  }
+  else if(lhs.type().id() == ID_struct || lhs.type().id() == ID_struct_tag)
+  {
+    const struct_typet &type = to_struct_type(ns.follow(lhs.type()));
+    const struct_union_typet::componentst &components = type.components();
+
+    PRECONDITION(
+      components.empty() ||
+      (lhs_fs.has_operands() && lhs_fs.operands().size() == components.size()));
+
+    exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
+    for(const auto &comp : components)
+    {
+      const member_exprt member_rhs(lhs, comp.get_name(), comp.type());
+      const exprt &member_lhs = *fs_it;
+
+      field_assignments_rec(ns, state, member_lhs, member_rhs, target);
+      ++fs_it;
+    }
+  }
+  else if(const auto &type = type_try_dynamic_cast<array_typet>(lhs.type()))
+  {
+    const std::size_t array_size =
+      numeric_cast_v<std::size_t>(to_constant_expr(type->size()));
+    PRECONDITION(
+      lhs_fs.has_operands() && lhs_fs.operands().size() == array_size);
+
+    exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
+    for(std::size_t i = 0; i < array_size; ++i)
+    {
+      const index_exprt index_rhs(lhs, from_integer(i, index_type()));
+      const exprt &index_lhs = *fs_it;
+
+      field_assignments_rec(ns, state, index_lhs, index_rhs, target);
+      ++fs_it;
+    }
+  }
+  else if(lhs_fs.has_operands())
+  {
+    PRECONDITION(
+      lhs.has_operands() && lhs_fs.operands().size() == lhs.operands().size());
+
+    exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
+    for(const exprt &op : lhs.operands())
+    {
+      field_assignments_rec(ns, state, *fs_it, op, target);
+      ++fs_it;
+    }
+  }
+  else
+  {
+    UNREACHABLE;
+  }
+}
+
+bool field_sensitivityt::is_divisible(
+  const namespacet &ns,
+  const ssa_exprt &expr)
+{
+  return expr != get_fields(ns, expr);
+}

src/goto-symex/field_sensitivity.h

@@ -0,0 +1,81 @@
+/*******************************************************************\
+
+Module: Field-sensitive SSA
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
+#define CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
+
+class exprt;
+class ssa_exprt;
+class namespacet;
+class goto_symex_statet;
+class symex_targett;
+
+/// \brief Control granularity of object accesses
+class field_sensitivityt
+{
+public:
+  /// Assign to the individual fields of a non-expanded symbol \p lhs. This is
+  /// required whenever prior steps have updated the full object rather than
+  /// individual fields, e.g., in case of assignments to an array at an unknown
+  /// index.
+  /// \param ns: a namespace to resolve type symbols/tag types
+  /// \param state: symbolic execution state
+  /// \param lhs: non-expanded symbol
+  /// \param target: symbolic execution equation store
+  void field_assignments(
+    const namespacet &ns,
+    goto_symex_statet &state,
+    const exprt &lhs,
+    symex_targett &target);
+
+  /// Turn an expression \p expr into a field-sensitive SSA expression.
+  /// Field-sensitive SSA expressions have individual symbols for each
+  /// component. While the exact granularity is an implementation detail,
+  /// possible implementations translate a struct-typed symbol into a struct of
+  /// member expressions, or an array-typed symbol into an array of index
+  /// expressions. Such expansions are not possible when the symbol is to be
+  /// written to (i.e., \p write is true); in such a case only translations from
+  /// existing member or index expressions into symbols are performed.
+  /// \param ns: a namespace to resolve type symbols/tag types
+  /// \param [in,out] expr: an expression to be (recursively) transformed - this
+  ///   parameter is both input and output.
+  /// \param write: set to true if the expression is to be used as an lvalue.
+  void apply(const namespacet &ns, exprt &expr, bool write) const;
+
+  /// Compute an expression representing the individual components of a
+  /// field-sensitive SSA representation of \p ssa_expr.
+  /// \param ns: a namespace to resolve type symbols/tag types
+  /// \param ssa_expr: the expression to evaluate
+  /// \return Expanded expression; for example, for a \p ssa_expr of some struct
+  ///   type, a `struct_exprt` with each component now being an SSA expression
+  ///   is built.
+  static exprt get_fields(const namespacet &ns, const ssa_exprt &ssa_expr);
+
+  /// Determine whether \p expr would translate to an atomic SSA expression
+  /// (returns false) or a composite object made of several SSA expressions as
+  /// components (such as a struct with each member becoming an individual SSA
+  /// expression, return true in this case).
+  /// \param ns: a namespace to resolve type symbols/tag types
+  /// \param expr: the expression to evaluate
+  /// \return False, if and only if, \p expr would be a single field-sensitive
+  /// SSA expression.
+  static bool is_divisible(const namespacet &ns, const ssa_exprt &expr);
+
+private:
+  /// whether or not to invoke \ref field_sensitivityt::apply
+  bool run_apply = true;
+
+  void field_assignments_rec(
+    const namespacet &ns,
+    goto_symex_statet &state,
+    const exprt &lhs_fs,
+    const exprt &lhs,
+    symex_targett &target);
+};
+
+#endif // CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H

src/goto-symex/goto_symex_state.cpp

@@ -334,6 +334,10 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
           c_expr.type() == to_if_expr(c_expr).false_case().type())),
       "Type of renamed expr should be the same as operands for with_exprt and "
       "if_exprt");
+
+    if(level == L2)
+      field_sensitivity.apply(ns, expr, false);
+
     return renamedt<exprt, level>{std::move(expr)};
   }
 }
@@ -360,6 +364,10 @@ bool goto_symex_statet::l2_thread_read_encoding(
     return false;
   }
 
+  // only continue if an indivisible object is being accessed
+  if(field_sensitivityt::is_divisible(ns, expr))
+    return false;
+
   ssa_exprt ssa_l1=expr;
   ssa_l1.remove_level_2();
   const irep_idt &l1_identifier=ssa_l1.get_identifier();
@@ -485,6 +493,10 @@ goto_symex_statet::write_is_shared_resultt goto_symex_statet::write_is_shared(
     return write_is_shared_resultt::NOT_SHARED;
   }
 
+  // only continue if an indivisible object is being accessed
+  if(field_sensitivityt::is_divisible(ns, expr))
+    return write_is_shared_resultt::NOT_SHARED;
+
   if(atomic_section_id != 0)
     return write_is_shared_resultt::IN_ATOMIC_SECTION;
 

src/goto-symex/goto_symex_state.h

@@ -25,6 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/goto_function.h>
 
 #include "call_stack.h"
+#include "field_sensitivity.h"
 #include "frame.h"
 #include "goto_state.h"
 #include "renaming_level.h"
@@ -115,6 +116,8 @@ public:
     bool record_value,
     bool allow_pointer_unsoundness=false);
 
+  field_sensitivityt field_sensitivity;
+
 protected:
   template <levelt>
   void rename_address(exprt &expr, const namespacet &ns);

src/goto-symex/symex_assign.cpp

@@ -16,9 +16,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/cprover_prefix.h>
 #include <util/exception_utils.h>
 #include <util/pointer_offset_size.h>
+#include <util/simplify_expr.h>
 
 #include "goto_symex_state.h"
 
+// We can either use with_exprt or update_exprt when building expressions that
+// modify components of an array or a struct. Set USE_UPDATE to use
+// update_exprt.
 // #define USE_UPDATE
 
 void goto_symext::symex_assign(statet &state, const code_assignt &code)
@@ -198,6 +202,167 @@ void goto_symext::symex_assign_rec(
       "assignment to `" + lhs.id_string() + "' not handled");
 }
 
+/// Replace "with" (or "update") expressions in \p ssa_rhs by their update
+/// values and move the index or member to the left-hand side \p lhs_mod. This
+/// effectively undoes the work that \ref goto_symext::symex_assign_array and
+/// \ref goto_symext::symex_assign_struct_member have done, but now making use
+/// of the index/member that may only be known after renaming to L2 has taken
+/// place.
+/// \param [in,out] ssa_rhs: right-hand side
+/// \param [in,out] lhs_mod: left-hand side
+/// \param ns: namespace
+/// \param field_sensitivity: field sensitivity object to turn left-hand side
+///   into individual fields
+static void rewrite_with_to_field_symbols(
+  exprt &ssa_rhs,
+  ssa_exprt &lhs_mod,
+  const namespacet &ns,
+  const field_sensitivityt &field_sensitivity)
+{
+#ifdef USE_UPDATE
+  while(ssa_rhs.id() == ID_update &&
+        to_update_expr(ssa_rhs).designator().size() == 1 &&
+        (lhs_mod.type().id() == ID_array || lhs_mod.type().id() == ID_struct ||
+         lhs_mod.type().id() == ID_struct_tag))
+  {
+    exprt field_sensitive_lhs;
+    const update_exprt &update = to_update_expr(ssa_rhs);
+    PRECONDITION(update.designator().size() == 1);
+    const exprt &designator = update.designator().front();
+
+    if(lhs_mod.type().id() == ID_array)
+    {
+      field_sensitive_lhs =
+        index_exprt(lhs_mod, to_index_designator(designator).index());
+    }
+    else
+    {
+      field_sensitive_lhs = member_exprt(
+        lhs_mod,
+        to_member_designator(designator).get_component_name(),
+        update.new_value().type());
+    }
+
+    field_sensitivity.apply(field_sensitive_lhs, true);
+
+    if(field_sensitive_lhs.id() != ID_symbol)
+      break;
+
+    ssa_rhs = update.new_value();
+    lhs_mod = to_ssa_expr(field_sensitive_lhs);
+  }
+#else
+  while(ssa_rhs.id() == ID_with &&
+        to_with_expr(ssa_rhs).operands().size() == 3 &&
+        (lhs_mod.type().id() == ID_array || lhs_mod.type().id() == ID_struct ||
+         lhs_mod.type().id() == ID_struct_tag))
+  {
+    exprt field_sensitive_lhs;
+    const with_exprt &with_expr = to_with_expr(ssa_rhs);
+
+    if(lhs_mod.type().id() == ID_array)
+    {
+      field_sensitive_lhs = index_exprt(lhs_mod, with_expr.where());
+    }
+    else
+    {
+      field_sensitive_lhs = member_exprt(
+        lhs_mod,
+        with_expr.where().get(ID_component_name),
+        with_expr.new_value().type());
+    }
+
+    field_sensitivity.apply(ns, field_sensitive_lhs, true);
+
+    if(field_sensitive_lhs.id() != ID_symbol)
+      break;
+
+    ssa_rhs = with_expr.new_value();
+    lhs_mod = to_ssa_expr(field_sensitive_lhs);
+  }
+#endif
+}
+
+/// Replace byte-update operations that only affect individual fields of an
+/// expression by assignments to just those fields. May generate "with" (or
+/// "update") expressions, which \ref rewrite_with_to_field_symbols will then
+/// take care of.
+/// \param [in,out] ssa_rhs: right-hand side
+/// \param [in,out] lhs_mod: left-hand side
+/// \param ns: namespace
+/// \param do_simplify: set to true if, and only if, simplification is enabled
+static void shift_indexed_access_to_lhs(
+  exprt &ssa_rhs,
+  ssa_exprt &lhs_mod,
+  const namespacet &ns,
+  const field_sensitivityt &field_sensitivity,
+  bool do_simplify)
+{
+  if(
+    ssa_rhs.id() == ID_byte_update_little_endian ||
+    ssa_rhs.id() == ID_byte_update_big_endian)
+  {
+    byte_update_exprt &byte_update = to_byte_update_expr(ssa_rhs);
+    exprt byte_extract = byte_extract_exprt(
+      byte_update.id() == ID_byte_update_big_endian
+        ? ID_byte_extract_big_endian
+        : ID_byte_extract_little_endian,
+      lhs_mod,
+      byte_update.offset(),
+      byte_update.value().type());
+    if(do_simplify)
+      simplify(byte_extract, ns);
+
+    if(byte_extract.id() == ID_symbol)
+    {
+      ssa_rhs = byte_update.value();
+      lhs_mod = to_ssa_expr(byte_extract);
+    }
+    else if(byte_extract.id() == ID_index || byte_extract.id() == ID_member)
+    {
+      ssa_rhs = byte_update.value();
+
+      while(byte_extract.id() == ID_index || byte_extract.id() == ID_member)
+      {
+        if(byte_extract.id() == ID_index)
+        {
+          index_exprt &idx = to_index_expr(byte_extract);
+
+#ifdef USE_UPDATE
+          update_exprt new_rhs{idx.array(), exprt{}, ssa_rhs};
+          new_rhs.designator().push_back(index_designatort{idx.index()});
+#else
+          with_exprt new_rhs{idx.array(), idx.index(), ssa_rhs};
+#endif
+
+          ssa_rhs = new_rhs;
+          byte_extract = idx.array();
+        }
+        else
+        {
+          member_exprt &member = to_member_expr(byte_extract);
+          const irep_idt &component_name = member.get_component_name();
+
+#ifdef USE_UPDATE
+          update_exprt new_rhs{member.compound(), exprt{}, ssa_rhs};
+          new_rhs.designator().push_back(member_designatort{component_name});
+#else
+          with_exprt new_rhs(member.compound(), exprt(ID_member_name), ssa_rhs);
+          new_rhs.where().set(ID_component_name, component_name);
+#endif
+
+          ssa_rhs = new_rhs;
+          byte_extract = member.compound();
+        }
+      }
+
+      lhs_mod = to_ssa_expr(byte_extract);
+    }
+  }
+
+  rewrite_with_to_field_symbols(ssa_rhs, lhs_mod, ns, field_sensitivity);
+}
+
 void goto_symext::symex_assign_symbol(
   statet &state,
   const ssa_exprt &lhs, // L1
@@ -216,9 +381,15 @@ void goto_symext::symex_assign_symbol(
   }
 
   exprt l2_rhs = state.rename(std::move(ssa_rhs), ns).get();
+
+  ssa_exprt lhs_mod = lhs;
+
+  shift_indexed_access_to_lhs(
+    l2_rhs, lhs_mod, ns, state.field_sensitivity, symex_config.simplify_opt);
+
   do_simplify(l2_rhs);
 
-  ssa_exprt ssa_lhs=lhs;
+  ssa_exprt ssa_lhs = lhs_mod;
   state.assignment(
     ssa_lhs,
     l2_rhs,
@@ -235,8 +406,7 @@ void goto_symext::symex_assign_symbol(
   state.record_events=record_events;
 
   // do the assignment
-  const symbolt &symbol =
-    ns.lookup(to_symbol_expr(ssa_lhs.get_original_expr()));
+  const symbolt &symbol = ns.lookup(ssa_lhs.get_object_name());
 
   if(symbol.is_auxiliary)
     assignment_type=symex_targett::assignment_typet::HIDDEN;
@@ -254,15 +424,19 @@ void goto_symext::symex_assign_symbol(
   // Temporarily add the state guard
   guard.emplace_back(state.guard.as_expr());
 
+  exprt original_lhs = l2_full_lhs;
+  get_original_name(original_lhs);
   target.assignment(
     conjunction(guard),
     ssa_lhs,
     l2_full_lhs,
-    add_to_lhs(full_lhs, ssa_lhs.get_original_expr()),
+    original_lhs,
     l2_rhs,
     state.source,
     assignment_type);
 
+  state.field_sensitivity.field_assignments(ns, state, lhs_mod, target);
+
   // Restore the guard
   guard.pop_back();
 }

src/goto-symex/symex_dead.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_symex.h"
 
+#include <util/find_symbols.h>
 #include <util/std_expr.h>
 
 #include <pointer-analysis/add_failed_symbols.h>
@@ -22,23 +23,25 @@ void goto_symext::symex_dead(statet &state)
   const code_deadt &code = instruction.get_dead();
 
   ssa_exprt ssa = state.rename_ssa<L1>(ssa_exprt{code.symbol()}, ns).get();
-  const irep_idt &l1_identifier = ssa.get_identifier();
 
-  // we cannot remove the object from the L1 renaming map, because L1 renaming
-  // information is not local to a path, but removing it from the propagation
-  // map and value-set is safe as 1) it is local to a path and 2) this instance
-  // can no longer appear
+  const exprt fields = field_sensitivityt::get_fields(ns, ssa);
+  find_symbols_sett fields_set;
+  find_symbols(fields, fields_set);
 
-  if(state.value_set.values.has_key(l1_identifier))
+  for(const irep_idt &l1_identifier : fields_set)
   {
-    state.value_set.values.erase(l1_identifier);
+    // We cannot remove the object from the L1 renaming map, because L1 renaming
+    // information is not local to a path, but removing it from the propagation
+    // map and value-set is safe as 1) it is local to a path and 2) this
+    // instance can no longer appear.
+    if(state.value_set.values.has_key(l1_identifier))
+      state.value_set.values.erase(l1_identifier);
+    state.propagation.erase(l1_identifier);
+    // Remove from the local L2 renaming map; this means any reads from the dead
+    // identifier will use generation 0 (e.g. x!N@M#0, where N and M are
+    // positive integers), which is never defined by any write, and will be
+    // dropped by `goto_symext::merge_goto` on merging with branches where the
+    // identifier is still live.
+    state.drop_l1_name(l1_identifier);
   }
-
-  state.propagation.erase(l1_identifier);
-  // Remove from the local L2 renaming map; this means any reads from the dead
-  // identifier will use generation 0 (e.g. x!N@M#0, where N and M are positive
-  // integers), which is never defined by any write, and will be dropped by
-  // `goto_symext::merge_goto` on merging with branches where the identifier
-  // is still live.
-  state.drop_l1_name(l1_identifier);
 }

src/goto-symex/symex_dereference.cpp

@@ -356,6 +356,7 @@ void goto_symext::dereference(exprt &expr, statet &state, bool write)
   // symbols whose address is taken.
   PRECONDITION(!state.call_stack().empty());
   exprt l1_expr = state.rename<L1>(expr, ns).get();
+  state.field_sensitivity.apply(ns, l1_expr, write);
 
   // start the recursion!
   dereference_rec(l1_expr, state, write);
@@ -388,4 +389,6 @@ void goto_symext::dereference(exprt &expr, statet &state, bool write)
       !has_subexpr(expr, ID_dereference),
       "simplify re-introduced dereferencing");
   }
+
+  state.field_sensitivity.apply(ns, expr, write);
 }

src/goto-symex/symex_goto.cpp

@@ -493,6 +493,10 @@ static void merge_names(
     return;
   }
 
+  // field sensitivity: only merge on individual fields
+  if(field_sensitivityt::is_divisible(ns, ssa))
+    return;
+
   // shared variables are renamed on every access anyway, we don't need to
   // merge anything
   const symbolt &symbol = ns.lookup(obj_identifier);

src/util/ssa_expr.h

@@ -35,6 +35,16 @@ public:
     return static_cast<const exprt &>(find(ID_expression));
   }
 
+  /// Replace the underlying, original expression by \p expr while maintaining
+  /// SSA indices.
+  /// \param expr: expression to store
+  void set_expression(const exprt &expr)
+  {
+    type() = expr.type();
+    add(ID_expression, expr);
+    update_identifier();
+  }
+
   irep_idt get_object_name() const
   {
     const exprt &original_expr = get_original_expr();