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.

Sign up for GitHub

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

Jump to bottom

[WIP] Stop materializing placeholder liveness at all points #157

Draft
wants to merge 5 commits into
base: master
Choose a base branch
from
Draft

[WIP] Stop materializing placeholder liveness at all points #157

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
7284e48
tests: re-enable comparisons of the `loan_live_at` relation
lqd Dec 22, 2020
539492d
location insensitive: handle placeholders explicitly instead of a by-…
lqd Dec 22, 2020
f103a75
naive: handle placeholders explicitly in the rules
lqd Dec 22, 2020
e6dd2fb
opt: handle placeholders explicitly in the rules
lqd Dec 22, 2020
c447751
liveness: stop materializing facts that placeholders are live at all …
lqd Dec 22, 2020
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
205 changes: 188 additions & 17 deletions polonius-engine/src/output/datafrog_opt.rs
View file
Open in desktop

Large diffs are not rendered by default.

20 changes: 2 additions & 18 deletions polonius-engine/src/output/liveness.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,6 @@

//! An implementation of the origin liveness calculation logic

use std::collections::BTreeSet;
use std::time::Instant;

use crate::facts::FactTypes;
Expand All @@ -23,7 +22,7 @@ pub(super) fn compute_live_origins<T: FactTypes>(
cfg_edge: &Relation<(T::Point, T::Point)>,
var_maybe_partly_initialized_on_exit: Relation<(T::Variable, T::Point)>,
output: &mut Output<T>,
) -> Vec<(T::Origin, T::Point)> {
) -> Relation<(T::Origin, T::Point)> {
let timer = Instant::now();
let mut iteration = Iteration::new();

Expand Down Expand Up @@ -151,20 +150,5 @@ pub(super) fn compute_live_origins<T: FactTypes>(
}
}

origin_live_on_entry.elements
}

