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.

[sim642]

How come this is different from the make_callee_rel change above?
Previously, both used the exact same condition (negated) to either remove or keep the corresponding locals.
Now, they are no longer symmetric like that.

[michael-schwarz]

It is not semantically different here, it's just that I broke the symmetry in formatting. I have restored the symmetry now.

[sim642]

Initially I thought so too that it's just different formatting, but that's not true.
For an escaped local:

• Before the symmetry fix, this immediately goes to false.
• After the symmetry fix, all the negated escape condition does is not allow it to go to that true. But there are other Local cases below with different conditions that may still return true.

[michael-schwarz]

That's true, I hadn't thought about this. Looking at it, the case where this can now actually go to true is

| Some ((Local v | Global v)) when not (TaintPartialContexts.VS.mem v tainted_vars) -> true (* keep locals and globals, which have not been touched by the call *)

This is correct: If the escaped variable was definitely not modified in the callee, we can preserve the caller state.