Support private functions and old expressions in Motoko-to-Viper translation

emacs/motoko-mode.el

@@ -79,6 +79,7 @@
                  "while"
                  "prim"
                  "invariant"
+                 "old"
                  "implies"
                  ))
               ;; Braces introduce blocks; it's nice to make them stand

src/ir_def/construct.ml

@@ -327,6 +327,13 @@ let orE : Ir.exp -> Ir.exp -> Ir.exp = fun e1 e2 ->
   ifE e1 (trueE ()) e2
 let impliesE : Ir.exp -> Ir.exp -> Ir.exp = fun e1 e2 ->
   orE (notE e1) e2
+let oldE : Ir.exp -> Ir.exp = fun e ->
+  { it = (primE (CallPrim [typ e]) [e]).it;
+    at = no_region;
+    note = Note.{ def with
+      typ = typ e;
+    }
+  }
 
 let rec conjE : Ir.exp list -> Ir.exp = function
   | [] -> trueE ()

src/ir_def/construct.mli

@@ -98,6 +98,7 @@ val notE : exp -> exp
 val andE : exp -> exp -> exp
 val orE : exp -> exp -> exp
 val impliesE : exp -> exp -> exp
+val oldE : exp -> exp
 val conjE : exp list -> exp
 
 val declare_idE : id -> typ -> exp -> exp

src/lowering/desugar.ml

@@ -202,6 +202,7 @@ and exp' at note = function
   | S.AndE (e1, e2) -> (andE (exp e1) (exp e2)).it
   | S.OrE (e1, e2) -> (orE (exp e1) (exp e2)).it
   | S.ImpliesE (e1, e2) -> (impliesE (exp e1) (exp e2)).it
+  | S.OldE (e) -> (oldE (exp e)).it
   | S.IfE (e1, e2, e3) -> I.IfE (exp e1, exp e2, exp e3)
   | S.SwitchE (e1, cs) -> I.SwitchE (exp e1, cases cs)
   | S.TryE (e1, cs) -> I.TryE (exp e1, cases cs)

src/mo_def/arrange.ml

@@ -93,6 +93,7 @@ module Make (Cfg : Config) = struct
     | AndE (e1, e2)       -> "AndE"    $$ [exp e1; exp e2]
     | OrE (e1, e2)        -> "OrE"     $$ [exp e1; exp e2]
     | ImpliesE (e1, e2)   -> "ImpliesE"$$ [exp e1; exp e2]
+    | OldE (e)            -> "OldE"    $$ [exp e]
     | IfE (e1, e2, e3)    -> "IfE"     $$ [exp e1; exp e2; exp e3]
     | SwitchE (e, cs)     -> "SwitchE" $$ [exp e] @ List.map case cs
     | WhileE (e1, e2)     -> "WhileE"  $$ [exp e1; exp e2]

src/mo_def/syntax.ml

@@ -176,6 +176,7 @@ and exp' =
   | AndE of exp * exp                          (* conjunction *)
   | OrE of exp * exp                           (* disjunction *)
   | ImpliesE of exp * exp                      (* implication *)
+  | OldE of exp                                (* old-expression *)
   | IfE of exp * exp * exp                     (* conditional *)
   | SwitchE of exp * case list                 (* switch *)
   | WhileE of exp * exp                        (* while-do loop *)

src/mo_frontend/assertions.mly

@@ -27,6 +27,7 @@ let is_verification () =
 (*
 %nonassoc IMPLIES  (* see parser.mly *)
 *)
+%token OLD
 
 %%
 
@@ -45,5 +46,7 @@ let is_verification () =
     { is_verification () &&& AssertE(Postcondition, e) @? at $sloc }
   | ASSERT COLON s=NAT COLON ASYNC e=exp_nest
     { is_verification () &&& AssertE(Concurrency s, e) @? at $sloc }
+  | OLD e=exp_nest
+    { is_verification () &&& OldE(e) @? at $sloc }
 
 %%

src/mo_frontend/definedness.ml

@@ -114,6 +114,7 @@ let rec exp msgs e : f = match e.it with
   | AndE (e1, e2)       -> exps msgs [e1; e2]
   | OrE (e1, e2)        -> exps msgs [e1; e2]
   | ImpliesE (e1, e2)   -> exps msgs [e1; e2]
+  | OldE (e)            -> exp msgs e
   | IfE (e1, e2, e3)    -> exps msgs [e1; e2; e3]
   | SwitchE (e, cs)     -> exp msgs e ++ cases msgs cs
   | TryE (e, cs)        -> exp msgs e ++ cases msgs cs

src/mo_frontend/effect.ml

