Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Compute subset errors everywhere #156

Merged
merged 15 commits into from
Jul 30, 2021

Conversation

lqd
Copy link
Member

@lqd lqd commented Dec 21, 2020

This PR implements what we discussed last sprint:

  • make the Opt variant compute subset errors, tracking the subsets of placeholder origins, because placeholder loans don't work in this situation
  • make the Naive variant compute subset errors using the "easy subset-filtering" because we compute the full subset transitive closure here
  • do nothing for now on the LocationInsensitive variant: placeholder loans are very natural in this variant, as we don't compute subsets at all
  • by adding the subset errors to the LocationInsensitive variant, we can re-enable it as a pre-pass in the Hybrid variant: if no potential illegal access errors nor potential illegal subset relations errors are detected, there's no need to run the full analysis.

I've also started to number and document the rules, as preparation for putting them in the book (and extracting them as soufflé .dl files if need be). This can be seen in the Naive variant (commit 321c23e, before the computation was simplified), and if that's interesting I'll apply it to the other variants (though the Opt rules are already more documented than the 2 others).

As the last bit of renaming, it also aligns the relation name and input fact files of the known_subsets to what the finalized rules look like in our hackmd (now known_placeholder_subsets). The commits starting with "tests" are the ones renaming input files and can be glossed over/ignored.

@lqd
Copy link
Member Author

lqd commented Dec 27, 2020

Working on documenting the LocationInsensitive variant in #126 made me realize I forgot to rename two relations in this PR here:

  • requires was renamed to origin_contains_loan_on_entry in the rules hackmd, but this name is specific to the Naive variant: this variant here does not track locations, and should be origin_contains_loan
  • known_contains still uses its old name dual to known_subset while the rules have it as placeholder_known_to_contain

I'll take care of both of these later, just to make my life easier until we have decided how to tackle #157, but I've used the correct names in the documentation PR.

@lqd lqd force-pushed the subset_errors_are_back_with_a_vengeance branch 2 times, most recently from ffe39d2 to ffd02f8 Compare April 28, 2021 21:29
@lqd lqd force-pushed the subset_errors_are_back_with_a_vengeance branch 2 times, most recently from 7886bb1 to 2b1d580 Compare June 3, 2021 21:33
@nikomatsakis
Copy link
Contributor

r=me with nit

lqd added 14 commits July 30, 2021 18:01
- make the location-insensitive variant compute potential subset errors using placeholder loans
- record those potential errors in the context for the Opt variant to make use of in the context of the Hybrid analysis
all 3 types of errors should always be the same between the naive and opt variants
This will help readability, and documentation, when we extract the rules to the book. Also describes more precisely why we need a duplicate liveness relation.
Since we're already computing the full subset TC, adding a check for placeholder origins at the same time is simpler, and as a bonus, barely noticeable performance-wise (therefore, faster than tracking the placeholder subsets).
@lqd lqd force-pushed the subset_errors_are_back_with_a_vengeance branch from 2b1d580 to cbe4512 Compare July 30, 2021 16:10
@lqd lqd force-pushed the subset_errors_are_back_with_a_vengeance branch from cbe4512 to 594c7df Compare July 30, 2021 16:12
@lqd lqd merged commit 1bcf40d into rust-lang:master Jul 30, 2021
@lqd lqd deleted the subset_errors_are_back_with_a_vengeance branch July 30, 2021 16:22
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants