Incorrect encoding of function pointer operations in CBMC #7213
Assignees
Labels
Comments
feliperodri
added
bug
aws
|
The example can be distilled down to this. #include <assert.h>
struct s_t {
int value;
};
struct s_t a = {.value = 0};
struct s_t b = {.value = 1};
int main() {
struct s_t *ptr;
__CPROVER_assume(ptr == &a || ptr == &b);
assert(ptr == &a || ptr == &b);
// if the assertion above holds then this should also hold
assert(ptr->value == 0 || ptr->value == 1);
return 0;
}The underlying problem is that pointer dereference depends on the value set associated with the pointer, and that the value set only reflects imperative updates made to the pointer and not declarative assumptions. |
|
I believe that #6326 was built to specifically address this case. Would adding explicit nondet initialisers solve the problem? |
|
Adding a nondet initializer does not seem to fix the problem: #include <assert.h>
struct s_t {
int value;
};
struct s_t a = {.value = 0};
struct s_t b = {.value = 1};
struct s_t *nondet_ptr();
int main() {
struct s_t *ptr = nondet_ptr();
__CPROVER_assume(ptr == &a || ptr == &b);
assert(ptr == &a || ptr == &b);
struct s_t * dummy_a = &a;
struct s_t * dummy_b = &b;
struct s_t * dummy_ptr = ptr;
int dummy_ptr_value = ptr->value;
// passes
assert(a.value == 0 && b.value == 1);
// fails with ptr->value == 3
assert(ptr->value == 0 || ptr->value == 1);
return 0;
} |
|
@remi-delmas-3000 haven't you address this issue with the latest DFCC work? |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
CBMC version: 5.67.0
Operating system: N/A
How to reproduce
Run
make all.Assertions are falsified when they shouldn't.
The issue
Consider the function below:
The contract says that the
obj->ftblcan point toftbl_0orftbl_1, two static structs that contain a field.set_valuewhich is a function pointer to functionset_value_0orset_value_1respectively. The contract declares the conditions under whichftbl_0orftlb_1gets used, and ensures the post conditions of whichever one is used. The contract and implementation are correct wrt each other.Yet the verification of this contract fails.
for the
postcondition.1assertion: The function table in dummy0 is set to ftbl_1, but extracting the function from the function table yields set_value_0 in dummy_1, should be set_value_1. So it really seems like any value can be dreamed up from this function pointer.For the
set_value.assertion.2assertion: the null function pointer back-propagates through the dummy assignments:for the
set_value.assertion.3, thedummy3 function pointer is equal toset_value_0` + a non-zero offset ?(Are function pointers encoded as object pointers in CBMC ?)
Here’s what is odd (in the program dump obtained using
cbmc --program-only ...):when
dummy1gets assigned fromdummy0it seems likecbmcassumes rather arbitrarily thatdummy0.ftblis eitherftbl_0or some invalid object and can be nothing else.However, what the contract tries to say is that
dummy0is free function pointer required to be equal to one of two possible addresses&ftbl_0or&ftbl_1(see the contract's__CPROVER_requiresclauses of the contract).So we see that this C code
yields this goto code :
and this realtively similar C-code :
yields this very different goto code:
I would have expected something like
It may be the encoding of the deref operation on
*(dummy.ftbl)(sincedummy0.ftblis a pointer, the deref could fail)so this is modelled like this, but it still does not explain why CBMC assumes that
dummy0!0@1#2..ftblcan only be equal to&ftbl_0(in reality it can also point to&ftbl_1).Next investigation steps
The text was updated successfully, but these errors were encountered: