motoko-san: fix locations for while loop invariants

serokell · Jun 17, 2024 · 4c1d28a · 4c1d28a
1 parent 34a6244
commit 4c1d28a
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 7 deletions.
diff --git a/src/viper/pretty.ml b/src/viper/pretty.ml
@@ -255,7 +255,8 @@ and pp_fldacc ppf fldacc =
     fprintf ppf "@[(%a).%s@]" pp_exp exp1 id.it
 
 and pp_loop_inv ppf inv =
-    fprintf ppf "invariant %a" pp_exp inv
+    marks := inv.at :: !marks;
+    fprintf ppf "\017invariant %a\019" pp_exp inv
 
 let prog_mapped file tuple_arities p =
     marks := [];

diff --git a/src/viper/trans.ml b/src/viper/trans.ml
@@ -138,8 +138,8 @@ let rec extract_loop_invariants (e : M.exp) : (M.exp list * M.exp) =
   | _ -> ([], 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)
+  | M.({ it = ExpD ({ it = AssertE (Loop_invariant, inv); at = assert_at; _ }); _ }) :: ds ->
+      extract_loop_invariants' ds ({ inv with at = assert_at } :: acc)
   | _ -> (List.rev acc, ds)
 
 let rec extract_concurrency (seq : seqn) : stmt' list * seqn =

diff --git a/test/viper/ok/reverse.vpr.ok b/test/viper/ok/reverse.vpr.ok
@@ -80,12 +80,13 @@ method reverseArray$Nat($Self: Ref, a: Array)
          invariant ((i < length) && (i >= 0))
          invariant ((j < length) && (j >= 0))
          invariant (i == (($size(a) - 1) - j))
-         invariant forall k : Int :: (((j <= k) && (k <= i)) ==> (($loc(a, k)).$int == 
-                   old(($loc(a, k)).$int)))
+         invariant forall k : Int :: (((j <= k) && (k <= i)) ==> (($loc(a,
+                                                                    k)).$int == 
+                    old(($loc(a, k)).$int)))
          invariant forall k : Int :: (((0 <= k) && (k < j)) ==> (($loc(a, k)).$int == 
-                   old(($loc(a, (($size(a) - 1) - k))).$int)))
+                    old(($loc(a, (($size(a) - 1) - k))).$int)))
          invariant forall k : Int :: (((i < k) && (k < $size(a))) ==> (
-                   ($loc(a, k)).$int == old(($loc(a, (($size(a) - 1) - k))).$int)))
+                    ($loc(a, k)).$int == old(($loc(a, (($size(a) - 1) - k))).$int)))
          invariant ($Perm($Self) && $Inv($Self))
          { var tmp: Int
            tmp := ($loc(a, i)).$int;