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
serokell · Apr 8, 2024 · 8a99834 · 8a99834
1 parent 85b4ce8
commit 8a99834
Show file tree

Hide file tree

Showing 16 changed files with 302 additions and 20 deletions.
diff --git 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
@@ -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
@@ -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/viper/counter.mo 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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 
+    }