Spurious type-based races for deep accesses to unknown pointers

[sim642]

Example

Program

// PARAM: --set lib.activated[+] zlib
#include <pthread.h>
#include <zlib.h>

void *t_fun(void *arg) {
  z_stream stream;
  inflateInit2(&stream, 32 + 15);
  return NULL;
}

int main(void) {
  pthread_t id;
  pthread_t id2;
  pthread_create(&id, NULL, t_fun, NULL);
  pthread_create(&id2, NULL, t_fun, NULL);
  return 0;
}

Races

[Warning][Race] Memory location (struct internal_state) (race with conf. 60):
  write with [mhp:{tid=[main, t_fun@tests/regression/04-mutex/01-simple_rc.c:14:3-14:40#top]}, thread:[main, t_fun@tests/regression/04-mutex/01-simple_rc.c:14:3-14:40#top]] (conf. 60)  (exp: & stream) (tests/regression/04-mutex/01-simple_rc.c:7:2-7:32)
  write with [mhp:{tid=[main, t_fun@tests/regression/04-mutex/01-simple_rc.c:15:3-15:41#top]}, thread:[main, t_fun@tests/regression/04-mutex/01-simple_rc.c:15:3-15:41#top]] (conf. 60)  (exp: & stream) (tests/regression/04-mutex/01-simple_rc.c:7:2-7:32)
  read with [mhp:{tid=[main, t_fun@tests/regression/04-mutex/01-simple_rc.c:14:3-14:40#top]}, thread:[main, t_fun@tests/regression/04-mutex/01-simple_rc.c:14:3-14:40#top]] (conf. 60)  (exp: & stream) (tests/regression/04-mutex/01-simple_rc.c:7:2-7:32)
  read with [mhp:{tid=[main, t_fun@tests/regression/04-mutex/01-simple_rc.c:15:3-15:41#top]}, thread:[main, t_fun@tests/regression/04-mutex/01-simple_rc.c:15:3-15:41#top]] (conf. 60)  (exp: & stream) (tests/regression/04-mutex/01-simple_rc.c:7:2-7:32)
[Warning][Race] Memory location (struct z_stream_s) (race with conf. 80):
  write with [mhp:{tid=[main, t_fun@tests/regression/04-mutex/01-simple_rc.c:14:3-14:40#top]}, thread:[main, t_fun@tests/regression/04-mutex/01-simple_rc.c:14:3-14:40#top]] (conf. 80)  (exp: & stream) (tests/regression/04-mutex/01-simple_rc.c:7:2-7:32)
  write with [mhp:{tid=[main, t_fun@tests/regression/04-mutex/01-simple_rc.c:15:3-15:41#top]}, thread:[main, t_fun@tests/regression/04-mutex/01-simple_rc.c:15:3-15:41#top]] (conf. 80)  (exp: & stream) (tests/regression/04-mutex/01-simple_rc.c:7:2-7:32)
  read with [mhp:{tid=[main, t_fun@tests/regression/04-mutex/01-simple_rc.c:14:3-14:40#top]}, thread:[main, t_fun@tests/regression/04-mutex/01-simple_rc.c:14:3-14:40#top]] (conf. 80)  (exp: & stream) (tests/regression/04-mutex/01-simple_rc.c:7:2-7:32)
  read with [mhp:{tid=[main, t_fun@tests/regression/04-mutex/01-simple_rc.c:15:3-15:41#top]}, thread:[main, t_fun@tests/regression/04-mutex/01-simple_rc.c:15:3-15:41#top]] (conf. 80)  (exp: & stream) (tests/regression/04-mutex/01-simple_rc.c:7:2-7:32)

Problem

There shouldn't be a race on the (struct z_stream_s) type because it is only accessed with a known pointer &stream. However, inflateInit2 writes its first argument deeply, so ReachableFrom &stream is used to find the written addresses. That also includes an unknown pointer from uninitialized pointer fields. That unknown pointer is turned into a type-based race warning for (struct z_stream_s), which is wrong because the unknown pointer isn't of that type, but (struct internal_state).

A proper solution would require ReachableFrom to return typed unknown pointers or something.