pub(super) fn make_universal_regions_live<T: FactTypes>(
origin_live_on_entry: &mut Vec<(T::Origin, T::Point)>,
cfg_node: &BTreeSet<T::Point>,
universal_regions: &[T::Origin],
) {
debug!("make_universal_regions_live()");

origin_live_on_entry.reserve(universal_regions.len() * cfg_node.len());
for &origin in universal_regions.iter() {
for &point in cfg_node.iter() {
origin_live_on_entry.push((origin, point));
}
}
origin_live_on_entry
}
33 changes: 31 additions & 2 deletions polonius-engine/src/output/location_insensitive.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,8 @@ pub(super) fn compute<T: FactTypes>(
let placeholder_loan = &ctx.placeholder_loan;
let known_contains = &ctx.known_contains;

// Rule 1: the subsets are the non-transitive `subset_base` static input.
//
// subset(Origin1, Origin2) :-
// subset_base(Origin1, Origin2, _).
let subset = Relation::from_iter(
Expand All @@ -52,6 +54,8 @@ pub(super) fn compute<T: FactTypes>(

// load initial facts.

// Rule 2: the issuing origins are the ones initially containing loans.
//
// origin_contains_loan_on_entry(Origin, Loan) :-
// loan_issued_at(Origin, Loan, _).
origin_contains_loan_on_entry.extend(
Expand All @@ -60,6 +64,8 @@ pub(super) fn compute<T: FactTypes>(
.map(|&(origin, loan, _point)| (origin, loan)),
);

// Rule 3: the placeholder origins also contain their placeholder loan.
//
// origin_contains_loan_on_entry(Origin, Loan) :-
// placeholder_loan(Origin, Loan).
origin_contains_loan_on_entry.extend(
Expand All @@ -70,6 +76,8 @@ pub(super) fn compute<T: FactTypes>(

// .. and then start iterating rules!
while iteration.changed() {
// Rule 4: propagate the loans from the origins to their subsets.
//
// origin_contains_loan_on_entry(Origin2, Loan) :-
// origin_contains_loan_on_entry(Origin1, Loan),
// subset(Origin1, Origin2).
Expand All @@ -82,9 +90,15 @@ pub(super) fn compute<T: FactTypes>(
|&_origin1, &loan, &origin2| (origin2, loan),
);

// Rule 5: compute potential errors, i.e. loans that are contained in an origin at any point in the CFG, and
// which are invalidated at a point where that origin is live.
//
// loan_live_at(Loan, Point) :-
// origin_contains_loan_on_entry(Origin, Loan),
// origin_live_on_entry(Origin, Point)
// (origin_live_on_entry(Origin, Point); placeholder_origin(Origin)). // -> A
//
// Since there is one alternative predicate, A, this will result in two expansions
// of this rule: one for each alternative for predicate A.
//
// potential_errors(Loan, Point) :-
// loan_invalidated_at(Loan, Point),
Expand All @@ -93,15 +107,30 @@ pub(super) fn compute<T: FactTypes>(
// Note: we don't need to materialize `loan_live_at` here
// so we can inline it in the `potential_errors` relation.
//
// 1) Rule 5, expansion 1 of 2
// - predicate A: `origin_live_on_entry(Origin, Point)`
potential_errors.from_leapjoin(
&origin_contains_loan_on_entry,
(
origin_live_on_entry.extend_with(|&(origin, _loan)| origin),
origin_live_on_entry.extend_with(|&(origin, _loan)| origin), // -> A
loan_invalidated_at.extend_with(|&(_origin, loan)| loan),
),
|&(_origin, loan), &point| (loan, point),
);
// 2) Rule 5, expansion 2 of 2
// - predicate A: `placeholder_origin(Origin)`
potential_errors.from_leapjoin(
&origin_contains_loan_on_entry,
(
placeholder_origin.filter_with(|&(origin, _loan)| (origin, ())), // -> A
loan_invalidated_at.extend_with(|&(_origin, loan)| loan),
),
|&(_origin, loan), &point| (loan, point),
);

// Rule 6: compute potential subset errors, i.e. the placeholder loans which ultimately
// flowed into another placeholder origin unexpectedly.
//
// potential_subset_errors(Origin1, Origin2) :-
// placeholder(Origin1, Loan1),
// placeholder(Origin2, _),
Expand Down
16 changes: 1 addition & 15 deletions polonius-engine/src/output/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -191,25 +191,13 @@ impl<T: FactTypes> Output<T> {
drop_of_var_derefs_origin: all_facts.drop_of_var_derefs_origin.clone(),
};

let mut origin_live_on_entry = liveness::compute_live_origins(
let origin_live_on_entry = liveness::compute_live_origins(
liveness_ctx,
&cfg_edge,
var_maybe_partly_initialized_on_exit,
&mut result,
);

let cfg_node = cfg_edge
.iter()
.map(|&(point1, _)| point1)
.chain(cfg_edge.iter().map(|&(_, point2)| point2))
.collect();

liveness::make_universal_regions_live::<T>(
&mut origin_live_on_entry,
&cfg_node,
&all_facts.universal_region,
);

// 3) Borrow checking

// Prepare data as datafrog relations, ready to join.
Expand All @@ -222,8 +210,6 @@ impl<T: FactTypes> Output<T> {
// analysis. If these facts happened to be recorded in separate MIR walks, we might also
// avoid generating those facts.

let origin_live_on_entry = origin_live_on_entry.into();

// TODO: also flip the order of this relation's arguments in rustc
// from `loan_invalidated_at(point, loan)` to `loan_invalidated_at(loan, point)`.
// to avoid this allocation.
Expand Down
92 changes: 83 additions & 9 deletions polonius-engine/src/output/naive.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -146,17 +146,61 @@ pub(super) fn compute<T: FactTypes>(

// Rule 3: propagate subsets along the CFG, according to liveness.
//
// Since there are two alternative predicates, A and B, this will result in four
// expansions of this rule: two alternatives for predicate A, and two alternatives for
// predicate B.
//
// subset(Origin1, Origin2, Point2) :-
// subset(Origin1, Origin2, Point1),
// cfg_edge(Point1, Point2),
// origin_live_on_entry(Origin1, Point2),
// origin_live_on_entry(Origin2, Point2).
// (origin_live_on_entry(Origin1, Point2); placeholder_origin(Origin1)), // -> A
// (origin_live_on_entry(Origin2, Point2); placeholder_origin(Origin2)). // -> B
//
// 1) Rule 3, expansion 1 of 4
// - predicate A: `origin_live_on_entry(Origin1, Point2)`
// - predicate B: `origin_live_on_entry(Origin2, Point2)`
subset.from_leapjoin(
&subset,
(
cfg_edge.extend_with(|&(_origin1, _origin2, point1)| point1),
origin_live_on_entry_rel.extend_with(|&(origin1, _origin2, _point1)| origin1), // -> A
origin_live_on_entry_rel.extend_with(|&(_origin1, origin2, _point1)| origin2), // -> B
),
|&(origin1, origin2, _point1), &point2| (origin1, origin2, point2),
);
// 2) Rule 3, expansion 2 of 4
// - predicate A: `origin_live_on_entry(Origin1, Point2)`
// - predicate B: `placeholder_origin(Origin2)`
subset.from_leapjoin(
&subset,
(
cfg_edge.extend_with(|&(_origin1, _origin2, point1)| point1),
origin_live_on_entry_rel.extend_with(|&(origin1, _origin2, _point1)| origin1),
origin_live_on_entry_rel.extend_with(|&(_origin1, origin2, _point1)| origin2),
origin_live_on_entry_rel.extend_with(|&(origin1, _origin2, _point1)| origin1), // -> A
placeholder_origin.filter_with(|&(_origin1, origin2, _point1)| (origin2, ())), // -> B
),
|&(origin1, origin2, _point1), &point2| (origin1, origin2, point2),
);
// 3) Rule 3, expansion 3 of 4
// - predicate A: `placeholder_origin(Origin1)`
// - predicate B: `origin_live_on_entry(Origin2, Point2)`
subset.from_leapjoin(
&subset,
(
cfg_edge.extend_with(|&(_origin1, _origin2, point1)| point1),
placeholder_origin.filter_with(|&(origin1, _origin2, _point1)| (origin1, ())), // -> A
origin_live_on_entry_rel.extend_with(|&(_origin1, origin2, _point1)| origin2), // -> B
),
|&(origin1, origin2, _point1), &point2| (origin1, origin2, point2),
);
// 4) Rule 3, expansion 4 of 4
// - predicate A: `placeholder_origin(Origin1)`
// - predicate B: `placeholder_origin(Origin2)`
subset.from_leapjoin(
&subset,
(
cfg_edge.extend_with(|&(_origin1, _origin2, point1)| point1),
placeholder_origin.filter_with(|&(origin1, _origin2, _point1)| (origin1, ())), // -> A
placeholder_origin.filter_with(|&(_origin1, origin2, _point1)| (origin2, ())), // -> B
),
|&(origin1, origin2, _point1), &point2| (origin1, origin2, point2),
);
Expand All @@ -176,32 +220,62 @@ pub(super) fn compute<T: FactTypes>(

// Rule 6: propagate loans along the CFG, according to liveness.
//
// Since there is one alternative predicate, A, this will result in two expansions
// of this rule: one for each alternative for predicate A.
//
// origin_contains_loan_on_entry(Origin, Loan, Point2) :-
// origin_contains_loan_on_entry(Origin, Loan, Point1),
// !loan_killed_at(Loan, Point1),
// cfg_edge(Point1, Point2),
// origin_live_on_entry(Origin, Point2).
// (origin_live_on_entry(Origin, Point2); placeholder_origin(Origin)). // -> A
//
// 1) Rule 6, expansion 1 of 2
// - predicate A: `origin_live_on_entry(Origin, Point2)`
origin_contains_loan_on_entry.from_leapjoin(
&origin_contains_loan_on_entry,
(
loan_killed_at.filter_anti(|&(_origin, loan, point1)| (loan, point1)),
cfg_edge.extend_with(|&(_origin, _loan, point1)| point1),
origin_live_on_entry_rel.extend_with(|&(origin, _loan, _point1)| origin), // -> A
),
|&(origin, loan, _point1), &point2| (origin, loan, point2),
);
// 2) Rule 6, expansion 2 of 2
// - predicate A: `placeholder_origin(Origin)`
origin_contains_loan_on_entry.from_leapjoin(
&origin_contains_loan_on_entry,
(
loan_killed_at.filter_anti(|&(_origin, loan, point1)| (loan, point1)),
cfg_edge.extend_with(|&(_origin, _loan, point1)| point1),
origin_live_on_entry_rel.extend_with(|&(origin, _loan, _point1)| origin),
placeholder_origin.filter_with(|&(origin, _loan, _point1)| (origin, ())), // -> A
),
|&(origin, loan, _point1), &point2| (origin, loan, point2),
);

// Rule 7: compute whether a loan is live at a given point, i.e. whether it is
// contained in a live origin at this point.
//
// Since there is one alternative predicate, A, this will result in two expansions
// of this rule: one for each alternative for predicate A.
//
// loan_live_at(Loan, Point) :-
// origin_contains_loan_on_entry(Origin, Loan, Point),
// origin_live_on_entry(Origin, Point).
// (origin_live_on_entry(Origin, Point); placeholder_origin(Origin)). // -> A
//
// 1) Rule 7, expansion 1 of 2
// - predicate A: `origin_live_on_entry(Origin, Point)`
loan_live_at.from_join(
&origin_contains_loan_on_entry_op,
&origin_live_on_entry_var,
&origin_live_on_entry_var, // -> A
|&(_origin, point), &loan, _| ((loan, point), ()),
);
// 2) Rule 7, expansion 2 of 2
// - predicate A: `placeholder_origin(Origin)`
loan_live_at.from_leapjoin(
&origin_contains_loan_on_entry_op,
placeholder_origin.extend_with(|&((origin, _point), _loan)| origin), // -> A
|&((_origin, point), loan), _| ((loan, point), ()),
);

// Rule 8: compute illegal access errors, i.e. an invalidation of a live loan.
//
Expand All @@ -226,7 +300,7 @@ pub(super) fn compute<T: FactTypes>(
// Here as well, WF-ness prevents this join from being a filter-only leapjoin. It
// doesn't matter much, as `placeholder_origin` is single-value relation.
//
// subset_error(Origin1, Origin2, Point) :-
// subset_errors(Origin1, Origin2, Point) :-
// subset(Origin1, Origin2, Point),
// placeholder_origin(Origin1),
// placeholder_origin(Origin2),
Expand Down
40 changes: 29 additions & 11 deletions src/test.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,7 @@ use std::path::Path;
fn test_facts(all_facts: &AllFacts, algorithms: &[Algorithm]) {
let naive = Output::compute(all_facts, Algorithm::Naive, true);

// Check that the "naive errors" are a subset of the "insensitive
// ones".
// Check that the "naive errors" are a subset of the "insensitive ones".
let insensitive = Output::compute(all_facts, Algorithm::LocationInsensitive, false);
for (naive_point, naive_loans) in &naive.errors {
match insensitive.errors.get(&naive_point) {
Expand Down Expand Up @@ -77,18 +76,37 @@ fn test_facts(all_facts: &AllFacts, algorithms: &[Algorithm]) {
for &optimized_algorithm in algorithms {
println!("Algorithm {:?}", optimized_algorithm);
let opt = Output::compute(all_facts, optimized_algorithm, true);
// TMP: until we reach our correctness goals, deactivate some comparisons between variants
// assert_equal(&naive.loan_live_at, &opt.loan_live_at);
assert_equal(&naive.errors, &opt.errors);
assert_equal(&naive.subset_errors, &opt.subset_errors);
assert_equal(&naive.move_errors, &opt.move_errors);
assert_equal(
&naive.loan_live_at,
&opt.loan_live_at,
"naive vs opt loan_live_at",
);
assert_equal(&naive.errors, &opt.errors, "naive vs opt errors");
assert_equal(
&naive.subset_errors,
&opt.subset_errors,
"naive vs opt subset_errors",
);
assert_equal(
&naive.move_errors,
&opt.move_errors,
"naive vs opt move_errors",
);
}

// The hybrid algorithm gets the same errors as the naive version
let opt = Output::compute(all_facts, Algorithm::Hybrid, true);
assert_equal(&naive.errors, &opt.errors);
assert_equal(&naive.subset_errors, &opt.subset_errors);
assert_equal(&naive.move_errors, &opt.move_errors);
assert_equal(&naive.errors, &opt.errors, "naive vs hybrid errors");
assert_equal(
&naive.subset_errors,
&opt.subset_errors,
"naive vs hybrid subset_errors",
);
assert_equal(
&naive.move_errors,
&opt.move_errors,
"naive vs hybrid move_errors",
);
}

fn test_fn(dir_name: &str, fn_name: &str, algorithm: Algorithm) -> Result<(), Box<dyn Error>> {
Expand Down Expand Up @@ -155,7 +173,7 @@ fn test_insensitive_errors() -> Result<(), Box<dyn Error>> {
expected.insert(Point::from(24), vec![Loan::from(1)]);
expected.insert(Point::from(50), vec![Loan::from(2)]);

assert_equal(&insensitive.errors, &expected);
assert_equal(&insensitive.errors, &expected, "insensitive errors");
Ok(())
}

Expand Down
Loading