Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Crash on pthread_mutex_lock with complicated argument #1421

Open
michael-schwarz opened this issue Apr 18, 2024 · 5 comments · May be fixed by #1480
Open

Crash on pthread_mutex_lock with complicated argument #1421

michael-schwarz opened this issue Apr 18, 2024 · 5 comments · May be fixed by #1480

Comments

@michael-schwarz
Copy link
Member

For the following program (extracted from the axel benchmark of Concrat), Goblint crashes with

Fatal error: exception Cilfacade.TypeOfError(typeOffset: Index on a non-array (0, struct a ))

struct a {
  pthread_mutex_t b;
};
struct c {
  struct a *conn;
} d();

int main() {
  struct a str = {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));
}

whereas gcc -Wall accepts the program without any issues.

@sim642
Copy link
Member

sim642 commented Apr 18, 2024

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.

@michael-schwarz
Copy link
Member Author

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!

@sim642
Copy link
Member

sim642 commented Apr 19, 2024

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.

michael-schwarz added a commit that referenced this issue Apr 19, 2024
@michael-schwarz
Copy link
Member Author

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?

@karoliineh
Copy link
Member

Debugging revealed that this is caused by the line:

| `NoOffset -> `Index(iDtoIdx n, `NoOffset)

  1. evalbinop_mustbeequal calls evalbinop_base with a1: {&str} a2: 0 t1: struct a * t2: int
  2. In evalbinop_base, Addr.to_mval addr gives x: str and o: NoOffset, where addToOffset is called
  3. And in addToOffset the NoOffset case returns Index

karoliineh added a commit that referenced this issue May 23, 2024
karoliineh added a commit that referenced this issue May 23, 2024
@karoliineh karoliineh linked a pull request May 23, 2024 that will close this issue
karoliineh added a commit that referenced this issue May 24, 2024
This reverts commit 3952a04.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants