All Non-Relational Privatizations except Miné-W unsound #1457
Description
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.