support own(x.f, a) syntax

nyu-acsys · Nov 12, 2024 · 29d1a6a · 29d1a6a
1 parent 9c16de7
commit 29d1a6a
Show file tree

Hide file tree

Showing 81 changed files with 450 additions and 432 deletions.
diff --git a/lib/frontend/typing.ml b/lib/frontend/typing.ml
@@ -161,8 +161,8 @@ let rec process_expr (expr : expr) (expected_typ : type_expr) : expr Rewriter.t
           Error.type_error (Expr.to_loc expr)
             (Expr.constr_to_string constr ^ " takes no arguments")
       (* Variables, fields, and call expressions *)
-      | Var qual_ident, args_list -> (
-          let* qual_ident, symbol =
+      | Var qual_ident, args_list ->
+        (let* qual_ident, symbol =
             Rewriter.resolve_and_find (Expr.to_loc expr) qual_ident
           in
           (*let _ = Logs.debug (fun m -> m !"process_expr: ident: %{QualIdent}" qual_ident) in*)
@@ -378,10 +378,33 @@ let rec process_expr (expr : expr) (expected_typ : type_expr) : expr Rewriter.t
           Error.type_error (Expr.to_loc expr)
             (Expr.constr_to_string constr ^ " takes exactly three arguments")
       (* Ownership predicates *)
-      | ( Own,
-          expr1
-          :: (App (Var qual_ident, [], expr_attr') as expr2)
-          :: expr3 :: expr4_opt ) ->
+      | ( Own, arg_list ) ->
+        let* expr1, expr2, expr3, expr4_opt =
+          match arg_list with
+          | App (Read, [expr1; (App (Var qual_ident, [], expr_attr') as expr2)], _) as expr12 :: expr3 :: expr4_opt ->
+            begin
+              try
+                let* qual_ident, symbol =
+                  Rewriter.resolve_and_find (Expr.to_loc expr) qual_ident
+                in
+                let+ symbol = Rewriter.Symbol.reify symbol in
+                match symbol with
+                | FieldDef _ -> expr1, expr2, expr3, expr4_opt
+                | _ -> failwith "retry below"
+              with _ ->
+              match expr4_opt with
+              | expr41 :: expr4_opt -> Rewriter.return (expr12, expr3, expr41, expr4_opt)
+              | _ -> Error.type_error (Expr.to_loc expr12) "Expected field location"
+            end
+          | expr1
+            :: (App (Var qual_ident, [], expr_attr') as expr2)
+            :: expr3 :: expr4_opt -> Rewriter.return (expr1, expr2, expr3, expr4_opt)
+          | _ ->
+            Error.type_error (Expr.to_loc expr)
+              (Expr.constr_to_string constr
+               ^ " takes either three or four arguments, and second argument is a \
+                  field name.")
+          in
           let* expr1 = process_expr expr1 Type.ref
           and* expr2 = process_expr expr2 Type.any in
 
@@ -406,11 +429,6 @@ let rec process_expr (expr : expr) (expected_typ : type_expr) : expr Rewriter.t
             Expr.App (Own, expr1 :: expr2 :: expr3 :: expr4_opt, expr_attr)
           in
           check_and_set expr Type.perm Type.perm expected_typ
-      | Own, _expr_list ->
-          Error.type_error (Expr.to_loc expr)
-            (Expr.constr_to_string constr
-            ^ " takes either three or four arguments, and second argument is a \
-               field name.")
       | AUPred call_name, token :: args_list ->
           let loc = Expr.to_loc expr in
           let* call_name, symbol = Rewriter.resolve_and_find loc call_name in

diff --git a/test/arrays/array.rav b/test/arrays/array.rav
@@ -19,7 +19,7 @@ interface Array[E: Library.Type] {
   val default_map: Map[Int, E] = {| i: Int :: default |}
 
   pred arr(a: T; m: Map[Int, E]) {
-    (forall j: Int :: {m[j]} 0 <= j < length(a) ==> own(loc(a, j), value, m[j], 1.0)) 
+    (forall j: Int :: {m[j]} 0 <= j < length(a) ==> own(loc(a, j).value, m[j], 1.0)) 
     && (forall j: Int :: {m[j]} (0 > j || j >= length(a)) ==> m[j] == default)
   }
 
@@ -236,4 +236,4 @@ interface Array[E: Library.Type] {
     }
   }
 
-}
+}
diff --git a/test/bugs/faulty_skolems.rav b/test/bugs/faulty_skolems.rav
@@ -5,6 +5,6 @@ func g(a: Int, b: Int) returns (r: Bool) { true }
 proc p() {
     var x: Ref;
 
-    inhale own(x, f, 5, 1.0);
-    exhale exists a: Int, b: Int :: g(a,b) ==> own(x, f, a, 1.0);
+    inhale own(x.f, 5, 1.0);
+    exhale exists a: Int, b: Int :: g(a,b) ==> own(x.f, a, 1.0);
 }
diff --git a/test/bugs/witness_comp.rav b/test/bugs/witness_comp.rav
@@ -6,14 +6,14 @@ pred pred1(x:Ref, v:Int) {
 
 proc p() {
     var x: Ref;
-    inhale exists v: Int :: own(x, c, v, 1.0) && pred1(x, v);
-    exhale exists v: Int :: own(x, c, v, 1.0) && pred1(x, v);
+    inhale exists v: Int :: own(x.c, v, 1.0) && pred1(x, v);
+    exhale exists v: Int :: own(x.c, v, 1.0) && pred1(x, v);
 
     // After witness computation, the above exhale gets replaced by:
-    //     exhale own(x, c, c$Heap[x].frac_proj1, 1.0) && pred1(x, c$Heap[x].frac_proj1);
+    //     exhale own(x.c, c$Heap[x].frac_proj1, 1.0) && pred1(x, c$Heap[x].frac_proj1);
 
     // which gets translated to:
-    //     exhale own(x, c, c$Heap[x].frac_proj1, 1.0) 
+    //     exhale own(x.c, c$Heap[x].frac_proj1, 1.0) 
     //     exhale pred1(x, c$Heap[x].frac_proj1);
 
     // After the first exhale, the value `c$Heap[x].frac_proj1` is no longer available.

diff --git a/test/bugs/witness_placeholders.rav b/test/bugs/witness_placeholders.rav
@@ -5,6 +5,6 @@ func g(a: Int, b: Int) returns (r: Bool) { true }
 proc p() {
     var x: Ref;
 
-    inhale own(x, f, 5, 1.0);
-    exhale exists a: Int :: true ==> own(x, f, a, 1.0);
+    inhale own(x.f, 5, 1.0);
+    exhale exists a: Int :: true ==> own(x.f, a, 1.0);
 }
diff --git a/test/ci/back-end/agree_inhale.rav b/test/ci/back-end/agree_inhale.rav
@@ -13,8 +13,8 @@ proc p() {
 
   assume (a1 != a2);
 
-  inhale own(x, f, NatAgree.agree(a1));
-  inhale own(x, f, NatAgree.agree(a2));
+  inhale own(x.f, NatAgree.agree(a1));
+  inhale own(x.f, NatAgree.agree(a2));
 
   assert false;
 }
diff --git a/test/ci/back-end/anti-aliasing.rav b/test/ci/back-end/anti-aliasing.rav
@@ -2,8 +2,8 @@ module Main {
     field f : Int
 
     proc test(x: Ref, y: Ref)
-        requires own(x, f, 1, 0.75) 
-        requires own(y, f, 1, 0.75)
+        requires own(x.f, 1, 0.75) 
+        requires own(y.f, 1, 0.75)
         ensures x != y
     { }
 }
diff --git a/test/ci/back-end/atomic_spec/counter_no_inv.rav b/test/ci/back-end/atomic_spec/counter_no_inv.rav
@@ -1,7 +1,7 @@
 field c: Int
 
 pred counter(x: Ref; v: Int) {
-  own(x, c, v, 1.0)
+  own(x.c, v, 1.0)
 }
 
 proc incr(x: Ref, implicit ghost v: Int) 

diff --git a/test/ci/back-end/atomic_spec/treiber_stack_atomics.rav b/test/ci/back-end/atomic_spec/treiber_stack_atomics.rav
@@ -15,11 +15,11 @@ type IntList = data {
 pred is_list(hd: Ref; xs: IntList) {
   hd == null ? 
     xs == nil() : 
-    (xs != nil() && (exists tl0: Ref, q:Real ::  q > 0.0 && (own(hd, value, xs.elem, q) && own(hd, next, tl0, q) && is_list(tl0, xs.tl))))
+    (xs != nil() && (exists tl0: Ref, q:Real ::  q > 0.0 && (own(hd.value, xs.elem, q) && own(hd.next, tl0, q) && is_list(tl0, xs.tl))))
 }
 
 pred is_stack(s: Ref; xs: IntList) {
-  exists hd: Ref :: (is_list(hd, xs) && own(s, head, hd, 1.0))
+  exists hd: Ref :: (is_list(hd, xs) && own(s.head, hd, 1.0))
 }
 
 proc push(s: Ref, x: Int, implicit ghost xs: IntList)
@@ -42,7 +42,7 @@ proc push(s: Ref, x: Int, implicit ghost xs: IntList)
 
   ghost var hd1: Ref;
   unfold is_stack(s, xs1);
-  hd1 :| is_list(hd1, xs1) && own(s, head, hd1, 1.0);
+  hd1 :| is_list(hd1, xs1) && own(s.head, hd1, 1.0);
 
   var res : Bool := cas(s.head, hd, s0);
 
@@ -51,7 +51,7 @@ proc push(s: Ref, x: Int, implicit ghost xs: IntList)
       assert   
         (s0 == null ? 
           cons(x, xs1) == nil() : 
-          (cons(x,xs1) != nil() && (1.0 > 0.0 && (own(s0, value, cons(x, xs1).elem, 1.0) && own(s0, next, hd1, 1.0) && is_list(hd1, cons(x, xs1).tl)))));
+          (cons(x,xs1) != nil() && (1.0 > 0.0 && (own(s0.value, cons(x, xs1).elem, 1.0) && own(s0.next, hd1, 1.0) && is_list(hd1, cons(x, xs1).tl)))));
 
       fold is_list(s0, cons(x, xs1)); 
       fold is_stack(s, cons(x, xs1));
@@ -101,11 +101,11 @@ proc pop(s: Ref, implicit ghost xs: IntList)
       tl0, q :| 
         hd == null ? 
         xs0 == nil() : 
-        (xs0 != nil() && (q > 0.0 && (own(hd, value, xs0.elem, q) && own(hd, next, tl0, q) && is_list(tl0, xs0.tl))));
+        (xs0 != nil() && (q > 0.0 && (own(hd.value, xs0.elem, q) && own(hd.next, tl0, q) && is_list(tl0, xs0.tl))));
 
       assert hd == null ? 
         xs0 == nil() : 
-        (xs0 != nil() && (q/2.0 > 0.0 && (own(hd, value, xs0.elem, q/2.0) && own(hd, next, tl0, q/2.0) && is_list(tl0, xs0.tl))));
+        (xs0 != nil() && (q/2.0 > 0.0 && (own(hd.value, xs0.elem, q/2.0) && own(hd.next, tl0, q/2.0) && is_list(tl0, xs0.tl))));
 
       fold is_list(hd, xs0);
       fold is_stack(s, xs0);
@@ -124,7 +124,7 @@ proc pop(s: Ref, implicit ghost xs: IntList)
 
   ghost var hd1: Ref;
   unfold is_stack(s, xs1);
-  hd1 :| is_list(hd1, xs1) && own(s, head, hd1, 1.0);
+  hd1 :| is_list(hd1, xs1) && own(s.head, hd1, 1.0);
 
   var res : Bool := cas(s.head, hd, hd_next);
 

diff --git a/test/ci/back-end/atomic_spec/treiber_stack_atomics.t b/test/ci/back-end/atomic_spec/treiber_stack_atomics.t
@@ -1,6 +1,6 @@
   $ dune exec -- raven --shh ./treiber_stack_atomics.rav
-  [Warning] File "./treiber_stack_atomics.rav", line 18, columns 21-136:
-  18 |     (xs != nil() && (exists tl0: Ref, q:Real ::  q > 0.0 && (own(hd, value, xs.elem, q) && own(hd, next, tl0, q) && is_list(tl0, xs.tl))))
-                            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+  [Warning] File "./treiber_stack_atomics.rav", line 18, columns 21-134:
+  18 |     (xs != nil() && (exists tl0: Ref, q:Real ::  q > 0.0 && (own(hd.value, xs.elem, q) && own(hd.next, tl0, q) && is_list(tl0, xs.tl))))
+                            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   Verification Error: No witnesses could be computed for: q.
   Verification successful.
diff --git a/test/ci/back-end/auth_inhale.rav b/test/ci/back-end/auth_inhale.rav
@@ -10,8 +10,8 @@ proc p() {
 
   // assume (a1 != a2);
 
-  inhale own(x, f, NatAuth.auth_frag(a1, b));
-  inhale own(x, f, NatAuth.auth_frag(a2, b));
+  inhale own(x.f, NatAuth.auth_frag(a1, b));
+  inhale own(x.f, NatAuth.auth_frag(a2, b));
 
   assert false;
 }
diff --git a/test/ci/back-end/bind_3.rav b/test/ci/back-end/bind_3.rav
@@ -1,8 +1,8 @@
 field f: Int
 
 proc p(x: Ref)
-  requires own(x, f, 5, 1.0)
+  requires own(x.f, 5, 1.0)
 {
   ghost var v: Int;
-  v :| own(x, f, v, 0.5);
+  v :| own(x.f, v, 0.5);
 }
diff --git a/test/ci/back-end/bind_4.rav b/test/ci/back-end/bind_4.rav
@@ -1,8 +1,8 @@
 field f: Int
 
 proc p(x: Ref)
-  requires own(x, f, 5, 0.5)
+  requires own(x.f, 5, 0.5)
 {
   ghost var v: Int;
-  v :| own(x, f, v, 1.0);
+  v :| own(x.f, v, 1.0);
 }
diff --git a/test/ci/back-end/bind_4.t b/test/ci/back-end/bind_4.t
@@ -1,6 +1,6 @@
   $ dune exec -- raven --shh bind_4.rav
-  [Error] File "bind_4.rav", line 7, columns 2-25:
-  7 |   v :| own(x, f, v, 1.0);
-        ^^^^^^^^^^^^^^^^^^^^^^^
+  [Error] File "bind_4.rav", line 7, columns 2-24:
+  7 |   v :| own(x.f, v, 1.0);
+        ^^^^^^^^^^^^^^^^^^^^^^
   Verification Error: The body of bind stmt could not be shown.
   [1]
diff --git a/test/ci/back-end/exhale_existential_quant_elim.rav b/test/ci/back-end/exhale_existential_quant_elim.rav
@@ -15,12 +15,12 @@ field h: IntSetRA
 proc p() {
   var x: Ref;
 
-  inhale own(x, f, NatAuth.auth_frag(3, 1));
-  inhale own(x, h, IntSetRA.set_constr({|3|}));
-  exhale exists v: Int :: own(x, h, IntSetRA.set_constr({|v|})) && own(x, f, NatAuth.auth_frag(v, 0));
-  // exhale exists v: Int :: own(x, f, NatAuth.auth_frag(v, 0));
+  inhale own(x.f, NatAuth.auth_frag(3, 1));
+  inhale own(x.h, IntSetRA.set_constr({|3|}));
+  exhale exists v: Int :: own(x.h, IntSetRA.set_constr({|v|})) && own(x.f, NatAuth.auth_frag(v, 0));
+  // exhale exists v: Int :: own(x.f, NatAuth.auth_frag(v, 0));
 
 
-  inhale forall z: Ref :: z != x ==> own(z, f, NatAuth.auth_frag(3, 1));
-  exhale forall z: Ref :: z != x ==> (exists v2: Int :: own(z, f, NatAuth.auth_frag(v2, 0)));
+  inhale forall z: Ref :: z != x ==> own(z.f, NatAuth.auth_frag(3, 1));
+  exhale forall z: Ref :: z != x ==> (exists v2: Int :: own(z.f, NatAuth.auth_frag(v2, 0)));
 }
diff --git a/test/ci/back-end/fail/fpu_fail.rav b/test/ci/back-end/fail/fpu_fail.rav
@@ -1,7 +1,7 @@
 field f: Int
 
 proc p(x:Ref, v:Int)
-  requires own(x, f, v, 0.75)
+  requires own(x.f, v, 0.75)
 
 {
   fpu(x, f, 4);

diff --git a/test/ci/back-end/fail/masks_1.rav b/test/ci/back-end/fail/masks_1.rav
@@ -1,7 +1,7 @@
 field f: Int
 
 inv inv1(x: Ref, v: Int) {
-  own(x, f, v, 1.0)
+  own(x.f, v, 1.0)
 }
 
 inv inv2(x: Ref, v: Int) {
@@ -11,7 +11,7 @@ inv inv2(x: Ref, v: Int) {
 
 proc q(x: Ref, v: Int) 
   requires inv1(x, v)
-  requires own(x, f, v, 1.0)
+  requires own(x.f, v, 1.0)
   ensures false
 {
   unfold inv1(x, v);

diff --git a/test/ci/back-end/fail/missing_permissions.rav b/test/ci/back-end/fail/missing_permissions.rav
@@ -2,15 +2,15 @@ module M {
   field f: Int
 
   proc q(x: Ref) 
-    requires exists v:Int :: own(x, f, v, 0.1)
-    // ensures exists v:Int :: own(x, f, v, 0.1)
+    requires exists v:Int :: own(x.f, v, 0.1)
+    // ensures exists v:Int :: own(x.f, v, 0.1)
   {
 
   }
 
   proc p(x: Ref)
-    requires exists v:Int :: own(x, f, v, 1.0)
-    ensures exists v:Int :: own(x, f, v, 1.0)
+    requires exists v:Int :: own(x.f, v, 1.0)
+    ensures exists v:Int :: own(x.f, v, 1.0)
   {
     q(x);
   }

diff --git a/test/ci/back-end/fail/missing_permissions.t b/test/ci/back-end/fail/missing_permissions.t
@@ -3,8 +3,8 @@
   16 |   }
           ^
   Verification Error: A postcondition may not hold at this return point.
-  [Error] File "./missing_permissions.rav", line 13, columns 12-45:
-  13 |     ensures exists v:Int :: own(x, f, v, 1.0)
-                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+  [Error] File "./missing_permissions.rav", line 13, columns 12-44:
+  13 |     ensures exists v:Int :: own(x.f, v, 1.0)
+                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   Related Location: This is the postcondition that may not hold.
   [1]
diff --git a/test/ci/back-end/forward_trg_assertions.rav b/test/ci/back-end/forward_trg_assertions.rav
@@ -17,7 +17,7 @@ proc p() {
     var b: Bool := true;
 
     if (b) {
-        inhale forall x: Ref :: { t(x) } guard(x, b) ==> own(loc_id(x), f, 1, 1.0);
+        inhale forall x: Ref :: { t(x) } guard(x, b) ==> own(loc_id(x).f, 1, 1.0);
     }
 
 }
diff --git a/test/ci/back-end/frac_ra_fpu.rav b/test/ci/back-end/frac_ra_fpu.rav
@@ -9,8 +9,8 @@ module Main {
     field f : M2
 
     proc test(x: Ref)
-        // requires own(x, f, M2.frac_chunk(4, 1/2))
-        requires own(x, f, M2.frac_chunk(4, 1.0))
+        // requires own(x.f, M2.frac_chunk(4, 1/2))
+        requires own(x.f, M2.frac_chunk(4, 1.0))
     {
         // var y: Ref = new(f);
         fpu(x, f, M2.frac_chunk(4, 1.0), M2.frac_chunk(5, 1.0));

diff --git a/test/ci/back-end/heap_valid_no_null_test.rav b/test/ci/back-end/heap_valid_no_null_test.rav
@@ -6,9 +6,9 @@ proc p() {
     x := new(f: 1, g: 1);
     x := new(g: 1);
 
-    inhale own(x, f, 1, 1.0);
-    inhale own(x, g, 1);
+    inhale own(x.f, 1, 1.0);
+    inhale own(x.g, 1);
 
-    exhale own(x, f, 1, 1.0);
-    exhale own(x, g, 1);
+    exhale own(x.f, 1, 1.0);
+    exhale own(x.g, 1);
 }