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. Also adjust the
malloc size computation to not rely on absence of padding.

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(Struct3) + 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

regression/cbmc/Pointer_byte_extract5/main.c

@@ -22,7 +22,7 @@ typedef struct
 
 int main()
 {
-  Struct3 *p = malloc (sizeof (int) + 2 * sizeof(Union));
+  Struct3 *p = malloc(sizeof(Struct3) + sizeof(Union));
   p->Count = 3;
   int po=0;
 

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/byte_operators.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,27 @@ 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