@@ -49,6 +49,7 @@ let rec infer_effect_exp (exp:Syntax.exp) : T.eff =
   | TagE (_, exp1)
   | DotE (exp1, _)
   | NotE exp1
+  | OldE (exp1)
   | AssertE (_, exp1)
   | LabelE (_, _, exp1)
   | BreakE (_, exp1)

src/mo_frontend/error_reporting.ml

@@ -119,6 +119,7 @@ let terminal2token (type a) (symbol : a terminal) : token =
       | T_ANDASSIGN -> ANDASSIGN
       | T_AND -> AND
       | T_IMPLIES -> IMPLIES
+      | T_OLD -> OLD
       | T_ADDOP -> ADDOP
       | T_ACTOR -> ACTOR
       | T_INVARIANT -> INVARIANT

src/mo_frontend/parser.mly

@@ -238,6 +238,7 @@ and objblock s dec_fields =
 
 %nonassoc IMPLIES (* see assertions.mly *)
 
+
 %nonassoc RETURN_NO_ARG IF_NO_ELSE LOOP_NO_WHILE
 %nonassoc ELSE WHILE
 

src/mo_frontend/printers.ml

@@ -134,6 +134,7 @@ let string_of_symbol = function
   | X (T T_ANDASSIGN) -> binassign "&="
   | X (T T_AND) -> "and"
   | X (T T_IMPLIES) -> "implies"
+  | X (T T_OLD) -> "old"
   | X (T T_ADDOP) -> unop "+"
   | X (T T_ACTOR) -> "actor"
   | X (T T_INVARIANT) -> "invariant"

src/mo_frontend/source_lexer.mll

@@ -219,6 +219,7 @@ rule token mode = parse
   | "in" { IN }
   | "invariant" as s { if mode.verification then INVARIANT else ID s }
   | "implies" as s { if mode.verification then IMPLIES else ID s }
+  | "old" as s { if mode.verification then OLD else ID s }
   | "import" { IMPORT }
   | "module" { MODULE }
   | "not" { NOT }

src/mo_frontend/source_token.ml

@@ -58,6 +58,7 @@ type token =
   | AND
   | OR
   | IMPLIES
+  | OLD
   | NOT
   | IMPORT
   | MODULE
@@ -184,6 +185,7 @@ let to_parser_token :
   | AND -> Ok Parser.AND
   | OR -> Ok Parser.OR
   | IMPLIES -> Ok Parser.IMPLIES
+  | OLD -> Ok Parser.OLD
   | NOT -> Ok Parser.NOT
   | IMPORT -> Ok Parser.IMPORT
   | MODULE -> Ok Parser.MODULE
@@ -373,6 +375,7 @@ let string_of_parser_token = function
   | Parser.UNDERSCORE -> "UNDERSCORE"
   | Parser.INVARIANT -> "INVARIANT"
   | Parser.IMPLIES -> "IMPLIES"
+  | Parser.OLD -> "OLD"
 
 let is_lineless_trivia : token -> void trivia option = function
   | SINGLESPACE -> Some (Space 1)

src/mo_frontend/static.ml

@@ -87,6 +87,7 @@ let rec exp m e = match e.it with
   | TryE _
   | BangE _
   | ImpliesE _
+  | OldE _
   -> err m e.at
 
 and dec_fields m dfs = List.iter (fun df -> dec m df.it.dec) dfs

src/mo_frontend/traversals.ml

@@ -39,6 +39,7 @@ let rec over_exp (f : exp -> exp) (exp : exp) : exp = match exp.it with
      f { exp with it = OrE (over_exp f exp1, over_exp f exp2) }
   | ImpliesE (exp1, exp2) ->
      f { exp with it = ImpliesE (over_exp f exp1, over_exp f exp2) }
+  | OldE exp1 -> f { exp with it = OldE (over_exp f exp1) }
   | WhileE (exp1, exp2) ->
      f { exp with it = WhileE (over_exp f exp1, over_exp f exp2) }
   | LoopE (exp1, exp2_opt) ->

src/mo_frontend/typing.ml

@@ -763,7 +763,7 @@ let rec is_explicit_exp e =
   | BreakE _ | RetE _ | ThrowE _ ->
     false
   | VarE _
-  | RelE _ | NotE _ | AndE _ | OrE _ | ImpliesE _ | ShowE _ | ToCandidE _ | FromCandidE _
+  | RelE _ | NotE _ | AndE _ | OrE _ | ImpliesE _ | OldE _ | ShowE _ | ToCandidE _ | FromCandidE _
   | AssignE _ | IgnoreE _ | AssertE _ | DebugE _
   | WhileE _ | ForE _
   | AnnotE _ | ImportE _ ->
