Merge pull request #6100 from tautschnig/boolbv_index-oob

boolbv_index: preserve endianness when generating byte extract

Author: tautschnig

regression/cbmc/member_bounds3/main.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+
+#pragma pack(push, 1)
+struct S
+{
+  int a[2];
+  int x;
+};
+#pragma pack(pop)
+
+#ifdef _MSC_VER
+#  define _Static_assert(x, m) static_assert(x, m)
+#endif
+
+int main()
+{
+  int A[3];
+  _Static_assert(sizeof(A) == sizeof(struct S), "");
+  struct S *s = A;
+  A[2] = 42;
+  assert(s->a[2] == 42);
+}

regression/cbmc/member_bounds3/test.desc

@@ -0,0 +1,8 @@
+CORE broken-smt-backend
+main.c
+--no-simplify
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/member_bounds4/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+#include <inttypes.h>
+
+union U {
+  uint8_t a[4];
+};
+
+int main()
+{
+  uint32_t x[2] = {0xDEADBEEF, 0xDEADBEEF};
+  union U *u = x;
+  uint8_t c4 = u->a[4];
+
+  unsigned word = 1;
+  if(*(char *)&word == 1)
+    assert(c4 == 0xEF); // little endian
+  else
+    assert(c4 == 0xDE); // big endian
+}

regression/cbmc/member_bounds4/test.desc

@@ -0,0 +1,8 @@
+CORE broken-smt-backend
+main.c
+--no-simplify
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/solvers/flattening/boolbv_index.cpp

@@ -321,11 +321,10 @@ bvt boolbvt::convert_index(
     std::size_t offset_int = numeric_cast_v<std::size_t>(offset);
     return bvt(tmp.begin() + offset_int, tmp.begin() + offset_int + width);
   }
-  else if(
-    array.id() == ID_member || array.id() == ID_index ||
-    array.id() == ID_byte_extract_big_endian ||
-    array.id() == ID_byte_extract_little_endian)
+  else if(array.id() == ID_member || array.id() == ID_index)
   {
+    // out of bounds for the component, but not necessarily outside the bounds
+    // of the underlying object
     object_descriptor_exprt o;
     o.build(array, ns);
     CHECK_RETURN(o.offset().id() != ID_unknown);
@@ -344,6 +343,30 @@ bvt boolbvt::convert_index(
 
     return convert_bv(be);
   }
+  else if(
+    array.id() == ID_byte_extract_big_endian ||
+    array.id() == ID_byte_extract_little_endian)
+  {
+    const byte_extract_exprt &byte_extract_expr = to_byte_extract_expr(array);
+
+    const auto subtype_bytes_opt =
+      pointer_offset_size(array_type.subtype(), ns);
+    CHECK_RETURN(subtype_bytes_opt.has_value());
+
+    // add offset to index
+    exprt new_offset = simplify_expr(
+      plus_exprt{
+        byte_extract_expr.offset(),
+        from_integer(
+          index * (*subtype_bytes_opt), byte_extract_expr.offset().type())},
+      ns);
+
+    byte_extract_exprt be = byte_extract_expr;
+    be.offset() = new_offset;
+    be.type() = array_type.subtype();
+
+    return convert_bv(be);
+  }
   else
   {
     // out of bounds