Remove well-alignedness assumption from pointer dereferencing

With void* pointers, pointer dereferencing would permit any type for the
dereferenced object. For arrays, alignment at the root level was
implicitly assumed, not taking into account that there may be a
well-aligned pointer to a nested element.

For the regression test we got `arr[11 / 7]` when dereferencing `(void
*)ptr`, where `ptr` was `(char *)&arr[0] + 11` (and the size of `arr`'s
elements is 7 bytes).

Fixes: #7036

Author: tautschnig

regression/cbmc/Array_operations2/main.c

@@ -0,0 +1,48 @@
+#include <assert.h>
+
+typedef struct my_struct
+{
+  char a;
+  char b;
+  char c[5];
+} my_struct;
+
+int main()
+{
+  my_struct arr[3] = {0};
+  char *ptr = &(arr[1].c[2]);
+  int offset;
+  __CPROVER_assume(offset < 1 && offset > -1);
+  void *ptr_plus = ptr + offset;
+  char nondet[3];
+
+  __CPROVER_array_replace(ptr_plus, &nondet[0]);
+
+  // expected valid and proved
+  assert(arr[0].a == 0);
+  assert(arr[0].b == 0);
+  assert(arr[0].c[0] == 0);
+  assert(arr[0].c[1] == 0);
+  assert(arr[0].c[2] == 0);
+  assert(arr[0].c[3] == 0);
+  assert(arr[0].c[4] == 0);
+
+  assert(arr[1].a == 0);    // expected valid, falsified
+  assert(arr[1].b == 0);    // expected valid, falsified
+  assert(arr[1].c[0] == 0); // expected valid, falsified
+  assert(arr[1].c[1] == 0); // expected valid, proved
+  assert(arr[1].c[2] == 0); // expected falsifiable, proved
+  assert(arr[1].c[3] == 0); // expected falsifiable, proved
+  assert(arr[1].c[4] == 0); // expected falsifiable, proved
+
+  // expected valid and proved
+  assert(arr[2].a == 0);
+  assert(arr[2].b == 0);
+  assert(arr[2].c[0] == 0);
+  assert(arr[2].c[1] == 0);
+  assert(arr[2].c[2] == 0);
+  assert(arr[2].c[3] == 0);
+  assert(arr[2].c[4] == 0);
+
+  return 0;
+}

regression/cbmc/Array_operations2/test.desc

@@ -0,0 +1,14 @@
+CORE broken-smt-backend
+main.c
+
+^\[main.assertion.12\] line 34 assertion arr\[1\].c\[2\] == 0: FAILURE$
+^\[main.assertion.13\] line 35 assertion arr\[1\].c\[3\] == 0: FAILURE$
+^\[main.assertion.14\] line 36 assertion arr\[1\].c\[4\] == 0: FAILURE$
+^\*\* 3 of 21 failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Verify the properties of various cprover array primitves

src/pointer-analysis/value_set_dereference.cpp

@@ -572,12 +572,12 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
     else if(
       root_object_type.id() == ID_array &&
       dereference_type_compare(
-        to_array_type(root_object_type).element_type(), dereference_type, ns))
+        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))
     {
       // We have an array with a subtype that matches
       // the dereferencing type.
-      // We will require well-alignedness!
-
       exprt offset;
 
       // this should work as the object is essentially the root object
@@ -609,13 +609,9 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
         adjusted_offset=binary_exprt(
           offset, ID_div, element_size_expr, offset.type());
 
-        // TODO: need to assert well-alignedness
       }
 
-      const index_exprt &index_expr = index_exprt(
-        root_object,
-        adjusted_offset,
-        to_array_type(root_object_type).element_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(