Skip to content

Handling escaped variables in region analysis#989

Draft
vesalvojdani wants to merge 8 commits into
masterfrom
region-escape
Draft

Handling escaped variables in region analysis#989
vesalvojdani wants to merge 8 commits into
masterfrom
region-escape

Conversation

@vesalvojdani
Copy link
Copy Markdown
Member

@vesalvojdani vesalvojdani commented Feb 14, 2023

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.

@sim642 sim642 added the bug label Feb 14, 2023
@sim642 sim642 mentioned this pull request Nov 17, 2023
Merged
@sim642 sim642 self-requested a review July 16, 2024 11:44
@jerhard
Copy link
Copy Markdown
Member

jerhard commented Jul 16, 2024

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
Copy link
Copy Markdown
Member

michael-schwarz commented May 7, 2026

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

@michael-schwarz
Add regression test for pthread argument escape in region analysis
284fcfc 
Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/564e520d-ac51-4680-9e7c-99ad250e4cca

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
Copy link
Copy Markdown
Contributor

Copilot AI commented May 7, 2026 •
edited
Loading

@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
Copy link
Copy Markdown
Member

michael-schwarz commented May 7, 2026

@copilot The tests fail

Copilot AI requested a review from michael-schwarz May 7, 2026 10:53
@michael-schwarz
Update CI workflows and opam lock file to match current master
98fa91e 
Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/5c1f51c9-4cd4-4964-9e5a-bf78bfed7685

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
Copy link
Copy Markdown
Contributor

Copilot AI commented May 7, 2026

@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
Copy link
Copy Markdown
Member

michael-schwarz commented May 7, 2026

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sim642 sim642 Awaiting requested review from sim642

@michael-schwarz michael-schwarz Awaiting requested review from michael-schwarz

Copilot code review Copilot Awaiting requested review from Copilot Copilot will automatically review once the pull request is marked ready for review

At least 1 approving review is required to merge this pull request.

Assignees

No one assigned

Labels

bug

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@vesalvojdani @jerhard @michael-schwarz @sim642