Merge pull request #7267 from tautschnig/bugfixes/7265-array-alignment

Remove well-alignedness assumption from pointer-into-array

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

@@ -142,9 +142,9 @@ exprt value_set_dereferencet::dereference(
   const exprt &pointer,
   bool display_points_to_sets)
 {
-  if(pointer.type().id()!=ID_pointer)
-    throw "dereference expected pointer type, but got "+
-          pointer.type().pretty();
+  PRECONDITION_WITH_DIAGNOSTICS(
+    pointer.type().id() == ID_pointer,
+    "dereference expected pointer type, but got " + pointer.type().pretty());
 
   // we may get ifs due to recursive calls
   if(pointer.id()==ID_if)
@@ -465,8 +465,9 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
     return valuet();
   }
 
-  if(what.id()!=ID_object_descriptor)
-    throw "unknown points-to: "+what.id_string();
+  PRECONDITION_WITH_DIAGNOSTICS(
+    what.id() == ID_object_descriptor,
+    "unknown points-to: " + what.id_string());
 
   const object_descriptor_exprt &o=to_object_descriptor_expr(what);
 
@@ -477,24 +478,28 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
   std::cout << "O: " << format(root_object) << '\n';
   #endif
 
-  valuet result;
-
   if(root_object.id() == ID_null_object)
   {
-    if(o.offset().is_zero())
-      result.pointer = null_pointer_exprt{pointer_type};
-    else
-      return valuet{};
+    if(!o.offset().is_zero())
+      return {};
+
+    valuet result;
+    result.pointer = null_pointer_exprt{pointer_type};
+    return result;
   }
   else if(root_object.id()==ID_dynamic_object)
   {
+    valuet result;
+
     // constraint that it actually is a dynamic object
     // this is also our guard
     result.pointer_guard = is_dynamic_object_exprt(pointer_expr);
 
     // can't remove here, turn into *p
     result.value = dereference_exprt{pointer_expr};
     result.pointer = pointer_expr;
+
+    return result;
   }
   else if(root_object.id()==ID_integer_address)
   {
@@ -514,8 +519,10 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
         pointer_offset(pointer_expr),
         to_array_type(memory_symbol.type).element_type());
 
+      valuet result;
       result.value=index_expr;
       result.pointer = address_of_exprt{index_expr};
+      return result;
     }
     else if(dereference_type_compare(
               to_array_type(memory_symbol.type).element_type(),
@@ -526,28 +533,32 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
         symbol_expr,
         pointer_offset(pointer_expr),
         to_array_type(memory_symbol.type).element_type());
+
+      valuet result;
       result.value=typecast_exprt(index_expr, dereference_type);
       result.pointer =
         typecast_exprt{address_of_exprt{index_expr}, pointer_type};
+      return result;
     }
     else
     {
       // We need to use byte_extract.
       // Won't do this without a commitment to an endianness.
 
       if(config.ansi_c.endianness==configt::ansi_ct::endiannesst::NO_ENDIANNESS)
-      {
-      }
-      else
-      {
-        result.value = make_byte_extract(
-          symbol_expr, pointer_offset(pointer_expr), dereference_type);
-        result.pointer = address_of_exprt{result.value};
-      }
+        return {};
+
+      valuet result;
+      result.value = make_byte_extract(
+        symbol_expr, pointer_offset(pointer_expr), dereference_type);
+      result.pointer = address_of_exprt{result.value};
+      return result;
     }
   }
   else
   {
+    valuet result;
+
     // something generic -- really has to be a symbol
     address_of_exprt object_pointer(object);
 
@@ -565,8 +576,6 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
     const typet &object_type = object.type();
     const typet &root_object_type = root_object.type();
 
-    exprt root_object_subexpression=root_object;
-
     if(
       dereference_type_compare(object_type, dereference_type, ns) &&
       o.offset().is_zero())
@@ -577,89 +586,81 @@ 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 =
         pointer_offset_size(to_array_type(root_object_type).element_type(), ns);
+      CHECK_RETURN(element_size.has_value());
+      CHECK_RETURN(*element_size > 0);
 
-      if(!element_size.has_value() || *element_size == 0)
-      {
-        throw "unknown or invalid type size of:\n" +
-          to_array_type(root_object_type).element_type().pretty();
-      }
-
-      exprt element_size_expr = from_integer(*element_size, offset.type());
-
-      exprt adjusted_offset =
-        simplify_expr(div_exprt{offset, element_size_expr}, ns);
+      const auto offset_int =
+        numeric_cast_v<mp_integer>(to_constant_expr(offset));
 
-      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);
-    }
-    else
-    {
-      // try to build a member/index expression - do not use byte_extract
-      auto subexpr = get_subexpression_at_offset(
-        root_object_subexpression, o.offset(), dereference_type, ns);
-      if(subexpr.has_value())
-        simplify(subexpr.value(), ns);
-      if(
-        subexpr.has_value() &&
-        subexpr.value().id() != ID_byte_extract_little_endian &&
-        subexpr.value().id() != ID_byte_extract_big_endian)
+      if(offset_int % *element_size == 0)
       {
-        // Successfully found a member, array index, or combination thereof
-        // that matches the desired type and offset:
-        result.value = subexpr.value();
+        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{skip_typecast(subexpr.value())}, pointer_type);
+          address_of_exprt{index_expr}, pointer_type);
+
         return result;
       }
