diff options
| -rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.ml | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index f9d45f20..80cd93cf 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -492,6 +492,39 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct borrowed value is modified in a loop iteration, then there is a fresh abstraction between this borrowed value and the fixed abstractions. + + Example: + ======== + {[ + fn clear(v: &mut Vec<u32>) { + let mut i = 0; + while i < v.len() { + v[i] = 0; + i += 1; + } + } + ]} + + When entering the loop, we have the following environment: + {[ + abs'0 { ML l0 } // input abstraction + v -> MB l0 s0 + i -> 0 + ]} + + At every iteration, we update the symbolic value of the vector [v] + (i.e., [s0]). + + For now, because the translation of the loop is responsible of the + execution of the end of the function (up to the [return]), we want + the loop to reborrow the vector [v]: this way, the forward loop + function returns nothing (it returns what [clear] returns, that is + to say [unit]) while the backward loop function gives back a new value + for [v] (i.e., a new symbolic value which will replace [s0]). + + In the future, we will also compute joins at the *loop exits*: when we + do so, we won't introduce reborrows like above: the forward loop function + will update [v], while the backward loop function will return nothing. *) assert (not (value_has_borrows S.ctx bv.V.value)); |