motoko-san: support labels, breaks, and continues

src/viper/syntax.ml

@@ -86,7 +86,7 @@ and stmt' =
   | WhileS of exp * invariants * seqn
   | LabelS of id
   | GotoS of id
-  (* TODO: these are temporary helper terms  that should not appear in the final translation 
+  (* TODO: these are temporary helper terms  that should not appear in the final translation
        we should avoid introducing them in the first place if possible, so they can be removed *)
   | PreconditionS of exp
   | PostconditionS of exp
@@ -103,4 +103,3 @@ and typ' =
   | TupleT
   | OptionT of typ
   | ConT of id * typ list
-

src/viper/trans.ml

@@ -100,6 +100,8 @@ module Env = T.Env
 type ctxt =
   { self : string option;
     ids : (sort * T.t) T.Env.t;
+    label_vars : (string, id) Hashtbl.t; (* Orig label var -> associated tmp variable. *)
+    mapped_labels : (string, string) Hashtbl.t; (* Orig label var -> label var in viper. *)
     ghost_items : (ctxt -> item) list ref;
     ghost_inits : (ctxt -> seqn') list ref;
     ghost_perms : (ctxt -> Source.region -> exp) list ref;
@@ -171,14 +173,31 @@ let rec unit (u : M.comp_unit) : prog Diag.result =
     reset_stamps();
     try return (unit' u) with
     | Unsupported (at, desc) -> error at "0" "viper" ("translation to viper failed:\n"^desc)
-    | _ -> error u.it.M.body.at "1" "viper" "translation to viper failed"
+    | exn ->
+      error
+        u.it.M.body.at
+        "1"
+        "viper"
+        (Format.asprintf
+          "translation to viper failed. Reason: %s"
+          (Printexc.to_string exn))
   )
 
 and unit' (u : M.comp_unit) : prog =
   let { M.imports; M.body } = u.it in
   match body.it with
   | M.ActorU(id_opt, decs) ->
-    let ctxt = { self = None; ids = Env.empty; ghost_items = ref []; ghost_inits = ref []; ghost_perms = ref []; ghost_conc = ref [] } in
+    let ctxt =
+      { self = None
+      ; ids = Env.empty
+      ; label_vars = Hashtbl.create 32
+      ; mapped_labels = Hashtbl.create 32
+      ; ghost_items = ref []
+      ; ghost_inits = ref []
+      ; ghost_perms = ref []
+      ; ghost_conc = ref []
+      }
+    in
     let ctxt', perms, inits, mk_is = dec_fields ctxt decs in
     let is' = List.map (fun mk_i -> mk_i ctxt') mk_is in
     (* given is', compute ghost_is *)
@@ -444,6 +463,31 @@ and dec ctxt d =
   | _ ->
      unsupported d.at (Arrange.dec d)
 
+and compile_while
+  ctxt
+  ?(label_id : M.id option)
+  ~(at : region)
+  ~(pred : M.exp)
+  ~(body : M.exp)
+  () : seqn =
+  let (!!) p = !!! at p in
+  let (invs, body) = extract_loop_invariants body in
+  let invs = List.map (exp ctxt) invs in
+  let invs = invs @ local_access_preds ctxt in
+  let invs = invs @ [!!(AndE(!!(CallE("$Perm", [self ctxt at])),
+                             !!(CallE("$Inv",  [self ctxt at]))))] in
+  let pred = exp ctxt pred in
+  let body =
+    match label_id with
+    | Some label_id ->
+      let label = loop_label ctxt label_id in
+      let stmts = stmt ctxt body in
+      let decls, stmts = stmts.it in
+      !!(decls, !!(LabelS label) :: stmts)
+    | None -> stmt ctxt body
+  in
+  !!([], [ !!(WhileS(pred, invs, body)) ])
+
 and stmt ctxt (s : M.exp) : seqn =
   let (!!) p = !!! (s.at) p in
   match s.it with
@@ -512,23 +556,18 @@ and stmt ctxt (s : M.exp) : seqn =
           !!(InhaleS (!!(AndE(!!(CallE("$Perm", [self ctxt at])),
                               !!(CallE("$Inv", [self ctxt at]))))));
         ])
-  | M.WhileE(e, s1) ->
-     let (invs, s1') = extract_loop_invariants s1 in
-     let invs' = List.map (fun inv -> exp ctxt inv) invs in
-     let invs'' = invs' @ local_access_preds ctxt in
-     let invs''' = invs'' @ [!!(AndE(!!(CallE("$Perm", [self ctxt s.at])),
-                                     !!(CallE("$Inv",  [self ctxt s.at]))))] in
-     !!([],
-        [ !!(WhileS(exp ctxt e, invs''', stmt ctxt s1')) ])
+  | M.WhileE(e, { it = M.LabelE (cont_label_id, _typ, s1); _}) ->
+      compile_while ~label_id:cont_label_id ~at:s.at ~pred:e ~body:s1 ctxt ()
+  | M.WhileE(e, s1) -> compile_while ~at:s.at ~pred:e ~body:s1 ctxt ()
   | M.(SwitchE(scrut, cs)) ->
       !!(switch_stmts ctxt s.at scrut cs)
   | M.(AssignE({it = VarE x; _}, e2)) ->
-      let lval = (match fst (Env.find x.it ctxt.ids) with
-                 | Local -> LValueVar (!!! (x.at) (x.it))
-                 | Field -> LValueFld (self ctxt x.at, id x)
-                 | _ -> unsupported s.at (Arrange.exp s)
-                 ) in
-      !!(assign_stmts ctxt s.at lval e2)
+      let lval =
+        match fst (Env.find x.it ctxt.ids) with
+        | Local -> LValueVar (!!! (x.at) (x.it))
+        | Field -> LValueFld (self ctxt x.at, id x)
+        | _ -> unsupported s.at (Arrange.exp s)
+      in !!(assign_stmts ctxt s.at lval e2)
   | M.(AssignE({it = IdxE (e1, e2);_}, e3)) ->
       let lval = LValueFld (array_loc ctxt s.at e1 e2 e3.note.M.note_typ) in
       !!(assign_stmts ctxt s.at lval e3)
@@ -557,6 +596,28 @@ and stmt ctxt (s : M.exp) : seqn =
       let ds, stmts = assign_stmts ctxt s.at lval e in
       let stmt = !!(GotoS(!!! (Source.no_region) "$Ret")) in
       !!(ds, stmts @ [stmt])
+  | M.LabelE (label_id, typ, e) ->
+      let label = !!! Source.no_region (LabelS (loop_label ctxt label_id)) in
+      let stmts = stmt ctxt e in
+      let decls, stmts = stmts.it in
+      let stmts = stmts @ [ label ] in
+      !!(decls, stmts)
+  | M.BreakE (label_id, ret) ->
+    let stmts =
+      match Hashtbl.find_opt ctxt.label_vars label_id.it with
+      | None -> stmt ctxt ret
+      | Some x ->
+        let lvalue = LValueVar x in
+        let stmts = assign_stmts ctxt ret.at lvalue ret in
+        !!stmts
+    in
+    let decls, stmts = stmts.it in
+    let label_name =
+      match Hashtbl.find_opt ctxt.mapped_labels label_id.it with
+      | Some name -> name
+      | None -> failwith (Format.asprintf "can't find mapped name for label \"%s\"" label_id.it)
+    in
+    !!(decls, stmts @ [ !!(GotoS !!label_name) ])
   | _ ->
      unsupported s.at (Arrange.exp s)
 
@@ -644,6 +705,9 @@ and assign_stmts ctxt at (lval : lvalue) (e : M.exp) : seqn' =
     via_tmp_var lval t (fun x ->
       let lhs = !!(LocalVar (x, tr_typ t)) in
       [], tuple_alloc at ctxt lhs (tuple_elem_ts t) es)
+  | M.{ it = LabelE (label_id, ret_typ, e); note; _ } ->
+    via_tmp_var lval t (fun x ->
+      label_alloc ~label_id ~label_type:ret_typ ~label_rhs:e ~label_note:note at ctxt x)
   | _ ->
     [], [!!(assign_stmt lval (exp ctxt e))]
 
@@ -766,6 +830,22 @@ and rets t_opt =
 
 and id id = { it = id.it; at = id.at; note = NoInfo }
 
+(* Make sure that you call it before translating inner expressions.
+   This thing mutates [ctxt] environment and we want to update it first. *)
+and loop_label ctxt loop_label =
+  let label_name =
+    loop_label.it
+      |> String.map (fun ch ->
+          (* Life without Core is hard... *)
+          if Char.equal ch ' '
+          then '_'
+          else ch)
+      |> Format.asprintf "$%s"
+      |> fresh_id
+  in
+  Hashtbl.add ctxt.mapped_labels loop_label.it label_name;
+  id { loop_label with it = label_name }
+
 and tr_typ typ =
   { it = tr_typ' typ;
     at = Source.no_region;
@@ -859,3 +939,33 @@ and tuple_alloc at ctxt lhs ts es : stmt list =
 and tuple_prj ctxt at e1 e2 t =
   prjE at (exp ctxt e1) (exp ctxt e2) (typed_field t)
 
+and label_alloc ~label_id ~label_type ~label_rhs ~label_note at ctxt lhs : seqn' =
+  (match label_type.it with
+  | M.TupT [] -> ()
+  | _ -> Hashtbl.add ctxt.label_vars label_id.it lhs);
+
+  let wrap_break exp =
+    match label_type.it, exp.it with
+    | M.TupT [], _ | _, M.BreakE _ -> exp
+    | _ -> { exp with it = M.BreakE (label_id, exp) }
+  in
+  let label_rhs =
+    match label_rhs.it with
+    | M.BlockE decs ->
+      let rec map_last ~f = function
+        | [] -> []
+        | [ x ] -> [ f x ]
+        | x :: xs -> x :: map_last ~f xs
+      in
+      let decs = map_last decs ~f:(fun dec ->
+        match dec.it with
+        | M.ExpD exp ->
+          let exp = wrap_break exp in
+          { dec with it = M.ExpD exp }
+        | _ -> dec) in
+      { label_rhs with it = M.BlockE decs }
+    | _ -> wrap_break label_rhs
+  in
+  let label = M.{ it = LabelE (label_id, label_type, label_rhs); at; note = label_note } in
+  let label_tr = stmt ctxt label in
+  label_tr.it

test/viper/label-break-continue.mo

@@ -0,0 +1,70 @@
+// @verify
+
+actor LabelBreakContinue {
+  func label_expressions() {
+    let simple_label = label simple : Int break simple(42);
+    assert simple_label == 42;
+
+    let implicit_leave = label implicit : Int 42;
+    assert implicit_leave == 42;
+
+    let block_label_early_expr = label block : (Int, Int) {
+      if (true) break block(42, 42);
+      (24, 24)
+    };
+    assert block_label_early_expr.0 == 42 and block_label_early_expr.1 == 42;
+
+    let block_label_expr = label block : (Int, Int) {
+      if (false) break block(42, 42);
+      (24, 24)
+    };
+    assert block_label_expr.0 == 24 and block_label_expr.1 == 24;
+
+    var v = 0;
+    let mut_label = label mutability : () {
+      if (true) break mutability(v := 42);
+      v := 100;
+    };
+    assert v == 42;
+
+    v := 0;
+    let mut_label_2 = label mutability : () {
+      if (false) break mutability(v := 42);
+      v := 100;
+    };
+    assert v == 100;
+  };
+
+  func loops() {
+    var i = 0;
+    label while_loop while (i < 5) {
+      assert:loop:invariant (i < 3);
+      i := i + 1;
+      if (i == 3) break while_loop;
+      continue while_loop;
+      i := 100
+    };
+
+    // TODO: uncomment this when for loops are supported.
+    /* let range = [0, 1, 2, 3, 4, 5];
+
+    i := 0;
+    label for_loop for(j in range.vals()) {
+      assert:loop:invariant (j == i);
+      assert:loop:invariant (j < 3);
+      i := i + 1;
+      if (j == 3) break for_loop;
+      continue for_loop;
+      i := 100;
+    }; */
+
+    // TODO: uncomment this when loops are supported.
+    /* i := 0;
+    label regular_loop loop {
+      assert:loop:invariant (i < 5);
+      i := i + 1;
+      if (i == 4) break regular_loop;
+      i := 100;
+    }; */
+  }
+}

test/viper/ok/label-break-continue.silicon.ok

@@ -0,0 +1,2 @@
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (label-break-continue.vpr@37.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (label-break-continue.vpr@38.1)

test/viper/ok/label-break-continue.tc.ok

@@ -0,0 +1,4 @@
+label-break-continue.mo:4.8-4.25: warning [M0194], unused identifier label_expressions (delete or rename to wildcard `_` or `_label_expressions`)
+label-break-continue.mo:24.9-24.18: warning [M0194], unused identifier mut_label (delete or rename to wildcard `_` or `_mut_label`)
+label-break-continue.mo:31.9-31.20: warning [M0194], unused identifier mut_label_2 (delete or rename to wildcard `_` or `_mut_label_2`)
+label-break-continue.mo:38.8-38.13: warning [M0194], unused identifier loops (delete or rename to wildcard `_` or `_loops`)