Fatal error on `continue`

[jschneider-bensch]

Running

cargo hax -C -p polytune --features "is_sync" ";" into -i "-** +**::faand::fhaand +**::faand::flaand" fstar

on the code in this repository at commit 296ecf7 results in

error: [HAX0002] (DropReturnBreakContinue) Fatal error: something we considered as impossible occurred! Please report this by submitting an issue on GitHub!Details: Return/Break/Continue are expected to be gone as this point
   --> src/faand.rs:720:23
    |
720 |               if k == i {
    |  _______________________^
721 | |                 continue;
722 | |             }
    | |_____________^
    |

With the offending continue located here within a nested loop:

    let mut phi = vec![0; l];
    for ll in 0..l {
        for k in 0..n {
            if k == i {
                continue;
            }
            let (mk_yi, ki_yk) = yshares[ll].1 .0[k];
            phi[ll] = phi[ll] ^ ki_yk.0 ^ mk_yi.0;
        }
        phi[ll] = phi[ll] ^ yshares[ll].0 as u128 * delta.0;
    }

I tried finding a minimized reproducer for this, but couldn't do it so far. I'm not sure what's happening as also the phase debugger (-d i) doesn't work in the context of this large crate.

Here's a reproducer

fn nested_loop(l: usize, n: usize, i: usize) {
    for ll in 0..l {
        for k in 0..n {
            if k == i {
                continue;
            }
        }
    }
}

Open this code snippet in the playground

[jschneider-bensch]

My workaround for now is writing that loop as

    let mut phi = vec![0; l];
    for ll in 0..l {
        for k in 0..n {
            if k == i {
            } else {
                let (mk_yi, ki_yk) = yshares[ll].1 .0[k];
                phi[ll] = phi[ll] ^ ki_yk.0 ^ mk_yi.0;
            }
        }
        phi[ll] = phi[ll] ^ yshares[ll].0 as u128 * delta.0;
    }

which looks weird, but works.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[clementblaudeau]

The original issue is fixed. However, an empty loop without side effect will still throw an error : https://github.com/cryspen/hax/issues/405