fixup! motoko-san: support immutable records

serokell · Jun 25, 2024 · 991f797 · 991f797
1 parent 9de79ff
commit 991f797
Show file tree

Hide file tree

Showing 6 changed files with 94 additions and 68 deletions.
diff --git a/src/viper/trans.ml b/src/viper/trans.ml
@@ -206,6 +206,14 @@ let get_record_name ctxt (typ : T.typ) : string =
   let record_ctor_name = (Type_map.find typ ctxt.type_to_record_ctor).it in
   String.sub record_ctor_name tag_len (String.length record_ctor_name - tag_len)
 
+let mk_record_field ~record_name ~fld_name =
+  Format.asprintf "$%s$%s" record_name fld_name
+
+let get_record_field ctxt (typ : T.typ) (fld : M.id) : M.id =
+  let record_name = get_record_name ctxt typ in
+  let fld_name = mk_record_field ~record_name ~fld_name:fld.it in
+  { fld with it = fld_name }
+
 let rec unit reqs (u : M.comp_unit) : prog Diag.result =
   Diag.(
     reset_stamps();
@@ -368,7 +376,7 @@ and dec_field' ctxt d =
     fun ctxt ->
       let adt_param tb = id tb.it.M.var in
       let adt_field field =
-        let field_name = !!! Source.no_region field.T.lab in
+        let field_name = !!! Source.no_region (mk_record_field ~record_name:typ_id.it ~fld_name:field.T.lab) in
         let field_typ = tr_typ ctxt field.T.typ in
         field_name, field_typ
       in
@@ -769,6 +777,7 @@ and pat_match ctxt (scrut : M.exp) (p : M.pat) : exp list * (id * T.typ) list *
     let stmts =
       List.map2
         (fun M.{ it = { id = fld_name; pat = _ }; _ } (x, _) ->
+          let fld_name = get_record_field ctxt (T.normalize p.note) fld_name in
           fld_assign_stmt (LValueUninitVar x) fld_name)
         pat_fields p_scope
     in
@@ -928,7 +937,7 @@ and exp ctxt e =
         | M.TupE es -> CallE (tag.it, List.map (exp ctxt) es)
         | _ -> CallE (tag.it, [exp ctxt e]))
   | M.ObjE ([], flds) ->
