Back-end encoding of pointers corrupts large offsets

[martin-cs]

This bug gives a correctness error sv-benchmarks/c/array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety.i

Pointers are represented as (object, offset) pairs. The back-end (bv_pointers.h) encodes these into config.ansi_c.pointer_width bit bvt's by using the top BV_ADDR_BITS (currently 8) for the object and the remaining bits for the offset. This means that if the offset uses more bits than that it will be truncated giving some really fun effects when the decode sign extends it.

It is not immediately clear how to fix this:

1. Have offset be a full word and add BV_ADDR_BITS on the front. This means that pointers will no longer have the correct size.
2. Another option is to make this limitation clearer by catching any offset large enough to trigger this problem. That would avoid this kind of silent mistake but its all shades of ugly.
3. There might be a semi-fix in which we rely on knowing the object size to do the encoding / decoding. That way we should only get weirdness like this in cases where the program would allocate more than an addressible amount of memory. I'll see what I can do.

int main() { int n = nondet_int(); __CPROVER_assume( (n > 0) && (n > (1 << 23)) );

int nm = n-1;

char *base = __builtin_alloca (n);
//char works = *(base + nm);

char *last = base + nm;
signed offset = __CPROVER_POINTER_OFFSET(last);

__CPROVER_assert(0 <= offset && offset < n, "range check");

return 0;
}


[tautschnig]

Just adding that regression/cbmc/Pointer_Arithmetic13 is an existing regression test that would be fixed if we were to eventually fix this problem...

[peterschrammel]

There are a few of related issues:

• Address space limit test doesn't work #243
• Pointer encoding limits address space to 24bits for ILP32 #94

In java, we have the opposite problem, namely that we often have more objects than encodable. @smowton has played with making the encoding more flexible, but obviously there is a tension between large-arrays and many-objects. Unless we want to figure out a suitable partitioning at runtime, I would be in favour of adding command line options to specify the partitioning, and increasing the number of objects by default.

[martin-cs]

Thanks all for comments and to @mgudemann for pointing me to @smowton 's patches:

https://github.com/diffblue/verification-engine-utils/issues/251
smowton@5f89782

A number of thoughts...

1. Allocating object numbers so that they do not contain 00, bit reversing them and putting them at the start of the pointer would allow a variable number of object/offset bits (we could even be clever with the ID depending on the size) at a minimal extra cost in terms of decode logic. There are various other things we could do with fancy encodings but in some way we shouldn't as we should be able to represent any base/offset pair, even the incorrect ones.
2. The offset can (and should) be user 'modifiable' but the object part really really shouldn't be or one can get the analyser to do counter factual and frankly downright weird things by accessing objects that the pointer analysis knows are impossible.
3. The Java and C cases are different. In Java we can just up the pointer length as the language guarantees that access to these will be type safe so there is no way to "see" the extra bits. See : https://github.com/martin-cs/cbmc/tree/proposal-%23311 for a sketch of how this could be done. I will be pleasantly surprised if this actually runs. I think this is ultimately the way to fix this with Java, possibly with a dynamic setting of object_bits.
4. The C case is harder as there are various non-type safe constructs that require that the "in memory" view of the bits is reasonable and correct. This is what makes the "remove pack/unpack" optimisation for floats hard. I think the eventual goal would be to have pointers represented as object_bit + pointer_bit with only the pointer_bits part accessible. We're going to need an extra operation, a "pack" or "flatten" for using when the formula is going to do something unsafe. This would pack floats, instantiate all fields of arrays, structures, etc., do something with strings and hide away the object part of pointers, only to reconstruct it after the flatten. Thus the user could do anything type unsafe they wanted but would only change the offset, not the base. This would be a bit change to the back end but would come with many benefits and fix and number of scalability problems. Maybe it isn't an insane amount of work. I'll give it some thought.

As ever; thoughts, comments, meditations, observations and reservations appreciated.

[martin-cs]

If we can add 'pack' and 'unpack' expressions before and after type unsafe accesses (pointers that have been cast and unions I think) then we should be able to alter the encodings as we like. The catch is when to add them. I think it can be done in symex as a new SSA name will be needed for anything that /might/ be modified in a type unsafe fashion. It is still not entirely clear to me how this would work for something like the double linked list pointer XOR trick. I think if we can do that then ... we should be good.

[tautschnig]

Since I've been looking at this again for the benefit of SV-COMP: how about increasing the pointer width in Java as proposed by @martin-cs while doing a much simpler hack for C: constrain the size of individual, dynamically allocated objects. This is 45cd1673 in #363. (And I am wondering whether Pointer_Arithmetic13/main.c is actually defined behaviour, since arithmetic outside object bounds may be invalid?)