Merge pull request #7045 from tautschnig/bugfixes/7036-array-ops

Remove well-alignedness assumption from pointer dereferencing

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

@@ -99,9 +99,11 @@ 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 `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.
+static optionalt<exprt>
+try_add_offset_to_indices(const exprt &expr, const exprt &offset_elements)
 {
   if(const auto *index_expr = expr_try_dynamic_cast<index_exprt>(expr))
   {
@@ -123,6 +125,13 @@ optionalt<exprt> value_set_dereferencet::try_add_offset_to_indices(
       return {};
     return if_exprt{if_expr->cond(), *true_case, *false_case};
   }
+  else if(can_cast_expr<typecast_exprt>(expr))
+  {
+    // the case of a type cast is _not_ handled here, because that would require
+    // doing arithmetic on the offset, and may result in an offset into some
+    // sub-element
+    return {};
+  }
   else
   {
     return {};
@@ -572,12 +581,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
@@ -586,8 +595,6 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
       else
         offset=pointer_offset(pointer_expr);
 
-      exprt adjusted_offset;
-
       // are we doing a byte?
       auto element_size =
         pointer_offset_size(to_array_type(root_object_type).element_type(), ns);
@@ -597,25 +604,13 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
         throw "unknown or invalid type size of:\n" +
           to_array_type(root_object_type).element_type().pretty();
       }
-      else if(*element_size == 1)
-      {
-        // no need to adjust offset
-        adjusted_offset = offset;
-      }
-      else
-      {
-        exprt element_size_expr = from_integer(*element_size, offset.type());
 
-        adjusted_offset=binary_exprt(
-          offset, ID_div, element_size_expr, offset.type());
+      exprt element_size_expr = from_integer(*element_size, offset.type());
 
-        // TODO: need to assert well-alignedness
-      }
+      exprt adjusted_offset =
+        simplify_expr(div_exprt{offset, element_size_expr}, ns);
 
-      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(

src/pointer-analysis/value_set_dereference.h

@@ -54,12 +54,6 @@ 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
   {