Add flag to check pointer validity only for those pointer primitives that lack defined semantics for invalid pointers

[jimgrundy]

CBMC version: 5.34.0
Operating system: N/A

The CBMC Manual section on “Memory Primitives / Detecting potential misuses of memory primitives” (http://cprover.diffblue.com/memory-primitives.html#autotoc_md108) ends with the following text:

"While the first three primitives [__CPROVER_POINTER_OBJECT, __CPROVER_POINTER_OFFSET, and __CPROVER_same_object] have well-defined semantics even on invalid pointers, using them on invalid pointers is usually unintended in user programs. Thus, they have been included in the --pointer-primitive-check option."

We are encountering various cases where it is our intention to use these primitives on invalid pointers — specifically as assumptions about uninitialized pointers so as to constrain them. For example, we may malloc one pointer p and then seek to constrain a second pointer q to point into the same region as p.

To facilitate this without abandoning the pointer primitive checks entirely we need the addition of a new flag that causes CBMC to check for valid pointer use only on those primitives where behavior on invalid pointers is undefined. One possible name might be --lax-pointer-primitive-check. There are probably better ones.

It should be possible to use both this new flag (--lax-pointer-primitive-check) and the existing flag (--pointer-primitive-check) such that a #pragma can be used to disable just the stricter checks on a region of code.

[feliperodri]

We need to be careful while using these primitives in assumptions (see #6057). Instead of creating a new flag, we might want to consider updating the behavior of these primitives to properly handle invalid pointers (see the discussion #6045 (comment)). For instance, consider the following code snippet:

int *a = malloc(sizeof(*a));
int *b;
__CPROVER_assume(__CPROVER_same_object(a, b));
assert(__CPROVER_r_ok(a, sizeof(*a)));
assert(__CPROVER_r_ok(b, sizeof(*b)));

I'd assume that without the pointer primitive check, both assertions should be valid.

[feliperodri]

cc. @SaswatPadhi

[jimgrundy]

We need to be careful while using these primitives in assumptions (see #6057). Instead of creating a new flag, we might want to consider updating the behavior of these primitives to properly handle invalid pointers (see the discussion #6045 (comment)). For instance, consider the following code snippet:

int *a = malloc(sizeof(*a));
int *b;
__CPROVER_assume(__CPROVER_same_object(a, b));
assert(__CPROVER_r_ok(a, sizeof(*a)));
assert(__CPROVER_r_ok(b, sizeof(*b)));

I'd assume that without the pointer primitive check, both assertions should be valid.

[jimgrundy]

Sorry, didn't mean to close this issue, just close a comment window I had open. I'll get used to this interface.

Above, "__CPROVER_assume(__CPROVER_same_object(a, b));" may be insufficient to cause "b" to be a valid pointer, since while this constrains the object-id component of the pointer it does not constrain the offset component, and -ve offsets are used mark invalid pointers (from what I read in the manual), so you may have to make some further assumption that b's offset was non-negative. After that, I would expect the 2nd assertion to fail because b's offset may be such that it places b outside the range of the allocated region.

[jimgrundy]

Daniel's take on this is that, in fact, these three predicates dot no act correctly when used on invalid pointers, and so that issue here is not that we should have a new flag that would allow them to be so called, but rather that we should fix the documentation to say that they cannot.