motoko-san: method calls

Bug fixes:
* pretty-printing of MethodCallS
* arguments in private functions
* calls with n=1 arguments

New features:
* method calls in let/var declarations
* method calls in assignments
* method calls in return statements

New test cases:
* test/viper/method-call.mo

src/viper/pretty.ml

@@ -188,30 +188,19 @@ and pp_stmt' ppf = function
       max
       pp_exp exp
   | MethodCallS (rs, m, args) ->
-    let () = match rs with
-    | [] -> ()
-    | r :: rs ->
-      let () = fprintf ppf "@[%s@]" r.it in
-      List.iter (fun r ->
-        fprintf ppf ", @[%s@]" r.it
-      ) rs
-    in
     let () = if rs != [] then
-      fprintf ppf " := "
+      fprintf ppf "@[%a@] := " (pp_print_list ~pp_sep:comma pp_res_var) rs
     in
     let () = fprintf ppf "@[%s(@]" m.it in
-    let () = match args with
-    | [] -> ()
-    | arg :: args ->
-      let () = fprintf ppf "@[%a@]" pp_exp arg in
-      fprintf ppf "@[%a@]" (pp_print_list ~pp_sep:comma pp_exp) args
-    in
+    let () = fprintf ppf "@[%a@]" (pp_print_list ~pp_sep:comma pp_exp) args in
     fprintf ppf ")"
   | LabelS lbl ->
       fprintf ppf "@[label %s@]" lbl.it
   | GotoS lbl ->
       fprintf ppf "@[goto %s@]" lbl.it
 
+and pp_res_var ppf r = fprintf ppf "%s" r.it
+
 and pp_fldacc ppf fldacc =
   match fldacc with
   | (exp1, id) ->

src/viper/trans.ml

@@ -267,13 +267,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'' } ),
         PrivateFunction f.it)
   | M.(ExpD { it = AssertE (Invariant, e); at; _ }) ->
       ctxt,
