]>
Commit | Line | Data |
---|---|---|
e1599b0c XL |
1 | use std::time::Instant; |
2 | ||
d9bb1a4e FG |
3 | use crate::facts::FactTypes; |
4 | use crate::output::{InitializationContext, Output}; | |
e1599b0c XL |
5 | |
6 | use datafrog::{Iteration, Relation, RelationLeaper}; | |
7 | ||
72b1a166 FG |
8 | // This represents the output of an intermediate elaboration step (step 1). |
9 | struct TransitivePaths<T: FactTypes> { | |
10 | path_moved_at: Relation<(T::Path, T::Point)>, | |
11 | path_assigned_at: Relation<(T::Path, T::Point)>, | |
12 | path_accessed_at: Relation<(T::Path, T::Point)>, | |
13 | path_begins_with_var: Relation<(T::Path, T::Variable)>, | |
14 | } | |
15 | ||
16 | struct InitializationStatus<T: FactTypes> { | |
17 | var_maybe_partly_initialized_on_exit: Relation<(T::Variable, T::Point)>, | |
18 | move_error: Relation<(T::Path, T::Point)>, | |
19 | } | |
20 | ||
21 | pub(super) struct InitializationResult<T: FactTypes>( | |
22 | pub(super) Relation<(T::Variable, T::Point)>, | |
23 | pub(super) Relation<(T::Path, T::Point)>, | |
24 | ); | |
25 | ||
26 | // Step 1: compute transitive closures of path operations. This would elaborate, | |
27 | // for example, an access to x into an access to x.f, x.f.0, etc. We do this for: | |
28 | // - access to a path | |
29 | // - initialization of a path | |
30 | // - moves of a path | |
31 | // FIXME: transitive rooting in a variable (path_begins_with_var) | |
32 | // Note that this step may not be entirely necessary! | |
33 | fn compute_transitive_paths<T: FactTypes>( | |
34 | child_path: Vec<(T::Path, T::Path)>, | |
35 | path_assigned_at_base: Vec<(T::Path, T::Point)>, | |
36 | path_moved_at_base: Vec<(T::Path, T::Point)>, | |
37 | path_accessed_at_base: Vec<(T::Path, T::Point)>, | |
38 | path_is_var: Vec<(T::Path, T::Variable)>, | |
39 | ) -> TransitivePaths<T> { | |
e1599b0c | 40 | let mut iteration = Iteration::new(); |
72b1a166 FG |
41 | let child_path: Relation<(T::Path, T::Path)> = child_path.into(); |
42 | ||
43 | let ancestor_path = iteration.variable::<(T::Path, T::Path)>("ancestor"); | |
44 | ||
45 | // These are the actual targets: | |
46 | let path_moved_at = iteration.variable::<(T::Path, T::Point)>("path_moved_at"); | |
47 | let path_assigned_at = iteration.variable::<(T::Path, T::Point)>("path_initialized_at"); | |
48 | let path_accessed_at = iteration.variable::<(T::Path, T::Point)>("path_accessed_at"); | |
49 | let path_begins_with_var = iteration.variable::<(T::Path, T::Variable)>("path_begins_with_var"); | |
50 | ||
51 | // ancestor_path(Parent, Child) :- child_path(Child, Parent). | |
52 | ancestor_path.extend(child_path.iter().map(|&(child, parent)| (parent, child))); | |
53 | ||
54 | // path_moved_at(Path, Point) :- path_moved_at_base(Path, Point). | |
55 | path_moved_at.insert(path_moved_at_base.into()); | |
56 | ||
57 | // path_assigned_at(Path, Point) :- path_assigned_at_base(Path, Point). | |
58 | path_assigned_at.insert(path_assigned_at_base.into()); | |
59 | ||
60 | // path_accessed_at(Path, Point) :- path_accessed_at_base(Path, Point). | |
61 | path_accessed_at.insert(path_accessed_at_base.into()); | |
62 | ||
63 | // path_begins_with_var(Path, Var) :- path_is_var(Path, Var). | |
64 | path_begins_with_var.insert(path_is_var.into()); | |
65 | ||
66 | while iteration.changed() { | |
67 | // ancestor_path(Grandparent, Child) :- | |
68 | // ancestor_path(Parent, Child), | |
69 | // child_path(Parent, Grandparent). | |
70 | ancestor_path.from_join( | |
71 | &ancestor_path, | |
72 | &child_path, | |
73 | |&_parent, &child, &grandparent| (grandparent, child), | |
74 | ); | |
75 | ||
76 | // moving a path moves its children | |
77 | // path_moved_at(Child, Point) :- | |
78 | // path_moved_at(Parent, Point), | |
79 | // ancestor_path(Parent, Child). | |
80 | path_moved_at.from_join(&path_moved_at, &ancestor_path, |&_parent, &p, &child| { | |
81 | (child, p) | |
82 | }); | |
83 | ||
84 | // initialising x at p initialises all x:s children | |
85 | // path_assigned_at(Child, point) :- | |
86 | // path_assigned_at(Parent, point), | |
87 | // ancestor_path(Parent, Child). | |
88 | path_assigned_at.from_join(&path_assigned_at, &ancestor_path, |&_parent, &p, &child| { | |
89 | (child, p) | |
90 | }); | |
e1599b0c | 91 | |
72b1a166 FG |
92 | // accessing x at p accesses all x:s children at p (actually, |
93 | // accesses should be maximally precise and this shouldn't happen?) | |
94 | // path_accessed_at(Child, point) :- | |
95 | // path_accessed_at(Parent, point), | |
96 | // ancestor_path(Parent, Child). | |
97 | path_accessed_at.from_join(&path_accessed_at, &ancestor_path, |&_parent, &p, &child| { | |
98 | (child, p) | |
99 | }); | |
100 | ||
101 | // path_begins_with_var(Child, Var) :- | |
102 | // path_begins_with_var(Parent, Var) | |
103 | // ancestor_path(Parent, Child). | |
104 | path_begins_with_var.from_join( | |
105 | &path_begins_with_var, | |
106 | &ancestor_path, | |
107 | |&_parent, &var, &child| (child, var), | |
108 | ); | |
109 | } | |
110 | ||
111 | TransitivePaths { | |
112 | path_assigned_at: path_assigned_at.complete(), | |
113 | path_moved_at: path_moved_at.complete(), | |
114 | path_accessed_at: path_accessed_at.complete(), | |
115 | path_begins_with_var: path_begins_with_var.complete(), | |
116 | } | |
117 | } | |
e1599b0c | 118 | |
72b1a166 FG |
119 | // Step 2: Compute path initialization and deinitialization across the CFG. |
120 | fn compute_move_errors<T: FactTypes>( | |
121 | ctx: TransitivePaths<T>, | |
122 | cfg_edge: &Relation<(T::Point, T::Point)>, | |
123 | output: &mut Output<T>, | |
124 | ) -> InitializationStatus<T> { | |
125 | let mut iteration = Iteration::new(); | |
e1599b0c XL |
126 | // Variables |
127 | ||
72b1a166 FG |
128 | // var_maybe_partly_initialized_on_exit(var, point): Upon leaving `point`, |
129 | // `var` is partially initialized for some path through the CFG, that is | |
130 | // there has been an initialization of var, and var has not been moved in | |
131 | // all paths through the CFG. | |
132 | let var_maybe_partly_initialized_on_exit = | |
133 | iteration.variable::<(T::Variable, T::Point)>("var_maybe_partly_initialized_on_exit"); | |
e1599b0c | 134 | |
72b1a166 FG |
135 | // path_maybe_initialized_on_exit(path, point): Upon leaving `point`, the |
136 | // move path `path` is initialized for some path through the CFG. | |
e1599b0c | 137 | let path_maybe_initialized_on_exit = |
d9bb1a4e | 138 | iteration.variable::<(T::Path, T::Point)>("path_maybe_initialized_on_exit"); |
e1599b0c | 139 | |
72b1a166 FG |
140 | // path_maybe_uninitialized_on_exit(Path, Point): There exists at least one |
141 | // path through the CFG to Point such that `Path` has been moved out by the | |
142 | // time we arrive at `Point` without it being re-initialized for sure. | |
143 | let path_maybe_uninitialized_on_exit = | |
144 | iteration.variable::<(T::Path, T::Point)>("path_maybe_uninitialized_on_exit"); | |
145 | ||
146 | // move_error(Path, Point): There is an access to `Path` at `Point`, but | |
147 | // `Path` is potentially moved (or never initialised). | |
148 | let move_error = iteration.variable::<(T::Path, T::Point)>("move_error"); | |
149 | ||
e1599b0c XL |
150 | // Initial propagation of static relations |
151 | ||
72b1a166 FG |
152 | // path_maybe_initialized_on_exit(path, point) :- path_assigned_at(path, point). |
153 | path_maybe_initialized_on_exit.insert(ctx.path_assigned_at.clone()); | |
154 | ||
155 | // path_maybe_uninitialized_on_exit(path, point) :- path_moved_at(path, point). | |
156 | path_maybe_uninitialized_on_exit.insert(ctx.path_moved_at.clone()); | |
e1599b0c XL |
157 | |
158 | while iteration.changed() { | |
d9bb1a4e FG |
159 | // path_maybe_initialized_on_exit(path, point2) :- |
160 | // path_maybe_initialized_on_exit(path, point1), | |
161 | // cfg_edge(point1, point2), | |
72b1a166 | 162 | // !path_moved_at(path, point2). |
e1599b0c XL |
163 | path_maybe_initialized_on_exit.from_leapjoin( |
164 | &path_maybe_initialized_on_exit, | |
165 | ( | |
d9bb1a4e | 166 | cfg_edge.extend_with(|&(_path, point1)| point1), |
72b1a166 | 167 | ctx.path_moved_at.extend_anti(|&(path, _point1)| path), |
e1599b0c | 168 | ), |
d9bb1a4e | 169 | |&(path, _point1), &point2| (path, point2), |
e1599b0c XL |
170 | ); |
171 | ||
72b1a166 FG |
172 | // path_maybe_uninitialized_on_exit(path, point2) :- |
173 | // path_maybe_uninitialized_on_exit(path, point1), | |
d9bb1a4e | 174 | // cfg_edge_(point1, point2) |
72b1a166 FG |
175 | // !path_assigned_at(point1, point2). |
176 | path_maybe_uninitialized_on_exit.from_leapjoin( | |
177 | &path_maybe_uninitialized_on_exit, | |
178 | ( | |
179 | cfg_edge.extend_with(|&(_path, point1)| point1), | |
180 | ctx.path_assigned_at.extend_anti(|&(path, _point1)| path), | |
181 | ), | |
182 | |&(path, _point1), &point2| (path, point2), | |
183 | ); | |
e1599b0c | 184 | |
72b1a166 FG |
185 | // var_maybe_partly_initialized_on_exit(var, point) :- |
186 | // path_maybe_initialized_on_exit(path, point). | |
187 | // path_begins_with(path, var). | |
188 | var_maybe_partly_initialized_on_exit.from_leapjoin( | |
e1599b0c | 189 | &path_maybe_initialized_on_exit, |
72b1a166 FG |
190 | ctx.path_begins_with_var.extend_with(|&(path, _point)| path), |
191 | |&(_path, point), &var| (var, point), | |
e1599b0c | 192 | ); |
e1599b0c | 193 | |
72b1a166 FG |
194 | // move_error(Path, TargetNode) :- |
195 | // path_maybe_uninitialized_on_exit(Path, SourceNode), | |
196 | // cfg_edge(SourceNode, TargetNode), | |
197 | // path_accessed_at(Path, TargetNode). | |
198 | move_error.from_leapjoin( | |
199 | &path_maybe_uninitialized_on_exit, | |
200 | ( | |
201 | cfg_edge.extend_with(|&(_path, source_node)| source_node), | |
202 | ctx.path_accessed_at | |
203 | .extend_with(|&(path, _source_node)| path), | |
204 | ), | |
205 | |&(path, _source_node), &target_node| (path, target_node), | |
206 | ); | |
207 | } | |
e1599b0c XL |
208 | |
209 | if output.dump_enabled { | |
72b1a166 | 210 | for &(path, location) in path_maybe_initialized_on_exit.complete().iter() { |
e1599b0c | 211 | output |
72b1a166 | 212 | .path_maybe_initialized_on_exit |
e1599b0c | 213 | .entry(location) |
d9bb1a4e | 214 | .or_default() |
e1599b0c XL |
215 | .push(path); |
216 | } | |
72b1a166 FG |
217 | } |
218 | ||
219 | InitializationStatus { | |
220 | var_maybe_partly_initialized_on_exit: var_maybe_partly_initialized_on_exit.complete(), | |
221 | move_error: move_error.complete(), | |
222 | } | |
223 | } | |
e1599b0c | 224 | |
72b1a166 FG |
225 | // Compute two things: |
226 | // | |
227 | // - an over-approximation of the initialization of variables. This is used in | |
228 | // the origin_live_on_entry computations to determine when a drop may happen; a | |
229 | // definitely moved variable would not be actually dropped. | |
230 | // - move errors. | |
231 | // | |
232 | // The process is split into two stages: | |
233 | // | |
234 | // 1. Compute the transitive closure of path accesses. That is, accessing `f.a` | |
235 | // would access `f.a.b`, etc. | |
236 | // 2. Use this to compute both paths that may be initialized and paths that may | |
237 | // have been deinitialized, which in turn can be used to find move errors (an | |
238 | // access to a path that may be deinitialized). | |
239 | pub(super) fn compute<T: FactTypes>( | |
240 | ctx: InitializationContext<T>, | |
241 | cfg_edge: &Relation<(T::Point, T::Point)>, | |
242 | output: &mut Output<T>, | |
243 | ) -> InitializationResult<T> { | |
244 | let timer = Instant::now(); | |
245 | ||
246 | let transitive_paths = compute_transitive_paths::<T>( | |
247 | ctx.child_path, | |
248 | ctx.path_assigned_at_base, | |
249 | ctx.path_moved_at_base, | |
250 | ctx.path_accessed_at_base, | |
251 | ctx.path_is_var, | |
252 | ); | |
253 | info!("initialization phase 1 completed: {:?}", timer.elapsed()); | |
254 | ||
255 | let InitializationStatus { | |
256 | var_maybe_partly_initialized_on_exit, | |
257 | move_error, | |
258 | } = compute_move_errors::<T>(transitive_paths, cfg_edge, output); | |
259 | info!( | |
260 | "initialization phase 2: {} move errors in {:?}", | |
261 | move_error.elements.len(), | |
262 | timer.elapsed() | |
263 | ); | |
264 | ||
265 | if output.dump_enabled { | |
266 | for &(var, location) in var_maybe_partly_initialized_on_exit.iter() { | |
e1599b0c | 267 | output |
72b1a166 | 268 | .var_maybe_partly_initialized_on_exit |
e1599b0c | 269 | .entry(location) |
d9bb1a4e | 270 | .or_default() |
e1599b0c XL |
271 | .push(var); |
272 | } | |
273 | } | |
274 | ||
72b1a166 | 275 | InitializationResult(var_maybe_partly_initialized_on_exit, move_error) |
e1599b0c | 276 | } |