motoko-san: loop invariants

New features:
* invariants in while-loops

New test cases:
* test/viper/loop-invariant.mo

src/mo_def/arrange.ml

@@ -116,6 +116,7 @@ module Make (Cfg : Config) = struct
     | AssertE (Loop_entry, e)    -> "Loop_entry" $$ [exp e]
     | AssertE (Loop_continue, e) -> "Loop_continue" $$ [exp e]
     | AssertE (Loop_exit, e)     -> "Loop_exit" $$ [exp e]
+    | AssertE (Loop_invariant, e)-> "Loop_invariant" $$ [exp e]
     | AssertE (Concurrency s, e) -> "Concurrency"^s $$ [exp e]
     | AnnotE (e, t)       -> "AnnotE"  $$ [exp e; typ t]
     | OptE e              -> "OptE"    $$ [exp e]

src/mo_def/syntax.ml

@@ -201,7 +201,7 @@ and exp' =
 *)
 
 and assert_kind =
-  | Runtime | Static | Invariant | Precondition | Postcondition | Concurrency of string | Loop_entry | Loop_continue | Loop_exit
+  | Runtime | Static | Invariant | Precondition | Postcondition | Concurrency of string | Loop_entry | Loop_continue | Loop_exit | Loop_invariant
 
 and dec_field = dec_field' Source.phrase
 and dec_field' = {dec : dec; vis : vis; stab: stab option}

src/mo_frontend/assertions.mly

@@ -40,6 +40,8 @@ let is_verification () =
     { is_verification () &&& AssertE(Static, e) @? at $sloc }
   | ASSERT COLON INVARIANT e=exp_nest
     { is_verification () &&& AssertE(Invariant, e) @? at $sloc }
+  | ASSERT COLON LOOP COLON INVARIANT e=exp_nest
+    { is_verification () &&& AssertE(Loop_invariant, e) @? at $sloc }
   | ASSERT COLON FUNC e=exp_nest
     { is_verification () &&& AssertE(Precondition, e) @? at $sloc }
   | ASSERT COLON RETURN e=exp_nest

src/viper/pretty.ml

@@ -152,9 +152,10 @@ and pp_stmt' ppf = function
       pp_exp exp1
       pp_seqn s1
       pp_seqn s2
-  | WhileS (exp, _, s) -> (* TODO: Invariant *)
-    fprintf ppf "@[<v 2>while (%a) {@ %a}@]"
+  | WhileS (exp, invs, s) ->
+    fprintf ppf "@[<v 2>while (%a)@;@[<v 0>%a@]@;%a@]"
       pp_exp exp
+      (pp_print_list pp_loop_inv) invs
       pp_seqn s
   | VarAssignS (id, exp) ->
     fprintf ppf "@[<v 2>%s := %a@]"
@@ -216,6 +217,9 @@ and pp_fldacc ppf fldacc =
   | (exp1, id) ->
     fprintf ppf "@[(%a).%s@]" pp_exp exp1 id.it
 
+and pp_loop_inv ppf inv =
+    fprintf ppf "invariant %a" pp_exp inv
+
 let prog_mapped file p =
     marks := [];
     let b = Buffer.create 16 in

src/viper/trans.ml

@@ -88,6 +88,18 @@ let rec extract_invariants : item list -> (par -> invariants -> invariants) = fu
         :: extract_invariants p self es
   | _ :: p -> extract_invariants p
 
+let rec extract_loop_invariants (e : M.exp) : (M.exp list * M.exp) =
+  match e with
+  | { it = M.BlockE ds; _ } ->
+    let (invs, ds') = extract_loop_invariants' ds [] in
+    (invs, { e with it = M.BlockE ds' })
+  | _ -> ([], e)
+and extract_loop_invariants' (ds : M.dec list) (acc : M.exp list) : (M.exp list * M.dec list) =
+  match ds with
+  | M.({ it = ExpD ({ it = AssertE (Loop_invariant, inv); _ }); _ }) :: ds ->
+      extract_loop_invariants' ds (inv :: acc)
+  | _ -> (List.rev acc, ds)
+
 let rec extract_concurrency (seq : seqn) : stmt' list * seqn =
   let open List in
   let extr (concs, stmts) s : stmt' list * stmt list =
@@ -390,8 +402,10 @@ and stmt ctxt (s : M.exp) : seqn =
                               !!(MacroCall("$Inv", self ctxt at))))));
         ])
   | M.WhileE(e, s1) ->
+     let (invs, s1') = extract_loop_invariants s1 in
+     let invs' = List.map (fun inv -> exp ctxt inv) invs in
      !!([],
-        [ !!(WhileS(exp ctxt e, [], stmt ctxt s1)) ]) (* TODO: Invariant *)
+        [ !!(WhileS(exp ctxt e, invs', stmt ctxt s1')) ])
   | M.(AssignE({it = VarE x; _}, e2)) ->
      begin match Env.find x.it ctxt.ids with
      | Local ->

test/fail/ok/verification-asserts.tc.ok

@@ -8,3 +8,4 @@ verification-asserts.mo:7.8-7.17: syntax error [M0001], unexpected token 'invari
   invariant <exp_nest>
   func <exp_nest>
   <nat> : async <exp_nest>
+  loop : invariant <exp_nest>

test/fail/verification-asserts.mo

@@ -5,3 +5,4 @@ assert:return true;
 
 // `invariant` is a keyword in verification mode only
 assert:invariant true;
+assert:loop:invariant true;

test/viper/loop-invariant.mo

@@ -0,0 +1,15 @@
+// @verify
+
+actor LoopInvariant {
+  public func double(n : Int) : async Int {
+    var i : Int = 0;
+    var j : Int = 0;
+    while (i < n) {
+      assert:loop:invariant (i * 2 == j);
+      assert:loop:invariant (j - i == i);
+      i := i + 1;
+      j := j + 2;
+    };
+    return j;
+  };
+}

test/viper/ok/invariant.vpr.ok

@@ -34,9 +34,10 @@ method loops($Self: Ref)
     ensures $Inv($Self)
     { var i: Int
       i := 0
-      while ((i > 0)) {
+      while ((i > 0))
+
          { 
            i := (i + 1) 
-         }}
+         }
       label $Ret 
     }

test/viper/ok/loop-invariant.silicon.ok

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

test/viper/ok/loop-invariant.vpr.ok

@@ -0,0 +1,31 @@
+define $Perm($Self) (true)
+define $Inv($Self) (true)
+method __init__($Self: Ref)
+
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+
+    }
+method double($Self: Ref, n: Int)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { var i: Int
+      var j: Int
+      i := 0
+      j := 0
+      while ((i < n))
+         invariant ((i * 2) == j)
+         invariant ((j - i) == i)
+         { 
+           i := (i + 1)
+           j := (j + 2) 
+         }
+      $Res := j
+      goto $Ret
+      label $Ret 
+    }

test/viper/ok/simple-funs.vpr.ok

@@ -105,11 +105,12 @@ method factorial($Self: Ref, n: Int)
       var i: Int
       prod := 1
       i := n
-      while ((i > 0)) {
+      while ((i > 0))
+
          { 
            prod := (prod * i)
            i := (i - 1) 
-         }}
+         }
       $Res := prod
       goto $Ret
       label $Ret