Bounds check for flexible array members

Example crafted by Martin, which now clarifies which bounds we check:

1) When the object is stack-allocated and does not use flexible array members,
the bounds are as specified in the type.
2) When flexible array members are used (zero-sized array), the semantics laid
out in the standard are used (the bound is the size of the full object).
3) When the allocation size does not match the type-specified size (necessarily
a case of heap allocation), use the size of the allocation.

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 int\)i2\]: FAILURE
+dest\[\(signed long int\)j2\]: FAILURE
+payload\[\(signed long int\)[kl]2\]: FAILURE
+\*\* 10 of 72 failed
+--
+^warning: ignoring
+\[\(signed long int\)i\]: FAILURE
+dest\[\(signed long int\)j\]: FAILURE
+payload\[\(signed 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
   {