Finalise initialisation calculations #110
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,117 @@ | ||
| use std::time::Instant; | ||
|
|
||
| use crate::output::Output; | ||
| use facts::Atom; | ||
|
|
||
| use datafrog::{Iteration, Relation, RelationLeaper}; | ||
|
|
||
| pub(super) fn init_var_maybe_initialized_on_exit<Region, Loan, Point, Variable, MovePath>( | ||
|
There was a problem hiding this comment. This function definitely wants a comment with some kind of Rust example showing where it's true and not true. |
||
| child: Vec<(MovePath, MovePath)>, | ||
| path_belongs_to_var: Vec<(MovePath, Variable)>, | ||
| initialized_at: Vec<(MovePath, Point)>, | ||
| moved_out_at: Vec<(MovePath, Point)>, | ||
| cfg_edge: &[(Point, Point)], | ||
| output: &mut Output<Region, Loan, Point, Variable, MovePath>, | ||
| ) -> Vec<(Variable, Point)> | ||
| where | ||
| Region: Atom, | ||
| Loan: Atom, | ||
| Point: Atom, | ||
| Variable: Atom, | ||
| MovePath: Atom, | ||
| { | ||
| debug!("compute_initialization()"); | ||
| let computation_start = Instant::now(); | ||
| let mut iteration = Iteration::new(); | ||
|
|
||
| // Relations | ||
| let child: Relation<(MovePath, MovePath)> = child.into(); | ||
| let path_belongs_to_var: Relation<(MovePath, Variable)> = path_belongs_to_var.into(); | ||
| let initialized_at: Relation<(MovePath, Point)> = initialized_at.into(); | ||
| let moved_out_at: Relation<(MovePath, Point)> = moved_out_at.into(); | ||
| // FIXME: is there no better way to do this? | ||
nikomatsakis marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| let cfg_edge: Relation<(Point, Point)> = cfg_edge.iter().map(|&(p, q)| (p, q)).collect(); | ||
|
|
||
| // Variables | ||
|
|
||
| // var_maybe_initialized_on_exit(V, P): Upon leaving `P`, at least one part of the | ||
| // variable `V` might be initialized for some path through the CFG. | ||
| let var_maybe_initialized_on_exit = | ||
| iteration.variable::<(Variable, Point)>("var_maybe_initialized_on_exit"); | ||
|
|
||
| // path_maybe_initialized_on_exit(M, P): Upon leaving `P`, the move path `M` | ||
| // might be initialized for some path through the CFG. | ||
| let path_maybe_initialized_on_exit = | ||
| iteration.variable::<(MovePath, Point)>("path_maybe_initialized_on_exit"); | ||
|
|
||
| // Initial propagation of static relations | ||
|
|
||
| // path_maybe_initialized_on_exit(Path, Point) :- initialized_at(Path, | ||
| // Point). | ||
| path_maybe_initialized_on_exit.insert(initialized_at); | ||
|
|
||
| while iteration.changed() { | ||
| // path_maybe_initialized_on_exit(M, Q) :- | ||
| // path_maybe_initialized_on_exit(M, P), | ||
| // cfg_edge(P, Q), | ||
| // !moved_out_at(M, Q). | ||
| path_maybe_initialized_on_exit.from_leapjoin( | ||
| &path_maybe_initialized_on_exit, | ||
| ( | ||
| cfg_edge.extend_with(|&(_m, p)| p), | ||
| moved_out_at.extend_anti(|&(m, _p)| m), | ||
| ), | ||
| |&(m, _p), &q| (m, q), | ||
| ); | ||
|
|
||
| // path_maybe_initialized_on_exit(Mother, P) :- | ||
| // path_maybe_initialized_on_exit(Daughter, P), | ||
| // child(Daughter, Mother). | ||
|
There was a problem hiding this comment. I'm debating the purpose of this rule. It feels sort of incomplete on its own. It also suggests that the name "maybe initialized" could be refined -- in particular I guess it includes partial initialization? That is, this rule says that if Well, I guess the point of this "maybe partially initialized" relation is precisely to inform the region-live-at computation in NLL, which is probably already imprecise in this manner? I guess I better double check, but I remember us making some decisions like that. There was a problem hiding this comment. Still, if the goal is to ultimately compute this relation, then why do we need the previous rule? Well, it doesn't seem harmful -- but I guess we can either do the elaboration at the initial point -- i.e., if some path M is initialized at a point P, then we could make the initial value include that all paths which are either parents or children of M are "maybe initialized" at the point P. And then we don't need this rule to be part of the iteration -- rather, we compute this transition closure before hand. I think this is what Lark did, but I suppose I should go back and try to write up the rules I used there. Maybe a good blog post. There was a problem hiding this comment. I think this connects with your next comment, so I'll reply to it there. |
||
| path_maybe_initialized_on_exit.from_leapjoin( | ||
| &path_maybe_initialized_on_exit, | ||
| child.extend_with(|&(daughter, _p)| daughter), | ||
| |&(_daughter, p), &mother| (mother, p), | ||
| ); | ||
|
|
||
| // var_maybe_initialized_on_exit(V, P) :- | ||
| // path_belongs_to_var(M, V), | ||
| // path_maybe_initialized_at(M, P). | ||
| var_maybe_initialized_on_exit.from_leapjoin( | ||
|
There was a problem hiding this comment. Something is tickling me here. If the goal ultimately is to compute which variables are maybe initialized, why do we have to extend to the parents? That is, it feels like we should track initialization precisely. Something like this:
then compute I guess the example where this differs is something like: The existing NLL is somewhat approximate here, so maybe this is intentional. Am I missing something? There was a problem hiding this comment. I think what you are detecting is that I am computing sort of two different transitive closures. What I want to do is to trace back partial initialisation to a variable for use in the next step to determine if a drop would happen. Probably, the cleanest design would be to compute the transitive closure over paths downwards, and separately extend the "variable-rootedness" across another transitive closure (tracing all paths back to their variable), and then finally perform the join, but I am also not sure if this is an over-approximation. The more I think about this, the less I feel like I understand it. I am fairly certain what we did in the original fact generation was this, though: we emitted |
||
| &path_maybe_initialized_on_exit, | ||
| path_belongs_to_var.extend_with(|&(m, _p)| m), | ||
| |&(_m, p), &v| (v, p), | ||
| ); | ||
| } | ||
|
|
||
| let var_maybe_initialized_on_exit = var_maybe_initialized_on_exit.complete(); | ||
|
|
||
| info!( | ||
| "compute_initialization() completed: {} tuples, {:?}", | ||
| var_maybe_initialized_on_exit.len(), | ||
| computation_start.elapsed() | ||
| ); | ||
|
|
||
| if output.dump_enabled { | ||
| let path_maybe_initialized_on_exit = path_maybe_initialized_on_exit.complete(); | ||
| for &(path, location) in &path_maybe_initialized_on_exit.elements { | ||
| output | ||
| .path_maybe_initialized_at | ||
| .entry(location) | ||
| .or_insert_with(Vec::new) | ||
| .push(path); | ||
| } | ||
|
|
||
| for &(var, location) in &var_maybe_initialized_on_exit.elements { | ||
| output | ||
| .var_maybe_initialized_on_exit | ||
| .entry(location) | ||
| .or_insert_with(Vec::new) | ||
| .push(var); | ||
| } | ||
| } | ||
|
|
||
| var_maybe_initialized_on_exit | ||
| .iter() | ||
| .map(|&(v, p)| (v, p)) | ||
| .collect() | ||
| } | ||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think it'd be useful to give an example. For example, I imagine:
child(M1, M2)would be true If M1 representsa.b.cand M2 representsa.b.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
That's true. The hand-wavyness was because I was not entirely sure if it was transitive or not. It is, though, which may or may not be what we want.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Interesting. The name strongly suggests non-transitive to me. I would have said something like
descendantfor a transitive child relationship.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
True, I'll make a note of fixing this at some point.