Spurious pointer arithmetic errors

[celinval]

I have created the following test case:

#include <stddef.h>
#include <assert.h>

int* add(int* ptr, size_t offset) {
    return ptr + offset;
}

int spurious() {
    int* pin_0 = 32;
    int* pin_1 = add(pin_0, 0);
    assert(pin_0 == pin_1);
}

int expected() {
    int* pin_0 = 32;
    int* pin_1 = pin_0 + 0;
    assert(pin_0 == pin_1);
}

The functions expected and spurious are functionally equivalent. One wraps the sum into an aux function and the other one performs the sum in-place. The results of CBMC proofs are rather different for these two functions:

$ cbmc test.c --pointer-overflow-check --function spurious | tail -n 18
** Results:
test.c function add
[add.pointer_arithmetic.1] line 5 pointer arithmetic: pointer NULL in ptr + (signed long int)offset: FAILURE
[add.pointer_arithmetic.2] line 5 pointer arithmetic: pointer invalid in ptr + (signed long int)offset: SUCCESS
[add.pointer_arithmetic.3] line 5 pointer arithmetic: deallocated dynamic object in ptr + (signed long int)offset: FAILURE
[add.pointer_arithmetic.4] line 5 pointer arithmetic: dead object in ptr + (signed long int)offset: FAILURE
[add.pointer_arithmetic.5] line 5 pointer arithmetic: pointer outside object bounds in ptr + (signed long int)offset: FAILURE
[add.pointer_arithmetic.6] line 5 pointer arithmetic: invalid integer address in ptr + (signed long int)offset: FAILURE

test.c function expected
[expected.pointer_arithmetic.1] line 16 pointer arithmetic: invalid integer address in pin_0 + (signed long int)0: SUCCESS
[expected.assertion.1] line 17 assertion pin_0 == pin_1: SUCCESS

test.c function spurious
[spurious.assertion.1] line 11 assertion pin_0 == pin_1: SUCCESS

** 5 of 9 failed (2 iterations)
VERIFICATION FAILED

The result below seems more reasonable:

$ cbmc test.c --pointer-overflow-check --function expected | tail -n 18
** Results:
test.c function add
[add.pointer_arithmetic.1] line 5 pointer arithmetic: pointer NULL in ptr + (signed long int)offset: SUCCESS
[add.pointer_arithmetic.2] line 5 pointer arithmetic: pointer invalid in ptr + (signed long int)offset: SUCCESS
[add.pointer_arithmetic.3] line 5 pointer arithmetic: deallocated dynamic object in ptr + (signed long int)offset: SUCCESS
[add.pointer_arithmetic.4] line 5 pointer arithmetic: dead object in ptr + (signed long int)offset: SUCCESS
[add.pointer_arithmetic.5] line 5 pointer arithmetic: pointer outside object bounds in ptr + (signed long int)offset: SUCCESS
[add.pointer_arithmetic.6] line 5 pointer arithmetic: invalid integer address in ptr + (signed long int)offset: SUCCESS

test.c function expected
[expected.pointer_arithmetic.1] line 16 pointer arithmetic: invalid integer address in pin_0 + (signed long int)0: FAILURE
[expected.assertion.1] line 17 assertion pin_0 == pin_1: SUCCESS

test.c function spurious
[spurious.assertion.1] line 11 assertion pin_0 == pin_1: SUCCESS

** 1 of 9 failed (2 iterations)
VERIFICATION FAILED

CBMC version: 5.50.0
Operating system: Ubuntu 18.04
Exact command line resulting in the issue: cbmc test.c --pointer-overflow-check --function spurious
What behaviour did you expect: Only one failure due to "pointer arithmetic: pointer invalid".
What happened instead: Checks like NULL pointer are failing even though the pointer is not NULL.

[tautschnig]

As far as I can tell, what you are seeing here is mainly a presentation problem. We use an intra procedural analysis to determine what checks to create for a use of a pointer. With spurious, this obviously runs into limitations. So we end up generating more checks than perhaps is practically meaningful. None of the results seem to be wrong, just the NULL one might be most confusing (we actually check for the "NULL object", not just the literal "NULL" pointer, and "32" is considered an offset of 32 bytes into the "NULL object").

That said, there does not seem to be any disagreement that verification should fail in this case. Is it perhaps necessary to dig deeper to understand why these results are giving you grief? With the background of model-checking/kani#763 I'm tempted to say that we really need to get #6616 merged so that Kani can annotate more precisely where checks are (not) to be generated?

[celinval]

Is there a way to explicitlygenerate the checks instead of using ppragmas to disable them?

[kroening]

Any good ideas what to call an access to an address that's a plain integer converted to a pointer? "No object"?

[kroening]

Kani: Is the memory model that C has a good fit for Rust at all? It may make sense to set up a memory safety checker that is specific to Rust and exploits whatever guarantees the Rust type system can give.

[tautschnig]

Is there a way to explicitlygenerate the checks instead of using ppragmas to disable them?

You can use the pragmas to both effects: a disable:pointer-overflow-check will disable those checks even when the command-line option --pointer-overflow-check was used; an enable:pointer-overflow-check pragma will enable the check irrespective of whether the command-line option was set or not.

But then it's all limited to statements and therefore a bit of a gamble until #6616 is approved and merged.

[celinval]

@kroening That's a great question and unfortunately Rust doesn't have a well defined memory model yet (https://doc.rust-lang.org/reference/memory-model.html). The semantics of the pointer arithmetic operations vary according to the std method users are calling. For now, we should be able to leverage the C model but it would be great if we could easily control when to check if a pointer is valid to account for the different behavior.

@tautschnig Does CBMC have any primitive to check if a pointer is valid? I would prefer that over pragmas.

[tautschnig]

@tautschnig Does CBMC have any primitive to check if a pointer is valid? I would prefer that over pragmas.

You could opt to use __CPROVER_r_ok:

cbmc/src/util/pointer_expr.h

Line 762 in 9fec06a

class r_ok_exprt : public r_or_w_ok_exprt

as documented here?

[celinval]

That would be awesome. I noticed that the primitive documentation says:

If p is neither null nor valid, the semantics is unspecified.

Is that still the case?

[celinval]

Hi @tautschnig, I just wanted to confirm, can we use __CPROVER_r_ok() to assert that a pointer is valid?

[tautschnig]

Hi @tautschnig, I just wanted to confirm, can we use __CPROVER_r_ok() to assert that a pointer is valid?

My apologies for taking this long to respond. #6416 removes the statement you quoted from the documentation. Despite me requesting changes on that pull request, the issue really only applies to assumptions. If you are doing assertions then you are safe and you can use it in the way you desire. For assumptions we'd additionally need #6506.

[celinval]

Awesome! @danielsn pointed out that the issue could be related to assumptions, but I wanted to double check since the documentation wasn't very clear. I'll close this issue and create one on the Kani side so we can add these checks manually.

Thanks again.