charon_lib::transform::ullbc_to_llbc

Function compute_switch_exits

source
fn compute_switch_exits(
    cfg: &CfgInfo,
    tsort_map: &HashMap<BlockId, usize>,
) -> HashMap<BlockId, Option<BlockId>>
Expand description

See compute_loop_switch_exits for explanations about what “exits” are.

In order to compute the switch exits, we simply recursively compute a topologically ordered set of “filtered successors” as follows (note that we work in the CFG without back edges):

  • for a block which doesn’t branch (only one successor), the filtered successors is the set of reachable nodes.
  • for a block which branches, we compute the nodes reachable from all the children, and find the “best” intersection between those. Note that we find the “best” intersection (a pair of branches which maximize the intersection of filtered successors) because some branches might never join the control-flow of the other branches, if they contain a break, return, panic, etc., like here:
    if b { x = 3; } { return; }
    y += x;
    ...

Note that with nested switches, the branches of the inner switches might goto the exits of the outer switches: for this reason, we give precedence to the outer switches.