[Civl] Ticket example (#828)

- add test driver back
- remove nil in favor of Option
- use Lval and Lset

Source/Concurrency/YieldingProcDuplicator.cs

@@ -188,32 +188,31 @@ public override Implementation VisitImplementation(Implementation impl)
 
     public override Block VisitBlock(Block node)
     {
-      Block block = base.VisitBlock(node);
+      var block = base.VisitBlock(node);
       absyMap[block] = node;
       return block;
     }
 
     public override Cmd VisitAssertCmd(AssertCmd node)
     {
-      AssertCmd assertCmd = (AssertCmd) base.VisitAssertCmd(node);
+      var assertCmd = (AssertCmd) base.VisitAssertCmd(node);
       if (!node.Layers.Contains(layerNum))
       {
         assertCmd.Expr = Expr.True;
       }
-
       return assertCmd;
     }
 
     public override Cmd VisitCallCmd(CallCmd call)
     {
-      CallCmd newCall = (CallCmd) base.VisitCallCmd(call);
+      var newCall = (CallCmd) base.VisitCallCmd(call);
       absyMap[newCall] = call;
       return newCall;
     }
 
     public override Cmd VisitParCallCmd(ParCallCmd parCall)
     {
-      ParCallCmd newParCall = (ParCallCmd) base.VisitParCallCmd(parCall);
+      var newParCall = (ParCallCmd) base.VisitParCallCmd(parCall);
       absyMap[newParCall] = parCall;
       foreach (var newCall in newParCall.CallCmds)
       {

Source/Core/AST/Absy.cs

@@ -2480,7 +2480,7 @@ public override void Resolve(ResolutionContext rc)
 
     public override void Typecheck(TypecheckingContext tc)
     {
-      tc.ExpectedLayerRange = Layers == null || Layers.Count == 0 ? null : new LayerRange(Layers[0], Layers[^1]);
+      tc.ExpectedLayerRange = Layers?.Count > 0 ? new LayerRange(Layers[0], Layers[^1]) : null;
       this.Condition.Typecheck(tc);
       tc.ExpectedLayerRange = null;
       Contract.Assert(this.Condition.Type != null); // follows from postcondition of Expr.Typecheck
@@ -2604,7 +2604,7 @@ public override void Resolve(ResolutionContext rc)
 
     public override void Typecheck(TypecheckingContext tc)
     {
-      tc.ExpectedLayerRange = Layers == null || Layers.Count == 0 ? null : new LayerRange(Layers[0], Layers[^1]);
+      tc.ExpectedLayerRange = Layers?.Count > 0 ?new LayerRange(Layers[0], Layers[^1]) : null;
       this.Condition.Typecheck(tc);
       tc.ExpectedLayerRange = null;
       Contract.Assert(this.Condition.Type != null); // follows from postcondition of Expr.Typecheck

Source/Core/AST/AbsyCmd.cs

@@ -4389,7 +4389,7 @@ public override void Emit(TokenTextWriter stream, int level)
     public override void Typecheck(TypecheckingContext tc)
     {
       (this as ICarriesAttributes).TypecheckAttributes(tc);
-      tc.ExpectedLayerRange = Layers == null || Layers.Count == 0 ? null : new LayerRange(Layers[0], Layers[^1]);
+      tc.ExpectedLayerRange = Layers?.Count > 0 ? new LayerRange(Layers[0], Layers[^1]) : null;
       Expr.Typecheck(tc);
       tc.ExpectedLayerRange = null;
       Contract.Assert(Expr.Type != null); // follows from Expr.Typecheck postcondition

Source/Core/base.bpl

@@ -217,8 +217,8 @@ function Set_Intersection<T>(a: Set T, b: Set T): Set T
   Set(MapAnd(a->val, b->val))
 }
 
-function Set_Choose<T>(a: Set T): T;
-axiom (forall<T> a: Set T :: {Set_Choose(a)} a == Set_Empty() || Set_Contains(a, Set_Choose(a)));
+function Choice<T>(a: [T]bool): T;
+axiom (forall<T> a: [T]bool :: {Choice(a)} a == MapConst(false) || a[Choice(a)]);
 
 /// finite maps
 datatype Map<T,U> {

Test/civl/samples/reserve.bpl

@@ -100,7 +100,7 @@ pure action PreAlloc({:linear "tid"} tid: Tid, set: Set int, allocMap: Bijection
 {
     var ptr: int;
     assert set != Set_Empty();
-    ptr := Set_Choose(set);
+    ptr := Choice(set->val);
     allocMap' := Bijection(Map_Update(allocMap->tidToPtr, tid, ptr), Map_Update(allocMap->ptrToTid, ptr, tid));
 }
 

Test/civl/samples/ticket.bpl

@@ -6,12 +6,12 @@ function RightClosed (n: int) : [int]bool;
 axiom (forall x: int, y: int :: RightOpen(x)[y] <==> y < x);
 axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x);
 
-type {:linear "tid"} X;
-const nil: X;
-var {:layer 0,1} t: int;       // next ticket to issue
-var {:layer 0,2} s: int;       // current ticket permitted to critical section
-var {:layer 1,2} cs: X;        // current thread in critical section
-var {:layer 1,2} T: [int]bool; // set of issued tickets
+type Tid;
+
+var {:layer 0,1} t: int;           // next ticket to issue
+var {:layer 0,2} s: int;           // current ticket permitted to critical section
+var {:layer 1,2} cs: Option Tid;   // current thread in critical section
+var {:layer 1,2} T: [int]bool;     // set of issued tickets
 
 // ###########################################################################
 // Invariants
@@ -21,31 +21,58 @@ function {:inline} Inv1 (tickets: [int]bool, ticket: int): (bool)
   tickets == RightOpen(ticket)
 }
 
-function {:inline} Inv2 (tickets: [int]bool, ticket: int, lock: X): (bool)
+function {:inline} Inv2 (tickets: [int]bool, ticket: int, lock: Option Tid): (bool)
 {
-  if (lock == nil) then tickets == RightOpen(ticket)
-                   else tickets == RightClosed(ticket)
+  if (lock is None) then tickets == RightOpen(ticket)
+                    else tickets == RightClosed(ticket)
 }
 
 // ###########################################################################
 // Yield invariants
 
-yield invariant {:layer 2} YieldSpec ({:linear "tid"} tid: X);
-invariant tid != nil && cs == tid;
+yield invariant {:layer 2} YieldSpec (tid: Lval Tid);
+invariant cs is Some && cs->t == tid->val;
 
 yield invariant {:layer 1} Yield1 ();
 invariant Inv1(T, t);
 
 yield invariant {:layer 2} Yield2 ();
 invariant Inv2(T, s, cs);
 
+// ###########################################################################
+// Test driver
+
+yield procedure {:layer 2} main ({:layer 1,2} {:linear_in} _tids: Lset Tid)
+requires call Yield1();
+requires call Yield2();
+{
+  var {:layer 1,2} tid: Lval Tid;
+  var {:layer 1,2} tids: Lset Tid;
+
+  tids := _tids;
+  while (*)
+  invariant {:yields} true;
+  invariant call Yield1();
+  invariant call Yield2();
+  {
+    call {:layer 1,2} tid, tids := Allocate(tids);
+    async call Customer(tid);
+  }
+}
+
+pure procedure {:inline 1} Allocate({:linear_in} _tids: Lset Tid) returns (tid: Lval Tid, tids: Lset Tid)
+{
+  tids := _tids;
+  assume {:layer 1,2} tids->dom != MapConst(false);
+  call {:layer 1,2} tid := Lval_Get(tids, Choice(tids->dom));
+}
+
 // ###########################################################################
 // Procedures and actions
 
-yield procedure {:layer 2} Customer ({:layer 1,2} {:linear_in "tid"} tid: X)
+yield procedure {:layer 2} Customer ({:layer 1,2} tid: Lval Tid)
 requires call Yield1();
 requires call Yield2();
-requires {:layer 2} tid != nil;
 {
   while (*)
   invariant {:yields} true;
@@ -58,22 +85,21 @@ requires {:layer 2} tid != nil;
   }
 }
 
-yield procedure {:layer 2} Enter ({:layer 1,2} {:linear "tid"} tid: X)
+yield procedure {:layer 2} Enter ({:layer 1,2} tid: Lval Tid)
 preserves call Yield1();
 preserves call Yield2();
 ensures   call YieldSpec(tid);
-requires {:layer 2} tid != nil;
 {
   var m: int;
 
   call m := GetTicket(tid);
   call WaitAndEnter(tid, m);
 }
 
-right action {:layer 2} AtomicGetTicket ({:linear "tid"} tid: X) returns (m: int)
+right action {:layer 2} AtomicGetTicket (tid: Lval Tid) returns (m: int)
 modifies T;
 { assume !T[m]; T[m] := true; }
-yield procedure {:layer 1} GetTicket ({:layer 1} {:linear "tid"} tid: X) returns (m: int)
+yield procedure {:layer 1} GetTicket ({:layer 1} tid: Lval Tid) returns (m: int)
 refines AtomicGetTicket;
 preserves call Yield1();
 {
@@ -87,31 +113,31 @@ modifies t;
 yield procedure {:layer 0} GetTicket#0 () returns (m: int);
 refines AtomicGetTicket#0;
 
-atomic action {:layer 2} AtomicWaitAndEnter ({:linear "tid"} tid: X, m:int)
+atomic action {:layer 2} AtomicWaitAndEnter (tid: Lval Tid, m:int)
 modifies cs;
-{ assume m == s; cs := tid; }
-yield procedure {:layer 1} WaitAndEnter ({:layer 1} {:linear "tid"} tid: X, m:int)
+{ assume m == s; cs := Some(tid->val); }
+yield procedure {:layer 1} WaitAndEnter ({:layer 1} tid: Lval Tid, m:int)
 refines AtomicWaitAndEnter;
 preserves call Yield1();
 {
   call WaitAndEnter#0(m);
-  call {:layer 1} cs := Copy(tid);
+  call {:layer 1} cs := Copy(Some(tid->val));
 }
 
 atomic action {:layer 1} AtomicWaitAndEnter#0 (m:int)
 { assume m == s; }
 yield procedure {:layer 0} WaitAndEnter#0 (m:int);
 refines AtomicWaitAndEnter#0;
 
-atomic action {:layer 2} AtomicLeave ({:linear "tid"} tid: X)
+atomic action {:layer 2} AtomicLeave (tid: Lval Tid)
 modifies cs, s;
-{ assert cs == tid; s := s + 1; cs := nil; }
-yield procedure {:layer 1} Leave ({:layer 1} {:linear "tid"} tid: X)
+{ assert cs == Some(tid->val); s := s + 1; cs := None(); }
+yield procedure {:layer 1} Leave ({:layer 1} tid: Lval Tid)
 refines AtomicLeave;
 preserves call Yield1();
 {
   call Leave#0();
-  call {:layer 1} cs := Copy(nil);
+  call {:layer 1} cs := Copy(None());
 }
 
 atomic action {:layer 1} AtomicLeave#0 ()

Test/civl/samples/ticket.bpl.expect

@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 11 verified, 0 errors
+Boogie program verifier finished with 10 verified, 0 errors