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

Port the Naive variant to leapjoin #92

Merged
merged 1 commit into from
Dec 7, 2018
Merged

Port the Naive variant to leapjoin #92

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
65 changes: 36 additions & 29 deletions polonius-engine/src/output/naive.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ use std::time::Instant;
use crate::output::Output;
use facts::{AllFacts, Atom};

use datafrog::{Iteration, Relation};
use datafrog::{Iteration, Relation, RelationLeaper};

pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom>(
dump_enabled: bool,
Expand Down Expand Up @@ -46,6 +46,10 @@ pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom>(
// Create a new iteration context, ...
let mut iteration = Iteration::new();

// static inputs
let cfg_edge_rel: Relation<(Point, Point)> = all_facts.cfg_edge.into();
let killed_rel: Relation<(Loan, Point)> = all_facts.killed.into();

// .. some variables, ..
let subset = iteration.variable::<(Region, Region, Point)>("subset");
let requires = iteration.variable::<(Region, Loan, Point)>("requires");
Expand All @@ -57,21 +61,14 @@ pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom>(
// different indices for `subset`.
let subset_r1p = iteration.variable_indistinct("subset_r1p");
let subset_r2p = iteration.variable_indistinct("subset_r2p");
let subset_p = iteration.variable_indistinct("subset_p");

// different indexes for `requires`.
// different index for `requires`.
let requires_rp = iteration.variable_indistinct("requires_rp");
let requires_bp = iteration.variable_indistinct("requires_bp");

// temporaries as we perform a multi-way join.
let subset_1 = iteration.variable_indistinct("subset_1");
let subset_2 = iteration.variable_indistinct("subset_2");
let requires_1 = iteration.variable_indistinct("requires_1");
let requires_2 = iteration.variable_indistinct("requires_2");

let killed = all_facts.killed.into();
let region_live_at = iteration.variable::<((Region, Point), ())>("region_live_at");
let cfg_edge_p = iteration.variable::<(Point, Point)>("cfg_edge_p");
// we need `region_live_at` in both variable and relation forms.
// (respectively, for the regular join and the leapjoin).
let region_live_at_var = iteration.variable::<((Region, Point), ())>("region_live_at");
let region_live_at_rel = Relation::from(all_facts.region_live_at.iter().cloned());

// output
let errors = iteration.variable("errors");
Expand All @@ -82,10 +79,9 @@ pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom>(
invalidates.insert(Relation::from(
all_facts.invalidates.iter().map(|&(p, b)| ((b, p), ())),
));
region_live_at.insert(Relation::from(
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.clone().into());

// .. and then start iterating rules!
while iteration.changed() {
Expand All @@ -106,10 +102,8 @@ pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom>(
// 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));
subset_p.from_map(&subset, |&(r1, r2, p)| (p, (r1, r2)));

requires_rp.from_map(&requires, |&(r, b, p)| ((r, p), b));
requires_bp.from_map(&requires, |&(r, b, p)| ((b, p), r));

// subset(R1, R2, P) :- outlives(R1, R2, P).
// Already loaded; outlives is static.
Expand All @@ -124,12 +118,18 @@ pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom>(
// cfg_edge(P, Q),
// region_live_at(R1, Q),
// region_live_at(R2, Q).
subset.from_leapjoin(
&subset,
&mut [
&mut cfg_edge_rel.extend_with(|&(_r1, _r2, p)| p),
&mut region_live_at_rel.extend_with(|&(r1, _r2, _p)| r1),
&mut region_live_at_rel.extend_with(|&(_r1, r2, _p)| r2),
],
|&(r1, r2, _p), &q| (r1, r2, q),
);

subset_1.from_join(&subset_p, &cfg_edge_p, |&_p, &(r1, r2), &q| ((r1, q), r2));
subset_2.from_join(&subset_1, &region_live_at, |&(r1, q), &r2, &()| {
((r2, q), r1)
});
subset.from_join(&subset_2, &region_live_at, |&(r2, q), &r1, &()| (r1, r2, q));
// requires(R, B, P) :- borrow_region(R, B, P).
// Already loaded; borrow_region is static.

// requires(R2, B, P) :-
// requires(R1, B, P),
Expand All @@ -141,12 +141,20 @@ pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom>(
// !killed(B, P),
// cfg_edge(P, Q),
// region_live_at(R, Q).
requires_1.from_antijoin(&requires_bp, &killed, |&(b, p), &r| (p, (b, r)));
requires_2.from_join(&requires_1, &cfg_edge_p, |&_p, &(b, r), &q| ((r, q), b));
requires.from_join(&requires_2, &region_live_at, |&(r, q), &b, &()| (r, b, q));
requires.from_leapjoin(
&requires,
&mut [
&mut killed_rel.filter_anti(|&(_r, b, p)| (b, p)),
&mut cfg_edge_rel.extend_with(|&(_r, _b, p)| p),
&mut region_live_at_rel.extend_with(|&(r, _b, _p)| r),
],
|&(r, b, _p), &q| (r, b, q),
);

// borrow_live_at(B, P) :- requires(R, B, P), region_live_at(R, P)
borrow_live_at.from_join(&requires_rp, &region_live_at, |&(_r, p), &b, &()| {
// 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), ())
});

Expand Down Expand Up @@ -181,8 +189,7 @@ pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom>(
.insert(*borrow);
}

let region_live_at = region_live_at.complete();
for ((region, location), _) in &region_live_at.elements {
for (region, location) in &region_live_at_rel.elements {
result
.region_live_at
.entry(*location)
Expand Down