Simplify multiple-of-element size access to arrays

Array operations may fall back to byte_extract or byte_update
expressions in parts of the code base. Simplify this to index or WITH
expressions, respectively, when the offset is known to be a multiple of
the array-element size, or a constant offset plus a multiple of the
array-element size.

Fixes: #8617

Author: tautschnig

regression/cbmc/Array_operations4/main.c

@@ -0,0 +1,14 @@
+int main()
+{
+  char source[8];
+  int int_source[2];
+  int target[4];
+  int n;
+  if(n >= 0 && n < 3)
+  {
+    __CPROVER_array_replace(&target[n], source);
+    __CPROVER_array_replace(&target[n], int_source);
+    __CPROVER_assert(target[n] == int_source[0], "");
+    __CPROVER_assert(target[n + 1] == int_source[1], "");
+  }
+}

regression/cbmc/Array_operations4/program-only.desc

@@ -0,0 +1,13 @@
+CORE paths-lifo-expected-failure
+main.c
+--program-only
+target!0@1#2 ==
+target!0@1#3 ==
+^EXIT=0$
+^SIGNAL=0$
+--
+byte_update_
+--
+This test demonstrates that we can simplify byte_update expressions to, e.g.,
+WITH expressions.
+Disabled for paths-lifo mode, which does not support --program-only.

regression/cbmc/Array_operations4/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/cbmc/havoc_slice/functional_assign.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 functional.c
 -DN=4 -DASSIGN --program-only
 ^EXIT=0$

regression/cbmc/havoc_slice/functional_slice_bytes.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 functional.c
 -DN=4 -DSLICE_BYTES --program-only
 ^EXIT=0$

regression/cbmc/havoc_slice/functional_slice_typed.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 functional.c
 -DN=4 -DSLICE_TYPED --program-only
 ^EXIT=0$

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

@@ -35,6 +35,7 @@
     ['show_properties1', 'test.desc'],
     # program-only instead of trace
     ['vla1', 'program-only.desc'],
+    ['Array_operations4', 'program-only.desc'],
     ['Pointer_Arithmetic19', 'test.desc'],
     ['Quantifiers-simplify', 'simplify_not_forall.desc'],
     ['array-cell-sensitivity15', 'test.desc'],

src/util/pointer_offset_size.cpp

