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_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;
 

regression/cbmc/Pointer_byte_extract5/no-simplify.desc

@@ -0,0 +1,14 @@
+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
+--
+Test is built from SV-COMP's memsafety/20051113-1.c_false-valid-memtrack.c.
+C90 did not have flexible arrays, and using arrays of size 1 was common
+practice: http://c-faq.com/struct/structhack.html. We need to treat those as if
+it were a zero-sized array.

regression/cbmc/Pointer_byte_extract5/test.desc

@@ -7,3 +7,8 @@ array\.List dynamic object upper bound in p->List\[2\]: FAILURE
 \*\* 1 of 11 failed 
 --
 ^warning: ignoring
+--
+Test is built from SV-COMP's memsafety/20051113-1.c_false-valid-memtrack.c.
+C90 did not have flexible arrays, and using arrays of size 1 was common
+practice: http://c-faq.com/struct/structhack.html. We need to treat those as if
+it were a zero-sized array.

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