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,
    }
}