A question on pointer operations with CBMC

[fangyi-zhou]

I have the question when I play around uintptr_t with CBMC

#include <stdio.h>
#include <stdint.h>

int main() {
    int x;
    int * ptr = &x;
    *ptr = 42;
    uintptr_t uptr = (uintptr_t) ptr;
    uptr = ~uptr;
    uptr = ~uptr;
    int * ptr2 = (int *) uptr;
    __CPROVER_assert(ptr == ptr2, "pointer is identical");
    printf("*ptr = %d, *ptr2 = %d\n", *ptr, *ptr2);
    __CPROVER_assert(*ptr == *ptr2, "pointer dereferenced is identical");
}

Result by CBMC:

CBMC version 5.8 64-bit x86_64 macos
Parsing ptr.c
Converting
Type-checking ptr
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 46 steps
simple slicing removed 5 assignments
Generated 2 VCC(s), 2 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
330 variables, 205 clauses
SAT checker: instance is SATISFIABLE
Solving with MiniSAT 2.2.1 with simplifier
330 variables, 0 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime decision procedure: 0.002s

** Results:
[main.assertion.1] pointer is identical: SUCCESS
[main.assertion.2] pointer dereferenced is identical: FAILURE

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

It is interesting why the pointers are identical, but the dereferenced pointers are not. With a trace, I made the following discovery:

State 20 file ptr.c line 6 function main thread 0
----------------------------------------------------
  ptr=&x!0@1 (0000001000000000000000000000000000000000000000000000000000000000)

(omitted)

State 27 file ptr.c line 11 function main thread 0
----------------------------------------------------
  ptr2=&x!0@1 (0000001000000000000000000000000000000000000000000000000000000000)
*ptr = 42, *ptr2 = 16384

For some reason, *ptr is 16384.

While I'm not entirely sure whether my code is triggering any undefined behaviour because C standard only guarantees that uintptr_t can be used for casting from and to void*, without specifying any operations permitted on the data type. The result of CBMC is cryptic and difficult to understand.

[fangyi-zhou]

Seems to be fixed on master. Closing.

(previous code has uptr &= ~(uintptr_t) 0U instead of 2 bitwise NOT)

[fangyi-zhou]

Looks like it's fixed by #1226 because ANDing with all 1 bits get simplified out.

New way to reproduced bug: applying bitwise NOT twice: uptr = ~uptr; uptr = ~uptr;

Reopening the issue with updated sample/result

[tautschnig]

This is a bug in value sets, because dereferencing ptr2 currently only yields __CPROVER_memory.

[fangyi-zhou]

int main() {
    int x;
    int * p = &x;
    *p = 1;
    int * q;
    __CPROVER_assume(p == q);
    __CPROVER_assert(*p == *q, "Dereferenced pointers have the same value");
}

A more straightforward example. I suspect pointer equality does not imply equality of the pointer metadata and the provenance so CBMC was not able to do further deductions.

[tautschnig]

Assumes are actually a slightly different problem (I think), which are also documented in the KNOWNBUG-regression test regression/cbmc/Pointer_Assume1. Either way, dereferencing needs work. (This is known, but finding time to work on it is not a solved problem.)

[fangyi-zhou]

Thanks for taking the time to have a look.

[fangyi-zhou]

If the deductions have been made that two pointers are equal, the issue will occur. So it is not limited to assume.

int main() {
    int x, *p, *q;
    x = 42;
    p = &x;
    if (q != p) return -1;
    __CPROVER_assert(p == q, "pointer equal");
    __CPROVER_assert(*p == *q, "dereference equal");
}

Another sample, this shares some similarities with the first sample. The pointer equalities are able to establish.

[TGWDB]

Can no longer reproduce, closing. Please reopen if you believe this is erroneous.