Skip to content

Avoid emitting reflexive pointer refines for locking#1407

Merged
sim642 merged 3 commits intomasterfrom
issue-1374-3
May 7, 2024
Merged

Avoid emitting reflexive pointer refines for locking#1407
sim642 merged 3 commits intomasterfrom
issue-1374-3

Conversation

@sim642
Copy link
Copy Markdown
Member

@sim642 sim642 commented Apr 4, 2024 •
edited
Loading

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 sim642 added the performance Analysis time, memory usage label Apr 4, 2024
@sim642 sim642 mentioned this pull request Apr 4, 2024
Merged
Base automatically changed from issue-1374-2 to master April 4, 2024 13:22
@sim642
Copy link
Copy Markdown
Member Author

sim642 commented Apr 4, 2024

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.

This was referenced May 3, 2024
Closed
Merged
@sim642 sim642 added the pr-dependency Depends or builds on another PR, which should be merged before label May 6, 2024
@sim642 sim642 changed the base branch from master to issue_1140 May 6, 2024 07:13
@sim642 sim642 marked this pull request as ready for review May 6, 2024 07:13
Base automatically changed from issue_1140 to master May 7, 2024 07:13
@sim642 sim642 added this to the v2.4.0 milestone May 7, 2024
@sim642 sim642 removed the pr-dependency Depends or builds on another PR, which should be merged before label May 7, 2024
@sim642 sim642 merged commit ff9b82d into master May 7, 2024
@sim642 sim642 deleted the issue-1374-3 branch May 7, 2024 07:35
sim642 added a commit to sim642/opam-repository that referenced this pull request Aug 2, 2024
@sim642
[new release] goblint (2.4.0)
38186e2 
CHANGES:

* Remove unmaintained analyses: spec, file (goblint/analyzer#1281).
* Add linear two-variable equalities analysis (goblint/analyzer#1297, goblint/analyzer#1412, goblint/analyzer#1466).
* Add callstring, loopfree callstring and context gas analyses (goblint/analyzer#1038, goblint/analyzer#1340, goblint/analyzer#1379, goblint/analyzer#1427, goblint/analyzer#1439).
* Add non-relational thread-modular value analyses with thread IDs (goblint/analyzer#1366, goblint/analyzer#1398, goblint/analyzer#1399).
* Add NULL byte array domain (goblint/analyzer#1076).
* Fix spurious overflow warnings from internal evaluations (goblint/analyzer#1406, goblint/analyzer#1411, goblint/analyzer#1511).
* Refactor non-definite mutex handling to fix unsoundness (goblint/analyzer#1430, goblint/analyzer#1500, goblint/analyzer#1503, goblint/analyzer#1409).
* Fix non-relational thread-modular value analysis unsoundness with ambiguous points-to sets (goblint/analyzer#1457, goblint/analyzer#1458).
* Fix mutex type analysis unsoundness and enable it by default (goblint/analyzer#1414, goblint/analyzer#1416, goblint/analyzer#1510).
* Add points-to set refinement on mutex path splitting (goblint/analyzer#1287, goblint/analyzer#1343, goblint/analyzer#1374, goblint/analyzer#1396, goblint/analyzer#1407).
* Improve narrowing operators (goblint/analyzer#1502, goblint/analyzer#1540, goblint/analyzer#1543).
* Extract automatic configuration tuning for soundness (goblint/analyzer#1369).
* Fix many locations in witnesses (goblint/analyzer#1355, goblint/analyzer#1372, goblint/analyzer#1400, goblint/analyzer#1403).
* Improve output readability (goblint/analyzer#1294, goblint/analyzer#1312, goblint/analyzer#1405, goblint/analyzer#1497).
* Refactor logging (goblint/analyzer#1117).
* Modernize all library function specifications (goblint/analyzer#1029, goblint/analyzer#688, goblint/analyzer#1174, goblint/analyzer#1289, goblint/analyzer#1447, goblint/analyzer#1487).
* Remove OCaml 4.10, 4.11, 4.12 and 4.13 support (goblint/analyzer#1448).
@sim642 sim642 mentioned this pull request Aug 2, 2024
Merged
avsm pushed a commit to avsm/opam-repository that referenced this pull request Sep 5, 2024
@sim642 @avsm
[new release] goblint (2.4.0)
2afe816 
CHANGES:

* Remove unmaintained analyses: spec, file (goblint/analyzer#1281).
* Add linear two-variable equalities analysis (goblint/analyzer#1297, goblint/analyzer#1412, goblint/analyzer#1466).
* Add callstring, loopfree callstring and context gas analyses (goblint/analyzer#1038, goblint/analyzer#1340, goblint/analyzer#1379, goblint/analyzer#1427, goblint/analyzer#1439).
* Add non-relational thread-modular value analyses with thread IDs (goblint/analyzer#1366, goblint/analyzer#1398, goblint/analyzer#1399).
* Add NULL byte array domain (goblint/analyzer#1076).
* Fix spurious overflow warnings from internal evaluations (goblint/analyzer#1406, goblint/analyzer#1411, goblint/analyzer#1511).
* Refactor non-definite mutex handling to fix unsoundness (goblint/analyzer#1430, goblint/analyzer#1500, goblint/analyzer#1503, goblint/analyzer#1409).
* Fix non-relational thread-modular value analysis unsoundness with ambiguous points-to sets (goblint/analyzer#1457, goblint/analyzer#1458).
* Fix mutex type analysis unsoundness and enable it by default (goblint/analyzer#1414, goblint/analyzer#1416, goblint/analyzer#1510).
* Add points-to set refinement on mutex path splitting (goblint/analyzer#1287, goblint/analyzer#1343, goblint/analyzer#1374, goblint/analyzer#1396, goblint/analyzer#1407).
* Improve narrowing operators (goblint/analyzer#1502, goblint/analyzer#1540, goblint/analyzer#1543).
* Extract automatic configuration tuning for soundness (goblint/analyzer#1369).
* Fix many locations in witnesses (goblint/analyzer#1355, goblint/analyzer#1372, goblint/analyzer#1400, goblint/analyzer#1403).
* Improve output readability (goblint/analyzer#1294, goblint/analyzer#1312, goblint/analyzer#1405, goblint/analyzer#1497).
* Refactor logging (goblint/analyzer#1117).
* Modernize all library function specifications (goblint/analyzer#1029, goblint/analyzer#688, goblint/analyzer#1174, goblint/analyzer#1289, goblint/analyzer#1447, goblint/analyzer#1487).
* Remove OCaml 4.10, 4.11, 4.12 and 4.13 support (goblint/analyzer#1448).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@michael-schwarz michael-schwarz michael-schwarz approved these changes

Assignees

No one assigned

Labels

performance Analysis time, memory usage

Projects

None yet

Milestone

v2.4.0

Development

Successfully merging this pull request may close these issues.

2 participants

@sim642 @michael-schwarz