vendor/polonius-engine/src/output/initialization.rs

   1 use std::time::Instant;
   2
   3 use crate::output::Output;
   4 use facts::Atom;
   5
   6 use datafrog::{Iteration, Relation, RelationLeaper};
   7
   8 pub(super) fn init_var_maybe_initialized_on_exit<Region, Loan, Point, Variable, MovePath>(
   9     child: Vec<(MovePath, MovePath)>,
  10     path_belongs_to_var: Vec<(MovePath, Variable)>,
  11     initialized_at: Vec<(MovePath, Point)>,
  12     moved_out_at: Vec<(MovePath, Point)>,
  13     path_accessed_at: Vec<(MovePath, Point)>,
  14     cfg_edge: &[(Point, Point)],
  15     output: &mut Output<Region, Loan, Point, Variable, MovePath>,
  16 ) -> Vec<(Variable, Point)>
  17 where
  18     Region: Atom,
  19     Loan: Atom,
  20     Point: Atom,
  21     Variable: Atom,
  22     MovePath: Atom,
  23 {
  24     debug!("compute_initialization()");
  25     let computation_start = Instant::now();
  26     let mut iteration = Iteration::new();
  27
  28     // Relations
  29     //let parent: Relation<(MovePath, MovePath)> = child.iter().map(|&(c, p)| (p, c)).collect();
  30     let child: Relation<(MovePath, MovePath)> = child.into();
  31     let path_belongs_to_var: Relation<(MovePath, Variable)> = path_belongs_to_var.into();
  32     let initialized_at: Relation<(MovePath, Point)> = initialized_at.into();
  33     let moved_out_at: Relation<(MovePath, Point)> = moved_out_at.into();
  34     let cfg_edge: Relation<(Point, Point)> = cfg_edge.iter().cloned().collect();
  35     let _path_accessed_at: Relation<(MovePath, Point)> = path_accessed_at.into();
  36
  37     // Variables
  38
  39     // var_maybe_initialized_on_exit(V, P): Upon leaving `P`, at least one part of the
  40     // variable `V` might be initialized for some path through the CFG.
  41     let var_maybe_initialized_on_exit =
  42         iteration.variable::<(Variable, Point)>("var_maybe_initialized_on_exit");
  43
  44     // path_maybe_initialized_on_exit(M, P): Upon leaving `P`, the move path `M`
  45     // might be *partially* initialized for some path through the CFG.
  46     let path_maybe_initialized_on_exit =
  47         iteration.variable::<(MovePath, Point)>("path_maybe_initialized_on_exit");
  48
  49     // Initial propagation of static relations
  50
  51     // path_maybe_initialized_on_exit(Path, Point) :- initialized_at(Path,
  52     // Point).
  53     path_maybe_initialized_on_exit.insert(initialized_at);
  54
  55     while iteration.changed() {
  56         // path_maybe_initialized_on_exit(M, Q) :-
  57         //     path_maybe_initialized_on_exit(M, P),
  58         //     cfg_edge(P, Q),
  59         //     !moved_out_at(M, Q).
  60         path_maybe_initialized_on_exit.from_leapjoin(
  61             &path_maybe_initialized_on_exit,
  62             (
  63                 cfg_edge.extend_with(|&(_m, p)| p),
  64                 moved_out_at.extend_anti(|&(m, _p)| m),
  65             ),
  66             |&(m, _p), &q| (m, q),
  67         );
  68
  69         // path_maybe_initialized_on_exit(Mother, P) :-
  70         //     path_maybe_initialized_on_exit(Daughter, P),
  71         //     child(Daughter, Mother).
  72         path_maybe_initialized_on_exit.from_leapjoin(
  73             &path_maybe_initialized_on_exit,
  74             child.extend_with(|&(daughter, _p)| daughter),
  75             |&(_daughter, p), &mother| (mother, p),
  76         );
  77
  78         // TODO: the following lines contain things left to implement for move
  79         // tracking:
  80
  81         // path_accessed :- path_accessed(M, P).
  82         //
  83         // -- transitive access of all children
  84         // path_accessed(Child, P) :-
  85         //     path_accessed(Mother, P),
  86         //     parent(Mother, Child).
  87
  88         // Propagate across CFG edges:
  89         // path_maybe_uninit(M, Q) :-
  90         //     path_maybe_uninit(M, P),
  91         //     cfg_edge_(P, Q)
  92         //     !initialized_at(P, Q).
  93
  94         // Initial value (static).
  95         // path_maybe_uninit(M, P) :- moved_out_at(M, P).
  96
  97         // NOTE: Double join!
  98         // errors(M, P) :-
  99         //     path_maybe_uninit(M, P),
 100         //     path_accessed(M, P).
 101
 102         // END TODO
 103
 104         // var_maybe_initialized_on_exit(V, P) :-
 105         //     path_belongs_to_var(M, V),
 106         //     path_maybe_initialized_at(M, P).
 107         var_maybe_initialized_on_exit.from_leapjoin(
 108             &path_maybe_initialized_on_exit,
 109             path_belongs_to_var.extend_with(|&(m, _p)| m),
 110             |&(_m, p), &v| (v, p),
 111         );
 112     }
 113
 114     let var_maybe_initialized_on_exit = var_maybe_initialized_on_exit.complete();
 115
 116     info!(
 117         "compute_initialization() completed: {} tuples, {:?}",
 118         var_maybe_initialized_on_exit.len(),
 119         computation_start.elapsed()
 120     );
 121
 122     if output.dump_enabled {
 123         let path_maybe_initialized_on_exit = path_maybe_initialized_on_exit.complete();
 124         for &(path, location) in &path_maybe_initialized_on_exit.elements {
 125             output
 126                 .path_maybe_initialized_at
 127                 .entry(location)
 128                 .or_insert_with(Vec::new)
 129                 .push(path);
 130         }
 131
 132         for &(var, location) in &var_maybe_initialized_on_exit.elements {
 133             output
 134                 .var_maybe_initialized_on_exit
 135                 .entry(location)
 136                 .or_insert_with(Vec::new)
 137                 .push(var);
 138         }
 139     }
 140
 141     var_maybe_initialized_on_exit
 142         .iter()
 143         .map(|&(v, p)| (v, p))
 144         .collect()
 145 }