Generate index expressions for deref(p + offset), where p points to an array in a struct

Currently if offset is unknown, value_set_dereference will resolve p + offset to [(o1, unknown), (o2, unknown), ...], ultimately leading to a byte-update operation that may touch any of o1, o2 etc and specifically knocks them both out of the constant propagator.

With this change if p is known to point to arrays or array-members of structs then we will produce an expression like (c1 ? array1[offset] : c2 ? someobj.array2[offset] : ...)

Field-sensitivity may then kick in and update only the array within someobj, rather than the whole struct (this is unsound, but mirrors our behaviour when an array-in-struct is directly referenced. We may want to make this behaviour optional if the user is intentionally searching for solutions involving out-of-bounds accesses)

Note this is quite similar to value_set_dereferencet::build_reference_to's behaviour when referring to an array (but not an array within a struct), which builds an index expression instead of a byte-extract op. We can't extend that code however as the (constant + nonconstant) form of the pointer being dereferenced is lost by then.

Fixes: #5397

Author: smowton

regression/cbmc/array-cell-sensitivity15/access.c

@@ -0,0 +1,16 @@
+struct st
+{
+  char c;
+  int n[4];
+};
+
+int main()
+{
+  unsigned i;
+  int k;
+  i %= 4;
+  struct st s;
+  int *p = s.n;
+  p[i] = k;
+  return 0;
+}

regression/cbmc/array-cell-sensitivity15/test.desc

@@ -0,0 +1,11 @@
+CORE paths-lifo-expected-failure
+access.c
+--program-only
+^EXIT=0$
+^SIGNAL=0$
+s!0@1#1\.\.n == \{ s!0@1#1\.\.n\[\[0\]\], s!0@1#1\.\.n\[\[1\]\], s!0@1#1\.\.n\[\[2\]\], s!0@1#1\.\.n\[\[3\]\] } WITH \[\(.*\)i!0@1#2:=k!0@1#1\]
+--
+byte_update
+--
+This tests applying field-sensitivity to a pointer to an array that is part of a struct. See cbmc issue #5397 and PR #5418 for more detail.
+Disabled for paths-lifo mode, which does not support --program-only.

regression/validate-trace-xml-schema/check.py

@@ -28,6 +28,7 @@
     # program-only instead of trace
     ['vla1', 'program-only.desc'],
     ['Quantifiers-simplify', 'simplify_not_forall.desc'],
+    ['array-cell-sensitivity15', 'test.desc'],
     # these test for invalid command line handling
     ['bad_option', 'test_multiple.desc'],
     ['bad_option', 'test.desc'],

src/pointer-analysis/value_set_dereference.cpp

@@ -99,6 +99,36 @@ static json_objectt value_set_dereference_stats_to_json(
   return json_result;
 }
 
+optionalt<exprt> value_set_dereferencet::try_add_offset_to_indices(
+  const exprt &expr,
+  const exprt &offset_elements)
+{
+  if(const auto *index_expr = expr_try_dynamic_cast<index_exprt>(expr))
+  {
+    return index_exprt{
+      index_expr->array(),
+      plus_exprt{index_expr->index(),
+                 typecast_exprt::conditional_cast(
+                   offset_elements, index_expr->index().type())}};
+  }
+  else if(const auto *if_expr = expr_try_dynamic_cast<if_exprt>(expr))
+  {
+    const auto true_case =
+      try_add_offset_to_indices(if_expr->true_case(), offset_elements);
+    if(!true_case)
+      return {};
+    const auto false_case =
+      try_add_offset_to_indices(if_expr->false_case(), offset_elements);
+    if(!false_case)
+      return {};
+    return if_exprt{if_expr->cond(), *true_case, *false_case};
+  }
+  else
+  {
+    return {};
+  }
+}
+
 exprt value_set_dereferencet::dereference(
   const exprt &pointer,
   bool display_points_to_sets)
@@ -140,6 +170,33 @@ exprt value_set_dereferencet::dereference(
           display_points_to_sets));
     }
   }
+  else if(pointer.id() == ID_plus && pointer.operands().size() == 2)
+  {
+    // Try to improve results for *(p + i) where p points to known offsets but
+    // i is non-constant-- if `p` points to known positions in arrays or array-members
+    // of structs then we can add the non-constant expression `i` to the index
+    // instead of using a byte-extract expression.
+
+    exprt pointer_expr = to_plus_expr(pointer).op0();
+    exprt offset_expr = to_plus_expr(pointer).op1();
+
+    if(can_cast_type<pointer_typet>(offset_expr.type()))
+      std::swap(pointer_expr, offset_expr);
+
+    if(
+      can_cast_type<pointer_typet>(pointer_expr.type()) &&
+      !can_cast_type<pointer_typet>(offset_expr.type()) &&
+      !can_cast_expr<constant_exprt>(offset_expr))
+    {
+      exprt derefd_pointer = dereference(pointer_expr);
+      if(
+        auto derefd_with_offset =
+          try_add_offset_to_indices(derefd_pointer, offset_expr))
+        return *derefd_with_offset;
+
+      // If any of this fails, fall through to use the normal byte-extract path.
+    }
+  }
 
   return handle_dereference_base_case(pointer, display_points_to_sets);
 }

src/pointer-analysis/value_set_dereference.h

@@ -59,6 +59,12 @@ class value_set_dereferencet final
   /// \param display_points_to_sets: Display size and contents of points to sets
   exprt dereference(const exprt &pointer, bool display_points_to_sets = false);
 
+  /// If `expr` is of the form (c1 ? e1[o1] : c2 ? e2[o2] : c3 ? ...)
+  /// then return `c1 ? e1[o1 + offset] : e2[o2 + offset] : c3 ? ...`
+  /// otherwise return an empty optionalt.
+  optionalt<exprt>
+  try_add_offset_to_indices(const exprt &expr, const exprt &offset);
+
   /// Return value for `build_reference_to`; see that method for documentation.
   class valuet
   {