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.

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

replace fact type parameters with FactTypes #130

Merged
merged 4 commits into from
Oct 3, 2019
Merged
Changes from 1 commit
Commits
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
Prev Previous commit
replace type parameters in polonius bin
csmoe committed Sep 25, 2019
commit 4cf4dbe6c6c8cf802ed1c9313ef1f94b803449aa
61 changes: 30 additions & 31 deletions polonius-engine/src/output/datafrog_opt.rs
Original file line number Diff line number Diff line change
@@ -18,31 +18,28 @@ use crate::output::Output;
use datafrog::{Iteration, Relation, RelationLeaper};
use facts::{AllFacts, FactTypes};

pub(super) fn compute<T: FactTypes>(
dump_enabled: bool,
all_facts: AllFacts<T>,
) -> Output<T> {
pub(super) fn compute<T: FactTypes>(dump_enabled: bool, all_facts: AllFacts<T>) -> Output<T> {
let mut result = Output::new(dump_enabled);

let var_maybe_initialized_on_exit = initialization::init_var_maybe_initialized_on_exit(
all_facts.child.clone(),
all_facts.path_belongs_to_var.clone(),
all_facts.initialized_at.clone(),
all_facts.moved_out_at.clone(),
all_facts.path_accessed_at.clone(),
&all_facts.cfg_edge.clone(),
all_facts.child,
all_facts.path_belongs_to_var,
all_facts.initialized_at,
all_facts.moved_out_at,
all_facts.path_accessed_at,
&all_facts.cfg_edge,
&mut result,
);

let region_live_at = liveness::init_region_live_at(
all_facts.var_used.clone(),
all_facts.var_drop_used.clone(),
all_facts.var_defined.clone(),
all_facts.var_uses_region.clone(),
all_facts.var_drops_region.clone(),
var_maybe_initialized_on_exit.clone(),
&all_facts.cfg_edge.clone(),
all_facts.universal_region.clone(),
all_facts.var_used,
all_facts.var_drop_used,
all_facts.var_defined,
all_facts.var_uses_region,
all_facts.var_drops_region,
var_maybe_initialized_on_exit,
&all_facts.cfg_edge,
all_facts.universal_region,
&mut result,
);

@@ -55,18 +52,20 @@ pub(super) fn compute<T: FactTypes>(
// static inputs
let cfg_edge_rel = Relation::from_iter(all_facts.cfg_edge.iter().map(|&(p, q)| (p, q)));

let killed_rel: Relation<(T::Loan, T::Point)> = all_facts.killed.clone().into();
let killed_rel: Relation<(T::Loan, T::Point)> = all_facts.killed.into();

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

// we need `region_live_at` in both variable and relation forms.
// (respectively, for join and antijoin).
let region_live_at_rel: Relation<(T::Origin, T::Point)> = region_live_at.into();
let region_live_at_var = iteration.variable::<((T::Origin, T::Point), ())>("region_live_at");
let region_live_at_var =
iteration.variable::<((T::Origin, T::Point), ())>("region_live_at");

// `borrow_region` input but organized for join
let borrow_region_rp = iteration.variable::<((T::Origin, T::Point), T::Loan)>("borrow_region_rp");
let borrow_region_rp =
iteration.variable::<((T::Origin, T::Point), T::Loan)>("borrow_region_rp");

// .decl subset(R1, R2, P)
//
@@ -94,15 +93,15 @@ pub(super) fn compute<T: FactTypes>(
// In that case, `Q` would like to add all the
// live things reachable from `R2` to `R1`.
//
let live_to_dying_regions_r2pq =
iteration.variable::<((T::Origin, T::Point, T::Point), T::Origin)>("live_to_dying_regions_r2pq");
let live_to_dying_regions_r2pq = iteration
.variable::<((T::Origin, T::Point, T::Point), T::Origin)>("live_to_dying_regions_r2pq");

// .decl dying_region_requires((R, P, Q), B)
//
// The origin `R` requires the borrow `B`, but the
// origin `R` goes dead along the edge `P -> Q`
let dying_region_requires =
iteration.variable::<((T::Origin, T::Point, T::Point), T::Loan)>("dying_region_requires");
let dying_region_requires = iteration
.variable::<((T::Origin, T::Point, T::Point), T::Loan)>("dying_region_requires");

// .decl dying_can_reach_origins(R, P, Q)
//
@@ -131,19 +130,19 @@ pub(super) fn compute<T: FactTypes>(
// relation. This is a subset of the full `dying_can_reach`
// relation where we filter down to those cases where R2 is
// live in Q.
let dying_can_reach_live =
iteration.variable::<((T::Origin, T::Point, T::Point), T::Origin)>("dying_can_reach_live");
let dying_can_reach_live = iteration
.variable::<((T::Origin, T::Point, T::Point), T::Origin)>("dying_can_reach_live");

// .decl dead_borrow_region_can_reach_root((R, P), B)
//
// Indicates a "borrow region" R at P which is not live on
// entry to P.
let dead_borrow_region_can_reach_root =
iteration.variable::<((T::Origin, T::Point), T::Loan)>("dead_borrow_region_can_reach_root");
let dead_borrow_region_can_reach_root = iteration
.variable::<((T::Origin, T::Point), T::Loan)>("dead_borrow_region_can_reach_root");

// .decl dead_borrow_region_can_reach_dead((R2, P), B)
let dead_borrow_region_can_reach_dead =
iteration.variable::<((T::Origin, T::Point), T::Loan)>("dead_borrow_region_can_reach_dead");
let dead_borrow_region_can_reach_dead = iteration
.variable::<((T::Origin, T::Point), T::Loan)>("dead_borrow_region_can_reach_dead");
let dead_borrow_region_can_reach_dead_1 =
iteration.variable_indistinct("dead_borrow_region_can_reach_dead_1");

7 changes: 2 additions & 5 deletions polonius-engine/src/output/hybrid.rs
Original file line number Diff line number Diff line change
@@ -16,11 +16,8 @@ use crate::output::location_insensitive;
use crate::output::Output;
use facts::{AllFacts, FactTypes};

pub(super) fn compute<T: FactTypes>(
dump_enabled: bool,
all_facts: AllFacts<T>,
) -> Output<T> {
let lins_output = location_insensitive::compute(dump_enabled, all_facts.clone());
pub(super) fn compute<T: FactTypes>(dump_enabled: bool, all_facts: AllFacts<T>) -> Output<T> {
let lins_output = location_insensitive::compute(dump_enabled, &all_facts);
if lins_output.errors.is_empty() {
lins_output
} else {
3 changes: 2 additions & 1 deletion polonius-engine/src/output/liveness.rs
Original file line number Diff line number Diff line change
@@ -34,7 +34,8 @@ pub(super) fn compute_live_regions<T: FactTypes>(

// Relations
let var_defined_rel: Relation<(T::Variable, T::Point)> = var_defined.into();
let cfg_edge_rel: Relation<(T::Point, T::Point)> = cfg_edge.iter().map(|(p, q)| (*p, *q)).collect();
let cfg_edge_rel: Relation<(T::Point, T::Point)> =
cfg_edge.iter().map(|(p, q)| (*p, *q)).collect();
let cfg_edge_reverse_rel: Relation<(T::Point, T::Point)> =
cfg_edge.iter().map(|(p, q)| (*q, *p)).collect();
let var_uses_region_rel: Relation<(T::Variable, T::Origin)> = var_uses_region.into();
5 changes: 1 addition & 4 deletions polonius-engine/src/output/location_insensitive.rs
Original file line number Diff line number Diff line change
@@ -18,10 +18,7 @@ use crate::output::Output;
use datafrog::{Iteration, Relation, RelationLeaper};
use facts::{AllFacts, FactTypes};

pub(super) fn compute<T: FactTypes>(
dump_enabled: bool,
all_facts: AllFacts<T>,
) -> Output<T> {
pub(super) fn compute<T: FactTypes>(dump_enabled: bool, all_facts: &AllFacts<T>) -> Output<T> {
let mut result = Output::new(dump_enabled);
let var_maybe_initialized_on_exit = initialization::init_var_maybe_initialized_on_exit(
all_facts.child.clone(),
26 changes: 14 additions & 12 deletions polonius-engine/src/output/mod.rs
Original file line number Diff line number Diff line change
@@ -118,20 +118,16 @@ fn compare_errors<Loan: Atom, Point: Atom>(
}

impl<T: FactTypes> Output<T> {
pub fn compute(
all_facts: AllFacts<T>,
algorithm: Algorithm,
dump_enabled: bool,
) -> Self {
pub fn compute(all_facts: &AllFacts<T>, algorithm: Algorithm, dump_enabled: bool) -> Self {
match algorithm {
Algorithm::Naive => naive::compute(dump_enabled, all_facts),
Algorithm::DatafrogOpt => datafrog_opt::compute(dump_enabled, all_facts),
Algorithm::Naive => naive::compute(dump_enabled, all_facts.clone()),
Algorithm::DatafrogOpt => datafrog_opt::compute(dump_enabled, all_facts.clone()),
Algorithm::LocationInsensitive => {
location_insensitive::compute(dump_enabled, all_facts)
location_insensitive::compute(dump_enabled, &all_facts)
}
Algorithm::Compare => {
let naive_output = naive::compute(dump_enabled, all_facts.clone());
let opt_output = datafrog_opt::compute(dump_enabled, all_facts);
let opt_output = datafrog_opt::compute(dump_enabled, all_facts.clone());
if compare_errors(&naive_output.errors, &opt_output.errors) {
panic!(concat!(
"The errors reported by the naive algorithm differ from ",
@@ -143,7 +139,7 @@ impl<T: FactTypes> Output<T> {
}
opt_output
}
Algorithm::Hybrid => hybrid::compute(dump_enabled, all_facts),
Algorithm::Hybrid => hybrid::compute(dump_enabled, all_facts.clone()),
}
}

@@ -179,7 +175,10 @@ impl<T: FactTypes> Output<T> {
}
}

pub fn restricts_at(&self, location: T::Point) -> Cow<'_, BTreeMap<T::Origin, BTreeSet<T::Loan>>> {
pub fn restricts_at(
&self,
location: T::Point,
) -> Cow<'_, BTreeMap<T::Origin, BTreeSet<T::Loan>>> {
assert!(self.dump_enabled);
match self.restricts.get(&location) {
Some(map) => Cow::Borrowed(map),
@@ -195,7 +194,10 @@ impl<T: FactTypes> Output<T> {
}
}

pub fn subsets_at(&self, location: T::Point) -> Cow<'_, BTreeMap<T::Origin, BTreeSet<T::Origin>>> {
pub fn subsets_at(
&self,
location: T::Point,
) -> Cow<'_, BTreeMap<T::Origin, BTreeSet<T::Origin>>> {
assert!(self.dump_enabled);
match self.subset.get(&location) {
Some(v) => Cow::Borrowed(v),
8 changes: 3 additions & 5 deletions polonius-engine/src/output/naive.rs
Original file line number Diff line number Diff line change
@@ -20,10 +20,7 @@ use facts::{AllFacts, FactTypes};

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

pub(super) fn compute<T: FactTypes>(
dump_enabled: bool,
all_facts: AllFacts<T>,
) -> Output<T> {
pub(super) fn compute<T: FactTypes>(dump_enabled: bool, all_facts: AllFacts<T>) -> Output<T> {
let mut result = Output::new(dump_enabled);

let var_maybe_initialized_on_exit = initialization::init_var_maybe_initialized_on_exit(
@@ -76,7 +73,8 @@ pub(super) fn compute<T: FactTypes>(

// 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::<((T::Origin, T::Point), ())>("region_live_at");
let region_live_at_var =
iteration.variable::<((T::Origin, T::Point), ())>("region_live_at");

// output
let errors = iteration.variable("errors");
2 changes: 1 addition & 1 deletion src/dump.rs
Original file line number Diff line number Diff line change
@@ -13,7 +13,7 @@ use std::hash::Hash;
use std::io::{self, Write};
use std::path::PathBuf;

pub(crate) type Output = PoloniusEngineOutput<T>;
pub(crate) type Output = PoloniusEngineOutput<LocalFacts>;

pub(crate) fn dump_output(
output: &Output,
15 changes: 13 additions & 2 deletions src/facts.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,9 @@
use polonius_engine;
use polonius_engine::{self, FactTypes};

pub(crate) type AllFacts = polonius_engine::AllFacts<T>;
#[derive(Copy, Clone, Debug)]
pub(crate) struct LocalFacts;

pub(crate) type AllFacts = polonius_engine::AllFacts<LocalFacts>;

macro_rules! index_type {
($t:ident) => {
@@ -36,3 +39,11 @@ index_type!(Loan);
index_type!(Point);
index_type!(Variable);
index_type!(MovePath);

impl FactTypes for LocalFacts {
type Origin = Origin;
type Loan = Loan;
type Point = Point;
type Variable = Variable;
type MovePath = MovePath;
}