From 61a7aafab4131b965a8053ddfbec9f31ad206ca7 Mon Sep 17 00:00:00 2001
From: Vladislav Zavialov <vlad.z.4096@gmail.com>
Date: Mon, 29 Apr 2024 21:26:52 +0300
Subject: [PATCH 1/6] motoko-san: add array prelude

---
 src/viper/prelude.ml                    | 17 +++++++++++++++++
 src/viper/pretty.ml                     |  3 ++-
 test/repl/ok/viper.stdout.ok            | 18 ++++++++++++++++++
 test/viper/ok/assertions.silicon.ok     |  4 ++--
 test/viper/ok/assertions.vpr.ok         | 18 ++++++++++++++++++
 test/viper/ok/async.silicon.ok          |  2 +-
 test/viper/ok/async.vpr.ok              | 18 ++++++++++++++++++
 test/viper/ok/claim-broken.silicon.ok   |  2 +-
 test/viper/ok/claim-broken.vpr.ok       | 18 ++++++++++++++++++
 test/viper/ok/claim-reward-naive.vpr.ok | 18 ++++++++++++++++++
 test/viper/ok/claim-simple.silicon.ok   |  2 +-
 test/viper/ok/claim-simple.vpr.ok       | 18 ++++++++++++++++++
 test/viper/ok/claim.vpr.ok              | 18 ++++++++++++++++++
 test/viper/ok/counter.silicon.ok        |  2 +-
 test/viper/ok/counter.vpr.ok            | 18 ++++++++++++++++++
 test/viper/ok/invariant.silicon.ok      |  2 +-
 test/viper/ok/invariant.vpr.ok          | 18 ++++++++++++++++++
 test/viper/ok/loop-invariant.silicon.ok |  4 ++--
 test/viper/ok/loop-invariant.vpr.ok     | 18 ++++++++++++++++++
 test/viper/ok/method-call.silicon.ok    |  4 ++--
 test/viper/ok/method-call.vpr.ok        | 18 ++++++++++++++++++
 test/viper/ok/nats.silicon.ok           |  2 +-
 test/viper/ok/nats.vpr.ok               | 18 ++++++++++++++++++
 test/viper/ok/private.vpr.ok            | 18 ++++++++++++++++++
 test/viper/ok/simple-funs.silicon.ok    |  4 ++--
 test/viper/ok/simple-funs.vpr.ok        | 18 ++++++++++++++++++
 26 files changed, 285 insertions(+), 15 deletions(-)
 create mode 100644 src/viper/prelude.ml

diff --git a/src/viper/prelude.ml b/src/viper/prelude.ml
new file mode 100644
index 00000000000..c0367f8c590
--- /dev/null
+++ b/src/viper/prelude.ml
@@ -0,0 +1,17 @@
+let prelude : string = {prelude|/* BEGIN PRELUDE */
+domain Array {
+  function $loc(a: Array, i: Int): Ref
+  function $size(a: Array): Int
+  function $first(r: Ref): Array
+  function $second(r: Ref): Int
+  axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i }
+  axiom $size_nonneg { forall a: Array :: $size(a) >= 0 }
+}
+define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t)
+define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2)
+define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+field $int: Int
+field $bool: Bool
+field $ref: Ref
+field $array: Array
+/* END PRELUDE */|prelude}
\ No newline at end of file
diff --git a/src/viper/pretty.ml b/src/viper/pretty.ml
index 5e251eb6c06..a91570b863a 100644
--- a/src/viper/pretty.ml
+++ b/src/viper/pretty.ml
@@ -1,5 +1,6 @@
 open Source
 open Syntax
+open Prelude
 
 open Format
 
@@ -213,7 +214,7 @@ let prog_mapped file p =
     marks := [];
     let b = Buffer.create 16 in
     let ppf = Format.formatter_of_buffer b in
-    Format.fprintf ppf "@[%a@]" pp_prog p;
+    Format.fprintf ppf "@[%s@]@.@.@[%a@]" prelude pp_prog p;
     Format.pp_print_flush ppf ();
     let in_file { left; right } =
       let left, right = { left with file }, { right with file } in
diff --git a/test/repl/ok/viper.stdout.ok b/test/repl/ok/viper.stdout.ok
index 098fbe22369..9104ff7b7bd 100644
--- a/test/repl/ok/viper.stdout.ok
+++ b/test/repl/ok/viper.stdout.ok
@@ -1,3 +1,21 @@
+/* BEGIN PRELUDE */
+domain Array {
+  function $loc(a: Array, i: Int): Ref
+  function $size(a: Array): Int
+  function $first(r: Ref): Array
+  function $second(r: Ref): Int
+  axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i }
+  axiom $size_nonneg { forall a: Array :: $size(a) >= 0 }
+}
+define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t)
+define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2)
+define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+field $int: Int
+field $bool: Bool
+field $ref: Ref
+field $array: Array
+/* END PRELUDE */
+
 field $message_async: Int
 define $Perm($Self) ((((true && acc(($Self).claimed,write)) && acc(($Self).count,write)) && 
   acc(($Self).$message_async,write)))
diff --git a/test/viper/ok/assertions.silicon.ok b/test/viper/ok/assertions.silicon.ok
index 202af03d0c2..032e89077dc 100644
--- a/test/viper/ok/assertions.silicon.ok
+++ b/test/viper/ok/assertions.silicon.ok
@@ -1,2 +1,2 @@
-  [0] Postcondition of __init__ might not hold. Assertion $Self.u might not hold. (assertions.vpr@10.13--10.24)
-  [1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. (assertions.vpr@28.15--28.44)
+  [0] Postcondition of __init__ might not hold. Assertion $Self.u might not hold. (assertions.vpr@28.13--28.24)
+  [1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. (assertions.vpr@46.15--46.44)
diff --git a/test/viper/ok/assertions.vpr.ok b/test/viper/ok/assertions.vpr.ok
index a82bb5216f9..27469915b21 100644
--- a/test/viper/ok/assertions.vpr.ok
+++ b/test/viper/ok/assertions.vpr.ok
@@ -1,3 +1,21 @@
+/* BEGIN PRELUDE */
+domain Array {
+  function $loc(a: Array, i: Int): Ref
+  function $size(a: Array): Int
+  function $first(r: Ref): Array
+  function $second(r: Ref): Int
+  axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i }
+  axiom $size_nonneg { forall a: Array :: $size(a) >= 0 }
+}
+define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t)
+define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2)
+define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+field $int: Int
+field $bool: Bool
+field $ref: Ref
+field $array: Array
+/* END PRELUDE */
+
 field $message_async: Int
 define $Perm($Self) ((((true && acc(($Self).u,write)) && acc(($Self).v,write)) && 
   acc(($Self).$message_async,write)))
diff --git a/test/viper/ok/async.silicon.ok b/test/viper/ok/async.silicon.ok
index 4cd9741c5a2..88be506c084 100644
--- a/test/viper/ok/async.silicon.ok
+++ b/test/viper/ok/async.silicon.ok
@@ -1 +1 @@
-  [0] Exhale might fail. Assertion $Self.$message_async <= 1 might not hold. (async.vpr@33.15--33.42)
+  [0] Exhale might fail. Assertion $Self.$message_async <= 1 might not hold. (async.vpr@51.15--51.42)
diff --git a/test/viper/ok/async.vpr.ok b/test/viper/ok/async.vpr.ok
index 8e10ad1f324..f7980e0c6b2 100644
--- a/test/viper/ok/async.vpr.ok
+++ b/test/viper/ok/async.vpr.ok
@@ -1,3 +1,21 @@
+/* BEGIN PRELUDE */
+domain Array {
+  function $loc(a: Array, i: Int): Ref
+  function $size(a: Array): Int
+  function $first(r: Ref): Array
+  function $second(r: Ref): Int
+  axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i }
+  axiom $size_nonneg { forall a: Array :: $size(a) >= 0 }
+}
+define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t)
+define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2)
+define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+field $int: Int
+field $bool: Bool
+field $ref: Ref
+field $array: Array
+/* END PRELUDE */
+
 field $message_async_4: Int
 field $message_async_2: Int
 field $message_async: Int