@@ -318,12 +322,12 @@ and dec ctxt d =
     { ctxt with ids = Env.add x.it Local ctxt.ids },
     fun ctxt' ->
       ([ !!(id x, tr_typ e.note.M.note_typ) ],
-       [ !!(VarAssignS (id x, exp ctxt' e)) ])
+       [ !!(assign_stmt ctxt' (id x) e) ])
   | M.(LetD ({it=VarP x;_}, e, None)) ->
      { ctxt with ids = Env.add x.it Local ctxt.ids },
      fun ctxt' ->
        ([ !!(id x, tr_typ e.note.M.note_typ) ],
-        [ !!(VarAssignS (id x, exp ctxt' e)) ])
+        [ !!(assign_stmt ctxt' (id x) e) ])
   | M.(ExpD e) -> (* TODO: restrict to e of unit type? *)
      (ctxt,
       fun ctxt' ->
@@ -409,9 +413,8 @@ and stmt ctxt (s : M.exp) : seqn =
   | M.(AssignE({it = VarE x; _}, e2)) ->
      begin match Env.find x.it ctxt.ids with
      | Local ->
-       let loc = !!! (x.at) (x.it) in
-       !!([],
-          [ !!(VarAssignS(loc, exp ctxt e2)) ])
+        let loc = !!! (x.at) (x.it) in
+        !!([], [!!(assign_stmt ctxt loc e2)])
      | Field ->
        let fld = (self ctxt x.at, id x) in
        !!([],
@@ -434,19 +437,32 @@ and stmt ctxt (s : M.exp) : seqn =
   | M.AssertE (M.Runtime, e) ->
     !!([],
        [ !!(AssumeS (exp ctxt e)) ])
-  | M.(CallE({it = VarE m; _}, inst, {it = TupE args; _})) ->
+  | M.(CallE({it = VarE m; _}, inst, args)) ->
     !!([],
        [ !!(MethodCallS ([], id m,
        let self_var = self ctxt m.at in
-       self_var :: List.map (fun arg -> exp ctxt arg) args))])
+       self_var :: call_args ctxt args))])
   | M.RetE e ->
      !!([],
-        [ !!(VarAssignS(!!! (Source.no_region) "$Res", exp ctxt e));
+        [ !!(assign_stmt ctxt (!!! (Source.no_region) "$Res") e);
           !!(GotoS(!!! (Source.no_region) "$Ret"))
         ])
   | _ ->
      unsupported s.at (Arrange.exp s)
 
+and assign_stmt ctxt x e =
+  match e with
+  | M.({it = CallE({it = VarE m; _}, inst, args); _}) ->
+    MethodCallS ([x], id m,
+      let self_var = self ctxt m.at in
+      self_var :: call_args ctxt args)
+  | _ -> VarAssignS(x, exp ctxt e)
+
+and call_args ctxt e =
+  match e with
+  | {it = M.TupE args; _} -> List.map (fun arg -> exp ctxt arg) args
+  | arg -> [exp ctxt arg]
+
 and exp ctxt e =
   let open Mo_values.Operator in
   let (!!) p = !!! (e.at) p in

test/viper/method-call.mo

@@ -0,0 +1,25 @@
+actor MethodCall {
+  func ignoreBool(_b : Bool) : () {
+  };
+
+  // take an Int argument and return it unmodified
+  func idInt(n : Int) : Int {
+    return n;
+  };
+
+  // take a Bool argument and return it unmodified
+  func idBool(b : Bool) : Bool {
+    return b;
+  };
+
+  public func ifThenElse(b : Bool, tru : Int, fls : Int) : async Int {
+    ignoreBool(b);        // standalone method call
+    let c1 = idBool(b);   // method call in let-declaration
+    var c2 = idBool(b);   // method call in var-declaration
+    c2 := idBool(c2);     // method call in assignment
+    if (c1 and c2) {
+      return idInt(tru);  // method call in return statement
+    };
+    return idInt(fls);    // method call in return statement
+  };
+}

test/viper/ok/claim-reward-naive.vpr.ok

@@ -19,7 +19,8 @@ method reward($Self: Ref)
     ensures $Perm($Self)
     ensures (($Self).count == (old(($Self).count) + 1))
     { 
-      ($Self).count := (($Self).count + 1) 
+      ($Self).count := (($Self).count + 1)
+      label $Ret 
     }
 method claim($Self: Ref)
 

test/viper/ok/method-call.silicon.ok

@@ -0,0 +1,2 @@
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (method-call.vpr@1.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (method-call.vpr@2.1)

test/viper/ok/method-call.vpr.ok

@@ -0,0 +1,56 @@
+define $Perm($Self) (true)
+define $Inv($Self) (true)
+method __init__($Self: Ref)
+
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+
+    }
+method ignoreBool($Self: Ref, _b: Bool)
+
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    { 
+      label $Ret 
+    }
+method idInt($Self: Ref, n: Int)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    { 
+      $Res := n
+      goto $Ret
+      label $Ret 
+    }
+method idBool($Self: Ref, b: Bool)
+     returns ($Res: Bool)
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    { 
+      $Res := b
+      goto $Ret
+      label $Ret 
+    }
+method ifThenElse($Self: Ref, b: Bool, tru: Int, fls: Int)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { var c1: Bool
+      var c2: Bool
+      ignoreBool($Self, b)
+      c1 := idBool($Self, b)
+      c2 := idBool($Self, b)
+      c2 := idBool($Self, c2)
+      if ((c1 && c2))
+         { 
+           $Res := idInt($Self, tru)
+           goto $Ret 
+         }
+      $Res := idInt($Self, fls)
+      goto $Ret
+      label $Ret 
+    }

test/viper/ok/private.vpr.ok

@@ -20,5 +20,6 @@ method reward($Self: Ref)
     ensures $Perm($Self)
     { 
       ($Self).count := (($Self).count + 1)
-      assert (($Self).count == 1) 
+      assert (($Self).count == 1)
+      label $Ret 
     }