Fix flattening of access beyond type-specified bounds

The test Pointer_byte_extract5 was previously only solved properly thanks to
hacks in the simplifier. We should not have to rely on those.

Author: tautschnig

regression/cbmc/Pointer_byte_extract10/main.c

@@ -0,0 +1,45 @@
+void *malloc(__CPROVER_size_t);
+
+typedef union
+{
+  int a;
+  int b;
+} Union;
+
+#ifdef __GNUC__
+typedef struct
+{
+  int Count;
+  Union List[1];
+} __attribute__((packed)) Struct3;
+#else
+typedef struct
+{
+  int Count;
+  Union List[1];
+} Struct3;
+#endif
+
+int main()
+{
+  Struct3 *p = malloc (sizeof (int) + 2 * sizeof(Union));
+  p->Count = 3;
+  int po=0;
+
+  // this should be fine
+  p->List[0].a = 555;
+
+  __CPROVER_assert(p->List[0].b==555, "p->List[0].b==555");
+  __CPROVER_assert(p->List[0].a==555, "p->List[0].a==555");
+
+  // this should be fine
+  p->List[1].b = 999;
+
+  __CPROVER_assert(p->List[1].b==999, "p->List[1].b==999");
+  __CPROVER_assert(p->List[1].a==999, "p->List[1].a==999");
+
+  // this is out-of-bounds
+  p->List[2].a = 0;
+
+  return 0;
+}

regression/cbmc/Pointer_byte_extract10/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--bounds-check --32 --no-simplify
+^EXIT=10$
+^SIGNAL=0$
+array\.List dynamic object upper bound in p->List\[2\]: FAILURE
+\*\* 1 of 14 failed 
+--
+^warning: ignoring

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/endianness_map.h>
+#include <util/pointer_offset_size.h>
 #include <util/std_expr.h>
 #include <util/throw_with_nested.h>
 
@@ -78,6 +79,30 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
   if(width==0)
     return conversion_failed(expr);
 
+  // see if the byte number is constant and within bounds, else work from the
+  // root object
+  const mp_integer op_bytes = pointer_offset_size(expr.op().type(), ns);
+  auto index = numeric_cast<mp_integer>(expr.offset());
+  if(
+    (!index.has_value() || (*index < 0 || *index >= op_bytes)) &&
+    (expr.op().id() == ID_member || expr.op().id() == ID_index ||
+     expr.op().id() == ID_byte_extract_big_endian ||
+     expr.op().id() == ID_byte_extract_little_endian))
+  {
+    object_descriptor_exprt o;
+    o.build(expr.op(), ns);
+    CHECK_RETURN(o.offset().id() != ID_unknown);
+    if(o.offset().type() != expr.offset().type())
+      o.offset().make_typecast(expr.offset().type());
+    byte_extract_exprt be(
+      expr.id(),
+      o.root_object(),
+      plus_exprt(o.offset(), expr.offset()),
+      expr.type());
+
+    return convert_bv(be);
+  }
+
   const exprt &op=expr.op();
   const exprt &offset=expr.offset();
 
@@ -106,13 +131,12 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
   // see if the byte number is constant
   unsigned byte_width=8;
 
-  mp_integer index;
-  if(!to_integer(offset, index))
+  if(index.has_value())
   {
-    if(index<0)
+    if(*index < 0)
       throw "byte_extract flatting with negative offset: "+expr.pretty();
 
-    mp_integer offset=index*byte_width;
+    const mp_integer offset = *index * byte_width;
 
     std::size_t offset_i=integer2unsigned(offset);
 

src/solvers/flattening/boolbv_index.cpp

@@ -11,8 +11,9 @@ Author: Daniel Kroening, [email protected]
 #include <cassert>
 
 #include <util/arith_tools.h>
-#include <util/std_expr.h>
+#include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
+#include <util/std_expr.h>
 
 bvt boolbvt::convert_index(const index_exprt &expr)
 {
@@ -333,6 +334,28 @@ bvt boolbvt::convert_index(
     for(std::size_t i=0; i<width; i++)
       bv[i]=tmp[integer2size_t(offset+i)];
   }
+  else if(
+    array.id() == ID_member || array.id() == ID_index ||
+    array.id() == ID_byte_extract_big_endian ||
+    array.id() == ID_byte_extract_little_endian)
+  {
+    object_descriptor_exprt o;
+    o.build(array, ns);
+    CHECK_RETURN(o.offset().id() != ID_unknown);
+
+    const mp_integer subtype_bytes =
+      pointer_offset_size(array_type.subtype(), ns);
+    exprt new_offset =
+      simplify_expr(
+        plus_exprt(
+          o.offset(),
+          from_integer(index * subtype_bytes, o.offset().type())), ns);
+
+    byte_extract_exprt be(
+      byte_extract_id(), o.root_object(), new_offset, array_type.subtype());
+
+    return convert_bv(be);
+  }
   else
   {
     // out of bounds