goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
160 stars 72 forks source link

Fix `mutex-meet` for malloc after thread creation #1492

Open michael-schwarz opened 1 month ago

michael-schwarz commented 1 month ago

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

TODO:

Closes #1489

sim642 commented 1 month ago
  • 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 commented 1 month ago

mutex:[__VERIFIER_atomic] also starts out with bottom (env: [||]), so that's not the difference I suspect. Rather, the difference comes from this check: https://github.com/goblint/analyzer/blob/896f236c98ba829aee25e5f02cb08d4bb2bba9b1/src/analyses/apron/relationPriv.apron.ml#L500-L504 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.