diff --git a/test/viper/ok/claim-broken.silicon.ok b/test/viper/ok/claim-broken.silicon.ok
index 2738a3acfa7..319c328500b 100644
--- a/test/viper/ok/claim-broken.silicon.ok
+++ b/test/viper/ok/claim-broken.silicon.ok
@@ -1 +1 @@
-  [0] Exhale might fail. Assertion $Self.$message_async == 1 ==> $Self.claimed && $Self.count == 0 might not hold. (claim-broken.vpr@31.20--31.47)
+  [0] Exhale might fail. Assertion $Self.$message_async == 1 ==> $Self.claimed && $Self.count == 0 might not hold. (claim-broken.vpr@49.20--49.47)
diff --git a/test/viper/ok/claim-broken.vpr.ok b/test/viper/ok/claim-broken.vpr.ok
index 2f9e89edf51..4e1ab2d9f8d 100644
--- a/test/viper/ok/claim-broken.vpr.ok
+++ b/test/viper/ok/claim-broken.vpr.ok
@@ -1,3 +1,21 @@
+/* BEGIN PRELUDE */
+domain Array {
+  function $loc(a: Array, i: Int): Ref
+  function $size(a: Array): Int
+  function $first(r: Ref): Array
+  function $second(r: Ref): Int
+  axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i }
+  axiom $size_nonneg { forall a: Array :: $size(a) >= 0 }
+}
+define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t)
+define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2)
+define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+field $int: Int
+field $bool: Bool
+field $ref: Ref
+field $array: Array
+/* END PRELUDE */
+
 field $message_async: Int
 define $Perm($Self) ((((true && acc(($Self).claimed,write)) && acc(($Self).count,write)) && 
   acc(($Self).$message_async,write)))
diff --git a/test/viper/ok/claim-reward-naive.vpr.ok b/test/viper/ok/claim-reward-naive.vpr.ok
index e2a098d0378..b64d52eee79 100644
--- a/test/viper/ok/claim-reward-naive.vpr.ok
+++ b/test/viper/ok/claim-reward-naive.vpr.ok
@@ -1,3 +1,21 @@
+/* BEGIN PRELUDE */
+domain Array {
+  function $loc(a: Array, i: Int): Ref
+  function $size(a: Array): Int
+  function $first(r: Ref): Array
+  function $second(r: Ref): Int
+  axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i }
+  axiom $size_nonneg { forall a: Array :: $size(a) >= 0 }
+}
+define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t)
+define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2)
+define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+field $int: Int
+field $bool: Bool
+field $ref: Ref
+field $array: Array
+/* END PRELUDE */
+
 define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write)))
 define $Inv($Self) (invariant_5($Self))
 method __init__($Self: Ref)
diff --git a/test/viper/ok/claim-simple.silicon.ok b/test/viper/ok/claim-simple.silicon.ok
index c704b94e8c8..0f575b37f8d 100644
--- a/test/viper/ok/claim-simple.silicon.ok
+++ b/test/viper/ok/claim-simple.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (claim-simple.vpr@2.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (claim-simple.vpr@20.1)
diff --git a/test/viper/ok/claim-simple.vpr.ok b/test/viper/ok/claim-simple.vpr.ok
index b26442befcf..859c7e93588 100644
--- a/test/viper/ok/claim-simple.vpr.ok
+++ b/test/viper/ok/claim-simple.vpr.ok
@@ -1,3 +1,21 @@
+/* BEGIN PRELUDE */
+domain Array {
+  function $loc(a: Array, i: Int): Ref
+  function $size(a: Array): Int
+  function $first(r: Ref): Array
+  function $second(r: Ref): Int
+  axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i }
+  axiom $size_nonneg { forall a: Array :: $size(a) >= 0 }
+}
+define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t)
+define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2)
+define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+field $int: Int
+field $bool: Bool
+field $ref: Ref
+field $array: Array
+/* END PRELUDE */
+
 define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write)))
 define $Inv($Self) (true)
 method __init__($Self: Ref)
diff --git a/test/viper/ok/claim.vpr.ok b/test/viper/ok/claim.vpr.ok
index 2a99877bfe9..e9f284e382d 100644
--- a/test/viper/ok/claim.vpr.ok
+++ b/test/viper/ok/claim.vpr.ok
@@ -1,3 +1,21 @@
+/* BEGIN PRELUDE */
+domain Array {
+  function $loc(a: Array, i: Int): Ref
+  function $size(a: Array): Int
+  function $first(r: Ref): Array
+  function $second(r: Ref): Int
+  axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i }
+  axiom $size_nonneg { forall a: Array :: $size(a) >= 0 }
+}
+define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t)
+define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2)
+define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+field $int: Int
+field $bool: Bool
+field $ref: Ref
+field $array: Array
+/* END PRELUDE */
+
 field $message_async: Int
 define $Perm($Self) ((((true && acc(($Self).claimed,write)) && acc(($Self).count,write)) && 
   acc(($Self).$message_async,write)))
diff --git a/test/viper/ok/counter.silicon.ok b/test/viper/ok/counter.silicon.ok
index 69fb8c629a0..9af3e35204a 100644
--- a/test/viper/ok/counter.silicon.ok
+++ b/test/viper/ok/counter.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (counter.vpr@2.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (counter.vpr@20.1)
diff --git a/test/viper/ok/counter.vpr.ok b/test/viper/ok/counter.vpr.ok
index 5196861d655..4fef56e0a8e 100644
--- a/test/viper/ok/counter.vpr.ok
+++ b/test/viper/ok/counter.vpr.ok
@@ -1,3 +1,21 @@
+/* BEGIN PRELUDE */
+domain Array {
+  function $loc(a: Array, i: Int): Ref
+  function $size(a: Array): Int
+  function $first(r: Ref): Array
+  function $second(r: Ref): Int
+  axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i }
+  axiom $size_nonneg { forall a: Array :: $size(a) >= 0 }
+}
+define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t)
+define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2)
+define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+field $int: Int
+field $bool: Bool
+field $ref: Ref
+field $array: Array
+/* END PRELUDE */
+
 define $Perm($Self) ((true && acc(($Self).count,write)))
 define $Inv($Self) (true)
 method __init__($Self: Ref)
diff --git a/test/viper/ok/invariant.silicon.ok b/test/viper/ok/invariant.silicon.ok
index 94a1ad16eff..c8f4e03fb6d 100644
--- a/test/viper/ok/invariant.silicon.ok
+++ b/test/viper/ok/invariant.silicon.ok
@@ -1 +1 @@
-  [0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. (invariant.vpr@7.13--7.24)
+  [0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. (invariant.vpr@25.13--25.24)
diff --git a/test/viper/ok/invariant.vpr.ok b/test/viper/ok/invariant.vpr.ok
index 4db1a7a12b5..e1b7f6e38d0 100644
--- a/test/viper/ok/invariant.vpr.ok
+++ b/test/viper/ok/invariant.vpr.ok
@@ -1,3 +1,21 @@
+/* BEGIN PRELUDE */
+domain Array {
+  function $loc(a: Array, i: Int): Ref
+  function $size(a: Array): Int
+  function $first(r: Ref): Array
+  function $second(r: Ref): Int
+  axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i }
+  axiom $size_nonneg { forall a: Array :: $size(a) >= 0 }
+}
+define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t)
+define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2)
+define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+field $int: Int
+field $bool: Bool
+field $ref: Ref
+field $array: Array
+/* END PRELUDE */
+
 define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write)))
 define $Inv($Self) (((invariant_9($Self) && invariant_10($Self)) && invariant_11($Self)))
 method __init__($Self: Ref)
diff --git a/test/viper/ok/loop-invariant.silicon.ok b/test/viper/ok/loop-invariant.silicon.ok
index d7ae1e8621c..ea4b44a4b95 100644
--- a/test/viper/ok/loop-invariant.silicon.ok
+++ b/test/viper/ok/loop-invariant.silicon.ok
@@ -1,2 +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)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (loop-invariant.vpr@19.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (loop-invariant.vpr@20.1)
diff --git a/test/viper/ok/loop-invariant.vpr.ok b/test/viper/ok/loop-invariant.vpr.ok
index d222eeac074..eb473412f89 100644
--- a/test/viper/ok/loop-invariant.vpr.ok
+++ b/test/viper/ok/loop-invariant.vpr.ok
@@ -1,3 +1,21 @@
+/* BEGIN PRELUDE */
+domain Array {
+  function $loc(a: Array, i: Int): Ref
+  function $size(a: Array): Int
+  function $first(r: Ref): Array
+  function $second(r: Ref): Int
+  axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i }
+  axiom $size_nonneg { forall a: Array :: $size(a) >= 0 }
+}
+define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t)
+define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2)
+define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+field $int: Int
+field $bool: Bool
+field $ref: Ref
+field $array: Array
+/* END PRELUDE */
+
 define $Perm($Self) (true)
 define $Inv($Self) (true)
 method __init__($Self: Ref)
