All Non-Relational Privatizations except Miné-W unsound

[michael-schwarz]

During #1456 I discovered that, in fact, all of our non-relational privatizations except the one casting Miné's analsysis in our framework are unsound.

// PARAM: --set ana.base.privatization protection --enable ana.int.enums
// Like 82-how-could-we-have-been-so-blind.c, but with syntactic globals instead of escaping ones.
#include<pthread.h>
#include<stdlib.h>
struct a {
  int b;
};

int *ptr;
int *immer_da_oane;

int da_oane = 0;
int de_andre = 42;

pthread_mutex_t m;

void doit() {
  pthread_mutex_lock(&m);
  *ptr = 5;

  // Should be either 0 or 5, depending on which one ptr points to
  int fear = *immer_da_oane;
  __goblint_check(fear == 5); //UNKNOWN!

  pthread_mutex_unlock(&m);

  pthread_mutex_lock(&m);
  // This works
  int hope = *immer_da_oane;
  __goblint_check(hope == 5); //UNKNOWN!
  pthread_mutex_unlock(&m);

}

void* k(void *arg) {
  // Force MT
  return NULL;
}

int main() {
    int top;

    if(top) {
      ptr = &da_oane;
    } else {
      ptr = &de_andre;
    }

    immer_da_oane = &da_oane;

    pthread_t t1;
    pthread_create(&t1, 0, k, 0);

    doit();
    return 0;
}

The problem is that upon setting *ptr = 5, all targets in the may-point-to-set are updated, rather than joining together the result of updating the different targets. This is likely due to some bot/top confusion inside the local states of the base analysis where the non-present bindings are all assumed to be \bot.

[michael-schwarz]

For protection, the problem seems to be that both get added to P when it should in fact be empty.

[michael-schwarz]

https://github.com/goblint/analyzer/blob/5cd8650a2872341152f48a7d1cd20ac9fa0de994/src/analyses/base.ml#L1735-L1743

In the set, it seems like we only join the cpa components after a non-definite assign and forget to also join priv components. :thinking: