Flattening of byte-update against variable-length arrays with non-char members is broken

[smowton]

Example test case:

struct A {
  int x;
};

int main(int argc, char** argv) {

  struct A a;
  int i;

  if(argc != 2)
    return;

  void** ptrs[argc];
  for(i = 0; i < 2; ++i)
    ptrs[i] = (void*)0;

  ((struct A**)ptrs)[1]=&a;
  assert(ptrs[1] == (void*)&a);

}

Naturally we expect the assert to pass, since we've just assigned a on the previous line. However the trace shows not &a as we might expect, but:

ptrs={ ((const void **)NULL), ((const void **)NULL) + 3 }

This is the result of the following byte-update VCC:

ptrs!0@1#4 == byte_update_little_endian(ptrs!0@1#3, 8l, &a!0@1, struct A { signed int x; } *)

Clearly sensible so far. However the byte-update-flattening logic (only used for VLAs) at flatten_byte_operators.cpp:191 has two problems for the case where the target array members are not bytes:

1. It loops over each byte in the value operand, but writes each one to the same target address.
2. When recursively using byte_update over scalar array members, it updates with respect to the original source operand, not any partially-updated array resulting from previous byte ops.

For example, if memory contained bytes {1,2,3,4} typed as an int[] and we tried to write (short){5,6} over the first two bytes, we would end up with intermediate result {5,6,3,4} but ultimate result {6,x,3,4} because the second overwrite doesn't use an appropriate shift+mask, hence parts of the address of a ending up in the less-significant bits of the target array and being reported as NULL + (void*)3

smowton@fd1bbd1 fixes the issue, but at the cost of introducing an overly large expression (quadratic in the number of bytes changed), as the intermediate result array must be referenced as both the byte_update operand and the with operand, and AFAIK it is illegal to introduce intermediate symbols at this stage.

I will have a go at producing a version of this patch that only touches each target array element once tomorrow morning.

[smowton]

smowton@fa2666b implements a better algorithm, and smowton@9612165 adds the test-case given above plus various misaligned update tests.

The formulae produced for the case where elements have different sizes are still quite large, probably because of the if test introduced to allow byte-update of a scalar with a negative offset (i.e. overwriting only the least-significant bytes). This could be worked around by zero-padding and adding instead; I'll give this a go when more free time presents itself.

[smowton]

smowton@d962d79 cleans up a little, but the time consumption turns out to result mainly from array-constraint generation taking a long time, a problem which should probably be considered orthogonally from this one.

Therefore if you're happy with this solution I'll put them together into a branch against master.

[smowton]

Fixed in #397