motoko-san: let-bound actor fields

serokell · May 15, 2024 · 2f34aa8 · 2f34aa8
1 parent db1167d
commit 2f34aa8
Show file tree

Hide file tree

Showing 7 changed files with 83 additions and 43 deletions.
diff --git a/src/viper/trans.ml b/src/viper/trans.ml
@@ -253,22 +253,6 @@ and static_invariants at lhs e =
 
 and dec_field' ctxt d =
   match d.M.dec.it with
-  | M.VarD (x, e) ->
-      let t = e.note.M.note_typ in
-      let fldacc = fun ctxt' -> (self ctxt' e.at, id x) in
-      let lhs = fun ctxt' -> !!! Source.no_region (FldAcc (fldacc ctxt')) in
-      let perms ctxt' at =
-            conjoin ([ accE at (self ctxt' at, id x) ]
-                     @ (access_pred (lhs ctxt') t |: [])
-                     @ static_invariants at (lhs ctxt') e) at in
-      { ctxt with ids = Env.add x.it (Field, t) ctxt.ids },
-      Some perms, (* perm *)
-      Some (fun ctxt' -> (* init *)
-          let at = span x.at e.at in
-          assign_stmts ctxt' at (LValueFld (fldacc ctxt')) e),
-      (fun ctxt' ->
-        (FieldI(id x, tr_typ t),
-        NoInfo))
   (* async functions *)
   | M.(LetD ({it=VarP f;note;_},
              {it=FuncE(x, sp, tp, p, t_opt, sugar,
@@ -284,7 +268,7 @@ and dec_field' ctxt d =
         let ctxt'' = { ctxt'
           with self = Some self_id.it;
                ids = List.fold_left (fun env (id, t) -> Env.add id.it (Local, t) env) ctxt.ids method_args }
-        in (* TODO: add args (and rets?) *)
+        in
         let stmts = stmt ctxt'' e in
         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
@@ -311,7 +295,7 @@ and dec_field' ctxt d =
         let ctxt'' = { ctxt'
           with self = Some self_id.it;
                ids = List.fold_left (fun env (id, t) -> Env.add id.it (Local, t) env) ctxt.ids method_args }
-        in (* TODO: add args (and rets?) *)
+        in
         let stmts = stmt ctxt'' e in
         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
@@ -323,6 +307,25 @@ and dec_field' ctxt d =
         let stmts'' = stmts' @ [!!! Source.no_region (LabelS(!!! (Source.no_region) "$Ret"))] in
         (MethodI(id f, (self_id, !!! Source.no_region RefT)::method_args', ret, pres, posts, Some { stmts with it = fst stmts.it, stmts'' } ),
         PrivateFunction f.it)
+  (* fields *)
+  | M.LetD ({it=M.VarP x;_}, e, None)
+  | M.VarD (x, e) ->
+      let t = e.note.M.note_typ in
+      let fldacc = fun ctxt' -> (self ctxt' e.at, id x) in
+      let lhs = fun ctxt' -> !!! Source.no_region (FldAcc (fldacc ctxt')) in
+      let perms ctxt' at =
+            conjoin ([ accE at (self ctxt' at, id x) ]
+                     @ (access_pred (lhs ctxt') t |: [])
+                     @ static_invariants at (lhs ctxt') e) at in
+      { ctxt with ids = Env.add x.it (Field, t) ctxt.ids },
+      Some perms, (* perm *)
+      Some (fun ctxt' -> (* init *)
+          let at = span x.at e.at in
+          assign_stmts ctxt' at (LValueFld (fldacc ctxt')) e),
+      (fun ctxt' ->
+        (FieldI(id x, tr_typ t),
+        NoInfo))
+  (* invariants *)
   | M.(ExpD { it = AssertE (Invariant, e); at; _ }) ->
       ctxt,
       None, (* no perm *)

diff --git a/test/viper/array.mo b/test/viper/array.mo
@@ -3,9 +3,10 @@
 
 actor {
 
+    let immut_arr = [42];
     var arr : [var Int] = [var 1, 2];
     var f : Int = 2;
-    var count : Int = 42; // let is not supported
+    var count : Int = 42;
 
     public func foo(): async Int {
         // declarations
@@ -68,4 +69,9 @@ actor {
     public func len(): async Int {
       return arr.size();
     };
+
+    public func reset(): async Int {
+      arr := [var 0, 0];
+      return 0;
+    }
 }
diff --git a/test/viper/ok/array.silicon.ok b/test/viper/ok/array.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array.vpr@22.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array.vpr@27.1)
diff --git a/test/viper/ok/array.tc.ok b/test/viper/ok/array.tc.ok
@@ -1,6 +1,7 @@
-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: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`)
+array.mo:6.9-6.18: warning [M0194], unused identifier immut_arr (delete or rename to wildcard `_` or `_immut_arr`)
+array.mo:8.9-8.10: warning [M0194], unused identifier f (delete or rename to wildcard `_` or `_f`)
+array.mo:9.9-9.14: warning [M0194], unused identifier count (delete or rename to wildcard `_` or `_count`)
+array.mo:43.18-43.22: warning [M0194], unused identifier baz2 (delete or rename to wildcard `_` or `_baz2`)
+array.mo:48.18-48.21: warning [M0194], unused identifier bar (delete or rename to wildcard `_` or `_bar`)
+array.mo:52.11-52.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`)
+array.mo:60.11-60.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
@@ -15,25 +15,38 @@ field $ref: Ref
 field $array: Array
 /* END PRELUDE */
 
-define $Perm($Self) ((((true && (acc(($Self).arr,write) && ($array_acc(
-                                                            ($Self).arr,
-                                                            $int, write) && (
+define $Perm($Self) (((((true && (acc(($Self).immut_arr,write) && ($array_acc(
+                                                                   ($Self).immut_arr,
+                                                                   $int,
+                                                                   wildcard) && (
+  $size(($Self).immut_arr) == 1)))) && (acc(($Self).arr,write) && ($array_acc(
+                                                                   ($Self).arr,
+                                                                   $int,
+                                                                   write) && (
   $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)
-    { var $t_arr: Array
-      inhale $array_acc($t_arr, $int, write);
-      inhale ($size($t_arr) == 2);
-      ($loc($t_arr, 0)).$int := 1;
-      ($loc($t_arr, 1)).$int := 2;
-      ($Self).arr := $t_arr;
+    { var $t_immut_arr: Array
+      var $t_arr_2: Array
+      inhale $array_acc($t_immut_arr, $int, write);
+      inhale ($size($t_immut_arr) == 1);
+      ($loc($t_immut_arr, 0)).$int := 42;
+      exhale $array_acc($t_immut_arr, $int, wildcard);
+      inhale $array_acc($t_immut_arr, $int, wildcard);
+      ($Self).immut_arr := $t_immut_arr;
+      inhale $array_acc($t_arr_2, $int, write);
+      inhale ($size($t_arr_2) == 2);
+      ($loc($t_arr_2, 0)).$int := 1;
+      ($loc($t_arr_2, 1)).$int := 2;
+      ($Self).arr := $t_arr_2;
       ($Self).f := 2;
       ($Self).count := 42; 
     }
+field immut_arr: Array
 field arr: Array
 field f: Int
 field count: Int
@@ -186,3 +199,19 @@ method len($Self: Ref)
       goto $Ret;
       label $Ret; 
     }
+method reset($Self: Ref)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { var $t_arr: Array
+      inhale $array_acc($t_arr, $int, write);
+      inhale ($size($t_arr) == 2);
+      ($loc($t_arr, 0)).$int := 0;
+      ($loc($t_arr, 1)).$int := 0;
+      ($Self).arr := $t_arr;
+      $Res := 0;
+      goto $Ret;
+      label $Ret; 
+    }
diff --git a/test/viper/ok/array.vpr.stderr.ok b/test/viper/ok/array.vpr.stderr.ok
@@ -1,6 +1,7 @@
-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: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`)
+array.mo:6.9-6.18: warning [M0194], unused identifier immut_arr (delete or rename to wildcard `_` or `_immut_arr`)
+array.mo:8.9-8.10: warning [M0194], unused identifier f (delete or rename to wildcard `_` or `_f`)
+array.mo:9.9-9.14: warning [M0194], unused identifier count (delete or rename to wildcard `_` or `_count`)
+array.mo:43.18-43.22: warning [M0194], unused identifier baz2 (delete or rename to wildcard `_` or `_baz2`)
+array.mo:48.18-48.21: warning [M0194], unused identifier bar (delete or rename to wildcard `_` or `_bar`)
+array.mo:52.11-52.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`)
+array.mo:60.11-60.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`)
diff --git a/test/viper/ok/unsupported.vpr.stderr.ok b/test/viper/ok/unsupported.vpr.stderr.ok
@@ -1,4 +1,4 @@
 unsupported.mo:5.7-5.8: warning [M0194], unused identifier x (delete or rename to wildcard `_` or `_x`)
-unsupported.mo:5.3-5.13: viper error [0], translation to viper failed:
-(LetD (VarP x) (LitE (TextLit )))
+(unknown location): viper error [0], translation to viper failed:
+(Prim Text)