diff --git a/test/viper/ok/method-call.silicon.ok b/test/viper/ok/method-call.silicon.ok
index 05a4c452841..8aa6cc1649a 100644
--- a/test/viper/ok/method-call.silicon.ok
+++ b/test/viper/ok/method-call.silicon.ok
@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (method-call.vpr@1.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (method-call.vpr@2.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (method-call.vpr@19.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (method-call.vpr@20.1)
diff --git a/test/viper/ok/method-call.vpr.ok b/test/viper/ok/method-call.vpr.ok
index 8cdce6e4f7d..b19574c5ba0 100644
--- a/test/viper/ok/method-call.vpr.ok
+++ b/test/viper/ok/method-call.vpr.ok
@@ -1,3 +1,21 @@
+/* BEGIN PRELUDE */
+domain Array {
+  function $loc(a: Array, i: Int): Ref
+  function $size(a: Array): Int
+  function $first(r: Ref): Array
+  function $second(r: Ref): Int
+  axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i }
+  axiom $size_nonneg { forall a: Array :: $size(a) >= 0 }
+}
+define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t)
+define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2)
+define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+field $int: Int
+field $bool: Bool
+field $ref: Ref
+field $array: Array
+/* END PRELUDE */
+
 define $Perm($Self) (true)
 define $Inv($Self) (true)
 method __init__($Self: Ref)
diff --git a/test/viper/ok/nats.silicon.ok b/test/viper/ok/nats.silicon.ok
index 1671de8e2f8..ec7e3600186 100644
--- a/test/viper/ok/nats.silicon.ok
+++ b/test/viper/ok/nats.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (nats.vpr@2.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (nats.vpr@20.1)
diff --git a/test/viper/ok/nats.vpr.ok b/test/viper/ok/nats.vpr.ok
index 472e810081c..082dd24aa0f 100644
--- a/test/viper/ok/nats.vpr.ok
+++ b/test/viper/ok/nats.vpr.ok
@@ -1,3 +1,21 @@
+/* BEGIN PRELUDE */
+domain Array {
+  function $loc(a: Array, i: Int): Ref
+  function $size(a: Array): Int
+  function $first(r: Ref): Array
+  function $second(r: Ref): Int
+  axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i }
+  axiom $size_nonneg { forall a: Array :: $size(a) >= 0 }
+}
+define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t)
+define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2)
+define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+field $int: Int
+field $bool: Bool
+field $ref: Ref
+field $array: Array
+/* END PRELUDE */
+
 define $Perm($Self) ((true && acc(($Self).x,write)))
 define $Inv($Self) (true)
 method __init__($Self: Ref)
diff --git a/test/viper/ok/private.vpr.ok b/test/viper/ok/private.vpr.ok
index ac51b18d3e4..582bc5a5a1f 100644
--- a/test/viper/ok/private.vpr.ok
+++ b/test/viper/ok/private.vpr.ok
@@ -1,3 +1,21 @@
+/* BEGIN PRELUDE */
+domain Array {
+  function $loc(a: Array, i: Int): Ref
+  function $size(a: Array): Int
+  function $first(r: Ref): Array
+  function $second(r: Ref): Int
+  axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i }
+  axiom $size_nonneg { forall a: Array :: $size(a) >= 0 }
+}
+define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t)
+define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2)
+define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+field $int: Int
+field $bool: Bool
+field $ref: Ref
+field $array: Array
+/* END PRELUDE */
+
 define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write)))
 define $Inv($Self) (invariant_7($Self))
 method __init__($Self: Ref)
diff --git a/test/viper/ok/simple-funs.silicon.ok b/test/viper/ok/simple-funs.silicon.ok
index d0c64d57d11..e104157e47e 100644
--- a/test/viper/ok/simple-funs.silicon.ok
+++ b/test/viper/ok/simple-funs.silicon.ok
@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (simple-funs.vpr@1.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (simple-funs.vpr@2.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (simple-funs.vpr@19.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (simple-funs.vpr@20.1)
diff --git a/test/viper/ok/simple-funs.vpr.ok b/test/viper/ok/simple-funs.vpr.ok
index 81d6dcc7626..eda789b59e5 100644
--- a/test/viper/ok/simple-funs.vpr.ok
+++ b/test/viper/ok/simple-funs.vpr.ok
@@ -1,3 +1,21 @@
+/* BEGIN PRELUDE */
+domain Array {
+  function $loc(a: Array, i: Int): Ref
+  function $size(a: Array): Int
+  function $first(r: Ref): Array
+  function $second(r: Ref): Int
+  axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i }
+  axiom $size_nonneg { forall a: Array :: $size(a) >= 0 }
+}
+define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t)
+define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2)
+define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+field $int: Int
+field $bool: Bool
+field $ref: Ref
+field $array: Array
+/* END PRELUDE */
+
 define $Perm($Self) (true)
 define $Inv($Self) (true)
 method __init__($Self: Ref)

From 1b1bc54449e264350e447c3b9810b68347ee4e71 Mon Sep 17 00:00:00 2001
From: Vladislav Zavialov <vlad.z.4096@gmail.com>
Date: Mon, 29 Apr 2024 22:09:43 +0300
Subject: [PATCH 2/6] motoko-san: assign_stmt -> assign_stmts

---
 src/viper/trans.ml | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/viper/trans.ml b/src/viper/trans.ml
