CBMC misbehaves in functions with pointer arithmetic computation

[AmPaschal]

We found some arbitrary behavior when using CBMC to verify a function with pointer arithmetic.

For example, in the code below.

void harness() {

    uint8_t bufsize;

    __CPROVER_assume(bufsize > 0);

    uint8_t *data = malloc(bufsize);

    __CPROVER_assume(data != NULL);

    uint8_t datasize;

    __CPROVER_assume(datasize > 0);

    if (datasize > bufsize) {
        return;
    }

    uint8_t *data2 = data + datasize;

    data2++; // Interestingly, if you remove this line, the memcpy read violation disappears

    uint8_t expected_len = 4;
    uint8_t dest[expected_len];

    uint8_t diff = (data2 - data); // In the trace, the value is diff is arbitrary

    if (diff + expected_len > bufsize) {
        // This validation is supposed to prevent the OOB read in the memcpy below.
        return;
    }

    memcpy(dest, data2, expected_len);

}

The validation if (diff + expected_len > bufsize) { is supposed to ensure that data2 contains up to expected_len bytes of data.
However, CBMC still reports an OOB read error in the memcpy line.
Looking at the error trace, we find that the diff computed is always arbitrary, regardless of the values of data and data2.

We tested this using CBMC v6.3.1

[kroening]

The data2++ moves the pointer out of the bounds of the object (you are allowed to point to the element that is just beyond the bound). This is hence already undefined behaviour.

[AmPaschal]

Thank you for your explanation.
I see that the C standard does not define behaviors for computing the address of pointers outside its valid bounds.

However, this code snippet was gotten from an embedded software code and the developers would still expect that the if (diff + expected_len > bufsize) check should be sufficient to prevent an OOB read in the memcpy line. Also, it seems that most modern compilers and systems correctly allow pointer computation and only result in an error if an invalid pointer is accessed.

This leads to a question -- to what extent should CBMC follow the standard and meet developer expectations without conflicting with each other?

For example, would it be okay if CBMC reports a pointer arithmetic error at data2++ (which already happens and signals a potential error) but still correctly compute the pointer data2 and the value diff. As a result, no OOB read will be reported since the if (diff + expected_len > bufsize) check will prevent an invalid memcpy in most modern systems (which is the behavior many developers expect).

[remi-delmas-3000]

I see that the C standard does not define behaviors for computing the address of pointers outside its valid bounds

UB is not just "Not defining behaviour" as in "the definition is omitted and something still reliably happens depending on the compiler", UB occurrences actually correspond to violations of assumptions that the compiler actively uses to reason when compiling the source code to machine code. The compiler may still produce an executable that happens to behave in a nice way, but you should not rely on that at all as a developer.

Even a verified compiler like Compcert only guarantees correct compilation under the assumption that the program is UB-free.

The C standard also has a notion of implementation-defined behaviour, which you can rely on if you know exactly what platform you're compiling to and all the compiler flags used to build the executable. But since there's a tremendous amount of compiler flags and some non-trivial interactions between them, relying on implementation-defined behaviour is also tricky.

[kroening]

--pointer-overflow-check should become a standard check.