Escaped variables are not communicated between threads

[jerhard]

In this test case, Goblint, with the default configuration, does not relax information about the escaped local variables x, even though another thread may be writing into it. In particular, Goblint unsoundly claims that the second __goblint_check will succeed:

analyzer/tests/regression/74-escape/01-local-esacpe.c

Lines 9 to 17 in 8dcc0b0

	int let_escape(){
	int x = 23;
	g = 23;
	__goblint_check(x == 23);
	p = &x;
	sleep(5);
	__goblint_check(x == 23); //UNKNOWN!
	}

[jerhard]

When *p is written in thread2, it the Base analysis knows that p may point to x, however is_global ask x returns false. This is due to the ThreadEscape analysis claiming that x has not escaped.

For the MayEscape x query, the ThreadEscape analysis looks up whether x is in its local state. But x escaped in thread1, and there seems to be no synchronization of this information to the analysis of thread2. So one somehow needs to answer the MayEscape queries based on some flow-insensitive-invariant.
There may be some ways to avoid being completely flow-insensitive by excluding some escapes that definitely have not happened yet: e.g. when there is a unique thread, a local variable of it must have escaped in its own past, to be considered esacped.
@michael-schwarz and I discussed some of this shortly yesterday.

[sim642]

In #686 we already added a global invariant to the threadescape analysis. Do you know why that doesn't already account for this?

[jerhard]

In the current state of the analysis, there is no ctx.getg, i.e. things that are side-effected are never considered, also not when answering queries.

Actually, in special and threadenter, the ctx.global is called, but this is not sufficient.