Goblint is currently not sound in some cases when dealing with offsets taken on casted pointers.
1. Comparison of casted pointers with offsets
On the current master, Goblint claims that the last two asserts will pass, even though they actually fail when compiled with Gcc. For the first two asserts Goblint says that the result is unknown, but this sound imprecision seems more incidental.
|
char* a_intoffset =(char*) (a + 1); |
|
char* b_intoffset = b_char + sizeof(int); |
|
|
|
__goblint_check(a_intoffset == b_intoffset); |
|
__goblint_check((char*) (a + 1) == b_char + sizeof(int)); |
|
|
|
char* a_4intoffset = (char*) (a + 4); |
|
|
|
__goblint_check(a_4intoffset == b_intoffset); // FAIL |
|
__goblint_check((char*) (a + 4) == b_char + sizeof(int)); // FAIL |
In the example, the char-pointer b_char points to the int-array a. Then, in a conccrete runIn line 22, the variable a_4intoffset points to &a[4], whereas b_intoffset points to (char* a) + 4 = (int* a) + 1 = &a[1].
When creating the index offset in the abstraction, Goblint currently does not take into account the static type of the pointer the offset is taken from. Thus, for b_intoffset, it keeps &a with offset 4 as its value, the same as for a_4intoffset.
2. Reading and writing with casted pointers with offsets
Reading from and writing to an address with such an offsets also needs to be handled soundly. In particular, code casting b_intoffset back to int* and dereferencing it should be soundly abstracted.
A related issue is #582, where only parts of a variable are overwritten with a char-pointer, and Goblint does not yield a sound value for a subsequent read. In #582, however, no offsets are involved.
Goblint is currently not sound in some cases when dealing with offsets taken on casted pointers.
1. Comparison of casted pointers with offsets
On the current
master,Goblintclaims that the last two asserts will pass, even though they actually fail when compiled with Gcc. For the first two asserts Goblint says that the result is unknown, but this sound imprecision seems more incidental.analyzer/tests/regression/69-addresses/02-array-cast.c
Lines 14 to 23 in 3cf768b
In the example, the char-pointer
b_charpoints to theint-arraya. Then, in a conccrete runIn line 22, the variablea_4intoffsetpoints to&a[4], whereasb_intoffsetpoints to(char* a) + 4 = (int* a) + 1 = &a[1].When creating the index offset in the abstraction,
Goblintcurrently does not take into account the static type of the pointer the offset is taken from. Thus, forb_intoffset, it keeps&awith offset4as its value, the same as fora_4intoffset.2. Reading and writing with casted pointers with offsets
Reading from and writing to an address with such an offsets also needs to be handled soundly. In particular, code casting
b_intoffsetback toint*and dereferencing it should be soundly abstracted.A related issue is #582, where only parts of a variable are overwritten with a char-pointer, and Goblint does not yield a sound value for a subsequent read. In #582, however, no offsets are involved.