Skip to main content

charon_lib/transform/simplify_output/
update_block_indices.rs

1//! Renumber rechable blocks to be consecutive and in topological order (ignoring loop backedges).
2use std::mem;
3
4use itertools::Itertools;
5use petgraph::graphmap::DiGraphMap;
6use petgraph::visit::{DfsPostOrder, Walker};
7
8use crate::ids::*;
9use crate::transform::TransformCtx;
10use crate::ullbc_ast::*;
11
12use crate::transform::ctx::UllbcPass;
13
14pub struct Transform;
15impl UllbcPass for Transform {
16    fn transform_body(&self, _ctx: &mut TransformCtx, b: &mut ExprBody) {
17        let mut graph = DiGraphMap::<BlockId, ()>::new();
18        for (id, block) in b.body.iter_enumerated() {
19            for target in block.targets() {
20                graph.add_edge(id, target, ());
21            }
22        }
23
24        let mut old_blocks = mem::take(&mut b.body);
25        let mut id_map: IndexVec<BlockId, Option<BlockId>> = old_blocks.map_ref(|_| None);
26        let postorder = DfsPostOrder::new(&graph, START_BLOCK_ID)
27            .iter(&graph)
28            .collect_vec();
29        for id in postorder.into_iter().rev() {
30            let new_id = b.body.push(old_blocks[id].take());
31            id_map[id] = Some(new_id);
32        }
33
34        // Update the ids.
35        b.visit_block_ids_mut(|id: &mut BlockId| *id = id_map[*id].unwrap());
36    }
37}