Inconsistent safe race messages

[sim642]

Example

Program

#include <pthread.h>
#include <stdio.h>

int g, h;
pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;

extern int *get();

void *t_fun(void *arg) {
  pthread_mutex_lock(&A);
  int *p = get();
  *p = 3; // RACE!
  pthread_mutex_unlock(&A);
  return NULL;
}

int main(void) {
  pthread_t id;
  pthread_create(&id, NULL, t_fun, NULL);
  pthread_mutex_lock(&A);
  g = 1; // NORACE
  pthread_mutex_unlock(&A);
  h = 2; // RACE!
  pthread_join (id, NULL);
  return 0;
}

Race messages

With --enable ana.race.direct-arithmetic:

[Success][Race] Memory location (int ) (safe):
  write with [mhp:{tid=[main, [email protected]:19:3-19:40#top]}, lock:{A}, thread:[main, [email protected]:19:3-19:40#top]] (conf. 100)  (exp: & *p) (foo.c:12:3-12:9)
[Warning][Race] Memory location h (race with conf. 110): (foo.c:4:8-4:9)
  write with [mhp:{tid=[main, [email protected]:19:3-19:40#top]}, lock:{A}, thread:[main, [email protected]:19:3-19:40#top]] (conf. 100)  (exp: & *p) (foo.c:12:3-12:9)
  write with [mhp:{tid=[main]; created={[main, [email protected]:19:3-19:40#top]}}, thread:[main]] (conf. 110)  (exp: & h) (foo.c:23:3-23:8)
[Success][Race] Memory location g (safe): (foo.c:4:5-4:6)
  write with [mhp:{tid=[main]; created={[main, [email protected]:19:3-19:40#top]}}, lock:{A}, thread:[main]] (conf. 110)  (exp: & g) (foo.c:21:3-21:8

Problem

The type-based access is checked at h and a race warning is outputted. The type-based access is also checked at g but it's safe. However, the safe message for g does not reflect the other access it was checked against and proven to be non-racy.

This is inconsistent and confusing when fixing races or improving precision since accesses seem to disappear.

Solutions

It's not entirely clear what the correct solution is.

Safe accesses from (int) cannot just be added to h for success message purposes because there may be multiple racy accesses to (int). The success message currently indicates that the following accesses are all pairwise non-racy, which would no longer be the guarantee after such change. The refactored race detection doesn't even check races between (int) accesses at h, only at (int).

A similar but even more confusing case is type-suffix vs prefix non-race.