index 562e9dfd2cf..0899a882f9d 100644
--- a/src/viper/trans.ml
+++ b/src/viper/trans.ml
@@ -322,12 +322,12 @@ and dec ctxt d =
     { ctxt with ids = Env.add x.it Local ctxt.ids },
     fun ctxt' ->
       ([ !!(id x, tr_typ e.note.M.note_typ) ],
-       [ !!(assign_stmt ctxt' (id x) e) ])
+       assign_stmts ctxt' d.at (id x) e)
   | M.(LetD ({it=VarP x;_}, e, None)) ->
      { ctxt with ids = Env.add x.it Local ctxt.ids },
      fun ctxt' ->
        ([ !!(id x, tr_typ e.note.M.note_typ) ],
-        [ !!(assign_stmt ctxt' (id x) e) ])
+        assign_stmts ctxt' d.at (id x) e)
   | M.(ExpD e) -> (* TODO: restrict to e of unit type? *)
      (ctxt,
       fun ctxt' ->
@@ -414,7 +414,7 @@ and stmt ctxt (s : M.exp) : seqn =
      begin match Env.find x.it ctxt.ids with
      | Local ->
         let loc = !!! (x.at) (x.it) in
-        !!([], [!!(assign_stmt ctxt loc e2)])
+        !!([], assign_stmts ctxt s.at loc e2)
      | Field ->
        let fld = (self ctxt x.at, id x) in
        !!([],
@@ -444,19 +444,19 @@ and stmt ctxt (s : M.exp) : seqn =
        self_var :: call_args ctxt args))])
   | M.RetE e ->
      !!([],
-        [ !!(assign_stmt ctxt (!!! (Source.no_region) "$Res") e);
-          !!(GotoS(!!! (Source.no_region) "$Ret"))
-        ])
+        assign_stmts ctxt s.at (!!! (Source.no_region) "$Res") e
+        @ [ !!(GotoS(!!! (Source.no_region) "$Ret")) ])
   | _ ->
      unsupported s.at (Arrange.exp s)
 
-and assign_stmt ctxt x e =
+and assign_stmts ctxt at x e =
+  let (!!) p = !!! at p in
   match e with
   | M.({it = CallE({it = VarE m; _}, inst, args); _}) ->
-    MethodCallS ([x], id m,
-      let self_var = self ctxt m.at in
-      self_var :: call_args ctxt args)
-  | _ -> VarAssignS(x, exp ctxt e)
+    [ !!(MethodCallS ([x], id m,
+          let self_var = self ctxt m.at in
+          self_var :: call_args ctxt args)) ]
+  | _ -> [ !!(VarAssignS(x, exp ctxt e)) ]
 
 and call_args ctxt e =
   match e with

From 6d1add9963092d783c102532b9d3808a94074a87 Mon Sep 17 00:00:00 2001
From: Vladislav Zavialov <vlad.z.4096@gmail.com>
Date: Mon, 29 Apr 2024 23:07:01 +0300
Subject: [PATCH 3/6] motoko-san: refactor perm/init collection

---
 src/viper/trans.ml | 45 +++++++++++++++++++++++++--------------------
 1 file changed, 25 insertions(+), 20 deletions(-)

diff --git a/src/viper/trans.ml b/src/viper/trans.ml
index 0899a882f9d..a7b8ee01a8e 100644
--- a/src/viper/trans.ml
+++ b/src/viper/trans.ml
@@ -56,6 +56,11 @@ let rec adjoin ctxt e = function
   | f :: fs -> f ctxt (adjoin ctxt e fs)
 
 
+let (|:) (x_opt : 'a option) (xs : 'a list) : 'a list =
+  match x_opt with
+  | None -> xs
+  | Some(x) -> x :: xs
+
 (* exception for reporting unsupported Motoko syntax *)
 exception Unsupported of Source.region * string
 
@@ -134,7 +139,7 @@ and unit' (u : M.comp_unit) : prog =
   match body.it with
   | M.ActorU(id_opt, decs) ->
     let ctxt = { self = None; ids = Env.empty; ghost_items = ref []; ghost_inits = ref []; ghost_perms = ref []; ghost_conc = ref [] } in
-    let ctxt', inits, mk_is = dec_fields ctxt decs in
+    let ctxt', perms, inits, mk_is = dec_fields ctxt decs in
     let is' = List.map (fun mk_i -> mk_i ctxt') mk_is in
     (* given is', compute ghost_is *)
     let ghost_is = List.map (fun mk_i -> mk_i ctxt') !(ctxt.ghost_items) in
@@ -142,23 +147,16 @@ and unit' (u : M.comp_unit) : prog =
     let self_id = !!! (Source.no_region) "$Self" in
     let self_typ = !!! (self_id.at) RefT in
     let ctxt'' = { ctxt' with self = Some self_id.it } in
-    let perms = List.map (fun (id, _) -> fun (at : region) ->
-       (accE at (self ctxt'' at, id))) inits in
-    let ghost_perms = List.map (fun mk_p -> mk_p ctxt'') !(ctxt.ghost_perms) in
     let perm =
       fun (at : region) ->
        List.fold_left
          (fun pexp -> fun p_fn ->
-           !!! at (AndE(pexp, p_fn at)))
+           !!! at (AndE(pexp, p_fn ctxt'' at)))
          (!!! at (BoolLitE true))
-         (perms @ ghost_perms)
+         (perms @ !(ctxt.ghost_perms))
     in
     (* Add initializer *)
-    let init_list = List.map (fun (id, init) ->
-        !!! { left = id.at.left; right = init.at.right }
-          (FieldAssignS((self ctxt'' init.at, id), exp ctxt'' init)))
-        inits in
-    let init_list = init_list @ List.map (fun mk_s -> mk_s ctxt'') !(ctxt.ghost_inits) in
+    let init_list = List.map (fun mk_s -> mk_s ctxt'') (inits @ !(ctxt.ghost_inits)) in
     let init_body =
       !!! (body.at) ([], init_list)(* ATG: Is this the correct position? *)
     in
@@ -215,15 +213,16 @@ and unit' (u : M.comp_unit) : prog =
 and dec_fields (ctxt : ctxt) (ds : M.dec_field list) =
   match ds with
   | [] ->
-    (ctxt, [], [])
+    (ctxt, [], [], [])
   | d :: ds ->
-    let ctxt, init, mk_i = dec_field ctxt d in
-    let ctxt, inits, mk_is = dec_fields ctxt ds in
-    (ctxt, (match init with Some i -> i::inits | _ -> inits), mk_i::mk_is)
+    let ctxt, perm, init, mk_i = dec_field ctxt d in
+    let ctxt, perms, inits, mk_is = dec_fields ctxt ds in
+    (ctxt, perm |: perms, init |: inits, mk_i::mk_is)
 
 and dec_field ctxt d =
-  let ctxt, init, mk_i = dec_field' ctxt d.it in
+  let ctxt, perm, init, mk_i = dec_field' ctxt d.it in
    (ctxt,
+    perm,
     init,
     fun ctxt' ->
       let (i, info) = mk_i ctxt' in
@@ -233,7 +232,10 @@ and dec_field' ctxt d =
   match d.M.dec.it with
   | M.VarD (x, e) ->
       { ctxt with ids = Env.add x.it Field ctxt.ids },
-      Some (id x, e),
+      Some(fun ctxt' (at : region) -> (accE at (self ctxt' at, id x))),
+      Some(fun ctxt' ->
+        !!! { left = x.at.left; right = e.at.right }
+          (FieldAssignS((self ctxt' e.at, id x), exp ctxt' e))),
       fun ctxt' ->
         (FieldI(id x, tr_typ e.note.M.note_typ),
         NoInfo)
@@ -242,7 +244,8 @@ and dec_field' ctxt d =
              {it=FuncE(x, sp, tp, p, t_opt, sugar,
              {it = AsyncE (T.Fut, _, e); _} );_}, None)) -> (* ignore async *)
       { ctxt with ids = Env.add f.it Method ctxt.ids },
-      None,
+      None, (* no perm *)
+      None, (* no init *)
       fun ctxt' ->
         let open Either in
         let self_id = !!! (Source.no_region) "$Self" in
@@ -263,7 +266,8 @@ and dec_field' ctxt d =
              {it=FuncE(x, sp, tp, p, t_opt, sugar, e );_},
              None)) ->
       { ctxt with ids = Env.add f.it Method ctxt.ids },
-      None,
+      None, (* no perm *)
+      None, (* no init *)
       fun ctxt' ->
         let open Either in
         let self_id = !!! (Source.no_region) "$Self" in
@@ -281,7 +285,8 @@ and dec_field' ctxt d =
         PrivateFunction f.it)
   | M.(ExpD { it = AssertE (Invariant, e); at; _ }) ->
       ctxt,
-      None,
+      None, (* no perm *)
+      None, (* no init *)
       fun ctxt' ->
         (InvariantI (Printf.sprintf "invariant_%d" at.left.line, exp { ctxt' with self = Some "$Self" }  e), NoInfo)
   | _ ->

From 4107ff2cf07fe33480c919e15698fbf19bdf71c1 Mon Sep 17 00:00:00 2001
From: Vladislav Zavialov <vlad.z.4096@gmail.com>
Date: Mon, 29 Apr 2024 23:12:02 +0300
Subject: [PATCH 4/6] motoko-san: multi-param macro calls

---
 src/viper/pretty.ml |  4 ++--
 src/viper/syntax.ml |  2 +-
 src/viper/trans.ml  | 28 ++++++++++++++--------------
 3 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/src/viper/pretty.ml b/src/viper/pretty.ml
index a91570b863a..b4092e018c5 100644
--- a/src/viper/pretty.ml
+++ b/src/viper/pretty.ml
@@ -100,8 +100,8 @@ and pp_exp ppf exp =
      fprintf ppf "%s" id.it
   | FldAcc fldacc ->
      pp_fldacc ppf fldacc
-  | MacroCall (m, e) ->
-     fprintf ppf "@[%s(%a)@]" m pp_exp e
+  | MacroCall (m, es) ->
+     fprintf ppf "@[%s(%a)@]" m (pp_print_list pp_exp ~pp_sep:comma) es
   | NotE e ->
      fprintf ppf "@[(!%a)@]" pp_exp e
   | MinusE e ->
diff --git a/src/viper/syntax.ml b/src/viper/syntax.ml
index 3c4517c4986..890790f0fd5 100644
--- a/src/viper/syntax.ml
+++ b/src/viper/syntax.ml
@@ -49,7 +49,7 @@ and exp' =
   | FldAcc of fldacc
   | PermE of perm          (* perm_amount *)
   | AccE of fldacc * exp   (* acc((rcvr: exp).field, (exp: perm_amount)) *)
-  | MacroCall of string * exp
+  | MacroCall of string * exp list
 
 and perm = (perm', info) Source.annotated_phrase
 
diff --git a/src/viper/trans.ml b/src/viper/trans.ml
index a7b8ee01a8e..bd45e62ab00 100644
--- a/src/viper/trans.ml
+++ b/src/viper/trans.ml
@@ -89,7 +89,7 @@ let rec extract_invariants : item list -> (par -> invariants -> invariants) = fu
   | [] -> fun _ x -> x
   | { it = InvariantI (s, e); at; _ } :: p ->
       fun self es ->
-        !!! at (MacroCall(s, !!! at (LocalVar (fst self, snd self))))
+        !!! at (MacroCall(s, [ !!! at (LocalVar (fst self, snd self)) ]))
         :: extract_invariants p self es
   | _ :: p -> extract_invariants p
 
@@ -170,8 +170,8 @@ and unit' (u : M.comp_unit) : prog =
       (^^^)
         at
         (MethodI (id, ins, outs,
-          !!! at (MacroCall("$Perm", self ctxt'' at))::pres,
-          !!! at (MacroCall("$Perm", self ctxt'' at))::posts,
+          !!! at (MacroCall("$Perm", [self ctxt'' at]))::pres,
+          !!! at (MacroCall("$Perm", [self ctxt'' at]))::posts,
           body))
         note
       | x -> x) is'' in
@@ -186,7 +186,7 @@ and unit' (u : M.comp_unit) : prog =
         at
         (MethodI(id, ins, outs,
           pres,
-          posts @ [!!! at (MacroCall("$Inv", self ctxt'' at))],
+          posts @ [!!! at (MacroCall("$Inv", [self ctxt'' at]))],
           body))
         ActorInit
       )
@@ -197,8 +197,8 @@ and unit' (u : M.comp_unit) : prog =
       } -> ((^^^)
         at
         (MethodI(id, ins, outs,
-          pres @ [!!! at (MacroCall("$Inv", self ctxt'' at))],
-          posts @ [!!! at (MacroCall("$Inv", self ctxt'' at))],
+          pres @ [!!! at (MacroCall("$Inv", [self ctxt'' at]))],
+          posts @ [!!! at (MacroCall("$Inv", [self ctxt'' at]))],
           body))
         (PublicFunction x)
       )
@@ -391,13 +391,13 @@ and stmt ctxt (s : M.exp) : seqn =
             (self ctxt Source.no_region, !!id),
             (!!(AddE(!!(FldAcc (self ctxt (s.at), !!id)),
                      intLitE Source.no_region 1)))));
