Function compute_loop_switch_exits

fn compute_loop_switch_exits(cfg_info: &CfgInfo) -> ExitInfo

Compute the exits for the loops and the switches (switch on integer and if … then … else …). We need to do this because control-flow in MIR is destructured: we have gotos everywhere.

Let’s consider the following piece of code:

if cond1 { ... } else { ... };
if cond2 { ... } else { ... };

Once converted to MIR, the control-flow is destructured, which means we have gotos everywhere. When reconstructing the control-flow, we have to be careful about the point where we should join the two branches of the first if. For instance, if we don’t notice they should be joined at some point (i.e, whatever the branch we take, there is a moment when we go to the exact same place, just before the second if), we might generate code like this, with some duplicata:

if cond1 { ...; if cond2 { ... } else { ...} }
else { ...; if cond2 { ... } else { ...} }

Such a reconstructed program is valid, but it is definitely non-optimal: it is very different from the original program (making it less clean and clear), more bloated, and might involve duplicating the proof effort.

For this reason, we need to find the “exit” of the first loop, which is the point where the two branches join. Note that this can be a bit tricky, because there may be more than two branches (if we do switch(x) { ... }), and some of them might not join (if they contain a break, panic, return, etc.).

Finally, some similar issues arise for loops. For instance, let’s consider the following piece of code:

while cond1 {
  e1;
  if cond2 {
    break;
  }
  e2;
}
e3;
return;

Note that in MIR, the loop gets desugared to an if … then … else …. From the MIR, We want to generate something like this:

loop {
  if cond1 {
    e1;
    if cond2 {
      break;
    }
    e2;
    continue;
  }
  else {
    break;
  }
};
e3;
return;

But if we don’t pay attention, we might end up with that, once again with duplications:

loop {
  if cond1 {
    e1;
    if cond2 {
      e3;
      return;
    }
    e2;
    continue;
  }
  else {
    e3;
    return;
  }
}

We thus have to notice that if the loop condition is false, we goto the same block as when following the goto introduced by the break inside the loop, and this block is dubbed the “loop exit”.

The following function thus computes the “exits” for loops and switches, which are basically the points where control-flow joins.