motoko-san: fix bug with array initialization

Problem: permissions are reset incorrectly. Namely, after initialization write
access was dropped by exhaling full permission which leads to forgetting
assigned before values

Solution: do not exhale anything for mutable array and exhale-inhale wildcard
for immutable which models losing write access better

src/viper/prelude.ml

@@ -7,9 +7,8 @@ domain Array {
   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)
+define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
+define $array_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

src/viper/trans.ml

@@ -36,11 +36,11 @@ let (!!!) at it = (^^^) at it NoInfo
 let intLitE at i =
   !!! at (IntLitE (Mo_values.Numerics.Int.of_int i))
 
-let accE at fldacc =
+let accE at ?(perm=FullP) fldacc =
   !!! at
     (AccE(
          fldacc,
-         !!! at (PermE (!!! at FullP))))
+         !!! at (PermE (!!! at perm))))
 
 let conjoin es at =
   match es with
@@ -56,6 +56,15 @@ let rec adjoin ctxt e = function
   | [] -> e
   | f :: fs -> f ctxt (adjoin ctxt e fs)
 
+let locE at exp_arr exp_ix field_name =
+  !!! at (CallE ("$loc", [exp_arr; exp_ix])), !!! at field_name
+
+let sizeE at lhs =
+  !!! at (CallE ("$size", [lhs]))
+
+let arrayAccE at lhs field_name perm =
+  let (!!) p = !!! at p in
+  !! (CallE ("$array_acc", [lhs; !!(FldE field_name); !!(PermE(!! perm))]))
 
 let (|:) (x_opt : 'a option) (xs : 'a list) : 'a list =
   match x_opt with
@@ -539,7 +548,7 @@ and exp ctxt e =
   | 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)
+      -> sizeE at (exp ctxt e1)
   | M.LitE r ->
     begin match !r with
     | M.BoolLit b ->
@@ -623,31 +632,28 @@ and array_field t =
   | 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))
+  !!! at (EqCmpE (sizeE 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"
+  | T.Mut _-> arrayAccE at lhs (array_field t) FullP
+  | _      -> arrayAccE at lhs (array_field t) WildcardP
 
 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 *)
+    FieldAssignS (locE at lhs (intLitE at i) (array_field t), exp ctxt e)) es in
+  (* InhaleS (!! (FldAcc (locE at lhs (intLitE at i) (array_field t))) === e)) es in *)
+  let reset_perm =
+    (match T.normalize t with
+     | T.Mut _ -> []
+     | _       -> [ExhaleS (array_acc at lhs t); InhaleS (array_acc at lhs t)])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)]
+              ; InhaleS (array_size_inv at ctxt lhs (List.length es))]
+              @ init_array
+              @ reset_perm
   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)
+  locE at (exp ctxt e1) (exp ctxt e2) (array_field t)

test/repl/ok/viper.stdout.ok

@@ -7,9 +7,8 @@ domain Array {
   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)
+define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
+define $array_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

test/viper/array.mo

@@ -8,16 +8,29 @@ actor {
     var count : Int = 42; // let is not supported
 
     public func foo(): async Int {
+        // declarations
         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];
+
+        assert:system vi_a[0] == 1;
+        assert:system vm_a[0] == 1;
+        assert:system li_a[0] == false;
+        assert:system lm_a[0] == false;
+
+        // assignments
         // vi_a = [1, 2]
         vi_a := [1, 2];
         // li_a := [1, 2]; // error
         vm_a := [var 42];
         // lm_a := [1, 2]; // error
 
+        assert:system vi_a[0] != 0;
+        assert:system vi_a[0] == 1;
+        assert:system vm_a[0] != 1;
+        assert:system vm_a[0] == 42;
+
         return 42;
     };
 

test/viper/ok/array.silicon.ok

@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array.vpr@23.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array.vpr@22.1)

test/viper/ok/array.tc.ok

