Merge remote-tracking branch 'origin/gabor/finally' into luc/merge-fi…

…nally-integrate-eop

Changelog.md

@@ -11,10 +11,10 @@
     presence of control-flow expressions (`return`, `break`, `continue`, `throw`).
 
     _Note_: `finally`-expressions that are in scope will be executed even if an execution
-    path _following_ an `await`-expression traps. This behaviour, not available before in Motoko,
-    allows programmers writing last-resort cleanups. For trapping execution paths _without_ an
-    intervening `await`, the replica-provided state rewinding mechanism stays in charge of
-    the cleanup.
+    path _following_ an `await`-expression traps. This feature, not available before 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 must 
+    ensure 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

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 obtains its value. The cleanup expression will additionaly also be executed when the processing after an intervening `await` (directly, or indirectly as `await*`) traps.
+
 See [Error type](#error-type).
 
 ### Assert

src/ir_def/check_ir.ml

@@ -365,13 +365,13 @@ let rec check_exp env (exp:Ir.exp) : unit =
   (* helpers *)
   let check p = check env exp.at p in
   let (<:) t1 t2 =
-  try
+(*  try *)
       check_sub env exp.at t1 t2
-  with e ->
+(*  with e ->
      (Printf.eprintf "(in here):\n%s"
         (Wasm.Sexpr.to_string 80 (Arrange_ir.exp exp));
       raise e)
-
+*)
   in
   (* check for aliasing *)
   if exp.note.Note.check_run = env.check_run
@@ -409,7 +409,7 @@ let rec check_exp env (exp:Ir.exp) : unit =
             check_concrete env exp.at t_ret;
           end;
           typ exp2 <: t_arg;
-          t_ret <: t;
+          t_ret <: t
         | T.Non -> () (* dead code, not much to check here *)
         | t1 -> error env exp1.at "expected function type, but expression produces type\n  %s"
              (T.string_of_typ_expand t1)
@@ -560,7 +560,7 @@ let rec check_exp env (exp:Ir.exp) : unit =
            (match ts2 with
             | [] -> ()
             | _ -> error env exp.at "CPSAwait answer type error");
-           typ krc <: T.Tup T.[cont_typ; Construct.err_contT (Tup ts2); Construct.bail_contT];
+           typ krc <: T.(Tup Construct.[cont_typ; err_contT (seq ts2); bail_contT]);
            t1 <: T.seq ts1;
            T.seq ts2 <: t;
          end;

src/ir_interpreter/interpret_ir.ml

@@ -490,20 +490,19 @@ and interpret_exp_mut env exp (k : V.value V.cont) =
     interpret_exp env exp1 (fun v1 ->
       interpret_cases env cases exp.at v1 k
     )
-  | TryE (exp1, cases, None) ->
-    let k' = fun v1 -> interpret_catches env cases exp.at v1 k in
-    let env' = { env with throws = Some k' } in
-    interpret_exp env' exp1 k
-  | TryE (exp1, cases, Some (id, ty)) ->
+  | TryE (exp1, cases, finally_opt) ->
     assert env.flavor.has_await;
-    let exp2 = Construct.(varE (var id ty) -*- unitE ()) in
-    let k' v1 =
-      interpret_catches env cases exp.at v1 k in
-    let out ret v = interpret_exp env exp2 (fun u -> V.as_unit u; ret v) in
-    let env' = { env with throws = Some k'
-                        ; rets = Option.map out env.rets
-                        ; labs = V.Env.map out env.labs } in
-    interpret_exp env' exp1 k
+    let k, env = match finally_opt with
+      | None -> k, env
+      | Some (id, ty) ->
+        let exp2 = Construct.(varE (var id ty) -*- unitE ()) in
+        let pre k v = interpret_exp env exp2 (fun v2 -> V.as_unit v2; k v) in
+        pre k,
+        { env with rets = Option.map pre env.rets
+                 ; labs = V.Env.map pre env.labs
+                 ; throws = Option.map pre env.throws } in
+    let k' v1 = interpret_catches env cases exp.at v1 k in
+    interpret_exp { env with throws = Some k' } exp1 k
   | LoopE exp1 ->
     interpret_exp env exp1 (fun v -> V.as_unit v; interpret_exp env exp k)
   | LabelE (id, _typ, exp1) ->

src/ir_passes/async.ml

@@ -341,7 +341,7 @@ let transform prog =
          )
          (varE nary_async))
         .it
-    | PrimE (OtherPrim "call_raw", [exp1; exp2; exp3]) ->(* HERE *)
+    | PrimE (OtherPrim "call_raw", [exp1; exp2; exp3]) ->
       let exp1' = t_exp exp1 in
       let exp2' = t_exp exp2 in
       let exp3' = t_exp exp3 in