@@ -1318,6 +1318,8 @@ and infer_exp'' env exp : T.typ =
       check_exp_strong env T.bool exp2
     end;
     T.bool
+  | OldE exp1 ->
+    infer_exp_promote env exp1
   | IfE (exp1, exp2, exp3) ->
     if not env.pre then check_exp_strong env T.bool exp1;
     let t2 = infer_exp env exp2 in

src/viper/pretty.ml

@@ -123,6 +123,8 @@ and pp_exp ppf exp =
        | Implies _ -> "==>" | OrE _ -> "||" | AndE _ -> "&&"
        | _ -> failwith "not a binary operator" in
      fprintf ppf "(%a %s %a)" pp_exp e1 op pp_exp e2
+  | Old e ->
+    fprintf ppf "@[old(%a)@]" pp_exp e
   | PermE p -> pp_perm ppf p
   | AccE (fldacc, perm) -> fprintf ppf "@[acc(%a,%a)@]" pp_fldacc fldacc pp_exp perm
   | _ -> fprintf ppf "@[// pretty printer not implemented for node at %s@]" (string_of_region exp.at)
@@ -184,8 +186,27 @@ and pp_stmt' ppf = function
     fprintf ppf "@[<v 2>/*concurrency max %s, cond: s %a*/@]"
       max
       pp_exp exp
-  | MethodCallS (_, _, _)
-  | LabelS (_, _) -> failwith "MethodCallS or LabelS?"
+  | 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 " := "
+    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
+    fprintf ppf ")"
+  | LabelS (_, _) -> failwith "LabelS?"
 
 and pp_fldacc ppf fldacc =
   match fldacc with

src/viper/syntax.ml

@@ -45,6 +45,7 @@ and exp' =
   | AndE of exp * exp
   | OrE of exp * exp
   | Implies of exp * exp
+  | Old of exp
   | FldAcc of fldacc
   | PermE of perm          (* perm_amount *)
   | AccE of fldacc * exp   (* acc((rcvr: exp).field, (exp: perm_amount)) *)
@@ -68,7 +69,7 @@ and tmpl' = (Mo_def.Syntax.exp -> exp) -> exp
 and fldacc = exp * id
 
 and stmt' =
-  | MethodCallS of id * exp list * id list
+  | MethodCallS of id list * id * exp list
   | ExhaleS of exp
   | InhaleS of exp
   | AssertS of exp

src/viper/trans.ml

@@ -415,6 +415,11 @@ 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; _})) ->
+    !!([],
+       [ !!(MethodCallS ([], id m, 
+       let self_var = self ctxt m.at in
+       self_var :: List.map (fun arg -> exp ctxt arg) args))])
   | _ ->
      unsupported s.at (Arrange.exp s)
 
@@ -469,6 +474,8 @@ and exp ctxt e =
      !!(AndE (exp ctxt e1, exp ctxt e2))
   | M.ImpliesE (e1, e2) ->
      !!(Implies (exp ctxt e1, exp ctxt e2))
+  | M.OldE e ->
+    !!(Old (exp ctxt e))
   | _ ->
      unsupported e.at (Arrange.exp e)
 

test/viper/claim-reward-naive.mo

@@ -0,0 +1,21 @@
+actor ClaimReward {
+  var claimed = false;
+  var count = 0 : Int;
+
+  assert:invariant 
+   (not claimed implies count == 0) // initially synchronized
+   and (count == 0 or count == 1);  // reward is unique
+
+  private func reward() : () {
+    // (send reward)
+    count += 1;
+    assert:return count == (old count) + 1;
+  };
+
+  public shared func claim() : async () {
+    if (not claimed) {
+      reward();
+      claimed := true;
+    };
+  };
+}

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

@@ -0,0 +1,36 @@
+define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write)))
+define $Inv($Self) (invariant_5($Self))
+method __init__($Self: Ref)
+
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+      ($Self).claimed := false
+      ($Self).count := 0 
+    }
+field claimed: Bool
+field count: Int
+define invariant_5($Self) ((((!($Self).claimed) ==> (($Self).count == 0)) && ((
+  ($Self).count == 0) || (($Self).count == 1))))
+method reward($Self: Ref)
+
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    ensures (($Self).count == (old(($Self).count) + 1))
+    { 
+      ($Self).count := (($Self).count + 1) 
+    }
+method claim($Self: Ref)
+
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+      if ((!($Self).claimed))
+         { 
+           reward($Self)
+           ($Self).claimed := true 
+         } 
+    }