@@ -687,7 +687,143 @@ std::optional<exprt> get_subexpression_at_offset(
   const auto offset_bytes = numeric_cast<mp_integer>(offset);
 
   if(!offset_bytes.has_value())
-    return {};
+  {
+    // offset is not a constant; try to see whether it is a multiple of a
+    // constant, or a sum that involves a multiple of a constant
+    if(auto array_type = type_try_dynamic_cast<array_typet>(expr.type()))
+    {
+      const auto target_size_bits = pointer_offset_bits(target_type, ns);
+      const auto elem_size_bits =
+        pointer_offset_bits(array_type->element_type(), ns);
+
+      // no arrays of zero-, or unknown-sized elements, or ones where elements
+      // have a bit-width that isn't a multiple of bytes
+      if(
+        !target_size_bits.has_value() || !elem_size_bits.has_value() ||
+        *elem_size_bits <= 0 ||
+        *elem_size_bits % config.ansi_c.char_width != 0 ||
+        *target_size_bits != *elem_size_bits)
+      {
+        return {};
+      }
+
+      // if we have an offset C + x (where C is a constant) we can try to
+      // recurse by first looking at the member at offset C
+      if(
+        offset.id() == ID_plus && offset.operands().size() == 2 &&
+        (to_multi_ary_expr(offset).op0().is_constant() ||
+         to_multi_ary_expr(offset).op1().is_constant()))
+      {
+        const plus_exprt &offset_plus = to_plus_expr(offset);
+        const auto &const_factor = numeric_cast_v<mp_integer>(to_constant_expr(
+          offset_plus.op0().is_constant() ? offset_plus.op0()
+                                          : offset_plus.op1()));
+        const exprt &other_factor = offset_plus.op0().is_constant()
+                                      ? offset_plus.op1()
+                                      : offset_plus.op0();
+
+        auto expr_at_offset_C =
+          get_subexpression_at_offset(expr, const_factor, target_type, ns);
+
+        if(
+          expr_at_offset_C.has_value() && expr_at_offset_C->id() == ID_index &&
+          to_index_expr(*expr_at_offset_C).index().is_zero())
+        {
+          return get_subexpression_at_offset(
+            to_index_expr(*expr_at_offset_C).array(),
+            other_factor,
+            target_type,
+            ns);
+        }
+      }
+
+      // give up if the offset expression isn't of the form K * i or i * K
+      // (where K is a constant)
+      if(
+        offset.id() != ID_mult || offset.operands().size() != 2 ||
+        (!to_multi_ary_expr(offset).op0().is_constant() &&
+         !to_multi_ary_expr(offset).op1().is_constant()))
+      {
+        return {};
+      }
+
+      const mult_exprt &offset_mult = to_mult_expr(offset);
+      const auto &const_factor = numeric_cast_v<mp_integer>(to_constant_expr(
+        offset_mult.op0().is_constant() ? offset_mult.op0()
+                                        : offset_mult.op1()));
+      const exprt &other_factor =
+        offset_mult.op0().is_constant() ? offset_mult.op1() : offset_mult.op0();
+
+      if(const_factor % (*elem_size_bits / config.ansi_c.char_width) != 0)
+        return {};
+
+      exprt index = mult_exprt{
+        other_factor,
+        from_integer(
+          const_factor / (*elem_size_bits / config.ansi_c.char_width),
+          other_factor.type())};
+
+      return get_subexpression_at_offset(
+        index_exprt{
+          expr,
+          typecast_exprt::conditional_cast(index, array_type->index_type())},
+        0,
+        target_type,
+        ns);
+    }
+    else if(
+      auto struct_tag_type =
+        type_try_dynamic_cast<struct_tag_typet>(expr.type()))
+    {
+      // If the offset expression is of the form K * i or i * K (where K is a
+      // constant) and the first component of the struct is an array we will
+      // recurse on that member.
+      const auto &components = ns.follow_tag(*struct_tag_type).components();
+      if(
+        !components.empty() &&
+        can_cast_type<array_typet>(components.front().type()) &&
+        offset.id() == ID_mult && offset.operands().size() == 2 &&
+        (to_multi_ary_expr(offset).op0().is_constant() ||
+         to_multi_ary_expr(offset).op1().is_constant()))
+      {
+        return get_subexpression_at_offset(
+          member_exprt{expr, components.front()}, offset, target_type, ns);
+      }
+      // if we have an offset C + x (where C is a constant) we can try to
+      // recurse by first looking at the member at offset C
+      else if(
+        offset.id() == ID_plus && offset.operands().size() == 2 &&
+        (to_multi_ary_expr(offset).op0().is_constant() ||
+         to_multi_ary_expr(offset).op1().is_constant()))
+      {
+        const plus_exprt &offset_plus = to_plus_expr(offset);
+        const auto &const_factor = numeric_cast_v<mp_integer>(to_constant_expr(
+          offset_plus.op0().is_constant() ? offset_plus.op0()
+                                          : offset_plus.op1()));
+        const exprt &other_factor = offset_plus.op0().is_constant()
+                                      ? offset_plus.op1()
+                                      : offset_plus.op0();
+
+        auto expr_at_offset_C =
+          get_subexpression_at_offset(expr, const_factor, target_type, ns);
+
+        if(
+          expr_at_offset_C.has_value() && expr_at_offset_C->id() == ID_index &&
+          to_index_expr(*expr_at_offset_C).index().is_zero())
+        {
+          return get_subexpression_at_offset(
+            to_index_expr(*expr_at_offset_C).array(),
+            other_factor,
+            target_type,
+            ns);
+        }
+      }
+
+      return {};
+    }
+    else
+      return {};
+  }
   else
     return get_subexpression_at_offset(expr, *offset_bytes, target_type, ns);
 }