search

goblint / analyzer

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

Avoid emitting reflexive pointer refines for locking #1407

Closed sim642 closed 2 months ago

sim642 commented 3 months ago

This is an alternative optimized fix for #1374.

This is extracted from the end of #1396.

This now depends on #1441 to pass all tests where it reveals previous unsoundness.

sim642 commented 3 months ago

This should work, but it seems to reveal some pre-existing issue in the relational atomic privatization stuff. Namely with the special [__VERIFIER_atomic] mutex variable used for that.

Quick tracing reveals something which definitely shouldn't be happening: the Apron environment contains a variable named [__VERIFIER_atomic]. This is because locking it and emitting a branch on &[__VERIFIER_atomic] == &[__VERIFIER_atomic] causes the relational analysis branch to read the global variable somehow. I guess because it happens to be a pointer to int, which [__VERIFIER_atomic]'s declared type. And that somehow changes everything.