Handle type-implied (but spurious) out-of-bounds in back-end

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.

regression/cbmc/bounds_check1/main.c

@@ -0,0 +1,115 @@
+#include <stdint.h>
+#include <stdlib.h>
+
+typedef struct _eth_frame_header
+{
+  uint8_t dest[6];
+  uint8_t src[6];
+  uint16_t length;
+  uint8_t payload[0];
+} eth_frame_header;
+
+typedef struct _eth_frame_header_with_tag
+{
+  uint8_t dest[6];
+  uint8_t src[6];
+  uint32_t tag;
+  uint16_t length;
+  uint8_t payload[0];
+} eth_frame_header_with_tag;
+
+typedef struct _eth_frame_footer
+{
+  uint32_t crc;
+} eth_frame_footer;
+
+#define FRAME_LENGTH                                                           \
+  sizeof(eth_frame_header_with_tag) + 1500 + sizeof(eth_frame_footer)
+
+typedef union _eth_frame {
+  uint8_t raw[FRAME_LENGTH];
+  eth_frame_header header;
+  eth_frame_header_with_tag header_with_tag;
+} eth_frame;
+
+typedef struct _eth_frame_with_control
+{
+  eth_frame frame;
+  uint32_t control; // Routing, filtering, inspection, etc.
+} eth_frame_with_control;
+
+void stack()
+{
+  eth_frame_with_control f;
+  unsigned i, i2, j, j2, k, k2, l, l2;
+
+  // Safe if 0 <= i < FRAME_LENGTH, viable attack over FRAME_LENGTH
+  __CPROVER_assume(i < FRAME_LENGTH);
+  // within array bounds
+  f.frame.raw[i] = 42;
+  __CPROVER_assume(i2 < FRAME_LENGTH + 4);
+  // possibly out-of-bounds, even though still within the object
+  f.frame.raw[i2] = 42;
+
+  // Safe if 0 <= j < 6, likely unsafe if over 6
+  __CPROVER_assume(j < 6);
+  // within array bounds
+  f.frame.header.dest[j] = 42;
+  // possibly out-of-bounds
+  f.frame.header.dest[j2] = 42;
+
+  // Safe if 0 <= k < 1500, could corrupt crc if k < 1508, viable attack over 1508
+  __CPROVER_assume(k < FRAME_LENGTH - 14);
+  // within array bounds
+  f.frame.header.payload[k] = 42;
+  // possibly out-of-bounds
+  f.frame.header.payload[k2] = 42;
+
+  // Safe if 0 <= l < 1504, wrong but probably harmless if l < 1508, viable attack over 1508
+  __CPROVER_assume(l < FRAME_LENGTH - 14);
+  // within array bounds
+  ((eth_frame_footer *)(&(f.frame.header.payload[l])))->crc = 42;
+  // possibly out-of-bounds
+  ((eth_frame_footer *)(&(f.frame.header.payload[l2])))->crc = 42;
+}
+
+void heap()
+{
+  eth_frame_with_control *f_heap = malloc(sizeof(eth_frame_with_control));
+  unsigned i, i2, j, j2, k, k2, l, l2;
+
+  // Safe if 0 <= i < FRAME_LENGTH, viable attack over FRAME_LENGTH
+  __CPROVER_assume(i < FRAME_LENGTH);
+  // within array bounds
+  f_heap->frame.raw[i] = 42;
+  __CPROVER_assume(i2 < FRAME_LENGTH + 4);
+  // possibly out-of-bounds, even though still within the object
+  f_heap->frame.raw[i2] = 42;
+
+  // Safe if 0 <= j < 6, likely unsafe if over 6
+  __CPROVER_assume(j < 6);
+  // within array bounds
+  f_heap->frame.header.dest[j] = 42;
+  // possibly out-of-bounds
+  f_heap->frame.header.dest[j2] = 42;
+
+  // Safe if 0 <= k < 1500, could corrupt crc if k < 1508, viable attack over 1508
+  __CPROVER_assume(k < FRAME_LENGTH - 14);
+  // within array bounds
+  f_heap->frame.header.payload[k] = 42;
+  // possibly out-of-bounds
+  f_heap->frame.header.payload[k2] = 42;
+
+  // Safe if 0 <= l < 1504, wrong but probably harmless if l < 1508, viable attack over 1508
+  __CPROVER_assume(l < FRAME_LENGTH - 14);
+  // within array bounds
+  ((eth_frame_footer *)(&(f_heap->frame.header.payload[l])))->crc = 42;
+  // possibly out-of-bounds
+  ((eth_frame_footer *)(&(f_heap->frame.header.payload[l2])))->crc = 42;
+}
+
+int main()
+{
+  stack();
+  heap();
+}

regression/cbmc/bounds_check1/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--bounds-check --pointer-check
+^EXIT=10$
+^SIGNAL=0$
+\[\(signed long( long)? int\)i2\]: FAILURE
+dest\[\(signed long( long)? int\)j2\]: FAILURE
+payload\[\(signed long( long)? int\)[kl]2\]: FAILURE
+\*\* 10 of 72 failed
+--
+^warning: ignoring
+\[\(signed long( long)? int\)i\]: FAILURE
+dest\[\(signed long( long)? int\)j\]: FAILURE
+payload\[\(signed long( long)? int\)[kl]\]: FAILURE

src/analyses/goto_check.cpp

@@ -1213,6 +1213,27 @@ void goto_checkt::bounds_check(
           expr.array().id()==ID_member)
   {
     // a variable sized struct member
+    //
+    // Excerpt from the C standard on flexible array members:
+    // However, when a . (or ->) operator has a left operand that is (a pointer
+    // to) a structure with a flexible array member and the right operand names
+    // that member, it behaves as if that member were replaced with the longest
+    // array (with the same element type) that would not make the structure
+    // larger than the object being accessed; [...]
+    const exprt type_size = size_of_expr(ode.root_object().type(), ns);
+
+    binary_relation_exprt inequality(
+      typecast_exprt::conditional_cast(ode.offset(), type_size.type()),
+      ID_lt,
+      type_size);
+
+    add_guarded_claim(
+      implies_exprt(type_matches_size, inequality),
+      name + " upper bound",
+      "array bounds",
+      expr.find_source_location(),
+      expr,
+      guard);
   }
   else
   {

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,22 +131,16 @@ 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)
-      throw "byte_extract flatting with negative offset: "+expr.pretty();
-
-    mp_integer offset=index*byte_width;
-
-    std::size_t offset_i=integer2unsigned(offset);
+    const mp_integer offset = *index * byte_width;
 
     for(std::size_t i=0; i<width; i++)
       // out of bounds?
-      if(offset<0 || offset_i+i>=op_bv.size())
+      if(offset + i < 0 || offset + i >= op_bv.size())
         bv[i]=prop.new_variable();
       else
-        bv[i]=op_bv[offset_i+i];
+        bv[i] = op_bv[numeric_cast_v<std::size_t>(offset) + i];
   }
   else
   {

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