Remove well-alignedness assumption from pointer-into-array

84df81e fixed the case for unaligned access into arrays when the
dereference type did not match the size of array elements. This was,
however, missing the case that an unaligned access into an array is done
with matching dereference type size.

Co-authored-by: Enrico Steffinlongo <[email protected]>

Fixes: #7265

Author: tautschnig

jbmc/src/java_bytecode/java_trace_validation.cpp

@@ -79,7 +79,8 @@ bool can_evaluate_to_constant(const exprt &expression)
 {
   return can_cast_expr<constant_exprt>(skip_typecast(expression)) ||
          can_cast_expr<symbol_exprt>(skip_typecast(expression)) ||
-         can_cast_expr<plus_exprt>(skip_typecast(expression));
+         can_cast_expr<plus_exprt>(skip_typecast(expression)) ||
+         can_cast_expr<mult_exprt>(skip_typecast(expression));
 }
 
 bool check_index_structure(const exprt &index_expr)

regression/cbmc/Pointer_Arithmetic19/test.desc

@@ -1,7 +1,7 @@
 CORE new-smt-backend
 main.c
 --program-only
-ASSERT\(\{ 42, 43 \}\[POINTER_OFFSET\(p!0@1#2\) / \d+l*\] == 43\)$
+ASSERT\(byte_extract_little_endian\(\{ 42, 43 \}, POINTER_OFFSET\(p!0@1#2\), signed int\) == 43\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cbmc/Pointer_array7/big-endian.desc

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

regression/cbmc/Pointer_array7/main.c

@@ -0,0 +1,29 @@
+#include <assert.h>
+#include <stdint.h>
+
+#if !defined(__LITTLE_ENDIAN__) && !defined(__BIG_ENDIAN__)
+
+#  if defined(__avr32__) || defined(__hppa__) || defined(__m68k__) ||          \
+    defined(__mips__) || defined(__powerpc__) || defined(__s390__) ||          \
+    defined(__s390x__) || defined(__sparc__)
+
+#    define __BIG_ENDIAN__
+
+#  endif
+
+#endif
+
+int main()
+{
+  uint16_t x[2];
+  x[0] = 1;
+  x[1] = 2;
+  uint8_t *y = (uint8_t *)x;
+  uint16_t z = *((uint16_t *)(y + 1));
+
+#ifdef __BIG_ENDIAN__
+  assert(z == 256u);
+#else
+  assert(z == 512u);
+#endif
+}

regression/cbmc/Pointer_array7/test.desc

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

regression/cbmc/address_space_size_limit3/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE thorough-smt-backend
 main.i
 --32 --little-endian --object-bits 25 --pointer-check
 ^EXIT=10$

src/pointer-analysis/value_set_dereference.cpp

@@ -577,23 +577,27 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
       result.value = typecast_exprt::conditional_cast(object, dereference_type);
       result.pointer =
         typecast_exprt::conditional_cast(object_pointer, pointer_type);
+
+      return result;
     }
-    else if(
+
+    // this is relative to the root object
+    exprt offset;
+    if(o.offset().is_constant())
+      offset = o.offset();
+    else
+      offset = simplify_expr(pointer_offset(pointer_expr), ns);
+
+    if(
       root_object_type.id() == ID_array &&
       dereference_type_compare(
         to_array_type(root_object_type).element_type(), dereference_type, ns) &&
       pointer_offset_bits(to_array_type(root_object_type).element_type(), ns) ==
-        pointer_offset_bits(dereference_type, ns))
+        pointer_offset_bits(dereference_type, ns) &&
+      offset.is_constant())
     {
       // We have an array with a subtype that matches
       // the dereferencing type.
-      exprt offset;
-
-      // this should work as the object is essentially the root object
-      if(o.offset().is_constant())
-        offset=o.offset();
-      else
-        offset=pointer_offset(pointer_expr);
 
       // are we doing a byte?
       auto element_size =
@@ -605,18 +609,25 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
           to_array_type(root_object_type).element_type().pretty();
       }
 
-      exprt element_size_expr = from_integer(*element_size, offset.type());
+      const auto offset_int =
+        numeric_cast_v<mp_integer>(to_constant_expr(offset));
 
-      exprt adjusted_offset =
-        simplify_expr(div_exprt{offset, element_size_expr}, ns);
+      if(offset_int % *element_size == 0)
+      {
+        index_exprt index_expr{
+          root_object,
+          from_integer(
+            offset_int / *element_size,
+            to_array_type(root_object_type).index_type())};
+        result.value =
+          typecast_exprt::conditional_cast(index_expr, dereference_type);
+        result.pointer = typecast_exprt::conditional_cast(
+          address_of_exprt{index_expr}, pointer_type);
 
-      index_exprt index_expr{root_object, adjusted_offset};
-      result.value =
-        typecast_exprt::conditional_cast(index_expr, dereference_type);
-      result.pointer = typecast_exprt::conditional_cast(
-        address_of_exprt{index_expr}, pointer_type);
+        return result;
+      }
     }
-    else
+
     {
       // try to build a member/index expression - do not use byte_extract
       auto subexpr = get_subexpression_at_offset(
@@ -641,13 +652,6 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
       result.pointer = typecast_exprt::conditional_cast(
         address_of_exprt{skip_typecast(o.root_object())}, pointer_type);
 
-      // this is relative to the root object
-      exprt offset;
-      if(o.offset().id()==ID_unknown)
-        offset=pointer_offset(pointer_expr);
-      else
-        offset=o.offset();
-
       if(memory_model(result.value, dereference_type, offset, ns))
       {
         // ok, done