From 3d632bf0a465b61a8b6b0c1c0d2a799c791e1dca Mon Sep 17 00:00:00 2001 From: Vladislav Zavialov Date: Thu, 4 Apr 2024 14:39:21 +0300 Subject: [PATCH] motoko-san: arguments and return values New features: * arguments and return values of primitive types (Int, Bool) * multiple function arguments * early return from functions New test cases: * test/viper/simple-funs.mo * test/viper/counter.mo --- src/viper/pretty.ml | 5 +- src/viper/syntax.ml | 3 +- src/viper/trans.ml | 31 ++++-- test/repl/ok/viper.stdout.ok | 3 +- test/viper/counter.mo | 17 +++ test/viper/ok/assertions.vpr.ok | 3 +- test/viper/ok/async.vpr.ok | 3 +- test/viper/ok/claim-broken.vpr.ok | 3 +- test/viper/ok/claim-reward-naive.vpr.ok | 3 +- test/viper/ok/claim-simple.vpr.ok | 3 +- test/viper/ok/claim.vpr.ok | 3 +- test/viper/ok/counter.silicon.ok | 1 + test/viper/ok/counter.vpr.ok | 42 ++++++++ test/viper/ok/invariant.vpr.ok | 6 +- test/viper/ok/simple-funs.silicon.ok | 2 + test/viper/ok/simple-funs.vpr.ok | 132 ++++++++++++++++++++++++ test/viper/simple-funs.mo | 65 ++++++++++++ 17 files changed, 304 insertions(+), 21 deletions(-) create mode 100644 test/viper/counter.mo create mode 100644 test/viper/ok/counter.silicon.ok create mode 100644 test/viper/ok/counter.vpr.ok create mode 100644 test/viper/ok/simple-funs.silicon.ok create mode 100644 test/viper/ok/simple-funs.vpr.ok create mode 100644 test/viper/simple-funs.mo diff --git a/src/viper/pretty.ml b/src/viper/pretty.ml index 11003f4429e..6e514e0e46f 100644 --- a/src/viper/pretty.ml +++ b/src/viper/pretty.ml @@ -206,7 +206,10 @@ and pp_stmt' ppf = function fprintf ppf "@[%a@]" (pp_print_list ~pp_sep:comma pp_exp) args in fprintf ppf ")" - | LabelS (_, _) -> failwith "LabelS?" + | LabelS lbl -> + fprintf ppf "@[label %s@]" lbl.it + | GotoS lbl -> + fprintf ppf "@[goto %s@]" lbl.it and pp_fldacc ppf fldacc = match fldacc with diff --git a/src/viper/syntax.ml b/src/viper/syntax.ml index c77af6026b8..3c4517c4986 100644 --- a/src/viper/syntax.ml +++ b/src/viper/syntax.ml @@ -79,7 +79,8 @@ and stmt' = | FieldAssignS of fldacc * exp | IfS of exp * seqn * seqn | WhileS of exp * invariants * seqn - | LabelS of id * invariants + | LabelS of id + | GotoS of id (* 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 diff --git a/src/viper/trans.ml b/src/viper/trans.ml index 454e079d6f6..37efb5479dc 100644 --- a/src/viper/trans.ml +++ b/src/viper/trans.ml @@ -234,13 +234,17 @@ and dec_field' ctxt d = fun ctxt' -> let open Either in let self_id = !!! (Source.no_region) "$Self" in - let ctxt'' = { ctxt' with self = Some self_id.it } + let method_args = args p in + let ctxt'' = { ctxt' + with self = Some self_id.it; + ids = List.fold_left (fun env (id, _) -> Env.add id.it Local env) ctxt.ids method_args } in (* TODO: add args (and rets?) *) let stmts = stmt ctxt'' e in let _, stmts = extract_concurrency stmts in let pres, stmts' = List.partition_map (function { it = PreconditionS exp; _ } -> Left exp | s -> Right s) (snd stmts.it) in let posts, stmts' = List.partition_map (function { it = PostconditionS exp; _ } -> Left exp | s -> Right s) stmts' in - (MethodI(id f, (self_id, !!! Source.no_region RefT)::args p, rets t_opt, pres, posts, Some { stmts with it = fst stmts.it, stmts' } ), + let stmts'' = stmts' @ [!!! Source.no_region (LabelS(!!! (Source.no_region) "$Ret"))] in + (MethodI(id f, (self_id, !!! Source.no_region RefT)::method_args, rets t_opt, pres, posts, Some { stmts with it = fst stmts.it, stmts'' } ), PublicFunction f.it) (* private sync functions *) | M.(LetD ({it=VarP f;_}, @@ -268,15 +272,15 @@ and dec_field' ctxt d = unsupported d.M.dec.at (Arrange.dec d.M.dec) and args p = match p.it with - | M.TupP ps -> - List.map - (fun p -> - match p.it with - | M.VarP x -> - (id x, tr_typ p.note) + | M.TupP ps -> List.map arg ps + | M.ParP p -> [arg p] + | _ -> unsupported p.at (Arrange.pat p) +and arg p = match p.it with + | M.AnnotP (p, t) -> + (match p.it with + | M.VarP x -> (id x, tr_typ t.note) | _ -> unsupported p.at (Arrange.pat p)) - ps - | _ -> unsupported p.at (Arrange.pat p) + | _ -> unsupported p.at (Arrange.pat p) and block ctxt at ds = let ctxt, mk_ss = decs ctxt ds in @@ -421,6 +425,11 @@ and stmt ctxt (s : M.exp) : seqn = [ !!(MethodCallS ([], id m, let self_var = self ctxt m.at in self_var :: List.map (fun arg -> exp ctxt arg) args))]) + | M.RetE e -> + !!([], + [ !!(VarAssignS(!!! (Source.no_region) "$Res", exp ctxt e)); + !!(GotoS(!!! (Source.no_region) "$Ret")) + ]) | _ -> unsupported s.at (Arrange.exp s) @@ -487,6 +496,8 @@ and rets t_opt = (match T.normalize t.note with | T.Tup [] -> [] | T.Async (T.Fut, _, _) -> [] + | T.Prim T.Int -> [(!!! (Source.no_region) "$Res", !!! (Source.no_region) IntT)] + | T.Prim T.Bool -> [(!!! (Source.no_region) "$Res", !!! (Source.no_region) BoolT)] | _ -> unsupported t.at (Arrange.typ t) ) diff --git a/test/repl/ok/viper.stdout.ok b/test/repl/ok/viper.stdout.ok index 7a1aaf1d945..098fbe22369 100644 --- a/test/repl/ok/viper.stdout.ok +++ b/test/repl/ok/viper.stdout.ok @@ -39,5 +39,6 @@ method claim($Self: Ref) exhale ($Perm($Self) && $Inv($Self)) } inhale ($Perm($Self) && $Inv($Self)) - } + } + label $Ret } diff --git a/test/viper/counter.mo b/test/viper/counter.mo new file mode 100644 index 00000000000..191c2a02b24 --- /dev/null +++ b/test/viper/counter.mo @@ -0,0 +1,17 @@ +// @verify + +actor Counter { + var count = 0 : Int; + + public func increment() : async () { + count += 1; + }; + + public func getCount() : async Int { + return count; + }; + + public func setCount(n : Int) : async () { + count := n; + }; +}; diff --git a/test/viper/ok/assertions.vpr.ok b/test/viper/ok/assertions.vpr.ok index c834272478d..a82bb5216f9 100644 --- a/test/viper/ok/assertions.vpr.ok +++ b/test/viper/ok/assertions.vpr.ok @@ -37,5 +37,6 @@ method claim($Self: Ref) } exhale ($Perm($Self) && $Inv($Self)) } - inhale ($Perm($Self) && $Inv($Self)) + inhale ($Perm($Self) && $Inv($Self)) + label $Ret } diff --git a/test/viper/ok/async.vpr.ok b/test/viper/ok/async.vpr.ok index b0a40dca425..8e10ad1f324 100644 --- a/test/viper/ok/async.vpr.ok +++ b/test/viper/ok/async.vpr.ok @@ -68,5 +68,6 @@ method claim($Self: Ref) exhale ($Perm($Self) && $Inv($Self)) } inhale ($Perm($Self) && $Inv($Self)) - } + } + label $Ret } diff --git a/test/viper/ok/claim-broken.vpr.ok b/test/viper/ok/claim-broken.vpr.ok index f2061664183..2f9e89edf51 100644 --- a/test/viper/ok/claim-broken.vpr.ok +++ b/test/viper/ok/claim-broken.vpr.ok @@ -39,5 +39,6 @@ method claim($Self: Ref) exhale ($Perm($Self) && $Inv($Self)) } inhale ($Perm($Self) && $Inv($Self)) - } + } + label $Ret } diff --git a/test/viper/ok/claim-reward-naive.vpr.ok b/test/viper/ok/claim-reward-naive.vpr.ok index b8c9c1680d9..e57e1366e67 100644 --- a/test/viper/ok/claim-reward-naive.vpr.ok +++ b/test/viper/ok/claim-reward-naive.vpr.ok @@ -32,5 +32,6 @@ method claim($Self: Ref) { reward($Self) ($Self).claimed := true - } + } + label $Ret } diff --git a/test/viper/ok/claim-simple.vpr.ok b/test/viper/ok/claim-simple.vpr.ok index 50d2875b529..b26442befcf 100644 --- a/test/viper/ok/claim-simple.vpr.ok +++ b/test/viper/ok/claim-simple.vpr.ok @@ -22,5 +22,6 @@ method claim($Self: Ref) { ($Self).claimed := true ($Self).count := (($Self).count + 1) - } + } + label $Ret } diff --git a/test/viper/ok/claim.vpr.ok b/test/viper/ok/claim.vpr.ok index 593ce616846..2a99877bfe9 100644 --- a/test/viper/ok/claim.vpr.ok +++ b/test/viper/ok/claim.vpr.ok @@ -39,5 +39,6 @@ method claim($Self: Ref) exhale ($Perm($Self) && $Inv($Self)) } inhale ($Perm($Self) && $Inv($Self)) - } + } + label $Ret } diff --git a/test/viper/ok/counter.silicon.ok b/test/viper/ok/counter.silicon.ok new file mode 100644 index 00000000000..69fb8c629a0 --- /dev/null +++ b/test/viper/ok/counter.silicon.ok @@ -0,0 +1 @@ +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (counter.vpr@2.1) diff --git a/test/viper/ok/counter.vpr.ok b/test/viper/ok/counter.vpr.ok new file mode 100644 index 00000000000..5196861d655 --- /dev/null +++ b/test/viper/ok/counter.vpr.ok @@ -0,0 +1,42 @@ +define $Perm($Self) ((true && acc(($Self).count,write))) +define $Inv($Self) (true) +method __init__($Self: Ref) + + requires $Perm($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + ($Self).count := 0 + } +field count: Int +method increment($Self: Ref) + + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + ($Self).count := (($Self).count + 1) + label $Ret + } +method getCount($Self: Ref) + returns ($Res: Int) + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + $Res := ($Self).count + goto $Ret + label $Ret + } +method setCount($Self: Ref, n: Int) + + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + ($Self).count := n + label $Ret + } diff --git a/test/viper/ok/invariant.vpr.ok b/test/viper/ok/invariant.vpr.ok index 06b14fe0dea..7593736d04b 100644 --- a/test/viper/ok/invariant.vpr.ok +++ b/test/viper/ok/invariant.vpr.ok @@ -23,7 +23,8 @@ method claim($Self: Ref) ensures (($Self).count >= 0) ensures $Inv($Self) { - assume (($Self).claimed ==> (($Self).count > 0)) + assume (($Self).claimed ==> (($Self).count > 0)) + label $Ret } method loops($Self: Ref) @@ -36,5 +37,6 @@ method loops($Self: Ref) while ((i > 0)) { { i := (i + 1) - }} + }} + label $Ret } diff --git a/test/viper/ok/simple-funs.silicon.ok b/test/viper/ok/simple-funs.silicon.ok new file mode 100644 index 00000000000..d0c64d57d11 --- /dev/null +++ b/test/viper/ok/simple-funs.silicon.ok @@ -0,0 +1,2 @@ +Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (simple-funs.vpr@1.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (simple-funs.vpr@2.1) diff --git a/test/viper/ok/simple-funs.vpr.ok b/test/viper/ok/simple-funs.vpr.ok new file mode 100644 index 00000000000..ba1c971ba66 --- /dev/null +++ b/test/viper/ok/simple-funs.vpr.ok @@ -0,0 +1,132 @@ +define $Perm($Self) (true) +define $Inv($Self) (true) +method __init__($Self: Ref) + + requires $Perm($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + + } +method getZero($Self: Ref) + returns ($Res: Int) + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + $Res := 0 + goto $Ret + label $Ret + } +method getFalse($Self: Ref) + returns ($Res: Bool) + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + $Res := false + goto $Ret + label $Ret + } +method idInt($Self: Ref, n: Int) + returns ($Res: Int) + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + $Res := n + goto $Ret + label $Ret + } +method idBool($Self: Ref, b: Bool) + returns ($Res: Bool) + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + $Res := b + goto $Ret + label $Ret + } +method abs($Self: Ref, n: Int) + returns ($Res: Int) + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + if ((n < 0)) + { + $Res := (0 - n) + goto $Ret + } + $Res := n + goto $Ret + label $Ret + } +method max($Self: Ref, n: Int, m: Int) + returns ($Res: Int) + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + if ((n >= m)) + { + $Res := n + goto $Ret + } + $Res := m + goto $Ret + label $Ret + } +method eq4($Self: Ref, n: Int, m: Int, p: Int, q: Int) + returns ($Res: Bool) + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + $Res := (((n == m) && (m == p)) && (p == q)) + goto $Ret + label $Ret + } +method factorial($Self: Ref, n: Int) + returns ($Res: Int) + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { var prod: Int + var i: Int + prod := 1 + i := n + while ((i > 0)) { + { + prod := (prod * i) + i := (i - 1) + }} + $Res := prod + goto $Ret + label $Ret + } +method bmul($Self: Ref, b: Bool, n: Int) + returns ($Res: Int) + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + if (b) + { + $Res := n + goto $Ret + } + $Res := 0 + goto $Ret + label $Ret + } diff --git a/test/viper/simple-funs.mo b/test/viper/simple-funs.mo new file mode 100644 index 00000000000..aee2bd09994 --- /dev/null +++ b/test/viper/simple-funs.mo @@ -0,0 +1,65 @@ +// @verify + +actor SimpleFuns { + + // return an Int constant + public func getZero() : async Int { + return 0; + }; + + // return a Bool constant + public func getFalse() : async Bool { + return false; + }; + + // take an Int argument and return it unmodified + public func idInt(n : Int) : async Int { + return n; + }; + + // take a Bool argument and return it unmodified + public func idBool(b : Bool) : async Bool { + return b; + }; + + // conditional early return from a function + public func abs(n : Int) : async Int { + if (n < 0) { + return (0 - n); + }; + return n; + }; + + // take multiple Int arguments, return Int + public func max(n : Int, m : Int) : async Int { + if (n >= m) { + return n; + }; + return m; + }; + + // take multiple Int arguments, return Bool + public func eq4(n : Int, m : Int, p : Int, q : Int) : async Bool { + return (n == m and m == p and p == q); + }; + + // return the value of a local mutable variable + public func factorial(n : Int) : async Int { + var prod : Int = 1; + var i : Int = n; + while (i > 0) { + prod *= i; + i -= 1; + }; + return prod; + }; + + // take an Int and a Bool, return an Int + public func bmul(b : Bool, n : Int) : async Int { + if (b) { + return n; + }; + return 0; + }; + +};