Skip to content

Commit 99275a9

Browse files
Rewrite polonius-engine
Each section ("naive", "initialization", etc.) is now expressed as a `Computation`, with defined inputs and outputs. Computations are organized into `Pipeline`s, which execute each computation in turn, storing the results in a `Db` where they are accessible to later computations in the pipeline. `Computation`s can also dump intermediate results using the creatively-named `Dump` struct. A series of `Dumper`s can be specified for a pipeline, each which will be given access to a type-erased version of the dumped data.
1 parent 4ed67c6 commit 99275a9

22 files changed

+2073
-1323
lines changed

polonius-engine/Cargo.toml

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,14 @@ license = "Apache-2.0/MIT"
77
repository = "https://github.com/rust-lang-nursery/polonius"
88
readme = "README.md"
99
keywords = ["compiler", "borrowck", "datalog"]
10+
edition = "2018"
1011

1112
[dependencies]
13+
contracts = "0.6.2"
1214
datafrog = "2.0.0"
13-
rustc-hash = "1.0.0"
15+
dyn-clone = "1.0.4"
1416
log = "0.4"
17+
paste = "1.0.6"
18+
pretty_assertions = "1.0.0"
19+
rustc-hash = "1.0.0"
20+
smallvec = "1.8.0"

polonius-engine/src/facts.rs renamed to polonius-engine/src/compat/all_facts.rs

Lines changed: 50 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
1-
use std::fmt::Debug;
2-
use std::hash::Hash;
1+
//! An adapter for the existing `polonius-engine` interface.
2+
3+
use crate::{Db, Dump, FactTypes, StoreTo};
34

45
/// The "facts" which are the basis of the NLL borrow analysis.
56
#[derive(Clone, Debug)]
@@ -114,16 +115,51 @@ impl<T: FactTypes> Default for AllFacts<T> {
114115
}
115116
}
116117

117-
pub trait Atom:
118-
From<usize> + Into<usize> + Copy + Clone + Debug + Eq + Ord + Hash + 'static
119-
{
120-
fn index(self) -> usize;
121-
}
122-
123-
pub trait FactTypes: Copy + Clone + Debug {
124-
type Origin: Atom;
125-
type Loan: Atom;
126-
type Point: Atom;
127-
type Variable: Atom;
128-
type Path: Atom;
118+
impl<T: FactTypes> StoreTo<T> for AllFacts<T> {
119+
const RELATIONS: crate::Rels = &[
120+
"loan_issued_at",
121+
"universal_region",
122+
"cfg_edge",
123+
"loan_killed_at",
124+
"subset_base",
125+
"loan_invalidated_at",
126+
"var_used_at",
127+
"var_defined_at",
128+
"var_dropped_at",
129+
"use_of_var_derefs_origin",
130+
"drop_of_var_derefs_origin",
131+
"child_path",
132+
"path_is_var",
133+
"path_assigned_at_base",
134+
"path_moved_at_base",
135+
"path_accessed_at_base",
136+
"known_placeholder_subset_base",
137+
"placeholder",
138+
];
139+
140+
fn store_to_db(self, db: &mut Db<T>, _: &mut Dump<'_>) {
141+
db.loan_issued_at = Some(self.loan_issued_at.into());
142+
db.universal_region = Some(self.universal_region.into_iter().map(|x| (x,)).collect());
143+
db.cfg_edge = Some(self.cfg_edge.into());
144+
db.loan_killed_at = Some(self.loan_killed_at.into());
145+
db.subset_base = Some(self.subset_base.into());
146+
db.loan_invalidated_at = Some(
147+
self.loan_invalidated_at
148+
.into_iter()
149+
.map(|(a, b)| (b, a))
150+
.collect(),
151+
);
152+
db.var_used_at = Some(self.var_used_at.into());
153+
db.var_defined_at = Some(self.var_defined_at.into());
154+
db.var_dropped_at = Some(self.var_dropped_at.into());
155+
db.use_of_var_derefs_origin = Some(self.use_of_var_derefs_origin.into());
156+
db.drop_of_var_derefs_origin = Some(self.drop_of_var_derefs_origin.into());
157+
db.child_path = Some(self.child_path.into());
158+
db.path_is_var = Some(self.path_is_var.into());
159+
db.path_assigned_at_base = Some(self.path_assigned_at_base.into());
160+
db.path_moved_at_base = Some(self.path_moved_at_base.into());
161+
db.path_accessed_at_base = Some(self.path_accessed_at_base.into());
162+
db.known_placeholder_subset_base = Some(self.known_placeholder_subset.into());
163+
db.placeholder = Some(self.placeholder.into());
164+
}
129165
}

polonius-engine/src/compat/mod.rs

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
use crate::{FactTypes, Pipeline};
2+
3+
mod all_facts;
4+
mod output;
5+
6+
pub use self::all_facts::AllFacts;
7+
pub use self::output::Output;
8+
9+
#[derive(Debug, Clone, Copy)]
10+
pub enum Algorithm {
11+
/// Simple rules, but slower to execute
12+
Naive,
13+
14+
/// Optimized variant of the rules
15+
DatafrogOpt,
16+
17+
/// Fast to compute, but imprecise: there can be false-positives
18+
/// but no false-negatives. Tailored for quick "early return" situations.
19+
LocationInsensitive,
20+
21+
/// Compares the `Naive` and `DatafrogOpt` variants to ensure they indeed
22+
/// compute the same errors.
23+
Compare,
24+
25+
/// Combination of the fast `LocationInsensitive` pre-pass, followed by
26+
/// the more expensive `DatafrogOpt` variant.
27+
Hybrid,
28+
}
29+
30+
impl Algorithm {
31+
/// Optimized variants that ought to be equivalent to "naive"
32+
pub const OPTIMIZED: &'static [Algorithm] = &[Algorithm::DatafrogOpt];
33+
34+
pub fn variants() -> [&'static str; 5] {
35+
[
36+
"Naive",
37+
"DatafrogOpt",
38+
"LocationInsensitive",
39+
"Compare",
40+
"Hybrid",
41+
]
42+
}
43+
44+
fn pipeline<T: FactTypes>(&self) -> Pipeline<T> {
45+
match self {
46+
Algorithm::Naive => Pipeline::naive(),
47+
Algorithm::DatafrogOpt => Pipeline::opt(),
48+
Algorithm::LocationInsensitive => Pipeline::location_insensitive(),
49+
Algorithm::Compare => Pipeline::compare(),
50+
Algorithm::Hybrid => Pipeline::hybrid(),
51+
}
52+
}
53+
}
54+
55+
impl ::std::str::FromStr for Algorithm {
56+
type Err = String;
57+
fn from_str(s: &str) -> Result<Self, Self::Err> {
58+
match s.to_lowercase().as_ref() {
59+
"naive" => Ok(Algorithm::Naive),
60+
"datafrogopt" => Ok(Algorithm::DatafrogOpt),
61+
"locationinsensitive" => Ok(Algorithm::LocationInsensitive),
62+
"compare" => Ok(Algorithm::Compare),
63+
"hybrid" => Ok(Algorithm::Hybrid),
64+
_ => Err(String::from(
65+
"valid values: Naive, DatafrogOpt, LocationInsensitive, Compare, Hybrid",
66+
)),
67+
}
68+
}
69+
}

0 commit comments

Comments
 (0)