From ae07bc15ff9218a33ee97f628ae2ea4a5db008e4 Mon Sep 17 00:00:00 2001 From: Leonid Vasilev Date: Tue, 25 Jun 2024 18:47:01 +0400 Subject: [PATCH] motoko-san: support immutable records --- src/viper/pretty.ml | 11 +- src/viper/syntax.ml | 2 +- src/viper/trans.ml | 97 +++++++- test/viper/ok/record.silicon.ok | 1 + test/viper/ok/record.tc.ok | 10 + test/viper/ok/record.vpr.ok | 147 ++++++++++++ test/viper/ok/record.vpr.stderr.ok | 10 + test/viper/ok/todo_record.vpr.ok | 350 +++++++++++++++++++++++++++++ test/viper/record.mo | 70 ++++++ test/viper/todo_record.mo | 213 ++++++++++++++++++ 10 files changed, 899 insertions(+), 12 deletions(-) create mode 100644 test/viper/ok/record.silicon.ok create mode 100644 test/viper/ok/record.tc.ok create mode 100644 test/viper/ok/record.vpr.ok create mode 100644 test/viper/ok/record.vpr.stderr.ok create mode 100644 test/viper/ok/todo_record.vpr.ok create mode 100644 test/viper/record.mo create mode 100644 test/viper/todo_record.mo diff --git a/src/viper/pretty.ml b/src/viper/pretty.ml index 33521fee5ac..f4c0d1164a6 100644 --- a/src/viper/pretty.ml +++ b/src/viper/pretty.ml @@ -62,13 +62,12 @@ and pp_adt_cons ppf cons = and pp_adt_con ppf con = fprintf ppf "%s@[(%a)@]" con.con_name.it - (pp_print_list ~pp_sep:comma pp_adt_con_field) (List.mapi (fun i fld -> con, i, fld) con.con_fields) + (pp_print_list ~pp_sep:comma pp_adt_con_field) con.con_fields -and pp_adt_con_field ppf (con, i, con_field) = - fprintf ppf "%s$%s : %a" - con.con_name.it - (string_of_int i) - pp_typ con_field +and pp_adt_con_field ppf (field_name, field_type) = + fprintf ppf "%s : %a" + field_name.it + pp_typ field_type and pp_block_opt ppf = function | None -> () diff --git a/src/viper/syntax.ml b/src/viper/syntax.ml index 092a8c69c2e..cb1ffb87b4f 100644 --- a/src/viper/syntax.ml +++ b/src/viper/syntax.ml @@ -16,7 +16,7 @@ and item' = | MethodI of id * par list * par list * exp list * exp list * seqn option | InvariantI of string * exp -and adt_con = { con_name : id; con_fields : typ list } +and adt_con = { con_name : id; con_fields : (id * typ) list } and par = id * typ diff --git a/src/viper/trans.ml b/src/viper/trans.ml index d43170a869b..5fa93669598 100644 --- a/src/viper/trans.ml +++ b/src/viper/trans.ml @@ -10,6 +10,8 @@ module Arrange = Mo_def.Arrange module String_map = Env.Make(String) module Stamps = String_map +module Type_map = Env.Make (T.Ord) + (* symbol generation *) let stamps : int Stamps.t ref = ref Stamps.empty @@ -107,6 +109,7 @@ type ctxt = label_to_tmp_var : id String_map.t; (* Motoko label -> associated tmp variable *) label_to_vpr_label : string String_map.t; (* Motoko label -> Viper label *) reqs : reqs; (* requirements for the prelude *) + type_to_record_ctor : id Type_map.t; ghost_items : (ctxt -> item) list ref; ghost_inits : (ctxt -> seqn') list ref; ghost_perms : (ctxt -> Source.region -> exp) list ref; @@ -192,6 +195,25 @@ let rec strip_mut_t (t : T.typ) : T.typ = | T.Mut t' -> strip_mut_t t' | _ -> t +let record_ctor_tag = "$RecordCtor_" + +let mk_record_ctor (typ_id : M.typ_id) : id = + let name = Format.asprintf "%s%s" record_ctor_tag typ_id.it in + !!! Source.no_region name + +let get_record_name ctxt (typ : T.typ) : string = + let tag_len = String.length record_ctor_tag in + let record_ctor_name = (Type_map.find typ ctxt.type_to_record_ctor).it in + String.sub record_ctor_name tag_len (String.length record_ctor_name - tag_len) + +let mk_record_field ~record_name ~fld_name = + Format.asprintf "$%s$%s" record_name fld_name + +let get_record_field ctxt (typ : T.typ) (fld : M.id) : M.id = + let record_name = get_record_name ctxt typ in + let fld_name = mk_record_field ~record_name ~fld_name:fld.it in + { fld with it = fld_name } + let rec unit reqs (u : M.comp_unit) : prog Diag.result = Diag.( reset_stamps(); @@ -218,6 +240,7 @@ and unit' reqs (u : M.comp_unit) : prog = label_to_tmp_var = String_map.empty; label_to_vpr_label = String_map.empty; reqs = reqs; + type_to_record_ctor = Type_map.empty; ghost_items = ref []; ghost_inits = ref []; ghost_perms = ref []; @@ -333,16 +356,39 @@ and dec_field' ctxt d = ctxt, None, None, fun ctxt -> let adt_param tb = id tb.it.M.var in let adt_con con = begin - { con_name = !!! Source.no_region con.T.lab; + let con_name = !!! Source.no_region con.T.lab in + let mk_field_name i = !!! Source.no_region (Format.asprintf "%s$%i" con.T.lab i) in + { con_name; con_fields = match con.T.typ with - | T.Tup ts -> List.map (tr_typ ctxt) ts - | t -> [tr_typ ctxt t] + | T.Tup ts -> List.mapi (fun i t -> mk_field_name i, tr_typ ctxt t) ts + | t -> [mk_field_name 0, tr_typ ctxt t] } end in AdtI ({ typ_id with note = NoInfo }, List.map adt_param typ_binds, List.map adt_con cons), NoInfo + | M.(TypD (typ_id, typ_binds, { note = T.Obj (T.Object, flds) as typ; _ })) -> + let con_name = mk_record_ctor typ_id in + { ctxt with type_to_record_ctor = Type_map.add typ con_name ctxt.type_to_record_ctor }, + None, + None, + fun ctxt -> + let adt_param tb = id tb.it.M.var in + let adt_field field = + let field_name = !!! Source.no_region (mk_record_field ~record_name:typ_id.it ~fld_name:field.T.lab) in + let field_typ = tr_typ ctxt field.T.typ in + field_name, field_typ + in + let adt_con = + { con_name; + con_fields = List.map adt_field flds + } + in + AdtI ({ typ_id with note = NoInfo }, + List.map adt_param typ_binds, + [ adt_con ]), + NoInfo (* async functions *) | M.(LetD ({it=VarP f;note;_}, {it=FuncE(x, sp, tp, p, t_opt, sugar, @@ -504,7 +550,7 @@ and compile_while let (!!) p = !!! at p in let (invs, body) = extract_loop_invariants body in let invs = (* TODO: automatic adding invariant into loop require more pondering*) - (* [!!(AndE(!!(CallE("$Perm", [self ctxt at])), *) + (* [!!(AndE(!!(CallE("$Perm", [self ctxt at])), *) (* !!(CallE("$Inv", [self ctxt at]))))] *) [!!(CallE("$Perm", [self ctxt at]))] @ local_access_preds ctxt @@ -720,6 +766,22 @@ and pat_match ctxt (scrut : M.exp) (p : M.pat) : exp list * (id * T.typ) list * end in let stmts = List.mapi (fun i (x, t) -> fld_assign_stmt i (LValueUninitVar x)) p_scope in [cond], p_scope, (ds, stmts) + | M.ObjP pat_fields -> + let e_scrut = exp ctxt scrut in + let p_scope = List.map (fun M.{ it = { id = _; pat }; _ } -> unwrap_var_pat pat) pat_fields in + let ds = List.map (fun (x, t) -> !!(x, tr_typ ctxt t)) p_scope in + let fld_assign_stmt lval fld_name = + let rhs = !!(FldAcc (e_scrut, id fld_name)) in + !!(assign_stmt lval rhs) + in + let stmts = + List.map2 + (fun M.{ it = { id = fld_name; pat = _ }; _ } (x, _) -> + let fld_name = get_record_field ctxt (T.normalize p.note) fld_name in + fld_assign_stmt (LValueUninitVar x) fld_name) + pat_fields p_scope + in + [], p_scope, (ds, stmts) | M.WildP -> [], [], ([], []) | _ -> unsupported p.at (Arrange.pat p) @@ -874,6 +936,27 @@ and exp ctxt e = !!(match e.it with | M.TupE es -> CallE (tag.it, List.map (exp ctxt) es) | _ -> CallE (tag.it, [exp ctxt e])) + | M.ObjE ([], flds) -> + (match T.normalize e.note.M.note_typ with + | T.Obj (T.Object, typ_flds) as t -> + let record_ctor_name = Type_map.find t ctxt.type_to_record_ctor in + let flds = List.map (fun M.{ it = { mut; id; exp }; _} -> + match mut.it with + | M.Const -> id.it, exp + | M.Var -> unsupported mut.at (Arrange.exp e)) flds + in + let args = List.map (fun T.{ lab; _ } -> + let rhs_exp = List.assoc lab flds in + exp ctxt rhs_exp) typ_flds + in + !!(CallE (record_ctor_name.it, args)) + | T.Obj _ -> unsupported e.at (Arrange.exp e) + | _ -> assert false) + | M.DotE (proj, fld) when Type_map.mem (T.normalize proj.note.M.note_typ) ctxt.type_to_record_ctor -> + let proj_t = T.normalize proj.note.M.note_typ in + let proj = exp ctxt proj in + let fld = id (get_record_field ctxt proj_t fld) in + !!(FldAcc (proj, fld)) | M.TupE es -> let n = List.length es in ctxt.reqs.tuple_arities := IntSet.add n !(ctxt.reqs.tuple_arities); @@ -949,7 +1032,8 @@ and tr_typ ctxt typ = at = Source.no_region; note = NoInfo } and tr_typ' ctxt typ = - match typ, T.normalize typ with + let norm_typ = T.normalize typ in + match typ, norm_typ with | _, T.Prim T.Int -> IntT | _, T.Prim T.Nat -> IntT (* Viper has no native support for Nat, so translate to Int *) | _, T.Prim T.Text -> IntT (* Viper has no native support for Text, so translate to uninterpreted Int values *) @@ -959,6 +1043,9 @@ and tr_typ' ctxt typ = | _, T.Tup ts -> ctxt.reqs.tuple_arities := IntSet.add (List.length ts) !(ctxt.reqs.tuple_arities); TupleT (List.map (tr_typ ctxt) ts) + | _, T.Obj (T.Object, flds) -> + let record_name = get_record_name ctxt norm_typ in + ConT (!!! Source.no_region record_name, []) | T.Con (con, ts), _ -> ConT (!!! Source.no_region (Mo_types.Cons.name con), List.map (tr_typ ctxt) ts) | _, t -> unsupported Source.no_region (Mo_types.Arrange_type.typ t) diff --git a/test/viper/ok/record.silicon.ok b/test/viper/ok/record.silicon.ok new file mode 100644 index 00000000000..ae35bfb69dd --- /dev/null +++ b/test/viper/ok/record.silicon.ok @@ -0,0 +1 @@ +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (record.vpr@29.1) diff --git a/test/viper/ok/record.tc.ok b/test/viper/ok/record.tc.ok new file mode 100644 index 00000000000..6646418363d --- /dev/null +++ b/test/viper/ok/record.tc.ok @@ -0,0 +1,10 @@ +record.mo:7.7-7.11: warning [M0194], unused identifier fld1 (delete or rename to wildcard `_` or `_fld1`) +record.mo:8.7-8.11: warning [M0194], unused identifier fld2 (delete or rename to wildcard `_` or `_fld2`) +record.mo:12.7-12.9: warning [M0194], unused identifier aa (delete or rename to wildcard `_` or `_aa`) +record.mo:14.8-14.20: warning [M0194], unused identifier array_record (delete or rename to wildcard `_` or `_array_record`) +record.mo:22.8-22.20: warning [M0194], unused identifier tuple_record (delete or rename to wildcard `_` or `_tuple_record`) +record.mo:33.8-33.19: warning [M0194], unused identifier call_record (delete or rename to wildcard `_` or `_call_record`) +record.mo:44.8-44.19: warning [M0194], unused identifier pass_record (delete or rename to wildcard `_` or `_pass_record`) +record.mo:49.8-49.23: warning [M0194], unused identifier match_on_record (delete or rename to wildcard `_` or `_match_on_record`) +record.mo:55.13-55.14: warning [M0194], unused identifier c (delete or rename to wildcard `_` or `_c`) +record.mo:61.8-61.35: warning [M0194], unused identifier record_types_are_structural (delete or rename to wildcard `_` or `_record_types_are_structural`) diff --git a/test/viper/ok/record.vpr.ok b/test/viper/ok/record.vpr.ok new file mode 100644 index 00000000000..614364b9116 --- /dev/null +++ b/test/viper/ok/record.vpr.ok @@ -0,0 +1,147 @@ +/* BEGIN PRELUDE */ +/* Array encoding */ +domain Array { + function $loc(a: Array, i: Int): Ref + function $size(a: Array): Int + function $loc_inv1(r: Ref): Array + function $loc_inv2(r: Ref): Int + axiom $all_diff_array { forall a: Array, i: Int :: {$loc(a, i)} $loc_inv1($loc(a, i)) == a && $loc_inv2($loc(a, i)) == i } + axiom $size_nonneg { forall a: Array :: $size(a) >= 0 } +} +define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) +define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x +/* Tuple encoding */ +adt Tuple$2 [T0, T1] { Tup$2(tup$2$0 : T0, tup$2$1 : T1) } +/* Option encoding */ +adt Option[T] { + None() + Some(some$0: T) +} +/* Text encoding */ +function $concat(a: Int, b: Int): Int +/* Typed references */ +field $c_R1: R1 +/* END PRELUDE */ + +define $Perm($Self) (((((true && acc(($Self).fld1,write)) && acc(($Self).fld2,write)) && + acc(($Self).empty,write)) && acc(($Self).aa,write))) +define $Inv($Self) (true) +method __init__($Self: Ref) + + requires $Perm($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + ($Self).fld1 := $RecordCtor_R1(42, 3); + ($Self).fld2 := $RecordCtor_R1(42, 3); + ($Self).empty := $RecordCtor_R1(0, 4); + ($Self).aa := 42; + } +adt R { $RecordCtor_R($R$aa : Int, $R$b : Int) } +adt R1 { $RecordCtor_R1($R1$aa : Int, $R1$b : Int) } +field fld1: R1 +field fld2: R1 +field empty: R1 +field aa: Int +method array_record($Self: Ref) + + requires $Perm($Self) + ensures $Perm($Self) + { var arr: Array + inhale $array_acc(arr, $c_R1, write); + inhale ($size(arr) == 2); + ($loc(arr, 0)).$c_R1 := ($Self).empty; + ($loc(arr, 1)).$c_R1 := ($Self).empty; + ($loc(arr, 0)).$c_R1 := $RecordCtor_R1(100, 0); + ($loc(arr, 1)).$c_R1 := $RecordCtor_R1(200, 1); + assert ((($loc(arr, 0)).$c_R1 == $RecordCtor_R1(100, 0)) && (( + $loc(arr, + 1)).$c_R1 == + $RecordCtor_R1(200, 1))); + label $Ret; + } +method tuple_record($Self: Ref) + + requires $Perm($Self) + ensures $Perm($Self) + { var tup: Tuple$2[R1, R1] + tup := Tup$2($RecordCtor_R1(100, 0), $RecordCtor_R1(200, 1)); + assert (((tup).tup$2$0 == $RecordCtor_R1(100, 0)) && ((tup).tup$2$1 == + $RecordCtor_R1(200, 1))); + label $Ret; + } +method get_record($Self: Ref) + returns ($Res: R1) + requires $Perm($Self) + ensures $Perm($Self) + ensures ($Res == $RecordCtor_R1(100, 0)) + { + $Res := $RecordCtor_R1(100, 0); + goto $Ret; + label $Ret; + } +method call_record($Self: Ref) + + requires $Perm($Self) + ensures $Perm($Self) + { var res: R1 + res := get_record($Self); + assert ((res).$R1$b == 0); + label $Ret; + } +method record_arg($Self: Ref, r: R1) + returns ($Res: R1) + requires $Perm($Self) + requires ((r).$R1$aa == 100) + ensures $Perm($Self) + ensures (($Res).$R1$aa == 100) + { + $Res := $RecordCtor_R1(100, 0); + goto $Ret; + label $Ret; + } +method pass_record($Self: Ref) + + requires $Perm($Self) + ensures $Perm($Self) + { var res: R1 + res := record_arg($Self, $RecordCtor_R1(100, 2)); + assert ((res).$R1$aa == 100); + label $Ret; + } +method match_on_record($Self: Ref) + returns ($Res: Int) + requires $Perm($Self) + ensures $Perm($Self) + ensures ($Res == 42) + { var r: R1 + r := get_record($Self); + if (true) + { var number: Int + var b: Int + var c: Int + number := (r).$R1$aa; + b := (r).$R1$b; + c := b; + $Res := (number - 58); + goto $Ret; + }; + label $Ret; + } +method record_types_are_structural($Self: Ref) + + requires $Perm($Self) + ensures $Perm($Self) + { var r: R1 + var r1: R1 + r := $RecordCtor_R1(100, 0); + r1 := $RecordCtor_R1(100, 0); + assert (r == r1); + label $Ret; + } +adt RecursiveRecord1 + { $RecordCtor_RecursiveRecord1($RecursiveRecord1$x : Option[RecursiveRecord1], + $RecursiveRecord1$y : Option[RecursiveRecord2]) } +adt RecursiveRecord2 + { $RecordCtor_RecursiveRecord2($RecursiveRecord2$x : Option[RecursiveRecord1]) } diff --git a/test/viper/ok/record.vpr.stderr.ok b/test/viper/ok/record.vpr.stderr.ok new file mode 100644 index 00000000000..6646418363d --- /dev/null +++ b/test/viper/ok/record.vpr.stderr.ok @@ -0,0 +1,10 @@ +record.mo:7.7-7.11: warning [M0194], unused identifier fld1 (delete or rename to wildcard `_` or `_fld1`) +record.mo:8.7-8.11: warning [M0194], unused identifier fld2 (delete or rename to wildcard `_` or `_fld2`) +record.mo:12.7-12.9: warning [M0194], unused identifier aa (delete or rename to wildcard `_` or `_aa`) +record.mo:14.8-14.20: warning [M0194], unused identifier array_record (delete or rename to wildcard `_` or `_array_record`) +record.mo:22.8-22.20: warning [M0194], unused identifier tuple_record (delete or rename to wildcard `_` or `_tuple_record`) +record.mo:33.8-33.19: warning [M0194], unused identifier call_record (delete or rename to wildcard `_` or `_call_record`) +record.mo:44.8-44.19: warning [M0194], unused identifier pass_record (delete or rename to wildcard `_` or `_pass_record`) +record.mo:49.8-49.23: warning [M0194], unused identifier match_on_record (delete or rename to wildcard `_` or `_match_on_record`) +record.mo:55.13-55.14: warning [M0194], unused identifier c (delete or rename to wildcard `_` or `_c`) +record.mo:61.8-61.35: warning [M0194], unused identifier record_types_are_structural (delete or rename to wildcard `_` or `_record_types_are_structural`) diff --git a/test/viper/ok/todo_record.vpr.ok b/test/viper/ok/todo_record.vpr.ok new file mode 100644 index 00000000000..87875a04ad2 --- /dev/null +++ b/test/viper/ok/todo_record.vpr.ok @@ -0,0 +1,350 @@ +/* BEGIN PRELUDE */ +/* Array encoding */ +domain Array { + function $loc(a: Array, i: Int): Ref + function $size(a: Array): Int + function $loc_inv1(r: Ref): Array + function $loc_inv2(r: Ref): Int + axiom $all_diff_array { forall a: Array, i: Int :: {$loc(a, i)} $loc_inv1($loc(a, i)) == a && $loc_inv2($loc(a, i)) == i } + axiom $size_nonneg { forall a: Array :: $size(a) >= 0 } +} +define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) +define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x +/* Tuple encoding */ +/* Option encoding */ +adt Option[T] { + None() + Some(some$0: T) +} +/* Text encoding */ +function $concat(a: Int, b: Int): Int +/* Typed references */ +field $c_ToDo: ToDo +/* END PRELUDE */ + +define $Perm($Self) ((((true && (acc(($Self).todos,write) && $array_acc( + ($Self).todos, + $c_ToDo, write))) && + acc(($Self).num,write)) && acc(($Self).nextId,write))) +define $Inv($Self) (invariant_14($Self)) +method __init__($Self: Ref) + + requires $Perm($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { var $t_todos: Array + inhale $array_acc($t_todos, $c_ToDo, write); + inhale ($size($t_todos) == 0); + ($Self).todos := $t_todos; + ($Self).num := 0; + ($Self).nextId := 1; + } +adt ToDo + { $RecordCtor_ToDo($ToDo$completed : State, $ToDo$desc : Int, + $ToDo$id : Int) } +adt State { DONE() + TODO() } +field todos: Array +field num: Int +field nextId: Int +define invariant_14($Self) (((0 <= ($Self).num) && (($Self).num <= $size( + ($Self).todos)))) +method resize($Self: Ref, n: Int) + + requires $Perm($Self) + requires ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos))) + ensures $Perm($Self) + ensures ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos))) + ensures ((($Self).num == old(($Self).num)) && (($Self).nextId == + old(($Self).nextId))) + ensures ($size(($Self).todos) >= n) + ensures (old($size(($Self).todos)) <= $size(($Self).todos)) + ensures (forall i : Int :: (((0 <= i) && (i < old($size(($Self).todos)))) ==> ( + ($loc(($Self).todos, i)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo)))) + { var new_array: Array + var i: Int + if ((n <= $size(($Self).todos))) + { + goto $Ret; + }; + assert (n >= 0); + inhale $array_acc(new_array, $c_ToDo, write); + inhale ($size(new_array) == n); + inhale $array_init(new_array, $c_ToDo, $RecordCtor_ToDo(TODO(), 0, 0)); + i := 0; + while ((i < $size(($Self).todos))) + invariant $Perm($Self) + invariant $array_acc(new_array, $c_ToDo, write) + invariant ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos))) + invariant ((($Self).num == old(($Self).num)) && (($Self).nextId == + old(($Self).nextId))) + invariant ((0 <= i) && (i <= $size(($Self).todos))) + invariant ($size(($Self).todos) < $size(new_array)) + invariant ($size(($Self).todos) == old($size(($Self).todos))) + invariant (forall ii : Int :: (((0 <= ii) && (ii < old($size( + ($Self).todos)))) ==> ( + ($loc(($Self).todos, ii)).$c_ToDo == old(($loc(($Self).todos, + ii)).$c_ToDo)))) + invariant (forall ii : Int :: (((0 <= ii) && (ii < i)) ==> ( + ($loc(($Self).todos, ii)).$c_ToDo == ($loc(new_array, ii)).$c_ToDo))) + { + ($loc(new_array, i)).$c_ToDo := ($loc(($Self).todos, i)).$c_ToDo; + i := (i + 1); + }; + ($Self).todos := new_array; + label $Ret; + } +method getTodos($Self: Ref) + returns ($Res: Array) + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures $array_acc($Res, $c_ToDo, wildcard) + ensures ((($Self).num == old(($Self).num)) && (($Self).nextId == + old(($Self).nextId))) + ensures ($size(($Self).todos) == old($size(($Self).todos))) + ensures (forall i : Int :: (((0 <= i) && (i < old($size(($Self).todos)))) ==> ( + ($loc(($Self).todos, i)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo)))) + ensures $Inv($Self) + { var new_array: Array + inhale $array_acc(new_array, $c_ToDo, write); + inhale ($size(new_array) == 1); + ($loc(new_array, 0)).$c_ToDo := $RecordCtor_ToDo(TODO(), 0, 0); + exhale $array_acc(new_array, $c_ToDo, wildcard); + inhale $array_acc(new_array, $c_ToDo, wildcard); + $Res := new_array; + goto $Ret; + label $Ret; + } +method getTodo($Self: Ref, id: Int) + returns ($Res: Option[ToDo]) + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures ((($Self).num == old(($Self).num)) && (($Self).nextId == + old(($Self).nextId))) + ensures ($size(($Self).todos) == old($size(($Self).todos))) + ensures (forall i : Int :: (((0 <= i) && (i < old($size(($Self).todos)))) ==> ( + ($loc(($Self).todos, i)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo)))) + ensures ((exists i : Int :: (((0 <= i) && (i < ($Self).num)) && ( + (($loc(($Self).todos, i)).$c_ToDo).$ToDo$id == id))) ==> true) + ensures $Inv($Self) + { var i: Int + var res: Option[ToDo] + i := 0; + res := None(); + while ((i < ($Self).num)) + invariant $Perm($Self) + invariant ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos))) + invariant ((($Self).num == old(($Self).num)) && (($Self).nextId == + old(($Self).nextId))) + invariant ($size(($Self).todos) == old($size(($Self).todos))) + invariant (forall ii : Int :: (((0 <= ii) && (ii < old($size( + ($Self).todos)))) ==> ( + ($loc(($Self).todos, ii)).$c_ToDo == old(($loc(($Self).todos, + ii)).$c_ToDo)))) + invariant ((0 <= i) && (i <= ($Self).num)) + { + label $lbl$continue$l; + if (((($loc(($Self).todos, i)).$c_ToDo).$ToDo$id == id)) + { + res := Some(($loc(($Self).todos, i)).$c_ToDo); + goto $lbl$l; + }; + }; + label $lbl$l; + $Res := res; + goto $Ret; + label $Ret; + } +method addTodo($Self: Ref, description: Int) + returns ($Res: Int) + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos))) + ensures (($Self).num == (old(($Self).num) + 1)) + ensures (($Self).nextId == (old(($Self).nextId) + 1)) + ensures ($Res == old(($Self).nextId)) + ensures (($loc(($Self).todos, (($Self).num - 1))).$c_ToDo == $RecordCtor_ToDo( + TODO(), + description, + $Res)) + ensures (forall i : Int :: (((0 <= i) && ((i + 1) < ($Self).num)) ==> ( + ($loc(($Self).todos, i)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo)))) + ensures $Inv($Self) + { var id: Int + id := ($Self).nextId; + if ((($Self).num >= $size(($Self).todos))) + { + resize($Self, ((($Self).num * 2) + 1)); + }; + ($loc(($Self).todos, ($Self).num)).$c_ToDo := $RecordCtor_ToDo( + TODO(), description, id); + ($Self).num := (($Self).num + 1); + ($Self).nextId := (($Self).nextId + 1); + $Res := id; + goto $Ret; + label $Ret; + } +method completeTodo($Self: Ref, id: Int) + + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures ((($Self).num == old(($Self).num)) && (($Self).nextId == + old(($Self).nextId))) + ensures ($size(($Self).todos) == old($size(($Self).todos))) + ensures (forall i : Int :: ((((0 <= i) && (i < ($Self).num)) && ( + (($loc(($Self).todos, i)).$c_ToDo).$ToDo$id != id)) ==> ( + ($loc(($Self).todos, i)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo)))) + ensures (forall i : Int :: ((((0 <= i) && (i < ($Self).num)) && ( + (($loc(($Self).todos, i)).$c_ToDo).$ToDo$id == id)) ==> ( + (($loc(($Self).todos, i)).$c_ToDo).$ToDo$completed == DONE()))) + ensures $Inv($Self) + { var i: Int + i := 0; + while ((i < ($Self).num)) + invariant $Perm($Self) + invariant ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos))) + invariant ((0 <= i) && (i <= $size(($Self).todos))) + invariant ((($Self).num == old(($Self).num)) && (($Self).nextId == + old(($Self).nextId))) + invariant ($size(($Self).todos) == old($size(($Self).todos))) + invariant (forall ii : Int :: (((i <= ii) && (ii < $size(($Self).todos))) ==> ( + ($loc(($Self).todos, ii)).$c_ToDo == old(($loc(($Self).todos, + ii)).$c_ToDo)))) + invariant (forall ii : Int :: ((((0 <= ii) && (ii < i)) && ( + (($loc(($Self).todos, ii)).$c_ToDo).$ToDo$id != id)) ==> ( + ($loc(($Self).todos, ii)).$c_ToDo == old(($loc(($Self).todos, + ii)).$c_ToDo)))) + invariant (forall ii : Int :: ((((0 <= ii) && (ii < i)) && ( + (($loc(($Self).todos, ii)).$c_ToDo).$ToDo$id == id)) ==> ( + (($loc(($Self).todos, ii)).$c_ToDo).$ToDo$completed == + DONE()))) + { + if (true) + { var taskId: Int + var taskDesc: Int + var _completed: State + taskId := (($loc(($Self).todos, i)).$c_ToDo).$ToDo$id; + taskDesc := (($loc(($Self).todos, i)).$c_ToDo).$ToDo$desc; + _completed := (($loc(($Self).todos, i)).$c_ToDo).$ToDo$completed; + if ((taskId == id)) + { + ($loc(($Self).todos, i)).$c_ToDo := $RecordCtor_ToDo( + DONE(), taskDesc, + taskId); + }; + i := (i + 1); + }; + }; + label $Ret; + } +method showTodos($Self: Ref) + returns ($Res: Int) + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures ((($Self).num == old(($Self).num)) && (($Self).nextId == + old(($Self).nextId))) + ensures ($size(($Self).todos) == old($size(($Self).todos))) + ensures (forall i : Int :: (((0 <= i) && (i < ($Self).num)) ==> ( + ($loc(($Self).todos, i)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo)))) + ensures $Inv($Self) + { var output: Int + var i: Int + output := 1; + i := 0; + while ((i < ($Self).num)) + invariant $Perm($Self) + invariant ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos))) + invariant ((($Self).num == old(($Self).num)) && (($Self).nextId == + old(($Self).nextId))) + invariant ($size(($Self).todos) == old($size(($Self).todos))) + invariant (forall ii : Int :: (((0 <= ii) && (ii < ($Self).num)) ==> ( + ($loc(($Self).todos, ii)).$c_ToDo == old(($loc(($Self).todos, + ii)).$c_ToDo)))) + { var todo: ToDo + todo := ($loc(($Self).todos, i)).$c_ToDo; + output := $concat($concat(output, 2), (todo).$ToDo$desc); + if (((todo).$ToDo$completed).isDONE) + { + output := $concat(output, 3); + }else + { + if (((todo).$ToDo$completed).isTODO) + { + output := $concat(output, 4); + }; + }; + }; + $Res := $concat(output, 2); + goto $Ret; + label $Ret; + } +method clearCompleted($Self: Ref) + + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures (($Self).num <= old(($Self).num)) + ensures (($Self).nextId == old(($Self).nextId)) + ensures ($size(($Self).todos) == old($size(($Self).todos))) + ensures (forall i : Int :: ((((0 <= i) && (i < old(($Self).num))) && ( + old((($loc(($Self).todos, i)).$c_ToDo).$ToDo$completed) == + TODO())) ==> (exists k : Int :: (((0 <= k) && (k < $size( + ($Self).todos))) && ( + ($loc(($Self).todos, k)).$c_ToDo == old(($loc( + ($Self).todos, + i)).$c_ToDo)))))) + ensures (forall i : Int :: (((0 <= i) && (i < ($Self).num)) ==> ( + (($loc(($Self).todos, i)).$c_ToDo).$ToDo$completed == TODO()))) + ensures $Inv($Self) + { var new_array: Array + var i: Int + var j: Int + assert ($size(($Self).todos) >= 0); + inhale $array_acc(new_array, $c_ToDo, write); + inhale ($size(new_array) == $size(($Self).todos)); + inhale $array_init(new_array, $c_ToDo, $RecordCtor_ToDo(TODO(), 0, 0)); + i := 0; + j := 0; + while ((i < ($Self).num)) + invariant $Perm($Self) + invariant $array_acc(new_array, $c_ToDo, write) + invariant ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos))) + invariant ((($Self).num == old(($Self).num)) && (($Self).nextId == + old(($Self).nextId))) + invariant ($size(($Self).todos) == old($size(($Self).todos))) + invariant (forall ii : Int :: (((0 <= ii) && (ii < old($size( + ($Self).todos)))) ==> ( + ($loc(($Self).todos, ii)).$c_ToDo == old(($loc(($Self).todos, + ii)).$c_ToDo)))) + invariant (($Self).num <= $size(new_array)) + invariant ((0 <= i) && (i <= ($Self).num)) + invariant (j <= i) + invariant ((0 <= j) && (j <= ($Self).num)) + invariant (forall ii : Int :: ((((0 <= ii) && (ii < i)) && ( + (($loc(($Self).todos, ii)).$c_ToDo).$ToDo$completed == + TODO())) ==> (exists k : Int :: (((0 <= k) && (k < j)) && ( + ($loc(new_array, k)).$c_ToDo == ($loc( + ($Self).todos, + ii)).$c_ToDo))))) + invariant (forall ii : Int :: (((0 <= ii) && (ii < j)) ==> ( + (($loc(new_array, ii)).$c_ToDo).$ToDo$completed == + TODO()))) + { + if (((($loc(($Self).todos, i)).$c_ToDo).$ToDo$completed == + TODO())) + { + ($loc(new_array, j)).$c_ToDo := ($loc(($Self).todos, i)).$c_ToDo; + j := (j + 1); + }; + i := (i + 1); + }; + ($Self).todos := new_array; + ($Self).num := j; + label $Ret; + } diff --git a/test/viper/record.mo b/test/viper/record.mo new file mode 100644 index 00000000000..d4d5f586f01 --- /dev/null +++ b/test/viper/record.mo @@ -0,0 +1,70 @@ +// @verify + +actor Record { + type R = { aa: Int; b: Text; }; + type R1 = { aa: Int; b: Text; }; + + let fld1: R = { aa = 42; b = "abacaba" }; + var fld2: R = { aa = 42; b = "abacaba" }; + + let empty: R = { aa = 0; b = "" }; + + let aa: Int = 42; // A field to check that "moc" handles disambiguation in record fields + + func array_record() { + let arr: [var R] = [var empty, empty]; + arr[0] := { aa = 100; b = "aaa" }; + arr[1] := { aa = 200; b = "bbb" }; + + assert:system arr[0] == { aa = 100; b = "aaa" } and arr[1] == { aa = 200; b = "bbb" }; + }; + + func tuple_record() { + let tup: (R, R) = ({ aa = 100; b = "aaa" }, { aa = 200; b = "bbb" }); + + assert:system tup.0 == { aa = 100; b = "aaa" } and tup.1 == { aa = 200; b = "bbb" }; + }; + + func get_record(): R { + assert:return (var:return) == { aa = 100; b = "aaa" }; + return { aa = 100; b = "aaa" }; + }; + + func call_record() { + let res = get_record(); + assert:system res.b == "aaa"; + }; + + func record_arg(r: R): R { + assert:func r.aa == 100; + assert:return (var:return).aa == 100; + return { aa = 100; b = "aaa" }; + }; + + func pass_record() { + let res = record_arg({ aa = 100; b = "42" }); + assert:system res.aa == 100; + }; + + func match_on_record(): Int { + assert:return (var:return) == 42; + + let r = get_record(); + switch r { + case { aa = number; b } { + let c = b; // Check that "b" in scope + return number - 58; + } + } + }; + + func record_types_are_structural() { + let r: R = { aa = 100; b = "aaa" }; + let r1: R1 = { aa = 100; b = "aaa" }; + + assert:system r == r1; + }; + + type RecursiveRecord1 = { x: ?RecursiveRecord1; y: ?RecursiveRecord2 }; + type RecursiveRecord2 = { x: ?RecursiveRecord1; }; +}; diff --git a/test/viper/todo_record.mo b/test/viper/todo_record.mo new file mode 100644 index 00000000000..26f4f6cff90 --- /dev/null +++ b/test/viper/todo_record.mo @@ -0,0 +1,213 @@ +// @verify + +import Prim "mo:⛔"; +import Array "mo:base/Array"; + +actor Assistant { + type ToDo = { id: Nat; desc: Text; completed: State }; + public type State = { #TODO; #DONE }; + + var todos : [var ToDo] = [var ]; + var num : Nat = 0; + var nextId : Nat = 1; + + assert:invariant 0 <= num and num <= todos.size(); + + private func resize(n: Nat) { + // Actor's invariant is preserved: + assert:func 0 <= num and num <= todos.size(); + assert:return 0 <= num and num <= todos.size(); + // unchanged fields: + assert:return num == (old(num)) and nextId == (old(nextId)); + // functional specification: + assert:return todos.size() >= n; + assert:return (old(todos.size())) <= todos.size(); + assert:return Prim.forall(func i = + (0 <= i and i < (old(todos.size())) implies todos[i] == (old(todos[i])))); + if (n <= todos.size()) + return; + let new_array = Array.init(n, { id = 0; desc = ""; completed = #TODO }); + var i: Nat = 0; + while (i < todos.size()) { + // actor invariant: + assert:loop:invariant 0 <= num and num <= todos.size(); + // unchanged fields: + assert:loop:invariant num == (old(num)) and nextId == (old(nextId)); + assert:loop:invariant 0 <= i and i <= todos.size(); + // functional specification: + assert:loop:invariant todos.size() < new_array.size(); + assert:loop:invariant todos.size() == (old(todos.size())); + assert:loop:invariant Prim.forall(func ii = + (0 <= ii and ii < (old(todos.size())) implies todos[ii] == (old(todos[ii])))); + assert:loop:invariant Prim.forall(func ii = + (0 <= ii and ii < i implies todos[ii] == new_array[ii])); + new_array[i] := todos[i]; + i += 1; + }; + todos := new_array; + }; + + public query func getTodos() : async [ToDo] { + assert:return num == (old(num)) and nextId == (old(nextId)); + assert:return todos.size() == (old(todos.size())); + assert:return Prim.forall(func i = + (0 <= i and i < (old(todos.size())) implies todos[i] == (old(todos[i])))); + // BUG: var:return here have type State + // assert:return Prim.forall(func i { + // 0 <= i and i < (old(todos.size())) implies todos[i] == (var:return)[i])}); + // TODO: is not supported yet, do it manually (as in reverse.mo) + // let new_array = Array.tabulate<(Nat, Text, State)>(num, func i = todos[i]); + let new_array : [ToDo] = [ { id = 0; desc = ""; completed = #TODO } ]; + return new_array; + }; + + public query func getTodo(id : Nat): async ?ToDo { + assert:return num == (old(num)) and nextId == (old(nextId)); + assert:return todos.size() == (old(todos.size())); + assert:return Prim.forall(func i = + (0 <= i and i < (old(todos.size())) implies todos[i] == (old(todos[i])))); + assert:return (Prim.exists(func i = (0 <= i and i < num and todos[i].id == id)) + implies + // BUG: problem with type of the (var:return) + true); // Prim.exists(func i = (0 <= i and i < num and todos[i] == (var:return)))); + var i : Nat = 0; + var res : ?ToDo = null; + label l while (i < num) { + // actor invariant: + assert:loop:invariant 0 <= num and num <= todos.size(); + // fields unchanged: + assert:loop:invariant num == (old(num)) and nextId == (old(nextId)); + // functional specification: + assert:loop:invariant todos.size() == (old(todos.size())); + assert:loop:invariant Prim.forall(func ii = + (0 <= ii and ii < (old(todos.size())) implies todos[ii] == (old(todos[ii])))); + assert:loop:invariant 0 <= i and i <= num; + if (todos[i].id == id) { + res := ?todos[i]; + break l; + }; + }; + return res; + }; + + // Returns the ID that was given to the ToDo item + public func addTodo(description : Text) : async Nat { + assert:return 0 <= num and num <= todos.size(); // actor invariant (rise it earler) + assert:return num == (old(num)) + 1; + assert:return nextId == (old(nextId)) + 1; + assert:return (var:return) == (old(nextId)); + assert:return todos[num-1] == ({ id = var:return; desc = description; completed = #TODO }); + assert:return Prim.forall(func i = + (0 <= i and i+1 < num implies todos[i] == (old(todos[i])))); + let id = nextId; + if (num >= todos.size()) { + resize(num * 2+1); + }; + todos[num] := { id = id; desc = description; completed = #TODO }; + num += 1; + nextId += 1; + return id; + }; + + public func completeTodo(id : Nat) : async () { + assert:return num == (old(num)) and nextId == (old(nextId)); + assert:return todos.size() == (old(todos.size())); + assert:return Prim.forall(func i = + ((0 <= i and i < num and todos[i].id != id) implies todos[i] == (old(todos[i])) )); + assert:return Prim.forall(func i = + ((0 <= i and i < num and todos[i].id == id) implies todos[i].completed == #DONE )); + var i : Nat = 0; + while (i < num) { + // actor invariant + assert:loop:invariant 0 <= num and num <= todos.size(); + // functional specifications: + assert:loop:invariant 0 <= i and i <= todos.size(); + assert:loop:invariant num == (old(num)) and nextId == (old(nextId)); + assert:loop:invariant todos.size() == (old(todos.size())); + assert:loop:invariant Prim.forall(func ii = + (i <= ii and ii < todos.size() implies todos[ii] == (old(todos[ii])))); + + assert:loop:invariant Prim.forall(func ii = + (0 <= ii and ii < i and todos[ii].id != id implies todos[ii] == (old(todos[ii])))); + assert:loop:invariant Prim.forall(func ii = + (0 <= ii and ii < i and todos[ii].id == id implies todos[ii].completed == #DONE)); + // let (taskId, taskDesc, _) = todos[i]; // TODO: requires recursive patterns + switch (todos[i]) { + case({ id = taskId; desc = taskDesc; /* _ */completed = (_completed: State) }) { + if (taskId == id) { + todos[i] := { id = taskId; desc = taskDesc; completed = #DONE }; + }; + i += 1; + }; + }; + } + }; + + public query func showTodos() : async Text { + assert:return num == (old(num)) and nextId == (old(nextId)); + assert:return todos.size() == (old(todos.size())); + assert:return Prim.forall(func i = + ((0 <= i and i < num) implies todos[i] == (old(todos[i])) )); + var output : Text = "\n___TO-DOs___"; + var i : Nat = 0; + while (i < num) { + // actor invariant + assert:loop:invariant 0 <= num and num <= todos.size(); + // unchanged fields: + assert:loop:invariant num == (old(num)) and nextId == (old(nextId)); + assert:loop:invariant todos.size() == (old(todos.size())); + // NOTE: translation is not handling shadowing here, so `func i` causes an error here + assert:loop:invariant Prim.forall(func ii = + ((0 <= ii and ii < num) implies todos[ii] == (old(todos[ii])) )); + let todo: ToDo = todos[i]; + output := output # "\n" # todo.desc; + switch (todo.completed) { + case (#DONE) { output := output # " ✔"; }; + case (#TODO) { output := output # " ❌"; }; + } + }; + return output # "\n"; + }; + + public func clearCompleted() : async () { + assert:return num <= (old(num)); + assert:return nextId == (old(nextId)); + assert:return todos.size() == (old(todos.size())); + assert:return Prim.forall(func i = + (0 <= i and i < (old(num)) and (old(todos[i].completed)) == #TODO + implies Prim.exists (func k = + ( 0 <= k and k < todos.size() and todos[k] == (old(todos[i])) )) )); + assert:return Prim.forall(func i = + (0 <= i and i < num implies todos[i].completed == #TODO)); + let new_array = Array.init(todos.size(), { id = 0; desc = ""; completed = #TODO }); + var i: Nat = 0; + var j: Nat = 0; + while (i < num) { + // actor invariant + assert:loop:invariant 0 <= num and num <= todos.size(); + // unchanged fields: + assert:loop:invariant num == (old(num)) and nextId == (old(nextId)); + assert:loop:invariant todos.size() == (old(todos.size())); + assert:loop:invariant Prim.forall(func ii = + (0 <= ii and ii < (old(todos.size())) implies todos[ii] == (old(todos[ii])))); + // functional specification: + assert:loop:invariant num <= new_array.size(); + assert:loop:invariant 0 <= i and i <= num; + assert:loop:invariant j <= i; + assert:loop:invariant 0 <= j and j <= num; + assert:loop:invariant Prim.forall(func ii = + (0 <= ii and ii < i and todos[ii].completed == #TODO + implies Prim.exists(func k = + (0 <= k and k < j and new_array[k] == todos[ii] )))); + assert:loop:invariant Prim.forall(func ii = + (0 <= ii and ii < j implies new_array[ii].completed == #TODO )); + if (todos[i].completed == #TODO) { + new_array[j] := todos[i]; + j += 1; + }; + i += 1; + }; + todos := new_array; + num := j; + }; +}