src/ir_passes/await.ml

@@ -344,26 +344,34 @@ and c_exp' context exp k =
                note = Note.{ exp.note with typ = typ' } }))
     end)
   | TryE (exp1, cases, finally_opt) ->
-    let pre = function
-      | Cont k -> (match finally_opt with
-                   | Some (id2, typ2) -> Cont (precont k (var id2 typ2))
-                   | None -> Cont k)
+     let pre k =
+       match finally_opt with
+       | Some (id2, typ2) -> precont k (var id2 typ2)
+       | None -> k in
+    let pre' = function
+      | Cont k -> Cont (pre k)
       | Label -> assert false in
-    (* All control-flow out must pass through the `finally` thunk *)
-    let context = LabelEnv.mapi (function | Return | Named _ | Cleanup -> pre
-                                          | Throw -> fun c -> c) context in
+    (* All control-flow out must pass through the potential `finally` thunk *)
+    let context = LabelEnv.map pre' context in
     (* assert that a surrounding `AwaitPrim _` has set up a `Cleanup` cont *)
     if finally_opt <> None
     then ignore (LabelEnv.find Cleanup context);
     (* TODO: do we need to reify f? *)
     let f = match LabelEnv.find Throw context with Cont f -> f | _ -> assert false in
     letcont f (fun f ->
-    letcont k (fun k ->
+    letcont (pre k) (fun k ->
     match eff exp1 with
     | T.Triv ->
       varE k -*- t_exp context exp1
+    | T.Await when cases = [] ->
+      c_exp context exp1 (ContVar k)
     | T.Await ->
       let error = fresh_var "v" T.catch in
+      let rethrow = { it = { pat = varP error; exp = varE f -*- varE error };
+                      at = no_region;
+                      note = ()
+                    } in
+      let omit_rethrow = List.exists (fun {it = {pat; exp}; _} -> Ir_utils.is_irrefutable pat) cases in
       let cases' =
         List.map
           (fun {it = { pat; exp }; at; note} ->
@@ -373,10 +381,7 @@ and c_exp' context exp k =
             in
             { it = { pat; exp = exp' }; at; note })
           cases
-        @ [{ it = { pat = varP error; exp = varE f -*- varE error };
-             at = no_region;
-             note = ()
-        }] in
+        @ if omit_rethrow then [] else [rethrow] in
       let throw = fresh_err_cont (answerT (typ_of_var k)) in
       let context' = LabelEnv.add Throw (Cont (ContVar throw)) context in
       blockE

src/lang_utils/error_codes.ml

@@ -203,5 +203,4 @@ let error_codes : (string * string option) list =
     "M0197", Some([%blob "lang_utils/error_codes/M0197.md"]); (* `system` capability required *)
     "M0198", Some([%blob "lang_utils/error_codes/M0198.md"]); (* Unused field pattern warning *)
     "M0199", Some([%blob "lang_utils/error_codes/M0199.md"]); (* Deprecate experimental stable memory *)
-    "M0200", Some([%blob "lang_utils/error_codes/M0200.md"]); (* Cleanup clause must have trivial effect *)
   ]

src/lib/lib.ml

@@ -1,3 +1,5 @@
+module StdList = List
+
 module Format =
 struct
   let with_str_formatter f x =
@@ -504,7 +506,9 @@ module Option =
 struct
   let get o x = Option.value o ~default:x
 
-  let map2 (f : 'a -> 'b -> 'c) (a : 'a option) (b : 'b option) =
+  let exists f o = Option.to_list o |> StdList.exists f
+
+  let map2 f a b =
     match a, b with
     | Some a, Some b -> Some (f a b)
     | _ -> None

src/lib/lib.mli

@@ -96,6 +96,7 @@ sig
     val (and+) : 'a option -> 'b option -> ('a * 'b) option
   end
   val get : 'a option -> 'a -> 'a
+  val exists : ('a -> bool) -> 'a option -> bool
   val map2 : ('a -> 'b -> 'c) -> 'a option -> 'b option -> 'c option
 end
 

src/lowering/desugar.ml

@@ -221,11 +221,9 @@ and exp' at note = function
     let thunk = T.(funcE ("$cleanup") Local Returns [] [] [] (exp e2)) in
     assert T.(is_func thunk.note.Note.typ);
     let th = fresh_var "thunk" thunk.note.Note.typ in
-    let v = fresh_var "res" note.Note.typ in
-    (blockE [ letD th thunk
-            ; letD v { e1 with it = I.TryE (exp e1, cases cs, Some (id_of_var th, typ_of_var th)); note }
-            ; expD (varE th -*- unitE ())
-            ] (varE v)).it
+    (blockE
+       [ letD th thunk ]
+       { e1 with it = I.TryE (exp e1, cases cs, Some (id_of_var th, typ_of_var th)); note }).it
   | S.WhileE (e1, e2) -> (whileE (exp e1) (exp e2)).it
   | S.LoopE (e1, None) -> I.LoopE (exp e1)
   | S.LoopE (e1, Some e2) -> (loopWhileE (exp e1) (exp e2)).it

src/mo_frontend/parser.mly

@@ -711,7 +711,7 @@ exp_un(B) :
     { TryE(e1, [c], None) @? at $sloc }
   | TRY e1=exp_nest c=catch FINALLY e2=exp_nest
     { TryE(e1, [c], Some e2) @? at $sloc }
-  | TRY e1=exp_nest FINALLY e2=exp_nest (* FIXME: needs a different keyword (`DO`?), provisional *)
+  | TRY e1=exp_nest FINALLY e2=exp_nest
     { TryE(e1, [], Some e2) @? at $sloc }
 (* TODO: enable multi-branch TRY (already supported by compiler)
   | TRY e=exp_nest LCURLY cs=seplist(case, semicolon) RCURLY

src/mo_frontend/typing.ml

@@ -1538,9 +1538,10 @@ and infer_exp'' env exp : T.typ =
     let t1 = infer_exp env exp1 in
     let t2 = infer_cases env T.catch T.Non cases in
     if not env.pre then begin
-      Option.iter (check_exp_strong { env with rets = None; labs = T.Env.empty } T.unit) exp2_opt;
       check_ErrorCap env "try" exp.at;
-      coverage_cases "try handler" env cases T.catch exp.at
+      if cases <> [] then
+        coverage_cases "try handler" env cases T.catch exp.at;
+      Option.iter (check_exp_strong { env with async = C.NullCap; rets = None; labs = T.Env.empty } T.unit) exp2_opt
     end;
     T.lub t1 t2
   | WhileE (exp1, exp2) ->
@@ -1841,15 +1842,10 @@ and check_exp' env0 t exp : T.typ =
     check_ErrorCap env "try" exp.at;
     check_exp env t exp1;
     check_cases env T.catch t cases;
-    coverage_cases "try handler" env cases T.catch exp.at;
+    if cases <> []
+    then coverage_cases "try handler" env cases T.catch exp.at;
     if not env.pre then
-      begin match exp2_opt with
-      | None -> ()
-      | Some exp2 ->
-        check_exp_strong { env with rets = None; labs = T.Env.empty } T.unit exp2;
-        if exp2.note.note_eff <> T.Triv then
-          local_error env exp2.at "M0200" "a cleanup clause must not send messages";
-      end;
+      Option.iter (check_exp_strong { env with async = C.NullCap; rets = None; labs = T.Env.empty; } T.unit) exp2_opt;
     t
   (* TODO: allow shared with one scope par *)
   | FuncE (_, shared_pat,  [], pat, typ_opt, _sugar, exp), T.Func (s, c, [], ts1, ts2) ->

src/mo_interpreter/interpret.ml

@@ -620,20 +620,17 @@ and interpret_exp_mut env exp (k : V.value V.cont) =
     interpret_exp env exp1 (fun v1 ->
       interpret_cases env cases exp.at v1 k
       )
-  | TryE (exp1, cases, None) ->
-    let k' = fun v1 -> interpret_catches env cases exp.at v1 k in
-    let env' = { env with throws = Some k' } in
-    interpret_exp env' exp1 k
-  | TryE (exp1, cases, Some exp2) ->
-    let k' v1 =
-      let cleanup v2 = interpret_exp env exp2 (fun _ -> k v2) in
-      interpret_catches env cases exp.at v1 cleanup in
-    let out ret v = interpret_exp env exp2 (fun _ -> ret v) in
-    let k'' v2 = interpret_exp env exp2 (fun _ -> k v2) in
-    let env' = { env with throws = Some k'
-                        ; rets = Option.map out env.rets
-                        ; labs = V.Env.map out env.labs } in
-    interpret_exp env' exp1 k''
+  | TryE (exp1, cases, exp2_opt) ->
+    let k, env = match exp2_opt with
+      | None -> k, env
+      | Some exp2 ->
+        let pre k v = interpret_exp env exp2 (fun v2 -> V.as_unit v2; k v) in
+        pre k,
+        { env with rets = Option.map pre env.rets
+                 ; labs = V.Env.map pre env.labs
+                 ; throws = Option.map pre env.throws } in
+    let k' v1 = interpret_catches env cases exp.at v1 k in
+    interpret_exp { env with throws = Some k' } exp1 k
   | WhileE (exp1, exp2) ->
     let k_continue = fun v -> V.as_unit v; interpret_exp env exp k in
     interpret_exp env exp1 (fun v1 ->

src/viper/traversals.ml

@@ -51,7 +51,7 @@ let rec over_exp (v : visitor) (exp : exp) : exp =
   | ObjBlockE (x, t, dfs) -> { exp with it = ObjBlockE (x, Option.map (over_typ v) t, List.map (over_dec_field v) dfs) }
   | ObjE (bases, efs) -> { exp with it = ObjE (List.map (over_exp v) bases, List.map (over_exp_field v) efs) }
   | IfE (exp1, exp2, exp3) -> { exp with it = IfE(over_exp v exp1, over_exp v exp2, over_exp v exp3) }
-  | TryE (exp1, cases) -> { exp with it = TryE (over_exp v exp1, List.map (over_case v) cases) }
+  | TryE (exp1, cases, exp2) -> { exp with it = TryE (over_exp v exp1, List.map (over_case v) cases, Option.map (over_exp v) exp2) }
   | SwitchE (exp1, cases) -> { exp with it = SwitchE (over_exp v exp1, List.map (over_case v) cases) }
   | FuncE (name, sort_pat, typ_binds, pat, typ_opt, sugar, exp1) -> { exp with it = FuncE (name, sort_pat, typ_binds, over_pat v pat, Option.map (over_typ v) typ_opt, sugar, over_exp v exp1) }
   | IgnoreE exp1 -> { exp with it = IgnoreE (over_exp v exp1)})

test/fail/ok/try-finally.tc.ok

@@ -1,5 +1,6 @@
-try-finally.mo:10.17-10.31: type error [M0200], a cleanup clause must not send messages
-try-finally.mo:16.17-16.39: type error [M0200], a cleanup clause must not send messages
+try-finally.mo:10.26-10.29: type error [M0047], send capability required, but not available
+ (need an enclosing async expression or function body)
+try-finally.mo:16.19-16.37: type error [M0039], misplaced throw
 try-finally.mo:22.19-22.21: type error [M0050], literal of type
   Nat
 does not have expected type

test/run-drun/ok/try-finally-bug.tc.ok

@@ -0,0 +1 @@
+try-finally-bug.mo:8.18-8.26: type error [M0037], misplaced async expression; try enclosing in an async function

test/run-drun/ok/try-finally-bug.tc.ret.ok

@@ -0,0 +1 @@
+Return code 1

test/run-drun/ok/try-finally.drun-run.ok

@@ -6,9 +6,31 @@ debug.print: INl
 debug.print: OUTl
 debug.print: INe
 debug.print: OUTe
+debug.print: BEFORE1
+debug.print: IN1
+debug.print: IN1Inner
+debug.print: OUT1Inner
+debug.print: CAUGHT1
+debug.print: OUT1
+debug.print: AFTER1
+debug.print: BEFORE1t
+debug.print: IN1t
+debug.print: IN1tInner
+debug.print: CAUGHT1tInner
+debug.print: OUT1tInner
+debug.print: CAUGHT1t
+debug.print: OUT1t
+debug.print: AFTER1t
 debug.print: IN2
 debug.print: CAUGHT2
 debug.print: OUT2
+debug.print: IN2r
+debug.print: CAUGHT2r
+debug.print: OUT2r
+debug.print: IN2b
+debug.print: CAUGHT2b
+debug.print: OUT2b
+debug.print: AFTER2b
 debug.print: IN2i
 debug.print: CAUGHT2i
 debug.print: OUT2i
@@ -76,7 +98,7 @@ debug.print: InnerLIVESTILL7
 debug.print: InnerOUT7
 debug.print: OUT7
 debug.print: It's over
-ingress Err: IC0503: Canister rwlgt-iiaaa-aaaaa-aaaaa-cai trapped explicitly: assertion failed at try-finally.mo:200.17-200.29
+ingress Err: IC0503: Canister rwlgt-iiaaa-aaaaa-aaaaa-cai trapped explicitly: assertion failed at try-finally.mo:238.17-238.29
 debug.print: go2
 debug.print: It's so over
-ingress Err: IC0503: Canister rwlgt-iiaaa-aaaaa-aaaaa-cai trapped explicitly: assertion failed at try-finally.mo:284.13-284.25
+ingress Err: IC0503: Canister rwlgt-iiaaa-aaaaa-aaaaa-cai trapped explicitly: assertion failed at try-finally.mo:325.13-325.25