Skip to content

Remove symmetries in the subset relation #78

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

Merged
merged 1 commit into from
Sep 21, 2018
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 18 additions & 0 deletions polonius-engine/src/output/datafrog_opt.rs
Original file line number Diff line number Diff line change
Expand Up @@ -109,6 +109,20 @@ pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom>(

// .. and then start iterating rules!
while iteration.changed() {
// Cleanup step: remove symmetries
// - remove regions which are `subset`s of themselves
//
// FIXME: investigate whether is there a better way to do that without complicating
// the rules too much, because it would also require temporary variables and
// impact performance. Until then, the big reduction in tuples improves performance
// a lot, even if we're potentially adding a small number of tuples
// per round just to remove them in the next round.
subset
.recent
.borrow_mut()
.elements
.retain(|&(r1, r2, _)| r1 != r2);

// remap fields to re-index by the different keys
subset_r1p.from_map(&subset, |&(r1, r2, p)| ((r1, p), r2));
subset_p.from_map(&subset, |&(r1, r2, p)| (p, (r1, r2)));
Expand Down Expand Up @@ -319,6 +333,10 @@ pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom>(
}

let subset = subset.complete();
assert!(
subset.iter().filter(|&(r1, r2, _)| r1 == r2).count() == 0,
"unwanted subset symmetries"
);
for (r1, r2, location) in &subset.elements {
result
.subset
Expand Down
18 changes: 18 additions & 0 deletions polonius-engine/src/output/naive.rs
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,20 @@ pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom>(

// .. and then start iterating rules!
while iteration.changed() {
// Cleanup step: remove symmetries
// - remove regions which are `subset`s of themselves
//
// FIXME: investigate whether is there a better way to do that without complicating
// the rules too much, because it would also require temporary variables and
// impact performance. Until then, the big reduction in tuples improves performance
// a lot, even if we're potentially adding a small number of tuples
// per round just to remove them in the next round.
subset
.recent
.borrow_mut()
.elements
.retain(|&(r1, r2, _)| r1 != r2);

// remap fields to re-index by keys.
subset_r1p.from_map(&subset, |&(r1, r2, p)| ((r1, p), r2));
subset_r2p.from_map(&subset, |&(r1, r2, p)| ((r2, p), r1));
Expand Down Expand Up @@ -125,6 +139,10 @@ pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom>(

if dump_enabled {
let subset = subset.complete();
assert!(
subset.iter().filter(|&(r1, r2, _)| r1 == r2).count() == 0,
"unwanted subset symmetries"
);
for (r1, r2, location) in &subset.elements {
result
.subset
Expand Down
34 changes: 34 additions & 0 deletions src/test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -76,6 +76,40 @@ fn test_sensitive_passes_issue_47680() -> Result<(), Error> {
}
}

#[test]
fn no_subset_symmetries_exist() -> Result<(), Error> {
try {
let facts_dir = Path::new(env!("CARGO_MANIFEST_DIR"))
.join("inputs")
.join("issue-47680")
.join("nll-facts")
.join("main");
let tables = &mut intern::InternerTables::new();
let all_facts = tab_delim::load_tab_delimited_facts(tables, &facts_dir)?;

let subset_symmetries_exist = |output: &Output<Region, Loan, Point>| {
for (_, subsets) in &output.subset {
for (r1, rs) in subsets {
if rs.contains(&r1) {
return true;
}
}
}
false
};

let naive = Output::compute(&all_facts, Algorithm::Naive, true);
assert!(!subset_symmetries_exist(&naive));

// FIXME: the issue-47680 dataset is suboptimal here as DatafrogOpt does not
// produce subset symmetries for it. It does for clap, and it was used to manually verify
// that the assert in verbose mode didn't trigger. Therefore, switch to this dataset
// whenever it's fast enough to be enabled in tests, or somehow create a test facts program
// or reduce it from clap.
let opt = Output::compute(&all_facts, Algorithm::DatafrogOpt, true);
assert!(!subset_symmetries_exist(&opt));
}
}

// The following 3 tests, `send_is_not_static_std_sync`, `escape_upvar_nested`, and `issue_31567`
// are extracted from rustc's test suite, and fail because of differences between the Naive
Expand Down