Question mark as early returns

[W95Psp]

This PR adds a few phases:

• Drop_needless_returns;
• Simplify_question_marks;
• Simplify_match_return;
• Simplify_hoisting.

Essentially, this PR is about question marks:

• Simplify_question_marks goes through the AST and detects matches that looks like question marks (just as Reconstruct_question_marks, which is now deprecated since we want to drop it, see Remove Reconstruct_question_marks phase and Question_mark nodes from the AST #567)
• such ? matches are produced by rustc and are quite complicated (it involves https://doc.rust-lang.org/std/ops/trait.Try.html): Simplify_question_marks simplify them into simple Err/Ok (or None/Some) matches;
• the last branch of those ?-matches are early returns: Simplify_match_return does some inlining so that those early returns are pushed to exit position, becoming non-early returns (note this mechanism doesn't handle every case);
• Drop_needless_returns removes useless return statements;
• Simplify_hoisting removes extra hoistN let-bindings.

This PR fixes:

• Engine: strip automatically return when in end position #254
• Add a RewriteControlFlow phase (return/continue/break) #393

[franziskuskiefer]

Please add an issue and put it on the board.

[jschneider-bensch]

Not a review, but I've tried this out for the ProVerif backend, basically copying the phase configuration from the F* backend and it works. (#564 is the result)

[W95Psp]

@jschneider-bensch I rebased my PR, can you rebase yours onto that qustion-mark-as-early-returns branch?

That's great that those patches work for you in the PV backend 😀

[franziskuskiefer]

Thanks!

You are adding phases. Where is the documentation for the phases? As there's probably none yet, this is a good point to start. Please add docs to https://hacspec.org/hax with placeholders for the other phases and some infos on the ones you added here (an extended version of what you have in the PR is enough).

It should also answer questions like which other cases in "note this mechanism doesn't handle every case"?

[W95Psp]

So, I had to do a bit of stupid macro things in OCaml, but now we have documentation for phases gathered in one place: https://hacspec.org/hax/engine/hax-engine/Hax_engine/Phases/index.html (this will be up to date whenever the PR is merged)