Bug: incorrect control-flow reconstruction in the presence of loops

[sonmarcho]

Code snippet to reproduce the bug:

fn f(mut y: u32) -> bool {
    if y > 0 {
        loop {
            if y == 0 {
                return true;
            }
            y -= 1;
            if y == 0 {
                break;
            }
        }
    }
    false
}

Resulting LLBC:

fn temp::f(y^1 : u32) -> bool
{
  v@0 : bool;
  y^1 : u32;
  v@2 : bool;
  v@3 : u32;
  v@4 : bool;
  v@5 : u32;
  v@6 : u32;
  v@7 : bool;
  v@8 : u32;

  storage_live v@6;
  storage_live v@2;
  storage_live v@3;
  v@3 := copy y^1;
  v@2 := move v@3 > 0u32;
  if (move v@2) {
    storage_dead v@3;
    loop {
      storage_live v@4;
      storage_live v@5;
      v@5 := copy y^1;
      v@4 := move v@5 == 0u32;
      if (move v@4) {
        // The return got replaced by a break
        break 0
      }
      else {
        storage_dead v@5;
        storage_dead v@4;
        v@6 := copy y^1 panic.- 1u32;
        y^1 := move v@6;
        storage_live v@7;
        storage_live v@8;
        v@8 := copy y^1;
        v@7 := move v@8 == 0u32;
        if (move v@7) {
          storage_dead v@8;
          storage_dead v@7
          // HERE: there was initially a break.
          // Generally speaking, we should never reach the end of a loop body without going through
          // a continue or break. Moreover, whatever the choice we make (insert a continue or a break)
          // the resulting LLBC is erroneous.
        }
        else {
          storage_dead v@8;
          storage_dead v@7;
          continue 0
        }
      }
    };
    storage_dead v@5;
    v@0 := true;
    storage_dead v@4;
    storage_dead v@2;
    return
  }
  else {
    storage_dead v@3
  };
  storage_dead v@2;
  v@0 := false;
  return
}

[sonmarcho]

This bug was revealed by AeneasVerif/aeneas#822