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

[tautschnig]

The Pointer_byte_extract5 test only succeeded because the simplifier was kind enough to flatten some operations. Now the test can also be handled without prior simplification. While at it, negative byte extracts can also be handled safely (they are out-of-bounds, but that's ok).

[martin-cs]

The changes look OK but I'm having a hard time finding the right place in the C standard that says whether the write to the second thing is out-of-bounds or not.

[martin-cs]

(sizeof(Struct3) + sizeof(Union)) because padding (think an architecture with strict alignment, 4 byte integers and 8 byte pointers)?

[tautschnig]

Good call - done (packing is only requested on for __GNUC__ in this test).

[martin-cs]

Maybe? I agree (modulo the change above) that this is in the dynamically allocated region, but I don't know that it is in inside the array and I don't know exact A. which we check and B. the standard would use for determining undefined behaviour.

[tautschnig]

I'm not sure this is covered by the C standard. As far as I recall this is an example from SV-COMP that originated from the Linux kernel. Using a proper flexible array would work, but I'm not sure it would expose the bug that this test was originally mean to expose (which is that we need to look at the actually allocated object instead of the type).

[martin-cs]

Ummm... I'm unsure. At the risk of making this "what exactly is the semantics of ..." week -- what is it that bounds check is checking? Is:

  int inputBuffer[LENGTH];
  int outputBuffer[LENGTH];
}

x = inputBuffer[LENGTH];```

An error?

[martin-cs]

Yeah; this one is right out!

[martin-cs]

Sorry to be a pain but I've tagged this "do not merge" for now because it is not clear to me if this is a bug or not.

[tautschnig]

@martin-cs Would you mind clarifying?

[martin-cs]

@tautschnig : Not at all. I guess the question in my mind is does bounds check:
A. check the boundaries on arrays.
B. check the boundaries on allocated units.
Consider the following fictious ethernot driver:

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 MAX(sizeof(eth_frame_header), 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;
  eth_control_data control;   // Routing, filtering, inspection, etc.
} eth_frame_with_control;

void doStuff (...) {
  eth_frame_with_control f;

  // Safe if 0 <= i < FRAME_LENGTH, viable attack over FRAME_LENGTH
  f.raw[i] = x;

  // Safe if 0 <= j < 6, likely unsafe if over 6
  f.header.dest[j] = y;

  // Safe if 0 <= k < 1500, could corrupt crc if k < 1508, viable attack over 1508
  f.header.payload[k] = z;

  // Safe if 0 <= l < 1504, wrong but probably harmless if l < 1508, viable attack over 1508
  ((eth_frame_footer*)(&f.header.payload[l]))->crc = c;
}

These seem to need a mix of A and B checking.

I think I'm going to need to read the C standard very carefully...

[tautschnig]

Just a note on the size-1 array: that was the way to do it in C90: http://c-faq.com/struct/structhack.html (and https://gcc.gnu.org/onlinedocs/gcc/Zero-Length.html).

[tautschnig]

@martin-cs I have now added your test as a regression test, which of course prompted another fix...! Would you mind taking another look and possibly remove the do-not-merge block?

[martin-cs]

Top of the stack for tomorrow :-) What policy are we implementing?

[tautschnig]

What policy are we implementing?

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.

Let me actually put that in the commit message...