charon_lib/transform/add_missing_info/
sccs.rs

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

charon_lib/transform/add_missing_info/
sccs.rs
