charon_lib/transform/graphs.rs
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173
use hashlink::LinkedHashSet;
use std::collections::BTreeSet as OrdSet;
use std::collections::HashMap;
use std::iter::FromIterator;
use std::vec::Vec;
/// A structure containing information about SCCs (Strongly Connected Components)
pub struct SCCs<Id> {
/// The SCCs themselves
pub sccs: Vec<Vec<Id>>,
/// The dependencies between SCCs
pub scc_deps: Vec<OrdSet<usize>>,
}
/// The order in which Tarjan's algorithm generates the SCCs is arbitrary,
/// while we want to keep as much as possible the original order (the order
/// in which the user generated the ids). For this, we iterate through
/// the ordered ids and try to add the SCC containing the id to a new list of SCCs
/// Of course, this SCC might have dependencies, so we need to add the dependencies
/// first (in which case we have reordering to do). This is what this function
/// does: we add an SCC and its dependencies to the list of reordered SCCs by
/// doing a depth-first search.
/// We also compute the SCC dependencies while performing this exploration.
fn insert_scc_with_deps<Id: Copy + std::hash::Hash + Eq>(
get_id_dependencies: &dyn Fn(Id) -> Vec<Id>,
reordered_sccs: &mut LinkedHashSet<usize>,
scc_deps: &mut Vec<OrdSet<usize>>,
sccs: &Vec<Vec<Id>>,
id_to_scc: &HashMap<Id, usize>,
scc_id: usize,
) {
// Check if the scc id has already been added
if reordered_sccs.contains(&scc_id) {
return;
}
// Add the dependencies.
// For every id in the dependencies, get the SCC containing this id.
// If this is the current SCC: continue. If it is a different one, it is
// a dependency: add it to the list of reordered SCCs.
let scc = &sccs[scc_id];
for id in scc.iter() {
let ids = get_id_dependencies(*id);
for dep_id in ids.iter() {
let dep_scc_id = id_to_scc.get(dep_id).unwrap();
if *dep_scc_id == scc_id {
continue;
} else {
// Insert the dependency
scc_deps[scc_id].insert(*dep_scc_id);
// Explore the parent SCC
insert_scc_with_deps(
get_id_dependencies,
reordered_sccs,
scc_deps,
sccs,
id_to_scc,
*dep_scc_id,
);
}
}
}
// Add the current SCC
reordered_sccs.insert(scc_id);
}
/// Provided we computed the SCCs (Strongly Connected Components) of a set of
/// identifier, and those identifiers are ordered, compute the set of SCCs where
/// the order of the SCCs and the order of the identifiers inside the SCCs attempt
/// to respect as much as possible the original order between the identifiers.
/// The `ids` vector gives the ordered set of identifiers.
///
///
/// This is used in several places, for instance to generate the translated
/// definitions in a consistent and stable manner. For instance, let's
/// say we extract 4 definitions `f`, `g1`, `g2` and `h`, where:
/// - `g1` and `g2` are mutually recursive
/// - `h` calls `g1`
///
/// When translating those functions, we group together the mutually recursive
/// functions, because they have to be extracted in one single group, and thus
/// apply Tarjan's algorithm on the call graph to find out which functions are
/// mutually recursive.
/// The implementation of Tarjan's algorithm we use gives us the Strongly Connected
/// SCCs of the call graph in an arbitrary order, so we can have:
/// `[[f], [g1, g2], [h]]`, but also `[[h], [f], [g2, g1]]`, etc.
///
/// If the user defined those functions in the order: `f, g1, h, g2`, we want
/// to reorder them into: `f, g1, g2, h`, so that we can translate the mutually
/// recursive functions together, while performing a minimal amount of reordering.
/// And if reordering is not needed, because the user defined those functions
/// in the order `f, g1, g2, h`, or `g1, g2, f, h` or ... then we want to translate
/// them in this exact order.
///
/// This function performs just that: provided the order in which the definitions
/// were defined, and the SCCs of the call graph, return an order suitable for
/// translation and where the amount of reorderings is minimal with regards to
/// the initial order.
///
/// This function is also used to generate the backward functions in a stable
/// manner: the order is provided by the order in which the user listed the
/// region parameters in the function signature, and the graph is the hierarchy
/// graph (or region subtyping graph) between those regions.
pub fn reorder_sccs<Id: std::fmt::Debug + Copy + std::hash::Hash + Eq>(
get_id_dependencies: &dyn Fn(Id) -> Vec<Id>,
ids: &Vec<Id>,
sccs: &[Vec<Id>],
) -> SCCs<Id> {
// Map the identifiers to the SCC indices
let mut id_to_scc = HashMap::<Id, usize>::new();
for (i, scc) in sccs.iter().enumerate() {
for id in scc {
id_to_scc.insert(*id, i);
}
}
// Reorder the identifiers inside the SCCs.
// We iterate over the identifiers (in the order in which we register them), and
// add them in their corresponding SCCs.
let mut reordered_sccs: Vec<Vec<Id>> = vec![];
sccs.iter().for_each(|_| reordered_sccs.push(vec![]));
for id in ids {
let scc_id = match id_to_scc.get(id) {
None => panic!("Could not find id: {:?}", id),
Some(id) => id,
};
reordered_sccs[*scc_id].push(*id);
}
// Reorder the SCCs themselves - just do a depth first search. Iterate over
// the def ids, and add the corresponding SCCs (with their dependencies).
let mut reordered_sccs_ids = LinkedHashSet::<usize>::new();
let mut scc_deps: Vec<OrdSet<usize>> = reordered_sccs.iter().map(|_| OrdSet::new()).collect();
for id in ids {
let scc_id = id_to_scc.get(id).unwrap();
insert_scc_with_deps(
get_id_dependencies,
&mut reordered_sccs_ids,
&mut scc_deps,
&reordered_sccs,
&id_to_scc,
*scc_id,
);
}
let reordered_sccs_ids: Vec<usize> = reordered_sccs_ids.into_iter().collect();
// Compute the map from the original SCC ids to the new SCC ids (after
// reordering).
let mut old_id_to_new_id: Vec<usize> = reordered_sccs_ids.iter().map(|_| 0).collect();
for (new_id, dep) in reordered_sccs_ids.iter().enumerate() {
old_id_to_new_id[*dep] = new_id;
}
// Generate the reordered SCCs
let tgt_sccs = reordered_sccs_ids
.iter()
.map(|scc_id| reordered_sccs[*scc_id].clone())
.collect();
// Compute the dependencies with the new indices
let mut tgt_deps: Vec<OrdSet<usize>> = reordered_sccs.iter().map(|_| OrdSet::new()).collect();
for (old_id, deps) in scc_deps.iter().enumerate() {
let new_id = old_id_to_new_id[old_id];
tgt_deps[new_id] = OrdSet::from_iter(deps.iter().map(|old| old_id_to_new_id[*old]));
}
SCCs {
sccs: tgt_sccs,
scc_deps: tgt_deps,
}
}