use std::time::Instant;
use crate::facts::FactTypes;
use crate::output::{InitializationContext, Output};
use datafrog::{Iteration, Relation, RelationLeaper};
struct TransitivePaths<T: FactTypes> {
path_moved_at: Relation<(T::Path, T::Point)>,
path_assigned_at: Relation<(T::Path, T::Point)>,
path_accessed_at: Relation<(T::Path, T::Point)>,
path_begins_with_var: Relation<(T::Path, T::Variable)>,
}
struct InitializationStatus<T: FactTypes> {
var_maybe_partly_initialized_on_exit: Relation<(T::Variable, T::Point)>,
move_error: Relation<(T::Path, T::Point)>,
}
pub(super) struct InitializationResult<T: FactTypes>(
pub(super) Relation<(T::Variable, T::Point)>,
pub(super) Relation<(T::Path, T::Point)>,
);
fn compute_transitive_paths<T: FactTypes>(
child_path: Vec<(T::Path, T::Path)>,
path_assigned_at_base: Vec<(T::Path, T::Point)>,
path_moved_at_base: Vec<(T::Path, T::Point)>,
path_accessed_at_base: Vec<(T::Path, T::Point)>,
path_is_var: Vec<(T::Path, T::Variable)>,
) -> TransitivePaths<T> {
let mut iteration = Iteration::new();
let child_path: Relation<(T::Path, T::Path)> = child_path.into();
let ancestor_path = iteration.variable::<(T::Path, T::Path)>("ancestor");
let path_moved_at = iteration.variable::<(T::Path, T::Point)>("path_moved_at");
let path_assigned_at = iteration.variable::<(T::Path, T::Point)>("path_initialized_at");
let path_accessed_at = iteration.variable::<(T::Path, T::Point)>("path_accessed_at");
let path_begins_with_var = iteration.variable::<(T::Path, T::Variable)>("path_begins_with_var");
ancestor_path.extend(child_path.iter().map(|&(child, parent)| (parent, child)));
path_moved_at.insert(path_moved_at_base.into());
path_assigned_at.insert(path_assigned_at_base.into());
path_accessed_at.insert(path_accessed_at_base.into());
path_begins_with_var.insert(path_is_var.into());
while iteration.changed() {
ancestor_path.from_join(
&ancestor_path,
&child_path,
|&_parent, &child, &grandparent| (grandparent, child),
);
path_moved_at.from_join(&path_moved_at, &ancestor_path, |&_parent, &p, &child| {
(child, p)
});
path_assigned_at.from_join(&path_assigned_at, &ancestor_path, |&_parent, &p, &child| {
(child, p)
});
path_accessed_at.from_join(&path_accessed_at, &ancestor_path, |&_parent, &p, &child| {
(child, p)
});
path_begins_with_var.from_join(
&path_begins_with_var,
&ancestor_path,
|&_parent, &var, &child| (child, var),
);
}
TransitivePaths {
path_assigned_at: path_assigned_at.complete(),
path_moved_at: path_moved_at.complete(),
path_accessed_at: path_accessed_at.complete(),
path_begins_with_var: path_begins_with_var.complete(),
}
}
fn compute_move_errors<T: FactTypes>(
ctx: TransitivePaths<T>,
cfg_edge: &Relation<(T::Point, T::Point)>,
output: &mut Output<T>,
) -> InitializationStatus<T> {
let mut iteration = Iteration::new();
let var_maybe_partly_initialized_on_exit =
iteration.variable::<(T::Variable, T::Point)>("var_maybe_partly_initialized_on_exit");
let path_maybe_initialized_on_exit =
iteration.variable::<(T::Path, T::Point)>("path_maybe_initialized_on_exit");
let path_maybe_uninitialized_on_exit =
iteration.variable::<(T::Path, T::Point)>("path_maybe_uninitialized_on_exit");
let move_error = iteration.variable::<(T::Path, T::Point)>("move_error");
path_maybe_initialized_on_exit.insert(ctx.path_assigned_at.clone());
path_maybe_uninitialized_on_exit.insert(ctx.path_moved_at.clone());
while iteration.changed() {
path_maybe_initialized_on_exit.from_leapjoin(
&path_maybe_initialized_on_exit,
(
cfg_edge.extend_with(|&(_path, point1)| point1),
ctx.path_moved_at.extend_anti(|&(path, _point1)| path),
),
|&(path, _point1), &point2| (path, point2),
);
path_maybe_uninitialized_on_exit.from_leapjoin(
&path_maybe_uninitialized_on_exit,
(
cfg_edge.extend_with(|&(_path, point1)| point1),
ctx.path_assigned_at.extend_anti(|&(path, _point1)| path),
),
|&(path, _point1), &point2| (path, point2),
);
var_maybe_partly_initialized_on_exit.from_leapjoin(
&path_maybe_initialized_on_exit,
ctx.path_begins_with_var.extend_with(|&(path, _point)| path),
|&(_path, point), &var| (var, point),
);
move_error.from_leapjoin(
&path_maybe_uninitialized_on_exit,
(
cfg_edge.extend_with(|&(_path, source_node)| source_node),
ctx.path_accessed_at
.extend_with(|&(path, _source_node)| path),
),
|&(path, _source_node), &target_node| (path, target_node),
);
}
if output.dump_enabled {
for &(path, location) in path_maybe_initialized_on_exit.complete().iter() {
output
.path_maybe_initialized_on_exit
.entry(location)
.or_default()
.push(path);
}
for &(path, location) in path_maybe_uninitialized_on_exit.complete().iter() {
output
.path_maybe_uninitialized_on_exit
.entry(location)
.or_default()
.push(path);
}
}
InitializationStatus {
var_maybe_partly_initialized_on_exit: var_maybe_partly_initialized_on_exit.complete(),
move_error: move_error.complete(),
}
}
pub(super) fn compute<T: FactTypes>(
ctx: InitializationContext<T>,
cfg_edge: &Relation<(T::Point, T::Point)>,
output: &mut Output<T>,
) -> InitializationResult<T> {
let timer = Instant::now();
let transitive_paths = compute_transitive_paths::<T>(
ctx.child_path,
ctx.path_assigned_at_base,
ctx.path_moved_at_base,
ctx.path_accessed_at_base,
ctx.path_is_var,
);
info!("initialization phase 1 completed: {:?}", timer.elapsed());
let InitializationStatus {
var_maybe_partly_initialized_on_exit,
move_error,
} = compute_move_errors::<T>(transitive_paths, cfg_edge, output);
info!(
"initialization phase 2: {} move errors in {:?}",
move_error.elements.len(),
timer.elapsed()
);
if output.dump_enabled {
for &(var, location) in var_maybe_partly_initialized_on_exit.iter() {
output
.var_maybe_partly_initialized_on_exit
.entry(location)
.or_default()
.push(var);
}
}
InitializationResult(var_maybe_partly_initialized_on_exit, move_error)
}