analyzer
analyzer copied to clipboard
Fix `mutex-meet` for malloc after thread creation
The issue in #1489 was that the global invariant for the blob was still bot, making the meet deadcode.
TODO:
- [x]
mutex-meet-atomicprivatization 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 inget_mutex_global_g_with_mutex_inits_atomicCC: @sim642)
Closes #1489
- Verify if these are really all changes needed for
mutex-meet-atomic(It seems weird that no handling of these cases is necessary inget_mutex_global_g_with_mutex_inits_atomicCC: @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?
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.