Skip to content

Fix mutex-meet for malloc after thread creation#1492

Merged
sim642 merged 4 commits intomasterfrom
issue_1489
Jul 31, 2024
Merged

Fix mutex-meet for malloc after thread creation#1492
sim642 merged 4 commits intomasterfrom
issue_1489

Conversation

@michael-schwarz
Copy link
Copy Markdown
Member

@michael-schwarz michael-schwarz commented May 27, 2024 •
edited by sim642
Loading

The issue in #1489 was that the global invariant for the blob was still bot, making the meet deadcode.

TODO:

  • mutex-meet-atomic privatization still unsound
  • Verify if these are really all changes needed for mutex-meet-atomic (It seems weird that no handling of these cases is necessary in get_mutex_global_g_with_mutex_inits_atomic CC: @sim642)

Closes #1489

@michael-schwarz michael-schwarz added bug unsound relational Relational analyses (Apron, affeq, lin2var) labels May 27, 2024
@michael-schwarz michael-schwarz marked this pull request as draft May 27, 2024 15:48
@michael-schwarz michael-schwarz marked this pull request as ready for review May 27, 2024 15:56
@michael-schwarz michael-schwarz mentioned this pull request May 27, 2024
Closed
7 tasks
@sim642 sim642 self-requested a review May 28, 2024 07:13
@sim642
Copy link
Copy Markdown
Member

sim642 commented May 28, 2024

  • Verify if these are really all changes needed for mutex-meet-atomic (It seems weird that no handling of these cases is necessary in get_mutex_global_g_with_mutex_inits_atomic CC: @sim642)

That doesn't restrict unprotected invariants to a single variable, which if missing, causes bot. It might just be pushing the issue further down the line though: at some point there could still be an Apron assignment from that variable to something else. But maybe the variable will never be missing, rather some meet will just unify it to top?

@sim642
Copy link
Copy Markdown
Member

sim642 commented May 30, 2024

mutex:[__VERIFIER_atomic] also starts out with bottom (env: [||]), so that's not the difference I suspect. Rather, the difference comes from this check:

analyzer/src/analyses/apron/relationPriv.apron.ml

Lines 500 to 504 in 896f236

if not (RD.mem_var get_mutex_inits' g_var) then (* TODO: is this just a workaround for an escape bug? https://github.com/goblint/analyzer/pull/1354/files#r1498882657 *)
(* This is an escaped variable whose value was never side-effected to get_mutex_inits' *)
get_mutex_global_g
else
RD.join get_mutex_global_g get_mutex_inits'

get_mutex_global_g_with_mutex_inits_atomic doesn't have such condition and always does the join (with non-bottom), which makes everything fine.
I wonder if also checking RD.mem_var get_mutex_global_g g_var before doing this would be a fix closer to the existing logic.

@michael-schwarz michael-schwarz mentioned this pull request Jun 3, 2024
Closed
@DrMichaelPetter DrMichaelPetter linked an issue Jun 3, 2024 that may be closed by this pull request
Both branches dead in char_generic_nvram_read_nvram_write_nvram.i with octagon enabled analysis #1498
Closed
@sim642 sim642 added this to the v2.4.0 milestone Jun 25, 2024
@sim642 sim642 merged commit a592680 into master Jul 31, 2024
@sim642 sim642 deleted the issue_1489 branch July 31, 2024 07:19
@sim642 sim642 mentioned this pull request Oct 9, 2024
Closed
5 tasks
@michael-schwarz michael-schwarz mentioned this pull request Feb 17, 2025
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sim642 sim642 sim642 approved these changes

Assignees

No one assigned

Labels

bug relational Relational analyses (Apron, affeq, lin2var) unsound

Projects

None yet

Milestone

v2.4.0

Development

Successfully merging this pull request may close these issues.

Both branches dead in char_generic_nvram_read_nvram_write_nvram.i with octagon enabled analysis Apron: Both branches dead after malloc

2 participants

@michael-schwarz @sim642