Skip to content

Commit

Permalink
DO NOT MERGE: Add a CondenseCfg algorithm according to rust-lang#20
Browse files Browse the repository at this point in the history
  • Loading branch information
ia0 committed May 28, 2018
1 parent 7d5a460 commit 6669183
Show file tree
Hide file tree
Showing 3 changed files with 165 additions and 0 deletions.
158 changes: 158 additions & 0 deletions polonius-engine/src/output/condense_cfg.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,158 @@
// Copyright 2018 The Rust Project Developers. See the COPYRIGHT
// file at the top-level directory of this distribution and at
// http://rust-lang.org/COPYRIGHT.
//
// Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
// option. This file may not be copied, modified, or distributed
// except according to those terms.

//! A fork of the Naive datalog analysis using Datafrog trying to condense the control flow graph.
//! See https://github.com/rust-lang-nursery/polonius/issues/20.

use std::collections::{BTreeMap, BTreeSet};

use facts::{AllFacts, Atom};

fn extract_singleton<Point: Atom>(m: &BTreeSet<Point>) -> Option<Point> {
if m.len() != 1 {
return None;
}
for &p in m {
return Some(p);
}
unreachable!();
}

pub(super) fn compute<Region: Atom, Loan: Atom, Point: Atom>(
verbose: bool,
all_facts: AllFacts<Region, Loan, Point>,
) -> AllFacts<Region, Loan, Point> {
let mut all_points = BTreeSet::new();
let mut pred = BTreeMap::new();
let mut succ = BTreeMap::new();
for &(p, q) in all_facts.cfg_edge.iter() {
assert!(succ.entry(p).or_insert_with(|| BTreeSet::new()).insert(q));
assert!(pred.entry(q).or_insert_with(|| BTreeSet::new()).insert(p));
if verbose {
all_points.insert(p);
all_points.insert(q);
}
}
let mut region_live_at = BTreeMap::new();
for &(r, p) in all_facts.region_live_at.iter() {
assert!(
region_live_at
.entry(p)
.or_insert_with(|| BTreeSet::new())
.insert(r)
);
}
let mut outlives_at = BTreeSet::new();
for &(_, _, p) in all_facts.outlives.iter() {
// We may have several outlives relations at a given point.
outlives_at.insert(p);
}

let mut merge_into = BTreeMap::new();
for (p, qs) in succ.iter() {
let q = match extract_singleton(qs) {
Some(q) => q,
None => continue,
};
if let Some(should_be_p) = pred.get(&q).and_then(extract_singleton) {
assert!(should_be_p == *p);
} else {
continue;
}
if region_live_at.get(p) != region_live_at.get(&q) {
continue;
}
if outlives_at.contains(p) || outlives_at.contains(&q) {
continue;
}
assert!(merge_into.insert(q, *p) == None);
}
if verbose {
println!(
"There are {}/{} nodes to be merged.",
merge_into.len(),
all_points.len()
);
}
let first_merge_into = |q: Point| -> Option<Point> {
match merge_into.get(&q) {
None => None,
Some(q) => {
let mut r = *q;
while let Some(p) = merge_into.get(&r) { r = *p; }
Some(r)
}
}
};
let last_merge_into = |mut p: Point| -> Point {
loop {
let qs = match succ.get(&p) {
None => return p,
Some(qs) => qs,
};
p = match extract_singleton(qs) {
None => return p,
Some(p) if merge_into.get(&p).is_some() => p,
Some(_) => return p,
};
}
};

let mut result = <AllFacts<Region, Loan, Point>>::default();
let mut borrow_region: BTreeMap<(Region, Loan), BTreeSet<Point>> = BTreeMap::new();
for &(r, l, q) in all_facts.borrow_region.iter() {
let s = borrow_region.entry((r, l)).or_insert_with(|| BTreeSet::new());
match first_merge_into(q) {
None => { assert!(s.insert(q)); }
Some(p) => { s.insert(p); }
};
}
for ((r, l), ps) in borrow_region {
for p in ps {
result.borrow_region.push((r, l, p));
}
}
result.universal_region = all_facts.universal_region;
for &(p, q) in all_facts.cfg_edge.iter() {
if first_merge_into(p).is_some() { continue; }
result.cfg_edge.push((p, last_merge_into(q)));
}
let mut killed: BTreeMap<Loan, BTreeSet<Point>> = BTreeMap::new();
for &(l, q) in all_facts.killed.iter() {
let s = killed.entry(l).or_insert_with(|| BTreeSet::new());
match first_merge_into(q) {
None => { assert!(s.insert(q)); }
Some(p) => { s.insert(p); }
};
}
for (l, ps) in killed {
for p in ps {
result.killed.push((l, p));
}
}
for &(r, p) in all_facts.region_live_at.iter() {
if merge_into.get(&p).is_some() { continue; }
result.region_live_at.push((r, p));
}
let mut invalidates: BTreeMap<Loan, BTreeSet<Point>> = BTreeMap::new();
for &(q, l) in all_facts.invalidates.iter() {
let s = invalidates.entry(l).or_insert_with(|| BTreeSet::new());
match first_merge_into(q) {
None => { assert!(s.insert(q)); }
Some(p) => { s.insert(p); }
};
}
for (l, ps) in invalidates {
for p in ps {
result.invalidates.push((p, l));
}
}
result
}
5 changes: 5 additions & 0 deletions polonius-engine/src/output/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,11 +15,13 @@ use std::collections::{BTreeMap, BTreeSet};
mod datafrog_opt;
mod location_insensitive;
mod naive;
mod condense_cfg;
use facts::{AllFacts, Atom};

#[derive(Debug, Clone, Copy)]
pub enum Algorithm {
Naive,
CondenseCfg,
DatafrogOpt,
LocationInsensitive,
}
Expand Down Expand Up @@ -53,6 +55,9 @@ where
) -> Self {
match algorithm {
Algorithm::Naive => naive::compute(dump_enabled, all_facts.clone()),
Algorithm::CondenseCfg => {
naive::compute(dump_enabled, condense_cfg::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.clone())
Expand Down
2 changes: 2 additions & 0 deletions src/cli.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ arg_enum! {
#[derive(Debug, Clone, Copy)]
pub enum AlgorithmOpts {
Naive,
CondenseCfg,
DatafrogOpt,
LocationInsensitive,
}
Expand All @@ -23,6 +24,7 @@ impl Into<Algorithm> for AlgorithmOpts {
fn into(self) -> Algorithm {
match self {
AlgorithmOpts::Naive => Algorithm::Naive,
AlgorithmOpts::CondenseCfg => Algorithm::CondenseCfg,
AlgorithmOpts::DatafrogOpt => Algorithm::DatafrogOpt,
AlgorithmOpts::LocationInsensitive => Algorithm::LocationInsensitive,
}
Expand Down

0 comments on commit 6669183

Please sign in to comment.