viper: int arguments and return values

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

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

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;_},
@@ -276,6 +280,11 @@ and args p = match p.it with
           (id x, tr_typ p.note)
         | _ -> unsupported p.at (Arrange.pat p))
       ps
+  | M.ParP p -> args p
+  | M.AnnotP (p, t) ->
+      (match p.it with
+        | M.VarP x -> [(id x, tr_typ t.note)]
+        | _ -> unsupported p.at (Arrange.pat p))
   |  _ -> unsupported p.at (Arrange.pat p)
 
 and block ctxt at ds =
@@ -421,6 +430,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 +501,7 @@ 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)]
      | _ -> unsupported t.at (Arrange.typ t)
     )