Skip to content

Commit 46b7c63

Browse files
authored
Merge pull request #134 from lqd/its_all_contextual
Proposal: split `AllFacts` into contexts dedicated to each component of the pipeline
2 parents ea5d4a0 + d580ea4 commit 46b7c63

File tree

8 files changed

+390
-371
lines changed

8 files changed

+390
-371
lines changed

polonius-engine/src/output/datafrog_opt.rs

Lines changed: 24 additions & 72 deletions
Original file line numberDiff line numberDiff line change
@@ -8,62 +8,32 @@
88
// option. This file may not be copied, modified, or distributed
99
// except according to those terms.
1010

11-
use std::time::Instant;
12-
13-
use crate::output::initialization;
14-
use crate::output::liveness;
15-
use crate::output::Output;
16-
1711
use datafrog::{Iteration, Relation, RelationLeaper};
18-
use facts::{AllFacts, FactTypes};
19-
20-
pub(super) fn compute<T: FactTypes>(dump_enabled: bool, all_facts: AllFacts<T>) -> Output<T> {
21-
let mut result = Output::new(dump_enabled);
22-
23-
let var_maybe_initialized_on_exit = initialization::init_var_maybe_initialized_on_exit(
24-
all_facts.child,
25-
all_facts.path_belongs_to_var,
26-
all_facts.initialized_at,
27-
all_facts.moved_out_at,
28-
all_facts.path_accessed_at,
29-
&all_facts.cfg_edge,
30-
&mut result,
31-
);
12+
use std::time::Instant;
3213

33-
let region_live_at = liveness::init_region_live_at(
34-
all_facts.var_used,
35-
all_facts.var_drop_used,
36-
all_facts.var_defined,
37-
all_facts.var_uses_region,
38-
all_facts.var_drops_region,
39-
var_maybe_initialized_on_exit,
40-
&all_facts.cfg_edge,
41-
all_facts.universal_region,
42-
&mut result,
43-
);
14+
use crate::facts::FactTypes;
15+
use crate::output::{Context, Output};
4416

17+
pub(super) fn compute<T: FactTypes>(
18+
ctx: &Context<T>,
19+
result: &mut Output<T>,
20+
) -> Relation<(T::Loan, T::Point)> {
4521
let timer = Instant::now();
4622

4723
let errors = {
24+
// Static inputs
25+
let region_live_at_rel = &ctx.region_live_at;
26+
let cfg_edge_rel = &ctx.cfg_edge;
27+
let killed_rel = &ctx.killed;
28+
4829
// Create a new iteration context, ...
4930
let mut iteration = Iteration::new();
5031

51-
// static inputs
52-
let cfg_edge_rel = Relation::from_iter(
53-
all_facts
54-
.cfg_edge
55-
.iter()
56-
.map(|&(point1, point2)| (point1, point2)),
57-
);
58-
59-
let killed_rel: Relation<(T::Loan, T::Point)> = all_facts.killed.into();
60-
6132
// `invalidates` facts, stored ready for joins
6233
let invalidates = iteration.variable::<((T::Loan, T::Point), ())>("invalidates");
6334

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

@@ -158,16 +128,14 @@ pub(super) fn compute<T: FactTypes>(dump_enabled: bool, all_facts: AllFacts<T>)
158128

159129
// Make "variable" versions of the relations, needed for joins.
160130
borrow_region_op.extend(
161-
all_facts
162-
.borrow_region
131+
ctx.borrow_region
163132
.iter()
164133
.map(|&(origin, loan, point)| ((origin, point), loan)),
165134
);
166135
invalidates.extend(
167-
all_facts
168-
.invalidates
136+
ctx.invalidates
169137
.iter()
170-
.map(|&(point, loan)| ((loan, point), ())),
138+
.map(|&(loan, point)| ((loan, point), ())),
171139
);
172140
region_live_at_var.extend(
173141
region_live_at_rel
@@ -177,16 +145,14 @@ pub(super) fn compute<T: FactTypes>(dump_enabled: bool, all_facts: AllFacts<T>)
177145

178146
// subset(origin1, origin2, point) :- outlives(origin1, origin2, point).
179147
subset_o1p.extend(
180-
all_facts
181-
.outlives
148+
ctx.outlives
182149
.iter()
183150
.map(|&(origin1, origin2, point)| ((origin1, point), origin2)),
184151
);
185152

186153
// requires(origin, loan, point) :- borrow_region(origin, loan, point).
187154
requires_op.extend(
188-
all_facts
189-
.borrow_region
155+
ctx.borrow_region
190156
.iter()
191157
.map(|&(origin, loan, point)| ((origin, point), loan)),
192158
);
@@ -408,15 +374,7 @@ pub(super) fn compute<T: FactTypes>(dump_enabled: bool, all_facts: AllFacts<T>)
408374
});
409375
}
410376

411-
if dump_enabled {
412-
for &(origin, location) in region_live_at_rel.iter() {
413-
result
414-
.region_live_at
415-
.entry(location)
416-
.or_default()
417-
.push(origin);
418-
}
419-
377+
if result.dump_enabled {
420378
let subset_o1p = subset_o1p.complete();
421379
assert!(
422380
subset_o1p
@@ -460,17 +418,11 @@ pub(super) fn compute<T: FactTypes>(dump_enabled: bool, all_facts: AllFacts<T>)
460418
errors.complete()
461419
};
462420

463-
if dump_enabled {
464-
info!(
465-
"errors is complete: {} tuples, {:?}",
466-
errors.len(),
467-
timer.elapsed()
468-
);
469-
}
470-
471-
for &(loan, location) in errors.iter() {
472-
result.errors.entry(location).or_default().push(loan);
473-
}
421+
info!(
422+
"errors is complete: {} tuples, {:?}",
423+
errors.len(),
424+
timer.elapsed()
425+
);
474426

475-
result
427+
errors
476428
}

polonius-engine/src/output/hybrid.rs

Lines changed: 0 additions & 26 deletions
This file was deleted.

polonius-engine/src/output/initialization.rs

Lines changed: 20 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -1,30 +1,25 @@
11
use std::time::Instant;
22

3-
use crate::output::Output;
4-
use facts::FactTypes;
3+
use crate::facts::FactTypes;
4+
use crate::output::{InitializationContext, Output};
55

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

88
pub(super) fn init_var_maybe_initialized_on_exit<T: FactTypes>(
9-
child: Vec<(T::Path, T::Path)>,
10-
path_belongs_to_var: Vec<(T::Path, T::Variable)>,
11-
initialized_at: Vec<(T::Path, T::Point)>,
12-
moved_out_at: Vec<(T::Path, T::Point)>,
13-
path_accessed_at: Vec<(T::Path, T::Point)>,
14-
cfg_edge: &[(T::Point, T::Point)],
9+
ctx: InitializationContext<T>,
10+
cfg_edge: &Relation<(T::Point, T::Point)>,
1511
output: &mut Output<T>,
16-
) -> Vec<(T::Variable, T::Point)> {
17-
let computation_start = Instant::now();
12+
) -> Relation<(T::Variable, T::Point)> {
13+
let timer = Instant::now();
1814
let mut iteration = Iteration::new();
1915

2016
// Relations
2117
//let parent: Relation<(Path, Path)> = child.iter().map(|&(child_path, parent_path)| (parent_path, child_path)).collect();
22-
let child: Relation<(T::Path, T::Path)> = child.into();
23-
let path_belongs_to_var: Relation<(T::Path, T::Variable)> = path_belongs_to_var.into();
24-
let initialized_at: Relation<(T::Path, T::Point)> = initialized_at.into();
25-
let moved_out_at: Relation<(T::Path, T::Point)> = moved_out_at.into();
26-
let cfg_edge: Relation<(T::Point, T::Point)> = cfg_edge.iter().cloned().collect();
27-
let _path_accessed_at: Relation<(T::Path, T::Point)> = path_accessed_at.into();
18+
let child: Relation<(T::Path, T::Path)> = ctx.child.into();
19+
let path_belongs_to_var: Relation<(T::Path, T::Variable)> = ctx.path_belongs_to_var.into();
20+
let initialized_at: Relation<(T::Path, T::Point)> = ctx.initialized_at.into();
21+
let moved_out_at: Relation<(T::Path, T::Point)> = ctx.moved_out_at.into();
22+
let _path_accessed_at: Relation<(T::Path, T::Point)> = ctx.path_accessed_at.into();
2823

2924
// Variables
3025

@@ -60,10 +55,10 @@ pub(super) fn init_var_maybe_initialized_on_exit<T: FactTypes>(
6055
// path_maybe_initialized_on_exit(Mother, point) :-
6156
// path_maybe_initialized_on_exit(Daughter, point),
6257
// child(Daughter, Mother).
63-
path_maybe_initialized_on_exit.from_leapjoin(
58+
path_maybe_initialized_on_exit.from_join(
6459
&path_maybe_initialized_on_exit,
65-
child.extend_with(|&(daughter, _point)| daughter),
66-
|&(_daughter, point), &mother| (mother, point),
60+
&child,
61+
|&_daughter, &point, &mother| (mother, point),
6762
);
6863

6964
// TODO: the following lines contain things left to implement for move
@@ -93,12 +88,12 @@ pub(super) fn init_var_maybe_initialized_on_exit<T: FactTypes>(
9388
// END TODO
9489

9590
// var_maybe_initialized_on_exit(var, point) :-
96-
// path_belongs_to_var(path, var),
97-
// path_maybe_initialized_at(path, point).
98-
var_maybe_initialized_on_exit.from_leapjoin(
91+
// path_maybe_initialized_on_exit(path, point),
92+
// path_belongs_to_var(path, var).
93+
var_maybe_initialized_on_exit.from_join(
9994
&path_maybe_initialized_on_exit,
100-
path_belongs_to_var.extend_with(|&(path, _point)| path),
101-
|&(_path, point), &var| (var, point),
95+
&path_belongs_to_var,
96+
|&_path, &point, &var| (var, point),
10297
);
10398
}
10499

@@ -107,7 +102,7 @@ pub(super) fn init_var_maybe_initialized_on_exit<T: FactTypes>(
107102
info!(
108103
"init_var_maybe_initialized_on_exit() completed: {} tuples, {:?}",
109104
var_maybe_initialized_on_exit.len(),
110-
computation_start.elapsed()
105+
timer.elapsed()
111106
);
112107

113108
if output.dump_enabled {
@@ -130,7 +125,4 @@ pub(super) fn init_var_maybe_initialized_on_exit<T: FactTypes>(
130125
}
131126

132127
var_maybe_initialized_on_exit
133-
.iter()
134-
.map(|&(var, point)| (var, point))
135-
.collect()
136128
}

0 commit comments

Comments
 (0)