Pointer subtraction underflows and leads to faulty verification result

[AmPaschal]

When using CBMC to verify a function containing pointer arithmetic, I noticed it is possible for the symbolic object a pointer points to to underflow.

When a pointer is allocated, it is assigned $dynamicObject.
Additions to this pointer is represented as $dynamicObject + X and subsequent subtractions as $dynamicObject + X - Y.
However, if we try to subtract more than we added, the resulting difference underflows and typically leads to an dynamicObject with a large offset and subsequently, incorrect pointer dereferencing errors.

For example, in the code

void harness() {

    uint8_t bufsize;

    __CPROVER_assume(bufsize > 0);

    uint8_t *data = malloc(bufsize);

    __CPROVER_assume(data != NULL);

    uint8_t *data2 = data + 5;

    uint8_t *data3 = data2 - 7;

    // If data is validly allocated, we expect that data3's address should be less than data's address
    __CPROVER_assert(data3 < data, "data3 should be less than data!");

}

data is allocated and points to $dynamicObject.
data2 points to $dynamicObject + 5.
However, we would expect data3 to be smaller than data ($dynamicObject - 2) but instead, it underflows and points to a buffer at a very large offset ($dynamicObject + X where X is a large number).

[kroening]

Please note that pointer arithmetic outside of the bounds of the object is undefined behaviour.

We should really add a check for this.