fixed bugs wrt renamings in newly added use_desc.use_binds and use_wi…

…tnesses; rewrote ticketLock to use a loop

lib/ast/astDef.ml

@@ -1332,10 +1332,24 @@ module Stmt = struct
 
     | Spec (spec_kind, sf) -> pr_spec_list (spec_kind_to_string spec_kind) ppf [ sf ]
     | Use use_desc ->
-      fprintf ppf "@[<2>%s %a(@[%a@])@]"
+      fprintf ppf "@[<2>%s %a(@[%a@])[%a]{%a}  @]"
         (use_kind_to_string use_desc.use_kind)
         QualIdent.pr use_desc.use_name
+
         Expr.pr_list use_desc.use_args
+
+        (Fmt.Dump.option (Util.Print.pr_list_comma (fun ppf (i,e) -> 
+          Stdlib.Format.fprintf ppf "%a := %a"
+          Ident.pr i
+          Expr.pr e
+        )))  use_desc.use_witnesses
+
+        (Fmt.Dump.option (Util.Print.pr_list_comma (fun ppf (i_b, i_e) -> 
+          Stdlib.Format.fprintf ppf "%a :| %a"
+          Ident.pr i_b
+          Ident.pr i_e
+        ))) use_desc.use_binds
+
     | Return e -> fprintf ppf "@[<2>return@ %a@]" Expr.pr e
     | Call cstm -> (
         match cstm.call_lhs with
@@ -1552,7 +1566,22 @@ module Stmt = struct
           Expr.symbols ~acc:accesses e
 
         | Use use_desc ->
-          scan_expr_list accesses use_desc.use_args
+          let accesses = scan_expr_list accesses use_desc.use_args in
+          let accesses = match use_desc.use_witnesses with
+          | None -> accesses
+          | Some use_witnesses ->
+            scan_expr_list accesses (List.map use_witnesses ~f:(fun (i_e, wtns) -> wtns))
+          in
+
+          let accesses = match use_desc.use_binds with
+            | None -> accesses
+            | Some use_binds_list ->
+              List.fold ~init:accesses use_binds_list ~f:(
+                fun acc (i_b, _i_e) -> 
+                  Set.add acc (QualIdent.from_ident i_b)
+              )
+            in
+          accesses
 
         | AUAction _ -> accesses
 
@@ -1845,7 +1874,7 @@ module Callable = struct
           fprintf ppf "returns (@[<0>%a@])" Expr.pr_var_decl_list rs
     in
     let pr_call_locals ppf = function
-      | [] -> ()
+      (* | [] -> () *)
       | ls ->
           fprintf ppf "@\n/*locals (@[<0>%a@])*/" Expr.pr_var_decl_list ls
     in

lib/ast/rewriter.ml

@@ -826,12 +826,37 @@ module Stmt = struct
             }
         | Use use_desc ->
             let use_name = f use_desc.use_name in
-            let+ use_args =
+
+            let* use_args =
               List.map use_desc.use_args ~f:(Expr.rewrite_qual_idents ~f)
             in
+            let+ use_witnesses = match use_desc.use_witnesses with
+              | None -> return None
+              | Some use_wtnss -> 
+                let+ use_wtnss = List.map use_wtnss ~f:(fun (i, e) -> 
+                  let+ e = Expr.rewrite_qual_idents ~f e in
+                    (i, e)
+                ) in
+
+                Some use_wtnss
+            in
+
+            let use_binds = match use_desc.use_binds with
+              | None -> None
+              | Some use_bnds -> Some (
+                Base.List.map use_bnds ~f:(fun (i_b, i_ex) -> 
+                  let i_b = QualIdent.to_ident (f (QualIdent.from_ident i_b)) in
+                    (i_b, i_ex)
+                )
+              )
+            in
+
             {
               stmt with
-              stmt_desc = Basic (Use { use_desc with use_name; use_args });
+              stmt_desc = Basic (Use { 
+                  use_desc with 
+                  use_name; use_args; use_witnesses; use_binds 
+              });
             }
         | New new_desc ->
             let new_lhs = f new_desc.new_lhs in

test/concurrent/lock/ticket-lock.rav

@@ -53,28 +53,6 @@ module TicketLock[R: LockResource]
     );
     fold lock_inv(l, r)[b := false];
   }
-
-  proc wait_loop(l: Ref, x: Int, implicit ghost r: R)
-    requires lock_inv(l, r) && own(l, tickets, ADS.frag(IntSet.set({|x|})))
-    ensures resource(r)
-  {
-    ghost var n: Int; ghost var c: Int; ghost var b: Bool;
-
-    unfold lock_inv(l, r){
-      b :| b, n :| n, c :| c 
-    };
-
-    val crr: Int := l.curr;
-
-    if (x == crr) {
-      fold lock_inv(l, r)[ b := true];
-      return;
-    } else{
-      fold lock_inv(l, r)[ b := b];
-      wait_loop(l, x);
-    }
-  }
-
 
   proc acquire(l: Ref, implicit ghost r: R)
     requires lock_inv(l, r)
@@ -92,13 +70,10 @@ module TicketLock[R: LockResource]
       if (res) {
         fpu( l, tickets, 
             ADS.auth_frag(
-              IntSet.set({|i: Int :: 0 <= i && i < x|}), 
-              IntSet.set({||})
-            ), 
-
+              IntSet.set({|i: Int :: 0 <= i && i < x|}), IntSet.set({||})
+            ),
             ADS.auth_frag(
-              IntSet.set({|i: Int :: 0 <= i && i < x+1|}), 
-              IntSet.set({|x|})
+              IntSet.set({|i: Int :: 0 <= i && i < x+1|}), IntSet.set({|x|})
             )
         );
 
@@ -109,7 +84,32 @@ module TicketLock[R: LockResource]
     !}
 
     if (res) {
-      wait_loop(l, x);
+      var acq_flag: Bool = false;
+
+      while(!acq_flag)
+        invariant 
+          lock_inv(l, r) && 
+          (
+            acq_flag ? 
+              resource(r) :
+              own(l, tickets, ADS.frag(  IntSet.set({| x |})  ))
+          )
+      {
+        ghost var b1: Bool;
+        unfold lock_inv(l, r) {  b1 :| b  };
+
+        var crr: Int := l.curr;
+
+        if (x != crr) {
+          fold lock_inv(l, r)[ b := b1];
+        } else {
+          fold lock_inv(l, r)[ b := true];
+          acq_flag := true;
+        }
+      }
+
+      return;
+
     } else {
       acquire(l);
     }