Investigate: Need for sides-pp widening strategy exacerbated

[michael-schwarz]

While investigating why #1500 leads to privatizations not terminating without the hack from #1475, I discovered that this seems to be due to some widening not happening as expected:

// SKIP PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet
// XXXX Add this to fix it  --set solvers.td3.side_widen sides-pp
#include <pthread.h>
#include <goblint.h>

int g;
pthread_mutex_t m = PTHREAD_MUTEX_INITIALIZER;

void fn() {
  // Just do nothing
  return;
}

void *t_fun(void *arg) {
  pthread_mutex_lock(&m);
  g = g+1;
  fn();
  pthread_mutex_unlock(&m);
  return NULL;
}

int main() {
  pthread_t id;
  pthread_create(&id, NULL, t_fun, NULL);

  return 0;
}

%%% solside: side to G:apron:MUTEX_INITS (wpx: false) from Some(L:node 9 "return;" on tests/regression/46-apron2/89-sides-pp.c:11:3-11:9): lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+6.>=0|] (env: [|0> g:int|]) -> lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+7.>=0|] (env: [|0> g:int|])
%%% solside: side to G:apron:MUTEX_INITS (wpx: false) from Some(L:node 9 "return;" on tests/regression/46-apron2/89-sides-pp.c:11:3-11:9): lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+7.>=0|] (env: [|0> g:int|]) -> lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+8.>=0|] (env: [|0> g:int|])
%%% solside: side to G:apron:MUTEX_INITS (wpx: false) from Some(L:node 9 "return;" on tests/regression/46-apron2/89-sides-pp.c:11:3-11:9): lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+8.>=0|] (env: [|0> g:int|]) -> lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+9.>=0|] (env: [|0> g:int|])
%%% solside: side to G:apron:MUTEX_INITS (wpx: false) from Some(L:node 9 "return;" on tests/regression/46-apron2/89-sides-pp.c:11:3-11:9): lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+9.>=0|] (env: [|0> g:int|]) -> lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+10.>=0|] (env: [|0> g:int|])
%%% solside: side to G:apron:MUTEX_INITS (wpx: false) from Some(L:node 9 "return;" on tests/regression/46-apron2/89-sides-pp.c:11:3-11:9): lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+10.>=0|] (env: [|0> g:int|]) -> lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+11.>=0|] (env: [|0> g:int|])
%%% solside: side to G:apron:MUTEX_INITS (wpx: false) from Some(L:node 9 "return;" on tests/regression/46-apron2/89-sides-pp.c:11:3-11:9): lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+11.>=0|] (env: [|0> g:int|]) -> lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+12.>=0|] (env: [|0> g:int|])
%%% solside: side to G:apron:MUTEX_INITS (wpx: false) from Some(L:node 9 "return;" on tests/regression/46-apron2/89-sides-pp.c:11:3-11:9): lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+12.>=0|] (env: [|0> g:int|]) -> lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+13.>=0|] (env: [|0> g:int|])
%%% solside: side to G:apron:MUTEX_INITS (wpx: false) from Some(L:node 9 "return;" on tests/regression/46-apron2/89-sides-pp.c:11:3-11:9): lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+13.>=0|] (env: [|0> g:int|]) -> lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+14.>=0|] (env: [|0> g:int|])
%%% solside: side to G:apron:MUTEX_INITS (wpx: false) from Some(L:node 9 "return;" on tests/regression/46-apron2/89-sides-pp.c:11:3-11:9): lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+14.>=0|] (env: [|0> g:int|]) -> lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+15.>=0|] (env: [|0> g:int|])
%%% solside: side to G:apron:MUTEX_INITS (wpx: false) from Some(L:node 9 "return;" on tests/regression/46-apron2/89-sides-pp.c:11:3-11:9): lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+15.>=0|] (env: [|0> g:int|]) -> lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+16.>=0|] (env: [|0> g:int|])
%%% solside: side to G:apron:MUTEX_INITS (wpx: false) from Some(L:node 9 "return;" on tests/regression/46-apron2/89-sides-pp.c:11:3-11:9): lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+16.>=0|] (env: [|0> g:int|]) -> lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+17.>=0|] (env: [|0> g:int|])
%%% solside: side to G:apron:MUTEX_INITS (wpx: false) from Some(L:node 9 "return;" on tests/regression/46-apron2/89-sides-pp.c:11:3-11:9): lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+17.>=0|] (env: [|0> g:int|]) -> lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+18.>=0|] (env: [|0> g:int|])
%%% solside: side to G:apron:MUTEX_INITS (wpx: false) from Some(L:node 9 "return;" on tests/regression/46-apron2/89-sides-pp.c:11:3-11:9): lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+18.>=0|] (env: [|0> g:int|]) -> lifted lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)) and contexts:lifted deadbranch and HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):deadbranch:MCP.G:apron:[|g>=0; -g+19.>=0|] (env: [|0> g:int|])

It seems that there are perpetually increasing side-effects from the return node(?) of the procedure, that always seem to be in new contexts.
I will try to determine where exactly this behavior arose.

[michael-schwarz]

The change happened somewhere between bf05c63 and 06a2fa7.

[michael-schwarz]

The commit that causes this regression is f41176c where sync Join edges are introduced for the start node of a procedure, because without a context-sensitive threadflag these are join points where we may go from single-threaded to multi-threaded mode.

[michael-schwarz]

This is somehow in the same vein as #1475, except that here it would even suffice for threadflag being context-sensitive to avoid having to do anything on thread creation.