Crash on `pthread_mutex_lock` with complicated argument

[michael-schwarz]

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]

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]

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]

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]

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]

Debugging revealed that this is caused by the line: https://github.com/goblint/analyzer/blob/a0309d10f311222c6f3757127dfe1c0bfd52e551/src/analyses/base.ml#L287

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