-          !@(ExhaleS (!@(AndE(!@(MacroCall("$Perm", self ctxt at)),
-                              !@(MacroCall("$Inv", self ctxt at))))));
+          !@(ExhaleS (!@(AndE(!@(MacroCall("$Perm", [self ctxt at])),
+                              !@(MacroCall("$Inv", [self ctxt at]))))));
           !@(SeqnS (
               !@([],
                  [
-                   !@(InhaleS (!@(AndE(!@(MacroCall("$Perm", self ctxt at)),
-                                  !@(AndE(!@(MacroCall("$Inv", self ctxt at)),
+                   !@(InhaleS (!@(AndE(!@(MacroCall("$Perm", [self ctxt at])),
+                                  !@(AndE(!@(MacroCall("$Inv", [self ctxt at])),
                                           !@(GtCmpE(!@(FldAcc (self ctxt at, !@id)),
                                                intLitE Source.no_region 0))))))));
                    !@(FieldAssignS(
@@ -405,10 +405,10 @@ and stmt ctxt (s : M.exp) : seqn =
                           (!@(SubE(!@(FldAcc (self ctxt at, !@id)),
                                    intLitE at 1)))));
                    !!! (e.at) (SeqnS stmts);
-                   !@(ExhaleS (!@(AndE(!@(MacroCall("$Perm", self ctxt at)),
-                                       !@(MacroCall("$Inv", self ctxt at)))))) ])));
-          !!(InhaleS (!!(AndE(!!(MacroCall("$Perm", self ctxt at)),
-                              !!(MacroCall("$Inv", self ctxt at))))));
+                   !@(ExhaleS (!@(AndE(!@(MacroCall("$Perm", [self ctxt at])),
+                                       !@(MacroCall("$Inv", [self ctxt at])))))) ])));
+          !!(InhaleS (!!(AndE(!!(MacroCall("$Perm", [self ctxt at])),
+                              !!(MacroCall("$Inv", [self ctxt at]))))));
         ])
   | M.WhileE(e, s1) ->
      let (invs, s1') = extract_loop_invariants s1 in

From 660e2adb0e8844c12f7020f695b8ef4aff4466bb Mon Sep 17 00:00:00 2001
From: Vladislav Zavialov <vlad.z.4096@gmail.com>
Date: Mon, 29 Apr 2024 23:35:41 +0300
Subject: [PATCH 5/6] motoko-san: MacroCall -> CallE

---
 src/viper/pretty.ml |  2 +-
 src/viper/syntax.ml |  2 +-
 src/viper/trans.ml  | 28 ++++++++++++++--------------
 3 files changed, 16 insertions(+), 16 deletions(-)

diff --git a/src/viper/pretty.ml b/src/viper/pretty.ml
index b4092e018c5..9ab5975c774 100644
--- a/src/viper/pretty.ml
+++ b/src/viper/pretty.ml
@@ -100,7 +100,7 @@ and pp_exp ppf exp =
      fprintf ppf "%s" id.it
   | FldAcc fldacc ->
      pp_fldacc ppf fldacc
-  | MacroCall (m, es) ->
+  | CallE (m, es) ->
      fprintf ppf "@[%s(%a)@]" m (pp_print_list pp_exp ~pp_sep:comma) es
   | NotE e ->
      fprintf ppf "@[(!%a)@]" pp_exp e
diff --git a/src/viper/syntax.ml b/src/viper/syntax.ml
index 890790f0fd5..35f915e6137 100644
--- a/src/viper/syntax.ml
+++ b/src/viper/syntax.ml
@@ -49,7 +49,7 @@ and exp' =
   | FldAcc of fldacc
   | PermE of perm          (* perm_amount *)
   | AccE of fldacc * exp   (* acc((rcvr: exp).field, (exp: perm_amount)) *)
-  | MacroCall of string * exp list
+  | CallE of string * exp list   (* macro or func call *)
 
 and perm = (perm', info) Source.annotated_phrase
 
diff --git a/src/viper/trans.ml b/src/viper/trans.ml
index bd45e62ab00..fa41214ce83 100644
--- a/src/viper/trans.ml
+++ b/src/viper/trans.ml
@@ -89,7 +89,7 @@ let rec extract_invariants : item list -> (par -> invariants -> invariants) = fu
   | [] -> fun _ x -> x
   | { it = InvariantI (s, e); at; _ } :: p ->
       fun self es ->
-        !!! at (MacroCall(s, [ !!! at (LocalVar (fst self, snd self)) ]))
+        !!! at (CallE(s, [ !!! at (LocalVar (fst self, snd self)) ]))
         :: extract_invariants p self es
   | _ :: p -> extract_invariants p
 
@@ -170,8 +170,8 @@ and unit' (u : M.comp_unit) : prog =
       (^^^)
         at
         (MethodI (id, ins, outs,
-          !!! at (MacroCall("$Perm", [self ctxt'' at]))::pres,
-          !!! at (MacroCall("$Perm", [self ctxt'' at]))::posts,
+          !!! at (CallE("$Perm", [self ctxt'' at]))::pres,
+          !!! at (CallE("$Perm", [self ctxt'' at]))::posts,
           body))
         note
       | x -> x) is'' in
@@ -186,7 +186,7 @@ and unit' (u : M.comp_unit) : prog =
         at
         (MethodI(id, ins, outs,
           pres,
-          posts @ [!!! at (MacroCall("$Inv", [self ctxt'' at]))],
+          posts @ [!!! at (CallE("$Inv", [self ctxt'' at]))],
           body))
         ActorInit
       )
@@ -197,8 +197,8 @@ and unit' (u : M.comp_unit) : prog =
       } -> ((^^^)
         at
         (MethodI(id, ins, outs,
-          pres @ [!!! at (MacroCall("$Inv", [self ctxt'' at]))],
-          posts @ [!!! at (MacroCall("$Inv", [self ctxt'' at]))],
+          pres @ [!!! at (CallE("$Inv", [self ctxt'' at]))],
+          posts @ [!!! at (CallE("$Inv", [self ctxt'' at]))],
           body))
         (PublicFunction x)
       )
@@ -391,13 +391,13 @@ and stmt ctxt (s : M.exp) : seqn =
             (self ctxt Source.no_region, !!id),
             (!!(AddE(!!(FldAcc (self ctxt (s.at), !!id)),
                      intLitE Source.no_region 1)))));
