From 6e23b722342dfbb5e1a9c20271cbe9726848e058 Mon Sep 17 00:00:00 2001 From: lqd Date: Thu, 6 Dec 2018 19:53:38 +0100 Subject: [PATCH] Port the Naive variant to leapjoin On the `clap` dataset: - before: around 30s - after: around 23.2s Once datafrog relaxes the leapjoin well-formedness check, we'll be able to port a couple more joins (and remove a big index). The other remaining joins are between dynamic variables, which datafrog leapjoins won't support for at least a while. --- polonius-engine/src/output/naive.rs | 65 ++++++++++++++++------------- 1 file changed, 36 insertions(+), 29 deletions(-) diff --git a/polonius-engine/src/output/naive.rs b/polonius-engine/src/output/naive.rs index 000c4e8279a..f0fee53fc78 100644 --- a/polonius-engine/src/output/naive.rs +++ b/polonius-engine/src/output/naive.rs @@ -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( dump_enabled: bool, @@ -46,6 +46,10 @@ pub(super) fn compute( // 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"); @@ -57,21 +61,14 @@ pub(super) fn compute( // 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"); @@ -82,10 +79,9 @@ pub(super) fn compute( 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() { @@ -106,10 +102,8 @@ pub(super) fn compute( // 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. @@ -124,12 +118,18 @@ pub(super) fn compute( // 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, ®ion_live_at, |&(r1, q), &r2, &()| { - ((r2, q), r1) - }); - subset.from_join(&subset_2, ®ion_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), @@ -141,12 +141,20 @@ pub(super) fn compute( // !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, ®ion_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, ®ion_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, ®ion_live_at_var, |&(_r, p), &b, &()| { ((b, p), ()) }); @@ -181,8 +189,7 @@ pub(super) fn compute( .insert(*borrow); } - let region_live_at = region_live_at.complete(); - for ((region, location), _) in ®ion_live_at.elements { + for (region, location) in ®ion_live_at_rel.elements { result .region_live_at .entry(*location)