Meta issue: support `return`/`continue`/`?`/`break`

[W95Psp]

This issue is about any expression that can yield an early return: ?, return, continue, break.

The engine has a module side_effect_utils.ml that deals with any expression with side effects: its approach is to hoist every side effect within an expression.

After applying this side effect phase, expressions are trees with let, if, match, loop nodes, and the side-effects occur only on rhs of lets.

Note early return is one of the different possible side effects. Also, one cannot rewrite early returns without considering other side effects: for instance, early returns can interact badly with mutation.

From there:

• CfIntoMonads lifts early return bottom up into various monads.
• we also want a phase that attempts to restructure control flow, to push early returns to end positions.

Road map

• [x] resugar questions marks (Rustc rewrite ? with returns);
• [x] add a phase that transforms early returns into monadic constructions;
  • [ ] test this monadic phase;
  • [ ] fix bugs;
• [x] add a phase that attempts at reformulating control flow to avoid early returns (i.e. we'd better do if c {return e1} return e2 -> return (if c {e1} {e2}) than a monadic transformation) (see #393 and #254);
• [ ] wrap the monadic and reformulation phase into another phase that decides heuristically which looks best.
• [ ] support continue/return within loops: #196

Original issue

This is related to the question mark operator, since e? actually expands to a match whose one branch is a return statement.

TODOs:

• (x) add a phase that transforms early returns into monadic constructions;
• fix the current monadic encoding #399;
• add a phase that attempts at reformulating control flow to avoid early returns (i.e. we'd better do if c {return e1} return e2 -> return (if c {e1} {e2}) than a monadic transformation) (see #393);
• add a phase that tries both monadic and control-flow reformulation phases and decides heuristically which seems better;
• (x) figure out how to translate code containing the ? operator nicely (some resugaring?).

[chrysn]

If it helps with planning this, my impression working on edhoc-rs is that most of the cases where we have a ? in there is in code without any nesting. These functions should be splittable into separate branches as shown in TODO item no.2 shows. Any partial solution that can just handle that case (with the ? in a separate let a = a?; statement mid-function if need be) would already greatly enhance the readability of edhoc-rs.

[W95Psp]

Yes, you are right, hax should already handle basic rewriting when it's possible. I'm gonna try to allocate some time to that somewhere next week!

[kaspar030]

I think we just hit this and were directed here to upvote:

error[HAX0001]: (CfIntoMonads) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/96.
                Please upvote or comment this issue if you see this error message.
                TODO: Monad for loop-related control flow
   --> src/riot-rs-runqueue/src/runqueue.rs:267:59
    |
267 |                       if self.next_idxs[prev as usize] == n {
    |  ___________________________________________________________^
268 | |                         break;
269 | |                     }
    | |_____________________^

[W95Psp]

Fixed by #988

[W95Psp]

This is closed, the regression is tracked by https://github.com/hacspec/hax/issues/1044, and is going to be fixed soon.