Fix Apron handling of escaped locals

[michael-schwarz]

Fix Apron’s handling of locals whose addresses escape through global pointers.

In single-threaded execution, escaped locals were read using their local relational variable but written using a separate global relational variable. Calls could also omit escaped locals from callee states and restore stale pre-call relations afterward. This allowed Apron to retain relations invalidated by indirect writes.

This change:

• consistently updates escaped locals using their local relational variables before entering multithreaded mode;
• retains escaped locals in callee relational states;
• avoids restoring stale pre-call relations for escaped locals;
• adds regressions for both entirely single-threaded execution and entering multithreaded mode inside the callee.

Tested with:

• opam exec -- scripts/update_suite.rb group apron3 -q
• opam exec -- dune build @runaprontest --display quiet

Closes #2091.

[jprotopopov-ut]

Locally, the change appears fine, although to me it looks like a whack-a-mole fix. For what it's worth, I tried to prompt AI to poke holes in the code for counterexamples, and (before the session got derailed by cybersecurity guardrails) it got me the following adjacent case:

// PARAM: --set ana.activated[+] apron --enable ana.sv-comp.functions
#include <goblint.h>
#include <string.h>

static int *target;

static void modify(void) {
  *target = __VERIFIER_nondet_int();
}

int main(void) {
  int left = __VERIFIER_nondet_int();
  int right = left;
  int *source = &right;
  memcpy(&target, &source, sizeof(target));

  modify();
  __goblint_check(left == right); // UNKNOWN!
}

which crashes Goblint with

Fatal error: exception Apron.Manager.Error
 {  exn = Exc_invalid_argument; funid = Funid_assign_texpr_array;
  msg = unknown variable right#671 in the environment; }

Given that the failure is different from the original one, I am approving this pull request.

[michael-schwarz]

Although to me it looks like a whack-a-mole fix.

I took a look at your example, thank you! I think the issue there is fundamentally different. The problem is that the escape analysis does not consider the escape via memcpy. This also leads to an unsoundness in the base issue.

// PARAM: --enable ana.sv-comp.functions
#include <goblint.h>
#include <pthread.h>
#include <string.h>

static int *target;

static void *modify(void *arg) {
  *target = 7;
  return NULL;
}

int main(void) {
  int right = 42;
  int *source = &right;
  memcpy(&target, &source, sizeof(target));

  pthread_t thread;
  pthread_create(&thread, NULL, modify, NULL);
  pthread_join(thread, NULL);

  __goblint_check(right == 42); // Incorrectly succeeds
}

Given that there it is an issue with threadEscape affecting different analyses, I'll move it to a separate issue.

[michael-schwarz]

@sim642: Can you have another look so we can merge? Or is this subsumed by one of your larger redsigns, in which cas we shoudl close this?