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

Make DatafrogOpt produce errors #42

Merged
merged 1 commit into from
May 24, 2018
Merged

Make DatafrogOpt produce errors #42

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
76 changes: 48 additions & 28 deletions src/output/datafrog_opt.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,25 +35,37 @@ pub(super) fn compute(dump_enabled: bool, mut all_facts: AllFacts) -> Output {

let mut result = Output::new(dump_enabled);

let borrow_live_at = {
let errors = {
// Create a new iteration context, ...
let mut iteration = Iteration::new();

// .. some variables and different indices for `subset`.
// static inputs
let cfg_edge = iteration.variable::<(Point, Point)>("cfg_edge");
let killed = all_facts.killed.into();

// `invalidates` facts, stored ready for joins
let invalidates = iteration.variable::<((Loan, Point), ())>("invalidates");

// we need `region_live_at` in both variable and relation forms.
// (respectively, for join and antijoin).
let region_live_at_rel =
Relation::from(all_facts.region_live_at.iter().map(|&(r, p)| (r, p)));
let region_live_at_var = iteration.variable::<((Region, Point), ())>("region_live_at");

// variables, indices for the computation rules, and temporaries for the multi-way joins
let subset = iteration.variable::<(Region, Region, Point)>("subset");
let subset_1 = iteration.variable_indistinct("subset_1");
let subset_2 = iteration.variable_indistinct("subset_2");
let subset_r1p = iteration.variable_indistinct("subset_r1p");
let subset_p = iteration.variable_indistinct("subset_p");

// temporaries as we perform a multi-way join, and more indices
let requires = iteration.variable::<(Region, Loan, Point)>("requires");
let requires_1 = iteration.variable_indistinct("requires_1");
let requires_2 = iteration.variable_indistinct("requires_2");
let requires_bp = iteration.variable_indistinct("requires_bp");
let requires_rp = iteration.variable_indistinct("requires_rp");

let borrow_live_at = iteration.variable::<(Loan, Point)>("borrow_live_at");
let borrow_live_at = iteration.variable::<((Loan, Point), ())>("borrow_live_at");

let live_to_dead_regions =
iteration.variable::<(Region, Region, Point, Point)>("live_to_dead_regions");
Expand All @@ -78,22 +90,19 @@ pub(super) fn compute(dump_enabled: bool, mut all_facts: AllFacts) -> Output {
iteration.variable::<((Region, Point, Point), Region)>("dead_can_reach_live");
let dead_can_reach_live_r1pq = iteration.variable_indistinct("dead_can_reach_live_r1pq");

// We need both relation and variable forms of this (for join and antijoin).
let region_live_at_rel =
Relation::from(all_facts.region_live_at.iter().map(|&(r, p)| (r, p)));
let region_live_at_var = iteration.variable::<((Region, Point), ())>("region_live_at");

let cfg_edge_p = iteration.variable::<(Point, Point)>("cfg_edge_p");

let killed = all_facts.killed.into();
// output
let errors = iteration.variable("errors");

// load initial facts.
subset.insert(all_facts.outlives.into());
requires.insert(all_facts.borrow_region.into());
cfg_edge.insert(all_facts.cfg_edge.into());
invalidates.insert(Relation::from(
all_facts.invalidates.iter().map(|&(p, b)| ((b, p), ())),
));
region_live_at_var.insert(Relation::from(
all_facts.region_live_at.iter().map(|&(r, p)| ((r, p), ())),
));
cfg_edge_p.insert(all_facts.cfg_edge.into());
subset.insert(all_facts.outlives.into());
requires.insert(all_facts.borrow_region.into());

// .. and then start iterating rules!
while iteration.changed() {
Expand Down Expand Up @@ -142,9 +151,8 @@ pub(super) fn compute(dump_enabled: bool, mut all_facts: AllFacts) -> Output {
// cfg_edge(P, Q),
// region_live_at(R1, Q),
// !region_live_at(R2, Q).
live_to_dead_regions_1.from_join(&subset_p, &cfg_edge_p, |&p, &(r1, r2), &q| {
((r1, q), (r2, p))
});
live_to_dead_regions_1
.from_join(&subset_p, &cfg_edge, |&p, &(r1, r2), &q| ((r1, q), (r2, p)));
live_to_dead_regions_2.from_join(
&live_to_dead_regions_1,
&region_live_at_var,
Expand All @@ -169,7 +177,7 @@ pub(super) fn compute(dump_enabled: bool, mut all_facts: AllFacts) -> Output {
dead_region_requires_1.from_antijoin(&requires_bp, &killed, |&(b, p), &r| (p, (b, r)));
dead_region_requires_2.from_join(
&dead_region_requires_1,
&cfg_edge_p,
&cfg_edge,
|&p, &(b, r), &q| ((r, q), (b, p)),
);
dead_region_requires.from_antijoin(
Expand Down Expand Up @@ -236,14 +244,14 @@ pub(super) fn compute(dump_enabled: bool, mut all_facts: AllFacts) -> Output {
);

// subset(R1, R2, Q) :-
// subset(R1, R2, P) :-
// subset(R1, R2, P),
// cfg_edge(P, Q),
// region_live_at(R1, Q),
// region_live_at(R2, Q).
//
// Carry `R1 <= R2` from P into Q if both `R1` and
// `R2` are live in Q.
subset_1.from_join(&subset_p, &cfg_edge_p, |&_p, &(r1, r2), &q| ((r1, q), r2));
subset_1.from_join(&subset_p, &cfg_edge, |&_p, &(r1, r2), &q| ((r1, q), r2));
subset_2.from_join(&subset_1, &region_live_at_var, |&(r1, q), &r2, &()| {
((r2, q), r1)
});
Expand Down Expand Up @@ -281,7 +289,7 @@ pub(super) fn compute(dump_enabled: bool, mut all_facts: AllFacts) -> Output {
// cfg_edge(P, Q),
// region_live_at(R, Q).
requires_1.from_antijoin(&requires_bp, &killed, |&(b, p), &r| (p, (r, b)));
requires_2.from_join(&requires_1, &cfg_edge_p, |&_p, &(r, b), &q| ((r, q), b));
requires_2.from_join(&requires_1, &cfg_edge, |&_p, &(r, b), &q| ((r, q), b));
requires.from_join(&requires_2, &region_live_at_var, |&(r, q), &b, &()| {
(r, b, q)
});
Expand All @@ -291,8 +299,11 @@ pub(super) fn compute(dump_enabled: bool, mut all_facts: AllFacts) -> Output {
//
// borrow_live_at(B, P) :- requires(R, B, P), region_live_at(R, P)
borrow_live_at.from_join(&requires_rp, &region_live_at_var, |&(_r, p), &b, &()| {
(b, p)
((b, p), ())
});

// .decl errors(B, P) :- invalidates(B, P), borrow_live_at(B, P).
errors.from_join(&invalidates, &borrow_live_at, |&(b, p), &(), &()| (b, p));
}

if dump_enabled {
Expand Down Expand Up @@ -326,22 +337,31 @@ pub(super) fn compute(dump_enabled: bool, mut all_facts: AllFacts) -> Output {
.or_insert(BTreeSet::new())
.insert(*borrow);
}

let borrow_live_at = borrow_live_at.complete();
for ((borrow, location), ()) in &borrow_live_at.elements {
result
.borrow_live_at
.entry(*location)
.or_insert(Vec::new())
.push(*borrow);
}
}

borrow_live_at.complete()
errors.complete()
};

if dump_enabled {
println!(
"borrow_live_at is complete: {} tuples, {:?}",
borrow_live_at.len(),
"errors is complete: {} tuples, {:?}",
errors.len(),
timer.elapsed()
);
}

for (borrow, location) in &borrow_live_at.elements {
for (borrow, location) in &errors.elements {
result
.borrow_live_at
.potential_errors
.entry(*location)
.or_insert(Vec::new())
.push(*borrow);
Expand Down
18 changes: 17 additions & 1 deletion src/test.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ fn test_fn(dir_name: &str, fn_name: &str) -> Result<(), Error> {
let tables = &mut intern::InternerTables::new();
let all_facts = tab_delim::load_tab_delimited_facts(tables, &facts_dir)?;
let naive = Output::compute(&all_facts, Algorithm::Naive, false);
let opt = Output::compute(&all_facts, Algorithm::DatafrogOpt, false);
let opt = Output::compute(&all_facts, Algorithm::DatafrogOpt, true);
assert_eq!(naive.borrow_live_at, opt.borrow_live_at);
}
}
Expand Down Expand Up @@ -60,3 +60,19 @@ fn test_insensitive_potential_error() -> Result<(), Error> {
assert_eq!(insensitive.potential_errors, expected);
}
}

#[test]
fn test_sensitive_passes_issue_47680() -> Result<(), Error> {
do catch {
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 sensitive = Output::compute(&all_facts, Algorithm::DatafrogOpt, false);

assert!(sensitive.potential_errors.is_empty());
}
}