charon_lib/transform/add_missing_info/
sccs.rs

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

charon_lib/transform/add_missing_info/
sccs.rs