+    }
 
-      // we extract something from the root object
-      result.value=o.root_object();
+    // try to build a member/index expression - do not use byte_extract
+    auto subexpr = get_subexpression_at_offset(
+      root_object, o.offset(), dereference_type, ns);
+    if(subexpr.has_value())
+      simplify(subexpr.value(), ns);
+    if(
+      subexpr.has_value() &&
+      subexpr.value().id() != ID_byte_extract_little_endian &&
+      subexpr.value().id() != ID_byte_extract_big_endian)
+    {
+      // Successfully found a member, array index, or combination thereof
+      // that matches the desired type and offset:
+      result.value = subexpr.value();
       result.pointer = typecast_exprt::conditional_cast(
-        address_of_exprt{skip_typecast(o.root_object())}, pointer_type);
+        address_of_exprt{skip_typecast(subexpr.value())}, pointer_type);
+      return result;
+    }
 
-      // this is relative to the root object
-      exprt offset;
-      if(o.offset().id()==ID_unknown)
-        offset=pointer_offset(pointer_expr);
-      else
-        offset=o.offset();
+    // we extract something from the root object
+    result.value = o.root_object();
+    result.pointer = typecast_exprt::conditional_cast(
+      address_of_exprt{skip_typecast(o.root_object())}, pointer_type);
 
-      if(memory_model(result.value, dereference_type, offset, ns))
-      {
-        // ok, done
-      }
-      else
-      {
-        return valuet(); // give up, no way that this is ok
-      }
-    }
-  }
+    if(!memory_model(result.value, dereference_type, offset, ns))
+      return {}; // give up, no way that this is ok
 
-  return result;
+    return result;
+  }
 }
 
 static bool is_a_bv_type(const typet &type)

src/solvers/flattening/bv_pointers.cpp

@@ -264,8 +264,8 @@ optionalt<bvt> bv_pointerst::convert_address_of_rec(const exprt &expr)
       UNREACHABLE;
 
     // get size
-    auto size = pointer_offset_size(array_type.element_type(), ns);
-    CHECK_RETURN(size.has_value() && *size >= 0);
+    auto size = size_of_expr(array_type.element_type(), ns);
+    CHECK_RETURN(size.has_value());
 
     bv = offset_arithmetic(type, bv, *size, index);
     CHECK_RETURN(bv.size()==bits);
@@ -732,7 +732,7 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
     to_typecast_expr(expr).op().type().id() == ID_pointer)
   {
     // pointer to int
-    bvt op0 = convert_pointer_type(to_typecast_expr(expr).op());
+    bvt op0 = convert_bv(to_typecast_expr(expr).op());
 
     // squeeze it in!
     std::size_t width=boolbv_width(expr.type());
@@ -844,6 +844,28 @@ bvt bv_pointerst::offset_arithmetic(
   return offset_arithmetic(type, bv, factor, bv_index);
 }
 
+bvt bv_pointerst::offset_arithmetic(
+  const pointer_typet &type,
+  const bvt &bv,
+  const exprt &factor,
+  const exprt &index)
+{
+  bvt bv_factor = convert_bv(factor);
+  bvt bv_index =
+    convert_bv(typecast_exprt::conditional_cast(index, factor.type()));
+
+  bv_utilst::representationt rep = factor.type().id() == ID_signedbv
+                                     ? bv_utilst::representationt::SIGNED
+                                     : bv_utilst::representationt::UNSIGNED;
+
+  bv_index = bv_utils.multiplier(bv_index, bv_factor, rep);
+
+  const std::size_t offset_bits = get_offset_width(type);
+  bv_index = bv_utils.extension(bv_index, offset_bits, rep);
+
+  return offset_arithmetic(type, bv, 1, bv_index);
+}
+
 bvt bv_pointerst::offset_arithmetic(
   const pointer_typet &type,
   const bvt &bv,

src/solvers/flattening/bv_pointers.h

@@ -66,6 +66,12 @@ class bv_pointerst:public boolbvt
     const mp_integer &factor,
     const exprt &index);
   NODISCARD
+  bvt offset_arithmetic(
+    const pointer_typet &type,
+    const bvt &bv,
+    const exprt &factor,
+    const exprt &index);
+  NODISCARD
   bvt offset_arithmetic(
     const pointer_typet &,
     const bvt &,