@@ -1,8 +1,6 @@
 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`)
+array.mo:42.18-42.22: warning [M0194], unused identifier baz2 (delete or rename to wildcard `_` or `_baz2`)
+array.mo:47.18-47.21: warning [M0194], unused identifier bar (delete or rename to wildcard `_` or `_bar`)
+array.mo:51.11-51.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`)
+array.mo:59.11-59.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`)

test/viper/ok/array.vpr.ok

@@ -7,18 +7,17 @@ domain Array {
   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)
+define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
+define $array_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(
+define $Perm($Self) ((((true && (acc(($Self).arr,write) && ($array_acc(
                                                             ($Self).arr,
-                                                            $int) && (
+                                                            $int, write) && (
   $size(($Self).arr) == 2)))) && acc(($Self).f,write)) && acc(($Self).count,write)))
 define $Inv($Self) (true)
 method __init__($Self: Ref)
@@ -27,12 +26,10 @@ method __init__($Self: Ref)
     ensures $Perm($Self)
     ensures $Inv($Self)
     { 
-      inhale $array_acc_mut(($Self).arr, $int)
+      inhale $array_acc(($Self).arr, $int, write)
       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 
     }
@@ -51,40 +48,42 @@ method foo($Self: Ref)
       var lm_a: Array
       var vi_a_2: Array
       var vm_a_2: Array
-      inhale $array_acc_mut(vi_a, $int)
+      inhale $array_acc(vi_a, $int, write)
       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)
+      exhale $array_acc(vi_a, $int, wildcard)
+      inhale $array_acc(vi_a, $int, wildcard)
+      inhale $array_acc(vm_a, $int, write)
       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 $array_acc(li_a, $bool, write)
       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)
+      exhale $array_acc(li_a, $bool, wildcard)
+      inhale $array_acc(li_a, $bool, wildcard)
+      inhale $array_acc(lm_a, $bool, write)
       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)
+      assert (($loc(vi_a, 0)).$int == 1)
+      assert (($loc(vm_a, 0)).$int == 1)
+      assert (($loc(li_a, 0)).$bool == false)
+      assert (($loc(lm_a, 0)).$bool == false)
+      inhale $array_acc(vi_a_2, $int, write)
       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)
+      exhale $array_acc(vi_a_2, $int, wildcard)
+      inhale $array_acc(vi_a_2, $int, wildcard)
       vi_a := vi_a_2
-      inhale $array_acc_mut(vm_a_2, $int)
+      inhale $array_acc(vm_a_2, $int, write)
       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
+      assert (($loc(vi_a, 0)).$int != 0)
+      assert (($loc(vi_a, 0)).$int == 1)
+      assert (($loc(vm_a, 0)).$int != 1)
+      assert (($loc(vm_a, 0)).$int == 42)
       $Res := 42
       goto $Ret
       label $Ret 
@@ -94,15 +93,15 @@ method baz1($Self: Ref)
     requires $Perm($Self)
     requires $Inv($Self)
     ensures $Perm($Self)
-    ensures $array_acc($Res, $int)
+    ensures $array_acc($Res, $int, wildcard)
     ensures $Inv($Self)
     { var r: Array
-      inhale $array_acc_mut(r, $int)
+      inhale $array_acc(r, $int, write)
       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)
+      exhale $array_acc(r, $int, wildcard)
+      inhale $array_acc(r, $int, wildcard)
       $Res := r
       goto $Ret
       label $Ret 
@@ -111,14 +110,12 @@ method baz2($Self: Ref)
      returns ($Res: Array)
     requires $Perm($Self)
     ensures $Perm($Self)
-    ensures $array_acc_mut($Res, $int)
+    ensures $array_acc($Res, $int, write)
     { var r: Array
-      inhale $array_acc_mut(r, $int)
+      inhale $array_acc(r, $int, write)
       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 
@@ -130,17 +127,15 @@ method bar($Self: Ref)
     { var x: Array
       var y: Array
       var z: Int
-      inhale $array_acc_mut(x, $int)
+      inhale $array_acc(x, $int, write)
       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)
+      exhale $array_acc(x, $int, wildcard)
+      inhale $array_acc(x, $int, wildcard)
+      inhale $array_acc(y, $bool, write)
       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
@@ -150,19 +145,17 @@ method bar($Self: Ref)
 method bar2($Self: Ref, x: Array)
      returns ($Res: Int)
     requires $Perm($Self)
-    requires $array_acc(x, $int)
+    requires $array_acc(x, $int, wildcard)
     requires ($size(x) == 2)
     requires $Inv($Self)
     ensures $Perm($Self)
-    ensures $array_acc(x, $int)
+    ensures $array_acc(x, $int, wildcard)
     ensures $Inv($Self)
     { var y: Array
       var z: Int
-      inhale $array_acc_mut(y, $bool)
+      inhale $array_acc(y, $bool, write)
       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

test/viper/ok/array.vpr.stderr.ok

@@ -1,8 +1,6 @@
 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`)
+array.mo:42.18-42.22: warning [M0194], unused identifier baz2 (delete or rename to wildcard `_` or `_baz2`)
+array.mo:47.18-47.21: warning [M0194], unused identifier bar (delete or rename to wildcard `_` or `_bar`)
+array.mo:51.11-51.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`)
+array.mo:59.11-59.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`)

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@28.13--28.24)
-  [1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. (assertions.vpr@46.15--46.44)
+  [0] Postcondition of __init__ might not hold. Assertion $Self.u might not hold. (assertions.vpr@27.13--27.24)
+  [1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. (assertions.vpr@45.15--45.44)

test/viper/ok/assertions.vpr.ok

@@ -7,9 +7,8 @@ domain Array {
   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)
+define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
+define $array_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

test/viper/ok/async.silicon.ok

@@ -1 +1 @@
-  [0] Exhale might fail. Assertion $Self.$message_async <= 1 might not hold. (async.vpr@51.15--51.42)
+  [0] Exhale might fail. Assertion $Self.$message_async <= 1 might not hold. (async.vpr@50.15--50.42)

test/viper/ok/async.vpr.ok

@@ -7,9 +7,8 @@ domain Array {
   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)
+define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
+define $array_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

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@49.20--49.47)
+  [0] Exhale might fail. Assertion $Self.$message_async == 1 ==> $Self.claimed && $Self.count == 0 might not hold. (claim-broken.vpr@48.20--48.47)

test/viper/ok/claim-broken.vpr.ok

@@ -7,9 +7,8 @@ domain Array {
   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)
+define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
+define $array_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