Buggy handling of assignments involving pointer dereference

[nianzelee]

• CBMC version: 6.5.0
• OS: Ubuntu 24.04
• Command: cbmc <mwe below>
• MWE triggering the issue:

#include <assert.h>

typedef struct {
    unsigned long long r;
} state_t;

typedef struct {
    state_t reg;
    state_t *ptr_reg;
} module_t;

module_t data;
state_t state;

extern void abort(void);
void assume_abort_if_not(int cond) {
    if (!cond)
        abort();
}

int main() {
    __CPROVER_havoc_object(&data);
    __CPROVER_havoc_object(&state);
    assume_abort_if_not(data.ptr_reg == &state);

    state_t shadow_1 = data.reg;
    assert(data.reg.r == shadow_1.r);

    state_t shadow_2 = *data.ptr_reg;
    assert((*data.ptr_reg).r == shadow_2.r);

    return 0;
}

• CBMC output:

CBMC version 6.5.0 (cbmc-6.5.0) 64-bit x86_64 linux
Type-checking minimal
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Passing problem to propositional reduction
converting SSA
Running propositional reduction
SAT checker: instance is SATISFIABLE
Running propositional reduction
SAT checker inconsistent: instance is UNSATISFIABLE

** Results:
minimal.c function main
[main.assertion.1] line 27 assertion data.reg.r == shadow_1.r: SUCCESS
[main.pointer_dereference.1] line 29 dereference failure: pointer NULL in *data.ptr_reg: SUCCESS
[main.pointer_dereference.2] line 29 dereference failure: pointer invalid in *data.ptr_reg: SUCCESS
[main.pointer_dereference.3] line 29 dereference failure: deallocated dynamic object in *data.ptr_reg: SUCCESS
[main.pointer_dereference.4] line 29 dereference failure: dead object in *data.ptr_reg: SUCCESS
[main.pointer_dereference.5] line 29 dereference failure: pointer outside object bounds in *data.ptr_reg: SUCCESS
[main.pointer_dereference.6] line 29 dereference failure: invalid integer address in *data.ptr_reg: SUCCESS
[main.assertion.2] line 30 assertion (*data.ptr_reg).r == shadow_2.r: FAILURE
[main.pointer_dereference.7] line 30 dereference failure: pointer NULL in data.ptr_reg->r: SUCCESS
[main.pointer_dereference.8] line 30 dereference failure: pointer invalid in data.ptr_reg->r: SUCCESS
[main.pointer_dereference.9] line 30 dereference failure: deallocated dynamic object in data.ptr_reg->r: SUCCESS
[main.pointer_dereference.10] line 30 dereference failure: dead object in data.ptr_reg->r: SUCCESS
[main.pointer_dereference.11] line 30 dereference failure: pointer outside object bounds in data.ptr_reg->r: SUCCESS
[main.pointer_dereference.12] line 30 dereference failure: invalid integer address in data.ptr_reg->r: SUCCESS

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

A false alarm is reported for the second assertion, following an assignment that involves a pointer dereference.
The first assignment, which directly copies a struct, verifies correctly.
However, the second assignment—using pointer dereference to copy the struct—results in an assertion failure, even though the copied values are identical.

[tautschnig]

This would be solved by #8494: we currently do not update our alias information upon assumptions.

[kroening]

An uninitialized pointer doesn't become valid by branching on a condition on it.
For further background, read https://dl.acm.org/doi/pdf/10.1145/3290380

[nianzelee]

Thanks for the prompt reply and information! I will take a look and adjust the encoding if necessary.

[tautschnig]

An uninitialized pointer doesn't become valid by branching on a condition on it. For further background, read https://dl.acm.org/doi/pdf/10.1145/3290380

But then __CPROVER_havoc_object is not part of the standard. To me, it doesn't seem unreasonable that this would create valid pointers?!

[kroening]

It is unreasonable to guarantee that the pointer out of __CPROVER_havoc_object is always valid. It's really not an object factory.

If it can be invalid, then the issue is that comparing with == doesn't imply that it is valid. There are many such scenarios. One is the case where two objects are adjacent in memory, and you increment a pointer to the first one until it becomes equal to the second one. Yes, equal as identified by ==, but not interchangeable.