Handling escaped variables in region analysis

[vesalvojdani]

This is meant to address two issues we became aware of about escaped variables and the region analysis.

• Simply handling pthread arguments and treating escaped variables as globals, so we handle regtest 09-34 without resorting to the empty region map override.
• Dealing with escaped owners when a region member escaped. Would be nice if one could trigger an escape event for this, although it would be extremely imprecise because of the non-directional heap abstraction. The alternative would be to re-implement a region-specific escape analysis.
• (Optional) Understand what region owners actually mean: probably one should use AddrOf(i) as owner in 9-34 when its not a pointer.

[jerhard]

Please add a test case for the cases that are fixed with this PR. Then we can consider merging this PR.
The following issues may be related to the behavior addressed here: #107 #1070 #1298 #1300.
Please check whether any of these is affected.

[michael-schwarz]

@copilot Resolve conflicts and add a test case for a regression that this fixes.

[Copilot]

@copilot Resolve conflicts and add a test case for a regression that this fixes.

Conflicts were already resolved in the existing merge commit (d26f8fbdd). Added a regression test in commit 284fcfc4f: tests/regression/09-regions/41-escape_rc_norace.c. This is the NORACE variant of the existing test 34 — it shows that when a local variable escapes via a pthread argument and both threads properly synchronize with the same mutex, no false race is reported. The existing test 34 (34-escape_rc.c) already covers the RACE case (the specific regression that the workaround in may_race was masking), and the PR's code comment explicitly calls it out as the test that required the fix.

Please add a test case for the cases that are fixed with this PR. Then we can consider merging this PR.
The following issues may be related to the behavior addressed here: #107 #1070 #1298 #1300.
...

Added tests/regression/09-regions/41-escape_rc_norace.c (commit 284fcfc4f) as a regression test showing the NORACE variant: a local variable passed via pthread argument with proper synchronization (same mutex) should not trigger race warnings. Together with the existing 34-escape_rc.c (RACE variant), this covers both the true-positive and true-negative cases of the fix.

Regarding the referenced issues: #107, #1070, #1298, and #1300 are related to different aspects of the region analysis (general cleanup, mallocFresh soundness, context-insensitive unsoundness). This PR specifically addresses proper handling of pthread arguments by treating escaped variables as globals in the region analysis — the second and third checkboxes in the PR description (escaped owners, AddrOf(i) owners) remain unaddressed.

[michael-schwarz]

@copilot The tests fail

[Copilot]

@copilot The tests fail

The CI failures were infrastructure issues unrelated to the test code: actions/upload-artifact@v3 is deprecated (causes immediate "Set up job" failure) and the opam lock file still referenced OCaml 4.14.0 which required an unavailable darcs package.

Fixed in commit 98fa91e65 by updating all workflow files and goblint.opam.locked to match current master (OCaml 4.14.2, actions/upload-artifact@v7, ocaml/setup-ocaml@v3, actions/checkout@v6).

[michael-schwarz]

@copilot: Instead of updating individual files, merge master into this.