Skip to content

Commit

Permalink
Merge pull request #92 from lqd/naive_frog
Browse files Browse the repository at this point in the history 
Port the Naive variant to leapjoin
  • Loading branch information
@nikomatsakis
nikomatsakis committed Dec 7, 2018
2 parents cd82bbc + 6e23b72 commit 3ed4378
Showing 1 changed file with 36 additions and 29 deletions.
65 changes: 36 additions & 29 deletions polonius-engine/src/output/naive.rs
View file
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

0 comments on commit 3ed4378

Please sign in to comment.