feat: finally to also clean up after trapping continuations (#4507)

Introduces an optional `finally` clause to `try` expressions that can be used for disciplined (structured) resource management. The clause comprises a unit-valued expression (or block) that may not perform sends (or similar). It gets executed for all control paths that leave the `try`-expression, i.e. `return`, `break`, etc. code paths. For nested `try` expressions the cleanups are performed in innermost to outermost order.

For last-resort cleanups (i.e. code paths trapping after an `await`) the replica invokes the callback registered as `ic0.call_on_cleanup`, and this will result in the execution of (exclusively) the `finally` blocks in (dynamic) scope. This is a new mechanism in Motoko, which was not possible to achieve earlier, and puts certain resource deallocations (e.g. of acquired locks) under the programmer's control.

-----------------
TODO:
- [ ] [invoke cleanup from the interpreter](https://github.com/dfinity/motoko/pull/4507/files/51bb8a1933bbf2c509447032f1ba26b8f91fa4e0#r1658678631)
- [ ] make `catch` optional (non-trapping when missing) — #4600
  - well, this was not really needed as pattern-match failure would just re-`throw`, so we were fine. Optimised, though.
- [x] remaining FIXMEs (`arrange.ml`, etc.)
- [x] `Triv` in `try` (respect edges)
  - [x] fix fallout
- [x] forbid control-flow edges out of `finally` blocks
- [x] remove all aliasing from IR
  - [ ] use `meta` (would `assert` currently, thus causing minor code duplication) — could be follow-up PR
- [x] handle `Throw` and regular continuations in `await.ml` (instead of desugaring)
  - [x] adjust (AST, IR)-interpreter
  - ❗️this is necessary when there is no `catch`, as the exception will escape
- how are label continuations invoked in the backend? (I need to know for the _last-resort callback_)
  - have a new `context` key sort `Cleanup`, stack up continuations of finally blocks only
  - extend the `kr` in `await.ml` to `krc` (`CPSAwait`), pass `Cleanup` continuations as `c`
  - add new primitive to compiler to set the last-resort field (not needed)
  - in `async.ml` lower `CPSAwait` to that too
  - [x] adapt `check_ir.ml`, etc.
- [x] tests with `await*`
- [x] fix up the syntax part
- `do` ... `finally` (when there is no `catch` clause necessary)
  - ~means: `TryE` needs `cases list option`~
- type checking for the `finally` clause
  -  [x] unit result
  -  [x] trivial effect (actually Claudio made this capability-based)
  -  [ ] that the `try` block has `await` effect — nope!
- [x] other type than unit for `try`
- `OtherPrim "call_raw"` + tests — nope!
- `cps_asyncE` similarly to `CallPrim/3` — nope!
- highlighting of `finally`
  - [x] for `emacs`
  - [x] for VSCode → dfinity/vscode-motoko#288
  - [x] GitHub highlighter
- [x] Changelog (breaking change, new keyword)
- [x] Docs
- [ ] adapt best practices: https://internetcomputer.org/docs/current/developer-docs/security/security-best-practices/inter-canister-calls#recommendation
- [ ] adapt Motoko examples where locking happens

Building.md

@@ -56,11 +56,11 @@ For more details on our CI and CI setup, see `CI.md`.
 
 ## Making releases
 
-We make frequent releases, at least weekly. The steps to make a release (say, version 0.11.2) are:
+We make frequent releases, at least weekly. The steps to make a release (say, version 0.12.1) are:
 
  * Make sure that the top section of `Changelog.md` has a title like
 
-        ## 0.11.2 (2024-02-29)
+        ## 0.12.1 (2024-07-29)
 
    with today’s date.
 
@@ -75,20 +75,20 @@ We make frequent releases, at least weekly. The steps to make a release (say, ve
 
    If not, create and merge a separate PR to update the doc (adding any new files) and goto step 0.
 
- * Define a shell variable `export MOC_MINOR=2`
+ * Define a shell variable `export MOC_MINOR=1`
 
- * Look at `git log --first-parent 0.11.$(expr $MOC_MINOR - 1)..HEAD` and check
+ * Look at `git log --first-parent 0.12.$(expr $MOC_MINOR - 1)..HEAD` and check
    that everything relevant is mentioned in the changelog section, and possibly
    clean it up a bit, curating the information for the target audience.
 
- * `git commit -am "chore: Releasing 0.11."$MOC_MINOR`
+ * `git commit -am "chore: Releasing 0.12."$MOC_MINOR`
  * Create a PR from this commit, and label it `automerge-squash`. E.g.
-   with `git push origin HEAD:$USER/0.11.$MOC_MINOR`. Mergify will
+   with `git push origin HEAD:$USER/0.12.$MOC_MINOR`. Mergify will
    merge it into `master` without additional approval, but it will take some
    time as the title (version number) enters into the `nix` dependency tracking.
  * `git switch master; git pull --rebase`. The release commit should be your `HEAD`
- * `git tag 0.11.$MOC_MINOR -m "Motoko 0.11."$MOC_MINOR`
- * `git push origin 0.11.$MOC_MINOR`
+ * `git tag 0.12.$MOC_MINOR -m "Motoko 0.12."$MOC_MINOR`
+ * `git push origin 0.12.$MOC_MINOR`
 
 Pushing the tag should cause GitHub Actions to create a “Release” on the GitHub
 project. This will fail if the changelog is not in order (in this case, fix and
@@ -102,12 +102,12 @@ branch to the `next-moc` branch.
 * Wait ca. 5min after releasing to give the CI/CD pipeline time to upload the release artifacts
 * Change into `motoko-base`
 * `git switch next-moc; git pull`
-* `git switch -c $USER/update-moc-0.11.$MOC_MINOR`
+* `git switch -c $USER/update-moc-0.12.$MOC_MINOR`
 * Update the `CHANGELOG.md` file with an entry at the top
 * Update the `moc_version` env variable in `.github/workflows/{ci, package-set}.yml` and `mops.toml`
   to the new released version:
-  `perl -pi -e "s/moc_version: \"0\.11\.\\d+\"/moc_version: \"0.11.$MOC_MINOR\"/g; s/moc = \"0\.11\.\\d+\"/moc = \"0.11.$MOC_MINOR\"/g; s/version = \"0\.11\.\\d+\"/version = \"0.11.$MOC_MINOR\"/g" .github/workflows/ci.yml .github/workflows/package-set.yml mops.toml`
-* `git add .github/ CHANGELOG.md mops.toml && git commit -m "Motoko 0.11."$MOC_MINOR`
+  `perl -pi -e "s/moc_version: \"0\.12\.\\d+\"/moc_version: \"0.12.$MOC_MINOR\"/g; s/moc = \"0\.12\.\\d+\"/moc = \"0.12.$MOC_MINOR\"/g; s/version = \"0\.12\.\\d+\"/version = \"0.12.$MOC_MINOR\"/g" .github/workflows/ci.yml .github/workflows/package-set.yml mops.toml`
+* `git add .github/ CHANGELOG.md mops.toml && git commit -m "Motoko 0.12."$MOC_MINOR`
 * Revise `CHANGELOG.md`, adding a top entry for the release
 * You can `git push` now
 
@@ -117,8 +117,8 @@ repo by a scheduled `niv-updater-action`.
 
 Finally tag the base release (so the documentation interpreter can do the right thing):
 * `git switch master && git pull`
-* `git tag moc-0.11.$MOC_MINOR`
-* `git push origin moc-0.11.$MOC_MINOR`
+* `git tag moc-0.12.$MOC_MINOR`
+* `git push origin moc-0.12.$MOC_MINOR`
 
 If you want to update the portal documentation, typically to keep in sync with a `dfx` release, follow the instructions in https://github.com/dfinity/portal/blob/master/MAINTENANCE.md.
 

Changelog.md

@@ -1,5 +1,29 @@
 # Motoko compiler changelog
 
+## 0.12.0 (to come)
+
+* motoko (`moc`)
+
+  * feat: `finally` clauses for `try` expressions (#4507).
+
+    A trailing `finally` clause to `try`/`catch` expressions facilitates structured
+    resource deallocation (e.g. acquired locks, etc.) and similar cleanups in the
+    presence of control-flow expressions (`return`, `break`, `continue`, `throw`).
+    Additionally, in presence of `finally` the `catch` clause becomes optional and
+    and any uncaught error from the `try` block will be propagated, after executing the `finally` block.
+
+    _Note_: `finally`-expressions that are in scope will be executed even if an execution
+    path _following_ an `await`-expression traps. This feature, formerly not available in Motoko,
+    allows programmers to implement cleanups even in the presence of traps. For trapping 
+    execution paths prior to any `await`, the replica-provided state roll-back mechanism 
+    ensures that no cleanup is required.
+
+    The relevant security best practices are accessible at
+    https://internetcomputer.org/docs/current/developer-docs/security/security-best-practices/inter-canister-calls#recommendation
+
+    BREAKING CHANGE (Minor): `finally` is now a reserved keyword,
+    programs using this identifier will break.
+
 ## 0.11.3 (2024-07-16)
 
 * motoko (`moc`)

doc/md/examples/grammar.txt

@@ -217,6 +217,8 @@
     'if' <exp_nullary> <exp_nest>
     'if' <exp_nullary> <exp_nest> 'else' <exp_nest>
     'try' <exp_nest> <catch>
+    'try' <exp_nest> <catch> 'finally' <exp_nest>
+    'try' <exp_nest> 'finally' <exp_nest>
     'throw' <exp_nest>
     'switch' <exp_nullary> '{' <list(<case>, ';')> '}'
     'while' <exp_nullary> <exp_nest>

doc/md/reference/language-manual.md

@@ -91,7 +91,7 @@ The following keywords are reserved and may not be used as identifiers:
 ``` bnf
 
 actor and assert async async* await await* break case catch class
-composite continue debug debug_show do else flexible false for
+composite continue debug debug_show do else false flexible finally for
 from_candid func if ignore import in module not null object or label
 let loop private public query return shared stable switch system throw
 to_candid true try type var while with
@@ -514,6 +514,9 @@ The syntax of an expression is as follows:
   await* <block-or-exp>                          Await a delayed computation (only in async)
   throw <exp>                                    Raise an error (only in async)
   try <block-or-exp> catch <pat> <block-or-exp>  Catch an error (only in async)
+  try <block-or-exp> finally <block-or-exp>      Guard with cleanup
+  try <block-or-exp> catch <pat> <block-or-exp> finally <block-or-exp>
+                                                 Catch an error (only in async) and cleanup
   assert <block-or-exp>                          Assertion
   <exp> : <typ>                                  Type annotation
   <dec>                                          Declaration
@@ -2547,6 +2550,11 @@ Because the [`Error`](../base/Error.md) type is opaque, the pattern match cannot
 
 :::
 
+The `try` expression can be provided with a `finally` cleanup clause to facilitate structured rollback of temporary state changes (e.g. to release a lock). 
+The preceding `catch` clause may be omitted in the presence of a `finally` clause.
+
+This form is `try <block-or-exp1> (catch <pat> <block-or-exp2>)? finally <block-or-exp3>`, and evaluation proceeds as above with the crucial addition that every control-flow path leaving `<block-or-exp1>` or `<block-or-exp2>` will execute the unit-valued `<block-or-exp3>` before the entire `try` expression produces its result. The cleanup expression will additionally also be executed when the processing after an intervening `await` (directly, or indirectly as `await*`) traps.
+
 See [Error type](#error-type).
 
 ### Assert

emacs/motoko-mode.el

@@ -47,6 +47,7 @@
                  "debug"
                  "debug_show"
                  "else"
+                 "finally"
                  "flexible"
                  "for"
                  "from_candid"

rts/motoko-rts/src/continuation_table.rs

@@ -109,7 +109,7 @@ pub unsafe fn remember_continuation<M: Memory>(mem: &mut M, ptr: Value) -> u32 {
 
 // Position of the future in explicit self-send ContinuationTable entries
 // Invariant: keep this synchronised with compiler.ml (see future_array_index)
-const FUTURE_ARRAY_INDEX: u32 = 2;
+const FUTURE_ARRAY_INDEX: u32 = 3;
 
 #[no_mangle]
 pub unsafe extern "C" fn peek_future_continuation(idx: u32) -> Value {

src/codegen/compile.ml

@@ -9149,39 +9149,39 @@ module FuncDec = struct
     ))
 
   let message_start env sort = match sort with
-      | Type.Shared Type.Write ->
-        Lifecycle.trans env Lifecycle.InUpdate
-      | Type.Shared Type.Query ->
-        Lifecycle.trans env Lifecycle.InQuery
-      | Type.Shared Type.Composite ->
-        Lifecycle.trans env Lifecycle.InComposite
+      | Type.(Shared Write) ->
+        Lifecycle.(trans env InUpdate)
+      | Type.(Shared Query) ->
+        Lifecycle.(trans env InQuery)
+      | Type.(Shared Composite) ->
+        Lifecycle.(trans env InComposite)
       | _ -> assert false
 
   let message_cleanup env sort = match sort with
-      | Type.Shared Type.Write ->
+      | Type.(Shared Write) ->
         GC.collect_garbage env ^^
-        Lifecycle.trans env Lifecycle.Idle
-      | Type.Shared Type.Query ->
-        Lifecycle.trans env Lifecycle.PostQuery
-      | Type.Shared Type.Composite ->
+        Lifecycle.(trans env Idle)
+      | Type.(Shared Query) ->
+        Lifecycle.(trans env PostQuery)
+      | Type.(Shared Composite) ->
         (* Stay in composite query state such that callbacks of 
         composite queries can also use the memory reserve. 
         The state is isolated since memory changes of queries 
         are rolled back by the IC runtime system. *)
-        Lifecycle.trans env Lifecycle.InComposite
+        Lifecycle.(trans env InComposite)
       | _ -> assert false
 
   let callback_start env =
-    Lifecycle.is_in env Lifecycle.InComposite ^^
+    Lifecycle.(is_in env InComposite) ^^
     G.if0
       (G.nop)
-      (message_start env (Type.Shared Type.Write))
+      (message_start env Type.(Shared Write))
 
   let callback_cleanup env =
-    Lifecycle.is_in env Lifecycle.InComposite ^^
+    Lifecycle.(is_in env InComposite) ^^
     G.if0
       (G.nop)
-      (message_cleanup env (Type.Shared Type.Write))
+      (message_cleanup env Type.(Shared Write))
 
   let compile_const_message outer_env outer_ae sort control args mk_body ret_tys at : E.func_with_names =
     let ae0 = VarEnv.mk_fun_ae outer_ae in
@@ -9383,7 +9383,7 @@ module FuncDec = struct
     (* result is a function that accepts a list of closure getters, from which
        the first and second must be the reply and reject continuations. *)
     fun closure_getters ->
-      let (set_cb_index, get_cb_index) = new_local env "cb_index" in
+      let set_cb_index, get_cb_index = new_local env "cb_index" in
       Arr.lit env closure_getters ^^
       ContinuationTable.remember env ^^
       set_cb_index ^^
@@ -9411,7 +9411,12 @@ module FuncDec = struct
     Func.define_built_in env name ["env", I32Type] [] (fun env ->
         G.i (LocalGet (nr 0l)) ^^
         ContinuationTable.recall env ^^
-        G.i Drop);
+        Arr.load_field env 2l ^^ (* get the cleanup closure *)
+        let set_closure, get_closure = new_local env "closure" in
+        set_closure ^^ get_closure ^^
+        Closure.prepare_closure_call env ^^
+        get_closure ^^
+        Closure.call_closure env 0 0);
     compile_unboxed_const (E.add_fun_ptr env (E.built_in env name))
 
   let ic_call_threaded env purpose get_meth_pair push_continuations
@@ -9460,29 +9465,29 @@ module FuncDec = struct
     | _ ->
       E.trap_with env (Printf.sprintf "cannot perform %s when running locally" purpose)
 
-  let ic_call env ts1 ts2 get_meth_pair get_arg get_k get_r =
+  let ic_call env ts1 ts2 get_meth_pair get_arg get_k get_r get_c =
     ic_call_threaded
       env
       "remote call"
       get_meth_pair
-      (closures_to_reply_reject_callbacks env ts2 [get_k; get_r])
+      (closures_to_reply_reject_callbacks env ts2 [get_k; get_r; get_c])
       (fun _ -> get_arg ^^ Serialization.serialize env ts1)
 
-  let ic_call_raw env get_meth_pair get_arg get_k get_r =
+  let ic_call_raw env get_meth_pair get_arg get_k get_r get_c =
     ic_call_threaded
       env
       "raw call"
       get_meth_pair
-      (closures_to_raw_reply_reject_callbacks env [get_k; get_r])
+      (closures_to_raw_reply_reject_callbacks env [get_k; get_r; get_c])
       (fun _ -> get_arg ^^ Blob.as_ptr_len env)
 
-  let ic_self_call env ts get_meth_pair get_future get_k get_r =
+  let ic_self_call env ts get_meth_pair get_future get_k get_r get_c =
     ic_call_threaded
       env
       "self call"
       get_meth_pair
-      (* Storing the tuple away, future_array_index = 2, keep in sync with rts/continuation_table.rs *)
-      (closures_to_reply_reject_callbacks env ts [get_k; get_r; get_future])
+      (* Storing the tuple away, future_array_index = 3, keep in sync with rts/continuation_table.rs *)
+      (closures_to_reply_reject_callbacks env ts [get_k; get_r; get_c; get_future])
       (fun get_cb_index ->
         get_cb_index ^^
         BoxedSmallWord.box env Type.Nat32 ^^
@@ -11783,7 +11788,7 @@ and compile_prim_invocation (env : E.t) ae p es at =
   | ICCallerPrim, [] ->
     SR.Vanilla, IC.caller env
 
-  | ICCallPrim, [f;e;k;r] ->
+  | ICCallPrim, [f;e;k;r;c] ->
     SR.unit, begin
     (* TBR: Can we do better than using the notes? *)
     let _, _, _, ts1, _ = Type.as_func f.note.Note.typ in
@@ -11792,19 +11797,22 @@ and compile_prim_invocation (env : E.t) ae p es at =
     let (set_arg, get_arg) = new_local env "arg" in
     let (set_k, get_k) = new_local env "k" in
     let (set_r, get_r) = new_local env "r" in
+    let (set_c, get_c) = new_local env "c" in
     let add_cycles = Internals.add_cycles env ae in
     compile_exp_vanilla env ae f ^^ set_meth_pair ^^
     compile_exp_vanilla env ae e ^^ set_arg ^^
     compile_exp_vanilla env ae k ^^ set_k ^^
     compile_exp_vanilla env ae r ^^ set_r ^^
-    FuncDec.ic_call env ts1 ts2 get_meth_pair get_arg get_k get_r add_cycles
+    compile_exp_vanilla env ae c ^^ set_c ^^
+    FuncDec.ic_call env ts1 ts2 get_meth_pair get_arg get_k get_r get_c add_cycles
     end
-  | ICCallRawPrim, [p;m;a;k;r] ->
+  | ICCallRawPrim, [p;m;a;k;r;c] ->
     SR.unit, begin
-    let (set_meth_pair, get_meth_pair) = new_local env "meth_pair" in
-    let (set_arg, get_arg) = new_local env "arg" in
-    let (set_k, get_k) = new_local env "k" in
-    let (set_r, get_r) = new_local env "r" in
+    let set_meth_pair, get_meth_pair = new_local env "meth_pair" in
+    let set_arg, get_arg = new_local env "arg" in
+    let set_k, get_k = new_local env "k" in
+    let set_r, get_r = new_local env "r" in
+    let set_c, get_c = new_local env "c" in
     let add_cycles = Internals.add_cycles env ae in
     compile_exp_vanilla env ae p ^^
     compile_exp_vanilla env ae m ^^ Text.to_blob env ^^
@@ -11813,7 +11821,8 @@ and compile_prim_invocation (env : E.t) ae p es at =
     compile_exp_vanilla env ae a ^^ set_arg ^^
     compile_exp_vanilla env ae k ^^ set_k ^^
     compile_exp_vanilla env ae r ^^ set_r ^^
-    FuncDec.ic_call_raw env get_meth_pair get_arg get_k get_r add_cycles
+    compile_exp_vanilla env ae c ^^ set_c ^^
+    FuncDec.ic_call_raw env get_meth_pair get_arg get_k get_r get_c add_cycles
     end
 
   | ICMethodNamePrim, [] ->
@@ -12022,11 +12031,12 @@ and compile_exp_with_hint (env : E.t) ae sr_hint exp =
     let return_arity = List.length return_tys in
     let mk_body env1 ae1 = compile_exp_as env1 ae1 (StackRep.of_arity return_arity) e in
     FuncDec.lit env ae x sort control captured args mk_body return_tys exp.at
-  | SelfCallE (ts, exp_f, exp_k, exp_r) ->
+  | SelfCallE (ts, exp_f, exp_k, exp_r, exp_c) ->
     SR.unit,
     let (set_future, get_future) = new_local env "future" in
     let (set_k, get_k) = new_local env "k" in
     let (set_r, get_r) = new_local env "r" in
+    let (set_c, get_c) = new_local env "c" in
     let mk_body env1 ae1 = compile_exp_as env1 ae1 SR.unit exp_f in
     let captured = Freevars.captured exp_f in
     let add_cycles = Internals.add_cycles env ae in
@@ -12036,13 +12046,15 @@ and compile_exp_with_hint (env : E.t) ae sr_hint exp =
 
     compile_exp_vanilla env ae exp_k ^^ set_k ^^
     compile_exp_vanilla env ae exp_r ^^ set_r ^^
+    compile_exp_vanilla env ae exp_c ^^ set_c ^^
 
     FuncDec.ic_self_call env ts
       IC.(get_self_reference env ^^
           actor_public_field env async_method_name)
       get_future
       get_k
       get_r
+      get_c
       add_cycles
   | ActorE (ds, fs, _, _) ->
     fatal "Local actors not supported by backend"

src/gen-grammar/grammar.sed

@@ -53,6 +53,7 @@ s/UNDERSCORE/\'_\'/g
 s/TYPE/\'type\'/g
 s/TRY/\'try\'/g
 s/THROW/\'throw\'/g
+s/FINALLY/\'finally\'/g
 s/TEXT/<text>/g
 s/SWITCH/\'switch\'/g
 s/SUBOP/\'-\'/g

src/idllib/escape.ml

@@ -73,6 +73,7 @@ let is_motoko_keyword = function
   | "do"
   | "else"
   | "false"
+  | "finally"
   | "flexible"
   | "for"
   | "from_candid"

src/ir_def/arrange_ir.ml

@@ -28,11 +28,12 @@ let rec exp e = match e.it with
   | DefineE (i, m, e1)  -> "DefineE" $$ [id i; mut m; exp e1]
   | FuncE (x, s, c, tp, as_, ts, e) ->
     "FuncE" $$ [Atom x; func_sort s; control c] @ List.map typ_bind tp @ args as_ @ [ typ (Type.seq ts); exp e]
-  | SelfCallE (ts, exp_f, exp_k, exp_r) ->
-    "SelfCallE" $$ [typ (Type.seq ts); exp exp_f; exp exp_k; exp exp_r]
+  | SelfCallE (ts, exp_f, exp_k, exp_r, exp_c) ->
+    "SelfCallE" $$ [typ (Type.seq ts); exp exp_f; exp exp_k; exp exp_r; exp exp_c]
   | ActorE (ds, fs, u, t) -> "ActorE"  $$ List.map dec ds @ fields fs @ [system u; typ t]
   | NewObjE (s, fs, t)  -> "NewObjE" $$ (Arrange_type.obj_sort s :: fields fs @ [typ t])
-  | TryE (e, cs)        -> "TryE" $$ [exp e] @ List.map case cs
+  | TryE (e, cs, None) -> "TryE" $$ [exp e] @ List.map case cs
+  | TryE (e, cs, Some (i, _)) -> "TryE" $$ [exp e] @ List.map case cs @ Atom ";" :: [id i]
 
 and system { meta; preupgrade; postupgrade; heartbeat; timer; inspect} = (* TODO: show meta? *)
   "System" $$ [