Open W95Psp opened 1 year ago
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.
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!
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 | | }
| |_____________________^
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 oflet
s.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.Road map
?
withreturn
s);if c {return e1} return e2
->return (if c {e1} {e2})
than a monadic transformation) (see #393 and #254);Original issue
This is related to the question mark operator, since
e?
actually expands to amatch
whose one branch is areturn
statement.TODOs:
if c {return e1} return e2
->return (if c {e1} {e2})
than a monadic transformation) (see #393);?
operator nicely (some resugaring?).