-          !@(ExhaleS (!@(AndE(!@(MacroCall("$Perm", [self ctxt at])),
-                              !@(MacroCall("$Inv", [self ctxt at]))))));
+          !@(ExhaleS (!@(AndE(!@(CallE("$Perm", [self ctxt at])),
+                              !@(CallE("$Inv", [self ctxt at]))))));
           !@(SeqnS (
               !@([],
                  [
-                   !@(InhaleS (!@(AndE(!@(MacroCall("$Perm", [self ctxt at])),
-                                  !@(AndE(!@(MacroCall("$Inv", [self ctxt at])),
+                   !@(InhaleS (!@(AndE(!@(CallE("$Perm", [self ctxt at])),
+                                  !@(AndE(!@(CallE("$Inv", [self ctxt at])),
                                           !@(GtCmpE(!@(FldAcc (self ctxt at, !@id)),
                                                intLitE Source.no_region 0))))))));
                    !@(FieldAssignS(
@@ -405,10 +405,10 @@ and stmt ctxt (s : M.exp) : seqn =
                           (!@(SubE(!@(FldAcc (self ctxt at, !@id)),
                                    intLitE at 1)))));
                    !!! (e.at) (SeqnS stmts);
-                   !@(ExhaleS (!@(AndE(!@(MacroCall("$Perm", [self ctxt at])),
-                                       !@(MacroCall("$Inv", [self ctxt at])))))) ])));
-          !!(InhaleS (!!(AndE(!!(MacroCall("$Perm", [self ctxt at])),
-                              !!(MacroCall("$Inv", [self ctxt at]))))));
+                   !@(ExhaleS (!@(AndE(!@(CallE("$Perm", [self ctxt at])),
+                                       !@(CallE("$Inv", [self ctxt at])))))) ])));
+          !!(InhaleS (!!(AndE(!!(CallE("$Perm", [self ctxt at])),
+                              !!(CallE("$Inv", [self ctxt at]))))));
         ])
   | M.WhileE(e, s1) ->
      let (invs, s1') = extract_loop_invariants s1 in

From 5cca67d13d028387445d8b6269d1b9c007fbb5be Mon Sep 17 00:00:00 2001
From: Vladislav Zavialov <vlad.z.4096@gmail.com>
Date: Tue, 30 Apr 2024 00:30:05 +0300
Subject: [PATCH 6/6] motoko-san: array support

---
 src/viper/pretty.ml               |   3 +
 src/viper/syntax.ml               |   2 +
 src/viper/trans.ml                | 114 ++++++++++++++++--
 test/viper/array.mo               |  58 +++++++++
 test/viper/ok/array.silicon.ok    |   1 +
 test/viper/ok/array.tc.ok         |   8 ++
 test/viper/ok/array.vpr.ok        | 192 ++++++++++++++++++++++++++++++
 test/viper/ok/array.vpr.stderr.ok |   8 ++
 8 files changed, 374 insertions(+), 12 deletions(-)
 create mode 100644 test/viper/array.mo
 create mode 100644 test/viper/ok/array.silicon.ok
 create mode 100644 test/viper/ok/array.tc.ok
 create mode 100644 test/viper/ok/array.vpr.ok
 create mode 100644 test/viper/ok/array.vpr.stderr.ok

diff --git a/src/viper/pretty.ml b/src/viper/pretty.ml
index 9ab5975c774..ac913370ad8 100644
--- a/src/viper/pretty.ml
+++ b/src/viper/pretty.ml
@@ -93,6 +93,7 @@ and pp_typ ppf t =
   | IntT -> pr ppf "Int"
   | BoolT -> pr ppf "Bool"
   | RefT -> pr ppf "Ref"
+  | ArrayT -> pr ppf "Array"
 
 and pp_exp ppf exp =
   match exp.it with
@@ -100,6 +101,8 @@ and pp_exp ppf exp =
      fprintf ppf "%s" id.it
   | FldAcc fldacc ->
      pp_fldacc ppf fldacc
+  | FldE s ->
+     fprintf ppf "%s" s
   | CallE (m, es) ->
      fprintf ppf "@[%s(%a)@]" m (pp_print_list pp_exp ~pp_sep:comma) es
   | NotE e ->
diff --git a/src/viper/syntax.ml b/src/viper/syntax.ml
index 35f915e6137..76692ba7019 100644
--- a/src/viper/syntax.ml
+++ b/src/viper/syntax.ml
@@ -49,6 +49,7 @@ and exp' =
   | FldAcc of fldacc
   | PermE of perm          (* perm_amount *)
   | AccE of fldacc * exp   (* acc((rcvr: exp).field, (exp: perm_amount)) *)
+  | FldE of string               (* top-level field name, e.g. to be passed as a macro argument *)
   | CallE of string * exp list   (* macro or func call *)
 
 and perm = (perm', info) Source.annotated_phrase
@@ -94,4 +95,5 @@ and typ' =
   | IntT
   | BoolT
   | RefT
+  | ArrayT
 
diff --git a/src/viper/trans.ml b/src/viper/trans.ml
index fa41214ce83..e223295a47d 100644
--- a/src/viper/trans.ml
+++ b/src/viper/trans.ml
@@ -75,7 +75,7 @@ type ctxt =
   { self : string option;
     ids : sort T.Env.t;
     ghost_items : (ctxt -> item) list ref;
-    ghost_inits : (ctxt -> stmt) list ref;
+    ghost_inits : (ctxt -> stmt list) list ref;
     ghost_perms : (ctxt -> Source.region -> exp) list ref;
     ghost_conc : (ctxt -> exp -> exp) list ref;
   }
@@ -156,7 +156,7 @@ and unit' (u : M.comp_unit) : prog =
          (perms @ !(ctxt.ghost_perms))
     in
     (* Add initializer *)
-    let init_list = List.map (fun mk_s -> mk_s ctxt'') (inits @ !(ctxt.ghost_inits)) in
+    let init_list = List.concat_map (fun mk_s -> mk_s ctxt'') (inits @ !(ctxt.ghost_inits)) in
     let init_body =
       !!! (body.at) ([], init_list)(* ATG: Is this the correct position? *)
     in
@@ -230,12 +230,25 @@ and dec_field ctxt d =
 
 and dec_field' ctxt d =
   match d.M.dec.it with
+  | M.VarD (x, {it=M.AnnotE ({it=M.ArrayE (mut, es); note;_}, _); at=e_at;_}) ->
+      let lhs = fun ctxt' -> !!! Source.no_region (FldAcc (self ctxt' e_at, id x)) in
+      let t = note.M.note_typ in
+      { ctxt with ids = Env.add x.it Field ctxt.ids },
+      Some (fun ctxt' at -> (* perm *)
+              !!! at (AndE (accE at (self ctxt' at, id x),
+                      !!! at (AndE (array_acc at (lhs ctxt') (T.Mut (array_elem_t t)),
+                                    array_size_inv at ctxt' (lhs ctxt')  (List.length es)))))),
+      Some (fun ctxt' -> (* init *)
+          array_alloc e_at ctxt' (lhs ctxt') (array_elem_t t) es),
+      (fun ctxt' ->
+        (FieldI(id x, tr_typ t),
+        NoInfo))
   | M.VarD (x, e) ->
       { ctxt with ids = Env.add x.it Field ctxt.ids },
       Some(fun ctxt' (at : region) -> (accE at (self ctxt' at, id x))),
       Some(fun ctxt' ->
-        !!! { left = x.at.left; right = e.at.right }
-          (FieldAssignS((self ctxt' e.at, id x), exp ctxt' e))),
+        [!!! { left = x.at.left; right = e.at.right }
+          (FieldAssignS((self ctxt' e.at, id x), exp ctxt' e))]),
       fun ctxt' ->
         (FieldI(id x, tr_typ e.note.M.note_typ),
         NoInfo)
@@ -249,7 +262,7 @@ and dec_field' ctxt d =
       fun ctxt' ->
         let open Either in
         let self_id = !!! (Source.no_region) "$Self" in
-        let method_args = args p in
+        let arg_preds, 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 }
@@ -258,6 +271,8 @@ and dec_field' ctxt d =
         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
+        let pres = arg_preds @ pres in
+        let posts = arg_preds @ posts in
         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)
@@ -271,7 +286,7 @@ and dec_field' ctxt d =
       fun ctxt' ->
         let open Either in
         let self_id = !!! (Source.no_region) "$Self" in
-        let method_args = args p in
+        let arg_preds, 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 }
@@ -280,6 +295,8 @@ and dec_field' ctxt d =
         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
+        let pres = arg_preds @ pres in
+        let posts = arg_preds @ posts in
         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'' } ),
         PrivateFunction f.it)
@@ -293,15 +310,23 @@ and dec_field' ctxt d =
      unsupported d.M.dec.at (Arrange.dec d.M.dec)
 
 and args p = match p.it with
-  | M.TupP ps -> List.map arg ps
-  | M.ParP p  -> [arg p]
+  | M.TupP ps -> rearrange_args (List.map arg ps)
+  | M.ParP p  -> rearrange_args [arg p]
   | _ -> unsupported p.at (Arrange.pat p)
 and arg p = match p.it with
   | M.AnnotP (p, t) ->
       (match p.it with
-        | M.VarP x -> (id x, tr_typ t.note)
+        | M.VarP x -> (arg_access_pred x t.note, (id x, tr_typ t.note))
         | _ -> unsupported p.at (Arrange.pat p))
   | _ -> unsupported p.at (Arrange.pat p)
+and arg_access_pred x t =
+  let lhs = !!! Source.no_region (LocalVar (id x, tr_typ t)) in
+  match T.normalize t with
+  | T.Array elem_t -> Some (array_acc Source.no_region lhs elem_t)
+  | _ -> None
+and rearrange_args arg_triples =
+  let arg_preds, arg_pairs = List.split arg_triples in
+  List.filter_map (fun x -> x) arg_preds, arg_pairs
 
 and block ctxt at ds =
   let ctxt, mk_ss = decs ctxt ds in
