charon_lib/transform/
merge_goto_chains.rs

1//! # Micro-pass: merge single-origin gotos into their parent to reduce CFG graph size.
2use crate::ids::Vector;
3use crate::transform::TransformCtx;
4use crate::ullbc_ast::*;
5
6use super::ctx::UllbcPass;
7
8/// Set of antecedents of a given block. We only care about block ids if there's a single
9/// antecedent.
10enum Antecedents {
11    Zero,
12    One {
13        id: BlockId,
14        /// Whether the antecedent is a goto.
15        is_goto: bool,
16    },
17    Many,
18}
19
20impl Antecedents {
21    fn add(&mut self, id: BlockId, is_goto: bool) {
22        match self {
23            Antecedents::Zero => *self = Antecedents::One { id, is_goto },
24            Antecedents::One { .. } => *self = Antecedents::Many,
25            Antecedents::Many => {}
26        }
27    }
28}
29
30pub struct Transform;
31impl UllbcPass for Transform {
32    fn transform_body(&self, ctx: &mut TransformCtx, body: &mut ExprBody) {
33        // Check the option which instructs to ignore this pass
34        if ctx.options.no_merge_goto_chains {
35            return;
36        }
37
38        // Compute for each block the set of blocks that points to it.
39        let mut antecedents: Vector<BlockId, Antecedents> =
40            body.body.map_ref(|_| Antecedents::Zero);
41        for (block_id, block) in body.body.iter_indexed() {
42            let is_goto = block.terminator.content.is_goto();
43            for target in block.targets() {
44                antecedents.get_mut(target).unwrap().add(block_id, is_goto);
45            }
46        }
47        // Merge blocks with a single antecedent into their antecedent.
48        for mut id in body.body.all_indices() {
49            // Go up the chain to find the first parent with zero (the start block) or multiple
50            // antecedents. This avoids quadratic behavior where we repeatedly copy a growing list
51            // of statements, since blocks may not be sorted..
52            while let Antecedents::One {
53                id: antecedent_id,
54                is_goto: true,
55            } = antecedents[id]
56            {
57                id = antecedent_id;
58            }
59            // While the current block is a straight goto, merge the target block back into this
60            // one.
61            while let Some(source) = body.body.get(id)
62                && let RawTerminator::Goto { target } = source.terminator.content
63                && let Antecedents::One { .. } = antecedents[target]
64            {
65                let mut target = body.body.remove(target).unwrap();
66                let source = &mut body.body[id];
67                source.statements.append(&mut target.statements);
68                source.terminator = target.terminator;
69            }
70        }
71    }
72}
charon_lib/transform/merge_goto_chains.rs

charon_lib/transform/
merge_goto_chains.rs
