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]

analyzer/src/analyses/base.ml

Lines 1735 to 1743 in 5cd8650

	(* We start from the current state and an empty list of global deltas,
	* and we assign to all the the different possible places: *)
	let nst = AD.fold update_one lval st in
	(* if M.tracing then M.tracel "set" ~var:firstvar "new state1 %a" CPA.pretty nst; *)
	(* If the address was definite, then we just return it. If the address
	* was ambiguous, we have to join it with the initial state. *)
	let nst = if AD.cardinal lval > 1 then { nst with cpa = CPA.join st.cpa nst.cpa } else nst in
	(* if M.tracing then M.tracel "set" ~var:firstvar "new state2 %a" CPA.pretty nst; *)
	nst

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