| 1 | use std::time::Instant; |
| 2 | |
| 3 | use crate::facts::FactTypes; |
| 4 | use crate::output::{InitializationContext, Output}; |
| 5 | |
| 6 | use datafrog::{Iteration, Relation, RelationLeaper}; |
| 7 | |
| 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> { |
| 40 | let mut iteration = Iteration::new(); |
| 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 | }); |
| 91 | |
| 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 | } |
| 118 | |
| 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(); |
| 126 | // Variables |
| 127 | |
| 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" ); |
| 134 | |
| 135 | // path_maybe_initialized_on_exit(path, point): Upon leaving `point`, the |
| 136 | // move path `path` is initialized for some path through the CFG. |
| 137 | let path_maybe_initialized_on_exit = |
| 138 | iteration.variable::<(T::Path, T::Point)>("path_maybe_initialized_on_exit" ); |
| 139 | |
| 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 | |
| 150 | // Initial propagation of static relations |
| 151 | |
| 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()); |
| 157 | |
| 158 | while iteration.changed() { |
| 159 | // path_maybe_initialized_on_exit(path, point2) :- |
| 160 | // path_maybe_initialized_on_exit(path, point1), |
| 161 | // cfg_edge(point1, point2), |
| 162 | // !path_moved_at(path, point2). |
| 163 | path_maybe_initialized_on_exit.from_leapjoin( |
| 164 | &path_maybe_initialized_on_exit, |
| 165 | ( |
| 166 | cfg_edge.extend_with(|&(_path, point1)| point1), |
| 167 | ctx.path_moved_at.extend_anti(|&(path, _point1)| path), |
| 168 | ), |
| 169 | |&(path, _point1), &point2| (path, point2), |
| 170 | ); |
| 171 | |
| 172 | // path_maybe_uninitialized_on_exit(path, point2) :- |
| 173 | // path_maybe_uninitialized_on_exit(path, point1), |
| 174 | // cfg_edge(point1, point2) |
| 175 | // !path_assigned_at(path, 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 | ); |
| 184 | |
| 185 | // var_maybe_partly_initialized_on_exit(var, point) :- |
| 186 | // path_maybe_initialized_on_exit(path, point). |
| 187 | // path_begins_with_var(path, var). |
| 188 | var_maybe_partly_initialized_on_exit.from_leapjoin( |
| 189 | &path_maybe_initialized_on_exit, |
| 190 | ctx.path_begins_with_var.extend_with(|&(path, _point)| path), |
| 191 | |&(_path, point), &var| (var, point), |
| 192 | ); |
| 193 | |
| 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 | } |
| 208 | |
| 209 | if output.dump_enabled { |
| 210 | for &(path, location) in path_maybe_initialized_on_exit.complete().iter() { |
| 211 | output |
| 212 | .path_maybe_initialized_on_exit |
| 213 | .entry(location) |
| 214 | .or_default() |
| 215 | .push(path); |
| 216 | } |
| 217 | |
| 218 | for &(path, location) in path_maybe_uninitialized_on_exit.complete().iter() { |
| 219 | output |
| 220 | .path_maybe_uninitialized_on_exit |
| 221 | .entry(location) |
| 222 | .or_default() |
| 223 | .push(path); |
| 224 | } |
| 225 | } |
| 226 | |
| 227 | InitializationStatus { |
| 228 | var_maybe_partly_initialized_on_exit: var_maybe_partly_initialized_on_exit.complete(), |
| 229 | move_error: move_error.complete(), |
| 230 | } |
| 231 | } |
| 232 | |
| 233 | // Compute two things: |
| 234 | // |
| 235 | // - an over-approximation of the initialization of variables. This is used in |
| 236 | // the origin_live_on_entry computations to determine when a drop may happen; a |
| 237 | // definitely moved variable would not be actually dropped. |
| 238 | // - move errors. |
| 239 | // |
| 240 | // The process is split into two stages: |
| 241 | // |
| 242 | // 1. Compute the transitive closure of path accesses. That is, accessing `f.a` |
| 243 | // would access `f.a.b`, etc. |
| 244 | // 2. Use this to compute both paths that may be initialized and paths that may |
| 245 | // have been deinitialized, which in turn can be used to find move errors (an |
| 246 | // access to a path that may be deinitialized). |
| 247 | pub(super) fn compute<T: FactTypes>( |
| 248 | ctx: InitializationContext<T>, |
| 249 | cfg_edge: &Relation<(T::Point, T::Point)>, |
| 250 | output: &mut Output<T>, |
| 251 | ) -> InitializationResult<T> { |
| 252 | let timer = Instant::now(); |
| 253 | |
| 254 | let transitive_paths = compute_transitive_paths::<T>( |
| 255 | ctx.child_path, |
| 256 | ctx.path_assigned_at_base, |
| 257 | ctx.path_moved_at_base, |
| 258 | ctx.path_accessed_at_base, |
| 259 | ctx.path_is_var, |
| 260 | ); |
| 261 | info!("initialization phase 1 completed: {:?}" , timer.elapsed()); |
| 262 | |
| 263 | let InitializationStatus { |
| 264 | var_maybe_partly_initialized_on_exit, |
| 265 | move_error, |
| 266 | } = compute_move_errors::<T>(transitive_paths, cfg_edge, output); |
| 267 | info!( |
| 268 | "initialization phase 2: {} move errors in {:?}" , |
| 269 | move_error.elements.len(), |
| 270 | timer.elapsed() |
| 271 | ); |
| 272 | |
| 273 | if output.dump_enabled { |
| 274 | for &(var, location) in var_maybe_partly_initialized_on_exit.iter() { |
| 275 | output |
| 276 | .var_maybe_partly_initialized_on_exit |
| 277 | .entry(location) |
| 278 | .or_default() |
| 279 | .push(var); |
| 280 | } |
| 281 | } |
| 282 | |
| 283 | InitializationResult(var_maybe_partly_initialized_on_exit, move_error) |
| 284 | } |
| 285 | |