@@ -360,10 +385,10 @@ and stmt ctxt (s : M.exp) : seqn =
          !!(FieldI (!!id, !!IntT))) ::
        !(ctxt.ghost_items);
      let mk_s = fun ctxt ->
-       !!! at
+       [!!! at
          (FieldAssignS (
             (self  ctxt s.at, !!id),
-            intLitE (s.at) 0))
+            intLitE (s.at) 0))]
      in
      ctxt.ghost_inits := mk_s :: !(ctxt.ghost_inits);
      let mk_p = fun ctxt at ->
@@ -415,6 +440,16 @@ and stmt ctxt (s : M.exp) : seqn =
      let invs' = List.map (fun inv -> exp ctxt inv) invs in
      !!([],
         [ !!(WhileS(exp ctxt e, invs', stmt ctxt s1')) ])
+
+  (* TODO: remove by Motoko->Motoko transformation *)
+  | M.(AssignE({it = VarE x; _}, {it = ArrayE (mut, es); note={note_typ=typ; _}; _})) ->
+     let typ' = tr_typ typ in
+     let temp_id = fresh_id (fresh_id (id x).it) in
+     let lhs = !!(LocalVar (!!temp_id, typ')) in
+     !! ([!!(!!temp_id, typ')],
+         array_alloc s.at ctxt lhs (array_elem_t typ) es
+         @ [!!(VarAssignS (id x, !!(LocalVar (!!temp_id, typ'))))])
+
   | M.(AssignE({it = VarE x; _}, e2)) ->
      begin match Env.find x.it ctxt.ids with
      | Local ->
@@ -427,6 +462,9 @@ and stmt ctxt (s : M.exp) : seqn =
      | _ ->
         unsupported s.at (Arrange.exp s)
      end
+  | M.(AssignE({it = IdxE (e1, e2);_}, e3)) ->
+     !!([],
+        [!!(FieldAssignS (array_loc ctxt s.at e1 e2 e3.note.M.note_typ, exp ctxt e3))])
   | M.AssertE (M.Precondition, e) ->
     !!( [],
         [ !!(PreconditionS (exp ctxt e)) ])
@@ -457,10 +495,15 @@ and stmt ctxt (s : M.exp) : seqn =
 and assign_stmts ctxt at x e =
   let (!!) p = !!! at p in
   match e with
+  | M.({it=AnnotE (e, _);_}) -> assign_stmts ctxt at x e
   | M.({it = CallE({it = VarE m; _}, inst, args); _}) ->
     [ !!(MethodCallS ([x], id m,
           let self_var = self ctxt m.at in
           self_var :: call_args ctxt args)) ]
+  | M.({it=ArrayE(mut, es); note; _}) ->
+      let t = note.M.note_typ in
+      let lhs = !!(LocalVar (x, tr_typ t)) in
+      array_alloc at ctxt lhs (array_elem_t t) es
   | _ -> [ !!(VarAssignS(x, exp ctxt e)) ]
 
 and call_args ctxt e =
@@ -484,6 +527,8 @@ and exp ctxt e =
     end
   | M.AnnotE(a, b) ->
     exp ctxt a
+  | M.CallE ({it=M.DotE (e1, {it="size";_});_}, _inst, {it=M.TupE ([]);at;_})
+      -> array_size at (exp ctxt e1)
   | M.LitE r ->
     begin match !r with
     | M.BoolLit b ->
@@ -523,6 +568,8 @@ and exp ctxt e =
      !!(Implies (exp ctxt e1, exp ctxt e2))
   | M.OldE e ->
     !!(Old (exp ctxt e))
+  | M.IdxE (e1, e2) ->
+     !!(FldAcc (array_loc ctxt e.at e1 e2 e.note.M.note_typ))
   | _ ->
      unsupported e.at (Arrange.exp e)
 
@@ -547,4 +594,47 @@ and tr_typ' typ =
   | T.Prim T.Int -> IntT
   | T.Prim T.Nat -> IntT    (* Viper has no native support for Nat, so translate to Int *)
   | T.Prim T.Bool -> BoolT
-  | _ -> unsupported Source.no_region (Mo_types.Arrange_type.typ (T.normalize typ))
+  | T.Array _ -> ArrayT     (* Viper arrays are not parameterised by element type *)
+  | t -> unsupported Source.no_region (Mo_types.Arrange_type.typ t)
+
+and array_elem_t t =
+  match T.normalize t with
+  | T.Array elem_t -> elem_t
+  | t -> unsupported Source.no_region (Mo_types.Arrange_type.typ t)
+
+and array_field t =
+  match T.normalize t  with
+  | T.Mut elem_t -> array_field elem_t
+  | T.Prim T.Int  -> "$int"
+  | T.Prim T.Nat  -> "$int"  (* Viper has no native support for Nat, so translate to Int *)
+  | T.Prim T.Bool -> "$bool"
+  | _ -> unsupported Source.no_region (Mo_types.Arrange_type.typ t)
+
+and array_size at lhs =
+  !!! at (CallE ("$size", [lhs]))
+
+and array_size_inv at ctxt lhs n =
+  !!! at (EqCmpE (array_size at lhs, intLitE at n))
+
+and array_acc at lhs t =
+  let (!!) p = !!! at p in
+  let call = fun pred -> !! (CallE (pred, [lhs; !!(FldE (array_field t))])) in
+  match T.normalize t with
+  | T.Mut _ -> call "$array_acc_mut"
+  | _ -> call "$array_acc"
+
+and array_alloc at ctxt lhs t es : stmt list =
+  let (!!) p = !!! at p in
+  let ref_field = !! (array_field t) in
+  let init_array = List.mapi (fun i e ->
+    FieldAssignS ((!! (CallE ("$loc", [lhs; intLitE at i])), ref_field), exp ctxt e)) es in
+  (* InhaleS (!! (FldAcc (!! (CallE ("$loc", [var; from_int i])), ref_field)) === e)) es in *)
+  let stmts = [ InhaleS (array_acc at lhs (T.Mut t))
+              ; InhaleS (array_size_inv at ctxt lhs (List.length es))
+              ] @ init_array @ [
+                ExhaleS (array_acc at lhs (T.Mut t))
+              ; InhaleS (array_acc at lhs t)]
+  in List.map (!!) stmts
+
+and array_loc ctxt at e1 e2 t =
+  !!! at (CallE ("$loc", [exp ctxt e1; exp ctxt e2])), !!! at (array_field t)
\ No newline at end of file
diff --git a/test/viper/array.mo b/test/viper/array.mo
new file mode 100644
index 00000000000..cd6a784af7b
--- /dev/null
+++ b/test/viper/array.mo
@@ -0,0 +1,58 @@
+// @verify
+// import Array "mo:base/Array";
+
+actor {
+
+    var arr : [var Int] = [var 1, 2];
+    var f : Int = 2;
+    var count : Int = 42; // let is not supported
+
+    public func foo(): async Int {
+        var vi_a : [Int] = (([1] : [Int]) : [Int]);
+        var vm_a : [var Int] = [var 1, 2];
+        let li_a : [Bool] = [false];
+        let lm_a : [var Bool] = [var false];
+        // vi_a = [1, 2]
+        vi_a := [1, 2];
+        // li_a := [1, 2]; // error
+        vm_a := [var 42];
+        // lm_a := [1, 2]; // error
+
+        return 42;
+    };
+
+    public func baz1(): async [Int] {
+      let r : [Int] = [1, 2];
+      return r;
+    };
+
+    private func baz2(): [var Int] {
+      let r : [var Int] = [var 1, 2];
+      return r;
+    };
+
+    private func bar(): Int {
+      let x : [Int] = [42, 24];
+      let y : [var Bool] = [var false];
+      y[0] := true;
+      let z : Int = x[0] + x[1];
+      return x[1];
+    };
+
+    public func bar2(x: [Int]):  async Int {
+      assert:func x.size() == 2;
+      let y : [var Bool] = [var false];
+      y[0] := true;
+      let z : Int = x[0] + x[1];
+      return x[1];
+    };
+
+    public func inc() : async Int {
+      arr[0] := arr[0] + 1;
+      return arr[0]
+    };
+
+    public func len(): async Int {
+      return arr.size();
+    };
+}
diff --git a/test/viper/ok/array.silicon.ok b/test/viper/ok/array.silicon.ok
new file mode 100644
index 00000000000..7b91a64ac36
--- /dev/null
+++ b/test/viper/ok/array.silicon.ok
@@ -0,0 +1 @@
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array.vpr@23.1)
diff --git a/test/viper/ok/array.tc.ok b/test/viper/ok/array.tc.ok
new file mode 100644
index 00000000000..bf84d27a2e0
--- /dev/null
+++ b/test/viper/ok/array.tc.ok
@@ -0,0 +1,8 @@
+array.mo:7.9-7.10: warning [M0194], unused identifier f (delete or rename to wildcard `_` or `_f`)
+array.mo:8.9-8.14: warning [M0194], unused identifier count (delete or rename to wildcard `_` or `_count`)
+array.mo:13.13-13.17: warning [M0194], unused identifier li_a (delete or rename to wildcard `_` or `_li_a`)
+array.mo:14.13-14.17: warning [M0194], unused identifier lm_a (delete or rename to wildcard `_` or `_lm_a`)
+array.mo:29.18-29.22: warning [M0194], unused identifier baz2 (delete or rename to wildcard `_` or `_baz2`)
+array.mo:34.18-34.21: warning [M0194], unused identifier bar (delete or rename to wildcard `_` or `_bar`)
+array.mo:38.11-38.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`)
+array.mo:46.11-46.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`)
diff --git a/test/viper/ok/array.vpr.ok b/test/viper/ok/array.vpr.ok
new file mode 100644
index 00000000000..a9513e97b25
--- /dev/null
+++ b/test/viper/ok/array.vpr.ok
@@ -0,0 +1,192 @@
+/* BEGIN PRELUDE */
+domain Array {
+  function $loc(a: Array, i: Int): Ref
+  function $size(a: Array): Int
+  function $first(r: Ref): Array
+  function $second(r: Ref): Int
+  axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i }
+  axiom $size_nonneg { forall a: Array :: $size(a) >= 0 }
+}
+define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t)
+define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2)
+define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+field $int: Int
+field $bool: Bool
+field $ref: Ref
+field $array: Array
+/* END PRELUDE */
+
+define $Perm($Self) ((((true && (acc(($Self).arr,write) && ($array_acc_mut(
+                                                            ($Self).arr,
+                                                            $int) && (
+  $size(($Self).arr) == 2)))) && acc(($Self).f,write)) && acc(($Self).count,write)))
+define $Inv($Self) (true)
+method __init__($Self: Ref)
+    
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+      inhale $array_acc_mut(($Self).arr, $int)
+      inhale ($size(($Self).arr) == 2)
+      ($loc(($Self).arr, 0)).$int := 1
+      ($loc(($Self).arr, 1)).$int := 2
+      exhale $array_acc_mut(($Self).arr, $int)
+      inhale $array_acc_mut(($Self).arr, $int)
+      ($Self).f := 2
+      ($Self).count := 42 
+    }
+field arr: Array
+field f: Int
+field count: Int
+method foo($Self: Ref)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { var vi_a: Array
+      var vm_a: Array
+      var li_a: Array
+      var lm_a: Array
+      var vi_a_2: Array
+      var vm_a_2: Array
+      inhale $array_acc_mut(vi_a, $int)
+      inhale ($size(vi_a) == 1)
+      ($loc(vi_a, 0)).$int := 1
+      exhale $array_acc_mut(vi_a, $int)
+      inhale $array_acc(vi_a, $int)
+      inhale $array_acc_mut(vm_a, $int)
+      inhale ($size(vm_a) == 2)
+      ($loc(vm_a, 0)).$int := 1
+      ($loc(vm_a, 1)).$int := 2
+      exhale $array_acc_mut(vm_a, $int)
+      inhale $array_acc_mut(vm_a, $int)
+      inhale $array_acc_mut(li_a, $bool)
+      inhale ($size(li_a) == 1)
+      ($loc(li_a, 0)).$bool := false
+      exhale $array_acc_mut(li_a, $bool)
+      inhale $array_acc(li_a, $bool)
+      inhale $array_acc_mut(lm_a, $bool)
+      inhale ($size(lm_a) == 1)
+      ($loc(lm_a, 0)).$bool := false
+      exhale $array_acc_mut(lm_a, $bool)
+      inhale $array_acc_mut(lm_a, $bool)
+      inhale $array_acc_mut(vi_a_2, $int)
+      inhale ($size(vi_a_2) == 2)
+      ($loc(vi_a_2, 0)).$int := 1
+      ($loc(vi_a_2, 1)).$int := 2
+      exhale $array_acc_mut(vi_a_2, $int)
+      inhale $array_acc(vi_a_2, $int)
+      vi_a := vi_a_2
+      inhale $array_acc_mut(vm_a_2, $int)
+      inhale ($size(vm_a_2) == 1)
+      ($loc(vm_a_2, 0)).$int := 42
+      exhale $array_acc_mut(vm_a_2, $int)
+      inhale $array_acc_mut(vm_a_2, $int)
+      vm_a := vm_a_2
+      $Res := 42
+      goto $Ret
+      label $Ret 
+    }
+method baz1($Self: Ref)
+     returns ($Res: Array)
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { var r: Array
+      inhale $array_acc_mut(r, $int)
+      inhale ($size(r) == 2)
+      ($loc(r, 0)).$int := 1
+      ($loc(r, 1)).$int := 2
+      exhale $array_acc_mut(r, $int)
+      inhale $array_acc(r, $int)
+      $Res := r
+      goto $Ret
+      label $Ret 
+    }
+method baz2($Self: Ref)
+     returns ($Res: Array)
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    { var r: Array
+      inhale $array_acc_mut(r, $int)
+      inhale ($size(r) == 2)
+      ($loc(r, 0)).$int := 1
+      ($loc(r, 1)).$int := 2
+      exhale $array_acc_mut(r, $int)
+      inhale $array_acc_mut(r, $int)
+      $Res := r
+      goto $Ret
+      label $Ret 
+    }
+method bar($Self: Ref)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    { var x: Array
+      var y: Array
+      var z: Int
+      inhale $array_acc_mut(x, $int)
+      inhale ($size(x) == 2)
+      ($loc(x, 0)).$int := 42
+      ($loc(x, 1)).$int := 24
+      exhale $array_acc_mut(x, $int)
+      inhale $array_acc(x, $int)
+      inhale $array_acc_mut(y, $bool)
+      inhale ($size(y) == 1)
+      ($loc(y, 0)).$bool := false
+      exhale $array_acc_mut(y, $bool)
+      inhale $array_acc_mut(y, $bool)
+      ($loc(y, 0)).$bool := true
+      z := (($loc(x, 0)).$int + ($loc(x, 1)).$int)
+      $Res := ($loc(x, 1)).$int
+      goto $Ret
+      label $Ret 
+    }
+method bar2($Self: Ref, x: Array)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    requires $array_acc(x, $int)
+    requires ($size(x) == 2)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $array_acc(x, $int)
+    ensures $Inv($Self)
+    { var y: Array
+      var z: Int
+      inhale $array_acc_mut(y, $bool)
+      inhale ($size(y) == 1)
+      ($loc(y, 0)).$bool := false
+      exhale $array_acc_mut(y, $bool)
+      inhale $array_acc_mut(y, $bool)
+      ($loc(y, 0)).$bool := true
+      z := (($loc(x, 0)).$int + ($loc(x, 1)).$int)
+      $Res := ($loc(x, 1)).$int
+      goto $Ret
+      label $Ret 
+    }
+method inc($Self: Ref)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+      ($loc(($Self).arr, 0)).$int := (($loc(($Self).arr, 0)).$int + 1)
+      $Res := ($loc(($Self).arr, 0)).$int
+      goto $Ret
+      label $Ret 
+    }
+method len($Self: Ref)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+      $Res := $size(($Self).arr)
+      goto $Ret
+      label $Ret 
+    }
diff --git a/test/viper/ok/array.vpr.stderr.ok b/test/viper/ok/array.vpr.stderr.ok
new file mode 100644
index 00000000000..bf84d27a2e0
--- /dev/null
+++ b/test/viper/ok/array.vpr.stderr.ok
@@ -0,0 +1,8 @@
+array.mo:7.9-7.10: warning [M0194], unused identifier f (delete or rename to wildcard `_` or `_f`)
+array.mo:8.9-8.14: warning [M0194], unused identifier count (delete or rename to wildcard `_` or `_count`)
+array.mo:13.13-13.17: warning [M0194], unused identifier li_a (delete or rename to wildcard `_` or `_li_a`)
+array.mo:14.13-14.17: warning [M0194], unused identifier lm_a (delete or rename to wildcard `_` or `_lm_a`)
+array.mo:29.18-29.22: warning [M0194], unused identifier baz2 (delete or rename to wildcard `_` or `_baz2`)
+array.mo:34.18-34.21: warning [M0194], unused identifier bar (delete or rename to wildcard `_` or `_bar`)
+array.mo:38.11-38.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`)
+array.mo:46.11-46.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`)