`mallocFresh` unsound due to blob non-uniqueness

While working on #1069, there was some behavior which seemed suspect. Namely that p->a = q->b style assignments where p and q point to the same fresh blob should not cause it to escape, but remain fresh, such that no race is reported. This is a pattern from the silver searcher.

But this style of exclusion is not sound since there's no guarantee that p and q point to the same physical memory, we just have the same alloc varinfo for it. #1069 is not at fault here, the issue exists already in the master version of mallocFresh.

The analysis is sound with region, from which mallocFresh was extracted, because region does not even distinguish allocation sites, but simply uses bullet for all of them. mallocFresh was made slightly more precise to handle some interactive story by maintaining a set of fresh alloc variables, but already this change is enough to turn it unsound.

I'm not sure if it's possible to fix this without making mallocFresh even less precise than it already is (and it is very!). Maybe some recency thing is the only way? Having separate varinfos for fresh and non-fresh/escaped blobs would allow distinguishing which instance a pointer is pointing to.

Example

Should report a race on the next field, but does not.

// PARAM: --set ana.activated[+] mallocFresh --set ana.activated[-] mhp --set ana.thread.domain plain
#include <pthread.h>
#include <stdlib.h>

struct s {
  struct s *next;
};

struct s *g = NULL;
pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;

void *t_fun(void *arg) {
  pthread_mutex_lock(&A);
  struct s *r = g->next; // RACE!
  pthread_mutex_unlock(&A);
  return NULL;
}

struct s* alloc_s() {
  return malloc(sizeof(struct s));
}

int main() {
  struct s *p, *q;
  int r;

  pthread_t id;
  pthread_create(&id, NULL, t_fun, NULL);

  p = alloc_s();
  // p->next = NULL; // NORACE (fresh)
  pthread_mutex_lock(&A);
  g = p; // NORACE
  pthread_mutex_unlock(&A);

  q = alloc_s(); // UNSOUND: same alloc varinfo without wrapper becomes fresh again!
  // q->next = NULL; // NORACE (fresh)

  // p and q point to same blob, so accessing via both should race
  if (r)
    p->next = q; // RACE!
  else
    g->next = q; // RACE!
  return 0;
}

The mallocFresh extracted from region shows a race between struct s *r = g->next; (read) and g->next = q; (write) but there is no race on the access of p->next = q;, showing that this attempt on extracting mallocFresh from region is unsound.

./goblint --enable warn.debug --enable dbg.regression --html --set ana.activated[+] region --set ana.activated[-] mhp --set ana.thread.domain plain --enable allglobs tests/regression/09-regions/41-malloc_fresh.c
[Warning][Race] Memory location (alloc@sid:18@tid:main(#top)).next (race with conf. 110): (tests/regression/09-regions/41-malloc_fresh.c:20:3-20:34)
  write with thread:main (conf. 110)  (exp: & g->next) (tests/regression/09-regions/41-malloc_fresh.c:43:5-43:16)
  read with lock:{A} (conf. 110)  (exp: & g->next) (tests/regression/09-regions/41-malloc_fresh.c:14:12-14:24)
[Success][Race] Memory location (alloc@sid:18@tid:main(#top)).next (safe): (tests/regression/09-regions/41-malloc_fresh.c:20:3-20:34)
  write with [region:no region, thread:main] (conf. 110)  (exp: & p->next) (tests/regression/09-regions/41-malloc_fresh.c:41:5-41:16)
[Success][Race] Memory location g (safe): (tests/regression/09-regions/41-malloc_fresh.c:9:10-9:18)
  write with [region:{g}, lock:{A}, thread:main] (conf. 110)  (exp: & g) (tests/regression/09-regions/41-malloc_fresh.c:33:3-33:8)
  read with [region:{g}, lock:{A}] (conf. 110)  (exp: & g) (tests/regression/09-regions/41-malloc_fresh.c:14:12-14:24)
  read with [region:{g}, thread:main] (conf. 110)  (exp: & g) (tests/regression/09-regions/41-malloc_fresh.c:43:5-43:16)

goblint / analyzer

`mallocFresh` unsound due to blob non-uniqueness #1070

Example