Skip to content

Make access outer distribution lazy#1136

Merged
sim642 merged 29 commits intomasterfrom
access-distr-outer
Sep 12, 2023
Merged

Make access outer distribution lazy#1136
sim642 merged 29 commits intomasterfrom
access-distr-outer

Conversation

@karoliineh
Copy link
Copy Markdown
Member

@karoliineh karoliineh commented Aug 15, 2023 •
edited by sim642
Loading

This is a continuation of #1089, which made access inner distribution to fields lazy. This now also does the outer distribution to type-based memory locations.

Documentaton for the new race detection is in raceAnalysis.ml.

This halves the number of race warnings on silver searcher.

karoliineh and others added 16 commits June 19, 2023 15:14
@karoliineh @sim642
Add more tests for covering different cases of access outer distribution
3525e49 
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
@karoliineh
Add cram tests and ASCII art to existing tests that cover access oute…
2a003ab 
…r distribution
@karoliineh
Fix test 04 93
91b64e8
@karoliineh @sim642
Move access outer distribute to raceAnalysis
4ac338d 
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
@karoliineh @sim642
Handle global variables in outer_memo
bdf116d 
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
@karoliineh @sim642
Split ancestor accs and outer ancestor accs
31ec579 
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
@karoliineh @sim642
Fix races between ancestor and outer accs
936d7b0 
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
@sim642
Fix memory location counts for cross races
edff1d3
@karoliineh
Replace print comments with tracing in group_may_race
f419f50
@karoliineh @sim642
Create warn_accs record and refactor
59feaf8 
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
@karoliineh
Refactor distribute_inner in raceAnalysis
49e529f
@karoliineh @sim642
Use warn_accs for todo
64c761b 
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
@karoliineh @sim642
Make warn_accs record to a module
b06b3e3 
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
@karoliineh @sim642
Refactor and document todo' computation
69ddfdf 
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
@karoliineh @sim642
Use Typsig for Access MemoRoot
857d1cb 
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
@karoliineh @sim642
Fix index in type_suffix_memo
b28cbba 
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
karoliineh and others added 3 commits August 15, 2023 13:53
@karoliineh
Merge branch 'master' into access-distr-outer
916acfa
@karoliineh @sim642
Make new cram tests deterministic
d6c5bba 
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
@karoliineh @sim642
Refactor distribute_outer
21332cc 
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
@sim642 sim642 added this to the v2.2.0 milestone Aug 15, 2023
@sim642 sim642 marked this pull request as ready for review August 15, 2023 14:45
@sim642 sim642 requested a review from vesalvojdani August 15, 2023 18:54
@karoliineh karoliineh mentioned this pull request Aug 16, 2023
Merged
vesalvojdani
vesalvojdani requested changes Aug 19, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@vesalvojdani vesalvojdani left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Overall, I'm extremely happy with these changes. The crazy things finally make sense. Now, I only skimmed the code and it looks good, but I would mainly like to play around with it on our familiar benchmarks before we merge in case something pops up. Meanwhile, here are some comments about the documentation.

@sim642 sim642 requested a review from vesalvojdani September 11, 2023 08:29
vesalvojdani
vesalvojdani approved these changes Sep 11, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@vesalvojdani vesalvojdani left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks good now. The details of the empty-access hack is not completely clear to me, but I would like to sit down after this merged and go over the full thing. This also made me wonder about what a more meaningful treatment of direct-arith or disjoint types assumptions should be.

@sim642 sim642 merged commit 8c8fd28 into master Sep 12, 2023
@sim642 sim642 deleted the access-distr-outer branch September 12, 2023 07:45
@sim642 sim642 mentioned this pull request Sep 13, 2023
Closed
sim642 added a commit to sim642/opam-repository that referenced this pull request Sep 13, 2023
@sim642
[new release] goblint (2.2.0)
eb80bce 
CHANGES:

* Add `setjmp`/`longjmp` analysis (goblint/analyzer#887, goblint/analyzer#970, goblint/analyzer#1015, goblint/analyzer#1019).
* Refactor race analysis to lazy distribution (goblint/analyzer#1084, goblint/analyzer#1089, goblint/analyzer#1136, goblint/analyzer#1016).
* Add thread-unsafe library function call analysis (goblint/analyzer#723, goblint/analyzer#1082).
* Add mutex type analysis and mutex API analysis (goblint/analyzer#800, goblint/analyzer#839, goblint/analyzer#1073).
* Add interval set domain and string literals domain (goblint/analyzer#901, goblint/analyzer#966, goblint/analyzer#994, goblint/analyzer#1048).
* Add affine equalities analysis (goblint/analyzer#592).
* Add use-after-free analysis (goblint/analyzer#1050, goblint/analyzer#1114).
* Add dead code elimination transformation (goblint/analyzer#850, goblint/analyzer#979).
* Add taint analysis for partial contexts (goblint/analyzer#553, goblint/analyzer#952).
* Add YAML witness validation via unassume (goblint/analyzer#796, goblint/analyzer#977, goblint/analyzer#1044, goblint/analyzer#1045, goblint/analyzer#1124).
* Add incremental analysis rename detection (goblint/analyzer#774, goblint/analyzer#777).
* Fix address sets unsoundness (goblint/analyzer#822, goblint/analyzer#967, goblint/analyzer#564, goblint/analyzer#1032, goblint/analyzer#998, goblint/analyzer#1031).
* Fix thread escape analysis unsoundness (goblint/analyzer#939, goblint/analyzer#984, goblint/analyzer#1074, goblint/analyzer#1078).
* Fix many incremental analysis issues (goblint/analyzer#627, goblint/analyzer#836, goblint/analyzer#835, goblint/analyzer#841, goblint/analyzer#932, goblint/analyzer#678, goblint/analyzer#942, goblint/analyzer#949, goblint/analyzer#950, goblint/analyzer#957, goblint/analyzer#955, goblint/analyzer#954, goblint/analyzer#960, goblint/analyzer#959, goblint/analyzer#1004, goblint/analyzer#558, goblint/analyzer#1010, goblint/analyzer#1091).
* Fix server mode for abstract debugging (goblint/analyzer#983, goblint/analyzer#990, goblint/analyzer#997, goblint/analyzer#1000, goblint/analyzer#1001, goblint/analyzer#1013, goblint/analyzer#1018, goblint/analyzer#1017, goblint/analyzer#1026, goblint/analyzer#1027).
* Add documentation for configuration JSON schema and OCaml API (goblint/analyzer#999, goblint/analyzer#1054, goblint/analyzer#1055, goblint/analyzer#1053).
* Add many library function specifications (goblint/analyzer#962, goblint/analyzer#996, goblint/analyzer#1028, goblint/analyzer#1079, goblint/analyzer#1121, goblint/analyzer#1135, goblint/analyzer#1138).
* Add OCaml 5.0 support (goblint/analyzer#1003, goblint/analyzer#945, goblint/analyzer#1162).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sim642 sim642 sim642 left review comments

@michael-schwarz michael-schwarz michael-schwarz left review comments

@vesalvojdani vesalvojdani vesalvojdani approved these changes

Assignees

@sim642 sim642

@karoliineh karoliineh

Labels

benchmarking feature usability

Projects

None yet

Milestone

v2.2.0

Development

Successfully merging this pull request may close these issues.

4 participants

@karoliineh @sim642 @vesalvojdani @michael-schwarz