Discrepancy between API specification and behavior for __CPROVER_r_ok

[celinval]

CBMC version: 5.95.1
Operating system: Ubuntu 22.04
Exact command line resulting in the issue: cbmc main.c
What behaviour did you expect: I expected the specification to say that the __CPROVER_r_ok returns non-deterministic value for non-null invalid pointers.
What happened instead: The specification explicitly says that calling __CPROVER_r_ok with invalid pointer has undefined behavior. Hence, I can only conclude that the assert(__CPROVER_r_ok()) will fail if the pointer is null.

I.e.: According to the specification, the following implementation would be perfectly fine:

int __CPROVER_r_ok(void* ptr, int sz) {
    return ptr != 0;
}

Which would make the following snippet unsound unless if user invokes it with --pointer-primitive-check:

int* function() {
    int* ptr;
    assume(ptr != NULL);
    assert(__CPROVER_r_ok(ptr, 1));
    return ptr;
}

[tautschnig]

With regard to documentation, are you referring to the following: "If p is neither null nor valid, the semantics is unspecified." This doesn't say anything to the effect of "undefined behavior" (which is a term very specific to the C language/the C standard). If there is any place where we claim "undefined behavior," then we need to fix that documentation.

[celinval]

Fair, I don't think UB shows up in the documentation. However, writing proofs that rely on unspecified semantics is still wrong and potentially unsound.

[tautschnig]

How about: "If p is neither null nor valid, it is unspecified whether the predicate evaluates to true or false."

[celinval]

Unspecified semantics means that it is ok to always be true, which will make proofs unsound. @remi-delmas-3000 @zhassan-aws any suggestions on how to capture the expected behavior?

[tautschnig]

Let me first make sure that we agree on what it means to be sound here. My take on that is that an analysis (in this case: bounded model checking of the given C program) is sound for a given property p, if, and only if, it reports that p holds on that given program when p holds for all possible executions of the program under the semantics specified by the C language standard (pick your version) plus any additional specification of semantics given in our documentation when we the program uses language extensions provided by CBMC.

For the given example program, it seems sufficient to consider three equivalence classes of possible executions:

1. Executions where ptr points to some existing object and there is at least one more byte in that object beyond where ptr points to. Then __CPROVER_r_ok(ptr, 1) evaluates to true, and the assertion holds.
2. Executions where ptr points to the end of some existing object, i.e., we could only read zero more bytes. Then, __CPROVER_r_ok(ptr, 1) evaluates to false, the assertion fails.
3. Executions where ptr does not point to any existing object. With the above definition of soundness, only the case where the analysis reports the assertion to hold is of interest. Our documentation, which at this point extends the language standard, says that __CPROVER_r_ok(ptr, 1) may take any value when ptr does not point to any existing object. So it could return true under all exections where ptr does not point to any existing object. Hence, the analysis appears sound when it reports the assertion to hold.

So: in what way does this make proofs unsound?

[celinval]

The execution 3 is the one that I was considering unsound, but I agree with you that according to the API specification this is perfectly fine.

It sounds that this is a misunderstanding on my part that using this API inside an assertion should be safe even if the pointer is invalid. But this is not correct, and it only applies today given its current implementation.

[remi-delmas-3000]

@tautschnig Indeed if we agree that __CPROVER_r_ok is unspecified on invalid pointers, then returning true for invalid pointers is an acceptable interpretation of the predicate, and reporting that assert(__CPROVER_r_ok(ptr, 1)) holds when ptr is or may be invalid is sound.

However this also implies that __CPROVER_r_ok cannot be used to detect occurrences of invalid pointers.

I have looked at how --pointer-primitive-check are instantiated, in practice the verification conditions seem identical or even weaker to that of __CPROVER_r_ok, so it seems like pointer primitive checks cannot reliably detect invalid pointers either, hence the impression that there is no way to detect invalid pointers.

[celinval]

I totally agree @remi-delmas-3000. I created #8217 to capture the request to provide an API to detect invalid pointers.

[celinval]

Reopening this based on this comment: #8217 (comment)