-    (match e.note.M.note_typ with
+    (match T.normalize e.note.M.note_typ with
     | T.Obj (T.Object, typ_flds) as t ->
       let record_ctor_name = Type_map.find t ctxt.type_to_record_ctor in
       let flds = List.map (fun M.{ it = { mut; id; exp }; _} ->
@@ -943,9 +952,10 @@ and exp ctxt e =
       !!(CallE (record_ctor_name.it, args))
     | T.Obj _ -> unsupported e.at (Arrange.exp e)
     | _ -> assert false)
-  | M.DotE (proj, fld) ->
+  | M.DotE (proj, fld) when Type_map.mem (T.normalize proj.note.M.note_typ) ctxt.type_to_record_ctor ->
+    let proj_t = T.normalize proj.note.M.note_typ in
     let proj = exp ctxt proj in
-    let fld = id fld in
+    let fld = id (get_record_field ctxt proj_t fld) in
     !!(FldAcc (proj, fld))
   | M.TupE es ->
       let n = List.length es in

diff --git a/test/viper/ok/record.tc.ok b/test/viper/ok/record.tc.ok
@@ -1,7 +1,9 @@
 record.mo:6.7-6.11: warning [M0194], unused identifier fld1 (delete or rename to wildcard `_` or `_fld1`)
 record.mo:7.7-7.11: warning [M0194], unused identifier fld2 (delete or rename to wildcard `_` or `_fld2`)
-record.mo:11.8-11.20: warning [M0194], unused identifier array_record (delete or rename to wildcard `_` or `_array_record`)
-record.mo:19.8-19.20: warning [M0194], unused identifier tuple_record (delete or rename to wildcard `_` or `_tuple_record`)
-record.mo:30.8-30.19: warning [M0194], unused identifier call_record (delete or rename to wildcard `_` or `_call_record`)
-record.mo:41.8-41.19: warning [M0194], unused identifier pass_record (delete or rename to wildcard `_` or `_pass_record`)
-record.mo:46.8-46.23: warning [M0194], unused identifier match_on_record (delete or rename to wildcard `_` or `_match_on_record`)
+record.mo:11.7-11.9: warning [M0194], unused identifier aa (delete or rename to wildcard `_` or `_aa`)
+record.mo:13.8-13.20: warning [M0194], unused identifier array_record (delete or rename to wildcard `_` or `_array_record`)
+record.mo:21.8-21.20: warning [M0194], unused identifier tuple_record (delete or rename to wildcard `_` or `_tuple_record`)
+record.mo:32.8-32.19: warning [M0194], unused identifier call_record (delete or rename to wildcard `_` or `_call_record`)
+record.mo:43.8-43.19: warning [M0194], unused identifier pass_record (delete or rename to wildcard `_` or `_pass_record`)
+record.mo:48.8-48.23: warning [M0194], unused identifier match_on_record (delete or rename to wildcard `_` or `_match_on_record`)
+record.mo:54.13-54.14: warning [M0194], unused identifier c (delete or rename to wildcard `_` or `_c`)
diff --git a/test/viper/ok/record.vpr.ok b/test/viper/ok/record.vpr.ok
@@ -24,8 +24,8 @@ function $concat(a: Int, b: Int): Int
 field $c_R: R
 /* END PRELUDE */
 
-define $Perm($Self) ((((true && acc(($Self).fld1,write)) && acc(($Self).fld2,write)) && 
-  acc(($Self).empty,write)))
+define $Perm($Self) (((((true && acc(($Self).fld1,write)) && acc(($Self).fld2,write)) && 
+  acc(($Self).empty,write)) && acc(($Self).aa,write)))
 define $Inv($Self) (true)
 method __init__($Self: Ref)
 
@@ -35,12 +35,14 @@ method __init__($Self: Ref)
     { 
       ($Self).fld1 := $RecordCtor_R(42, 3);
       ($Self).fld2 := $RecordCtor_R(42, 3);
-      ($Self).empty := $RecordCtor_R(0, 4); 
+      ($Self).empty := $RecordCtor_R(0, 4);
+      ($Self).aa := 42; 
     }
-adt R  { $RecordCtor_R(a : Int, b : Int) }
+adt R  { $RecordCtor_R($R$aa : Int, $R$b : Int) }
 field fld1: R
 field fld2: R
 field empty: R
+field aa: Int
 method array_record($Self: Ref)
 
     requires $Perm($Self)
@@ -83,15 +85,15 @@ method call_record($Self: Ref)
     ensures $Perm($Self)
     { var res: R
       res := get_record($Self);
-      assert ((res).b == 0);
+      assert ((res).$R$b == 0);
       label $Ret; 
     }
 method record_arg($Self: Ref, r: R)
      returns ($Res: R)
     requires $Perm($Self)
-    requires ((r).a == 100)
+    requires ((r).$R$aa == 100)
     ensures $Perm($Self)
-    ensures (($Res).a == 100)
+    ensures (($Res).$R$aa == 100)
     { 
       $Res := $RecordCtor_R(100, 0);
       goto $Ret;
@@ -103,7 +105,7 @@ method pass_record($Self: Ref)
     ensures $Perm($Self)
     { var res: R
       res := record_arg($Self, $RecordCtor_R(100, 2));
-      assert ((res).a == 100);
+      assert ((res).$R$aa == 100);
       label $Ret; 
     }
 method match_on_record($Self: Ref)
@@ -116,8 +118,10 @@ method match_on_record($Self: Ref)
       if (true)
          { var number: Int
            var b: Int
-           number := (r).a;
-           b := (r).b;
+           var c: Int
+           number := (r).$R$aa;
+           b := (r).$R$b;
+           c := b;
            $Res := (number - 58);
            goto $Ret; 
          };

diff --git a/test/viper/ok/record.vpr.stderr.ok b/test/viper/ok/record.vpr.stderr.ok
@@ -1,7 +1,9 @@
 record.mo:6.7-6.11: warning [M0194], unused identifier fld1 (delete or rename to wildcard `_` or `_fld1`)
 record.mo:7.7-7.11: warning [M0194], unused identifier fld2 (delete or rename to wildcard `_` or `_fld2`)
-record.mo:11.8-11.20: warning [M0194], unused identifier array_record (delete or rename to wildcard `_` or `_array_record`)
-record.mo:19.8-19.20: warning [M0194], unused identifier tuple_record (delete or rename to wildcard `_` or `_tuple_record`)
-record.mo:30.8-30.19: warning [M0194], unused identifier call_record (delete or rename to wildcard `_` or `_call_record`)
-record.mo:41.8-41.19: warning [M0194], unused identifier pass_record (delete or rename to wildcard `_` or `_pass_record`)
-record.mo:46.8-46.23: warning [M0194], unused identifier match_on_record (delete or rename to wildcard `_` or `_match_on_record`)
+record.mo:11.7-11.9: warning [M0194], unused identifier aa (delete or rename to wildcard `_` or `_aa`)
+record.mo:13.8-13.20: warning [M0194], unused identifier array_record (delete or rename to wildcard `_` or `_array_record`)
+record.mo:21.8-21.20: warning [M0194], unused identifier tuple_record (delete or rename to wildcard `_` or `_tuple_record`)
+record.mo:32.8-32.19: warning [M0194], unused identifier call_record (delete or rename to wildcard `_` or `_call_record`)
+record.mo:43.8-43.19: warning [M0194], unused identifier pass_record (delete or rename to wildcard `_` or `_pass_record`)
+record.mo:48.8-48.23: warning [M0194], unused identifier match_on_record (delete or rename to wildcard `_` or `_match_on_record`)
+record.mo:54.13-54.14: warning [M0194], unused identifier c (delete or rename to wildcard `_` or `_c`)
diff --git a/test/viper/ok/todo_record.vpr.ok b/test/viper/ok/todo_record.vpr.ok
@@ -40,7 +40,9 @@ method __init__($Self: Ref)
       ($Self).num := 0;
       ($Self).nextId := 1; 
     }
-adt ToDo  { $RecordCtor_ToDo(completed : State, desc : Int, id : Int) }
+adt ToDo 
+  { $RecordCtor_ToDo($ToDo$completed : State, $ToDo$desc : Int,
+                    $ToDo$id : Int) }
 adt State  { DONE()
              TODO() }
 field todos: Array
@@ -126,7 +128,7 @@ method getTodo($Self: Ref, id: Int)
     ensures (forall i : Int :: (((0 <= i) && (i < old($size(($Self).todos)))) ==> (
             ($loc(($Self).todos, i)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo))))
     ensures ((exists i : Int :: (((0 <= i) && (i < ($Self).num)) && (
-             (($loc(($Self).todos, i)).$c_ToDo).id == id))) ==> true)
+             (($loc(($Self).todos, i)).$c_ToDo).$ToDo$id == id))) ==> true)
     ensures $Inv($Self)
     { var i: Int
       var res: Option[ToDo]
@@ -145,7 +147,7 @@ method getTodo($Self: Ref, id: Int)
          invariant ((0 <= i) && (i <= ($Self).num))
          { 
            label $lbl$continue$l;
-           if (((($loc(($Self).todos, i)).$c_ToDo).id == id))
+           if (((($loc(($Self).todos, i)).$c_ToDo).$ToDo$id == id))
               { 
                 res := Some(($loc(($Self).todos, i)).$c_ToDo);
                 goto $lbl$l; 
@@ -195,15 +197,11 @@ method completeTodo($Self: Ref, id: Int)
       old(($Self).nextId)))
     ensures ($size(($Self).todos) == old($size(($Self).todos)))
     ensures (forall i : Int :: ((((0 <= i) && (i < ($Self).num)) && (
-            (($loc(($Self).todos, i)).$c_ToDo).id != id)) ==> (($loc(
-                                                                ($Self).todos,
-                                                                i)).$c_ToDo == 
-            old(($loc(($Self).todos, i)).$c_ToDo))))
+            (($loc(($Self).todos, i)).$c_ToDo).$ToDo$id != id)) ==> (
+            ($loc(($Self).todos, i)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo))))
     ensures (forall i : Int :: ((((0 <= i) && (i < ($Self).num)) && (
-            (($loc(($Self).todos, i)).$c_ToDo).id == id)) ==> ((($loc(
-                                                                 ($Self).todos,
-                                                                 i)).$c_ToDo).completed == 
-            DONE())))
+            (($loc(($Self).todos, i)).$c_ToDo).$ToDo$id == id)) ==> (
+            (($loc(($Self).todos, i)).$c_ToDo).$ToDo$completed == DONE())))
     ensures $Inv($Self)
     { var i: Int
       i := 0;
@@ -218,21 +216,21 @@ method completeTodo($Self: Ref, id: Int)
                     ($loc(($Self).todos, ii)).$c_ToDo == old(($loc(($Self).todos,
                                                               ii)).$c_ToDo))))
          invariant (forall ii : Int :: ((((0 <= ii) && (ii < i)) && (
-                    (($loc(($Self).todos, ii)).$c_ToDo).id != id)) ==> (
+                    (($loc(($Self).todos, ii)).$c_ToDo).$ToDo$id != id)) ==> (
                     ($loc(($Self).todos, ii)).$c_ToDo == old(($loc(($Self).todos,
                                                               ii)).$c_ToDo))))
          invariant (forall ii : Int :: ((((0 <= ii) && (ii < i)) && (
-                    (($loc(($Self).todos, ii)).$c_ToDo).id == id)) ==> (
-                    (($loc(($Self).todos, ii)).$c_ToDo).completed == 
+                    (($loc(($Self).todos, ii)).$c_ToDo).$ToDo$id == id)) ==> (
+                    (($loc(($Self).todos, ii)).$c_ToDo).$ToDo$completed == 
                     DONE())))
          { 
            if (true)
               { var taskId: Int
                 var taskDesc: Int
                 var _completed: State
-                taskId := (($loc(($Self).todos, i)).$c_ToDo).id;
-                taskDesc := (($loc(($Self).todos, i)).$c_ToDo).desc;
-                _completed := (($loc(($Self).todos, i)).$c_ToDo).completed;
+                taskId := (($loc(($Self).todos, i)).$c_ToDo).$ToDo$id;
+                taskDesc := (($loc(($Self).todos, i)).$c_ToDo).$ToDo$desc;
+                _completed := (($loc(($Self).todos, i)).$c_ToDo).$ToDo$completed;
                 if ((taskId == id))
                    { 
                      ($loc(($Self).todos, i)).$c_ToDo := $RecordCtor_ToDo(
@@ -270,13 +268,13 @@ method showTodos($Self: Ref)
                                                               ii)).$c_ToDo))))
          { var todo: ToDo
            todo := ($loc(($Self).todos, i)).$c_ToDo;
-           output := $concat($concat(output, 2), (todo).desc);
-           if (((todo).completed).isDONE)
+           output := $concat($concat(output, 2), (todo).$ToDo$desc);
+           if (((todo).$ToDo$completed).isDONE)
               { 
                 output := $concat(output, 3); 
               }else
               { 
-                if (((todo).completed).isTODO)
+                if (((todo).$ToDo$completed).isTODO)
                    { 
                      output := $concat(output, 4); 
                    }; 
@@ -295,11 +293,14 @@ method clearCompleted($Self: Ref)
     ensures (($Self).nextId == old(($Self).nextId))
     ensures ($size(($Self).todos) == old($size(($Self).todos)))
     ensures (forall i : Int :: ((((0 <= i) && (i < old(($Self).num))) && (
-            old((($loc(($Self).todos, i)).$c_ToDo).completed) == TODO())) ==> 
-            (exists k : Int :: (((0 <= k) && (k < $size(($Self).todos))) && (
-            ($loc(($Self).todos, k)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo))))))
+            old((($loc(($Self).todos, i)).$c_ToDo).$ToDo$completed) == 
+            TODO())) ==> (exists k : Int :: (((0 <= k) && (k < $size(
+                                                               ($Self).todos))) && (
+                         ($loc(($Self).todos, k)).$c_ToDo == old(($loc(
+                                                                  ($Self).todos,
+                                                                  i)).$c_ToDo))))))
     ensures (forall i : Int :: (((0 <= i) && (i < ($Self).num)) ==> (
-            (($loc(($Self).todos, i)).$c_ToDo).completed == TODO())))
+            (($loc(($Self).todos, i)).$c_ToDo).$ToDo$completed == TODO())))
     ensures $Inv($Self)
     { var new_array: Array
       var i: Int
@@ -326,15 +327,17 @@ method clearCompleted($Self: Ref)
          invariant (j <= i)
          invariant ((0 <= j) && (j <= ($Self).num))
          invariant (forall ii : Int :: ((((0 <= ii) && (ii < i)) && (
-                    (($loc(($Self).todos, ii)).$c_ToDo).completed == 
+                    (($loc(($Self).todos, ii)).$c_ToDo).$ToDo$completed == 
                     TODO())) ==> (exists k : Int :: (((0 <= k) && (k < j)) && (
                                  ($loc(new_array, k)).$c_ToDo == ($loc(
                                                                   ($Self).todos,
                                                                   ii)).$c_ToDo)))))
          invariant (forall ii : Int :: (((0 <= ii) && (ii < j)) ==> (
-                    (($loc(new_array, ii)).$c_ToDo).completed == TODO())))
+                    (($loc(new_array, ii)).$c_ToDo).$ToDo$completed == 
+                    TODO())))
          { 
-           if (((($loc(($Self).todos, i)).$c_ToDo).completed == TODO()))
+           if (((($loc(($Self).todos, i)).$c_ToDo).$ToDo$completed == 
+              TODO()))
               { 
                 ($loc(new_array, j)).$c_ToDo := ($loc(($Self).todos, i)).$c_ToDo;
                 j := (j + 1); 

diff --git a/test/viper/record.mo b/test/viper/record.mo
@@ -1,30 +1,32 @@
 // @verify
 
 actor Record {
-  type R = { a: Int; b: Text; };
+  type R = { aa: Int; b: Text; };
 
-  let fld1: R = { a = 42; b = "abacaba" };
-  var fld2: R = { a = 42; b = "abacaba" };
+  let fld1: R = { aa = 42; b = "abacaba" };
+  var fld2: R = { aa = 42; b = "abacaba" };
 
-  let empty: R = { a = 0; b = "" };
+  let empty: R = { aa = 0; b = "" };
+
+  let aa: Int = 42; // A field to check that "moc" handles disambiguation in record fields
 
   func array_record() {
     let arr: [var R] = [var empty, empty];
-    arr[0] := { a = 100; b = "aaa" };
-    arr[1] := { a = 200; b = "bbb" };
+    arr[0] := { aa = 100; b = "aaa" };
+    arr[1] := { aa = 200; b = "bbb" };
 
-    assert:system arr[0] == { a = 100; b = "aaa" } and arr[1] == { a = 200; b = "bbb" };
+    assert:system arr[0] == { aa = 100; b = "aaa" } and arr[1] == { aa = 200; b = "bbb" };
   };
 
   func tuple_record() {
-    let tup: (R, R) = ({ a = 100; b = "aaa" }, { a = 200; b = "bbb" });
+    let tup: (R, R) = ({ aa = 100; b = "aaa" }, { aa = 200; b = "bbb" });
 
-    assert:system tup.0 == { a = 100; b = "aaa" } and tup.1 == { a = 200; b = "bbb" };
+    assert:system tup.0 == { aa = 100; b = "aaa" } and tup.1 == { aa = 200; b = "bbb" };
   };
 
   func get_record(): R {
-    assert:return (var:return) == { a = 100; b = "aaa" };
-    return { a = 100; b = "aaa" };
+    assert:return (var:return) == { aa = 100; b = "aaa" };
+    return { aa = 100; b = "aaa" };
   };
 
   func call_record() {
@@ -33,22 +35,25 @@ actor Record {
   };
 
   func record_arg(r: R): R {
-    assert:func r.a == 100;
-    assert:return (var:return).a == 100;
-    return { a = 100; b = "aaa" };
+    assert:func r.aa == 100;
+    assert:return (var:return).aa == 100;
+    return { aa = 100; b = "aaa" };
   };
 
   func pass_record() {
-    let res = record_arg({ a = 100; b = "42" });
-    assert:system res.a == 100;
+    let res = record_arg({ aa = 100; b = "42" });
+    assert:system res.aa == 100;
   };
 
   func match_on_record(): Int {
     assert:return (var:return) == 42;
 
     let r = get_record();
     switch r {
-      case { a = number; b } return number - 58;
+      case { aa = number; b } {
+        let c = b; // Check that "b" in scope
+        return number - 58;
+      }
     }
   };
 };