Open michael-schwarz opened 5 months ago
The easy workaround would be to just allow constant 0 index offset on a struct as a no-op.
However, I think we might have a deeper issue here: axel.conn + 0
is a perfectly valid addition of a constant to a pointer (to a struct). Somehow we forget about the pointer being there.
Somehow we forget about the pointer being there.
What do you mean by this? The points-to set for ptr
is { str[0].b }
which seems ok!
The points-to set for
ptr
is{ str[0].b }
which seems ok!
But it isn't OK because it's indexing a struct. That indexing should not be there at all, because really it just points to str.b
.
The indexing would be valid if there was a pointer to the first element of an array:
struct a {
pthread_mutex_t b;
};
struct c {
struct a *conn;
} d();
int main() {
struct a str[1] = {0};
struct c axel = {0};
axel.conn = &str;
pthread_mutex_t* ptr = &((axel.conn + 0)->b);
pthread_mutex_lock(ptr);
pthread_mutex_unlock(ptr);
pthread_mutex_lock(&((axel.conn + 0)->b));
}
Here str[0].b
would be right.
Somewhere in the pointer arithmetic we're going wrong and assuming an array where there isn't one. This probably stems from the fact that arrays are the same as their first element pointer in such code.
In 811c183, I made a hotfix to be able to continue benchmarking that catches this error and errors and returns a top of the corresponding type. Do we also want to have this hotfix on master?
Debugging revealed that this is caused by the line: https://github.com/goblint/analyzer/blob/a0309d10f311222c6f3757127dfe1c0bfd52e551/src/analyses/base.ml#L287
evalbinop_mustbeequal
calls evalbinop_base
with a1: {&str}
a2: 0
t1: struct a *
t2: int
evalbinop_base
, Addr.to_mval addr
gives x: str
and o: NoOffset
, where addToOffset
is calledaddToOffset
the NoOffset
case returns Index
For the following program (extracted from the
axel
benchmark of Concrat), Goblint crashes withwhereas
gcc -Wall
accepts the program without any issues.