[motoko-san] bugfix: add parenthesis around quantifiers

Problem: `Forall(func i => i == i) ==> B` is translated as `forall i, i == i ==> B` that is wrong since involving `i` in the context of `B`.
serokell · Jun 24, 2024 · ff28427 · ff28427
1 parent 5f24a3c
commit ff28427
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 12 deletions.
diff --git a/src/viper/pretty.ml b/src/viper/pretty.ml
@@ -172,8 +172,8 @@ and pp_exp ppf exp =
     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
-  | ForallE (binders, exp) -> fprintf ppf "@[forall %a :: %a@]" (pp_print_list ~pp_sep:comma pp_binder) binders pp_exp exp
-  | ExistsE (binders, exp) -> fprintf ppf "@[exists %a :: %a@]" (pp_print_list ~pp_sep:comma pp_binder) binders pp_exp exp
+  | ForallE (binders, exp) -> fprintf ppf "@[(forall %a :: %a)@]" (pp_print_list ~pp_sep:comma pp_binder) binders pp_exp exp
+  | ExistsE (binders, exp) -> fprintf ppf "@[(exists %a :: %a)@]" (pp_print_list ~pp_sep:comma pp_binder) binders pp_exp exp
   | _ -> fprintf ppf "@[// pretty printer not implemented for node at %s@]" (string_of_region exp.at)
 
 and pp_perm ppf perm =

diff --git a/test/viper/ok/odd-even.vpr.ok b/test/viper/ok/odd-even.vpr.ok
@@ -38,7 +38,7 @@ method odd($Self: Ref, n: Int)
     requires ((n % 2) == 1)
     ensures $Perm($Self)
     { 
-      assert exists k : Int :: (((2 * k) + 1) == n);
+      assert (exists k : Int :: (((2 * k) + 1) == n));
       $Res := n;
       goto $Ret;
       label $Ret; 
@@ -49,7 +49,7 @@ method even($Self: Ref, n: Int)
     requires ((n % 2) == 0)
     ensures $Perm($Self)
     { 
-      assert exists k : Int :: ((2 * k) == n);
+      assert (exists k : Int :: ((2 * k) == n));
       $Res := n;
       goto $Ret;
       label $Ret; 

diff --git a/test/viper/ok/reverse.vpr.ok b/test/viper/ok/reverse.vpr.ok
@@ -51,8 +51,8 @@ method reverseArray$Nat($Self: Ref, a: Array)
     ensures $array_acc(a, $int, write)
     ensures ($size(($Self).xarray) == 5)
     ensures ($size(a) == old($size(a)))
-    ensures forall k : Int :: (((0 <= k) && (k < $size(a))) ==> (($loc(a, k)).$int == 
-            old(($loc(a, (($size(a) - 1) - k))).$int)))
+    ensures (forall k : Int :: (((0 <= k) && (k < $size(a))) ==> (($loc(a, k)).$int == 
+            old(($loc(a, (($size(a) - 1) - k))).$int))))
     { var b: Array
       var length: Int
       var i: Int
@@ -79,13 +79,15 @@ 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,
+         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)))
-         invariant forall k : Int :: (((i < k) && (k < $size(a))) ==> (
-                    ($loc(a, k)).$int == old(($loc(a, (($size(a) - 1) - 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))))
+         invariant (forall k : Int :: (((i < k) && (k < $size(a))) ==> (
+                    ($loc(a, k)).$int == old(($loc(a, (($size(a) - 1) - k))).$int))))
          { var tmp: Int
            tmp := ($loc(a, i)).$int;
            ($loc(a, i)).$int := ($loc(a, j)).$int;