[Civl] eliminate use of Lval (#843)

Test/civl/regression-tests/linear-test.bpl

@@ -8,15 +8,6 @@ yield procedure {:layer 1} foo1({:linear "A"} x: int, {:linear "A"} y: int)
     assert {:layer 1} x != y;
 }
 
-yield procedure {:layer 1} foo2({:layer 1} {:linear_in} x: Lset int, i: int) returns ({:layer 1} y: Lset int)
-requires {:layer 1} x->dom[i];
-{
-    var {:layer 1} v: Lval int;
-    y := x;
-    call {:layer 1} v := Lval_Get(y, i);
-    assert {:layer 1} !Lset_Contains(y, i);
-}
-
 yield procedure {:layer 1} foo3({:layer 1} {:linear_in} x: Lset int, i: [int]bool) returns ({:layer 1} y: Lset int)
 requires {:layer 1} IsSubset(i, x->dom);
 {

Test/civl/regression-tests/linear-test.bpl.expect

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

Test/civl/regression-tests/linear_types.bpl

@@ -7,13 +7,6 @@ atomic action {:layer 1, 2} A3({:linear_in} path: Lset int, {:linear_out} l: Lse
     call Lset_Split(path', l);
 }
 
-atomic action {:layer 1, 2} A4({:linear_in} path: Lset int, l: Lval int) returns (path': Lset int) {
-    call path' := Lset_Empty();
-    call Lset_Put(path', path);
-    call Lval_Put(path', l);
-    call Lval_Split(path', l);
-}
-
 atomic action {:layer 1, 2} A5({:linear_in} path: Lheap int) returns (path': Lheap int) {
     path' := path;
 }
@@ -22,22 +15,9 @@ var {:layer 0, 2} g: Lheap int;
 
 datatype Foo { Foo(f: Lheap int) }
 
-atomic action {:layer 1, 2} A8({:linear_out} l: Lval int, {:linear_in} path: Lset int) returns (path': Lset int)
-{
-    path' := path;
-    call Lval_Split(path', l);
-}
-
 atomic action {:layer 1, 2} A10({:linear_in} a: Foo) returns (b: Foo)
 {
     var x: Lheap int;
     Foo(x) := a;
     b := Foo(x);
 }
-
-datatype Bar { Bar(x: Lval int, y: int) }
-
-atomic action {:layer 1, 2} A11({:linear_in} a: Lval int) returns (b: Bar)
-{
-    b := Bar(a, 3+4);
-}

Test/civl/regression-tests/linear_types_error.bpl

@@ -37,16 +37,6 @@ atomic action {:layer 1, 2} A13({:linear_in} a: Foo) returns (b: Foo)
     b := Foo(x);
 }
 
-datatype Bar { Bar(x: Lval int, y: int) }
-
-atomic action {:layer 1, 2} A14({:linear_in} a: Lval int) returns (b: Bar)
-{
-    b := Bar(Lval(3), 3+4);
-}
-
-type {:linear "X"} X = int;
-yield procedure {:layer 1} A15({:linear_in "X"} a: Lval int);
-
 yield procedure {:layer 1} Foo1(x: Lheap int)
 {
   call Lmap_Assume(x, x);

Test/civl/regression-tests/linear_types_error.bpl.expect

@@ -1,12 +1,10 @@
-linear_types_error.bpl(48,48): Error: Variable of linear type must not have a domain name
 linear_types_error.bpl(4,73): Error: Output variable l must be available at a return
 linear_types_error.bpl(8,0): Error: Input variable path must be available at a return
 linear_types_error.bpl(13,0): Error: Input variable path must be available at a return
 linear_types_error.bpl(19,64): Error: Input variable path must be available at a return
 linear_types_error.bpl(25,0): Error: Output variable b must be available at a return
 linear_types_error.bpl(31,14): Error: unavailable source for a linear read
 linear_types_error.bpl(37,9): Error: unavailable source for a linear read
-linear_types_error.bpl(44,6): Error: A source of pack of linear type must be a variable
-linear_types_error.bpl(52,2): Error: Linear variable x can occur only once as an input parameter
-linear_types_error.bpl(57,2): Error: Linear variable x can occur only once as an input parameter
-11 type checking errors detected in linear_types_error.bpl
+linear_types_error.bpl(42,2): Error: Linear variable x can occur only once as an input parameter
+linear_types_error.bpl(47,2): Error: Linear variable x can occur only once as an input parameter
+9 type checking errors detected in linear_types_error.bpl

Test/civl/samples/MutexOverFutex.bpl

@@ -1,7 +1,7 @@
 // RUN: %parallel-boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-type Tid; // thread identifiers
+type {:linear "tid"} Tid; // thread identifiers
 
 type Mutex = Option Tid;
 
@@ -13,21 +13,21 @@ var {:layer 0, 1} futex: Futex;           // implementation
 
 /// Implementation of Mutex
 
-atomic action {:layer 2} AtomicLock(tid: Lval Tid)
+atomic action {:layer 2} AtomicLock({:linear "tid"} tid: Tid)
 modifies mutex;
 {
   assume mutex == None();
-  mutex := Some(tid->val);
+  mutex := Some(tid);
 }
-yield procedure {:layer 1} Lock(tid: Lval Tid)
+yield procedure {:layer 1} Lock({:linear "tid"} tid: Tid)
 refines AtomicLock;
 preserves call YieldInv();
 preserves call YieldWait(tid);
 {
   var oldValue, temp: int;
   call oldValue := CmpXchg(0, 1);
   if (oldValue != 0) {
-    call {:layer 1} inSlowPath := Copy(inSlowPath[tid->val := true]);
+    call {:layer 1} inSlowPath := Copy(inSlowPath[tid := true]);
     while (true)
     invariant {:yields} true;
     invariant call YieldInv();
@@ -39,28 +39,28 @@ preserves call YieldWait(tid);
       }
       par YieldInv() | YieldWait(tid) | YieldSlowPath(tid);
       if (oldValue == 2 || temp != 0) {
-        call WaitEnter(tid->val, 2);
+        call WaitEnter(tid, 2);
         par YieldInv() | YieldSlowPath(tid);
-        call WaitExit(tid->val);
+        call WaitExit(tid);
       }
       par YieldInv() | YieldWait(tid) | YieldSlowPath(tid);
       call oldValue := CmpXchg(0, 2);
       if (oldValue == 0) {
-        call {:layer 1} inSlowPath := Copy(inSlowPath[tid->val := false]);
+        call {:layer 1} inSlowPath := Copy(inSlowPath[tid := false]);
         break;
       }
     }
   }
-  call {:layer 1} mutex := Copy(Some(tid->val));
+  call {:layer 1} mutex := Copy(Some(tid));
 }
 
-atomic action {:layer 2} AtomicUnlock(tid: Lval Tid)
+atomic action {:layer 2} AtomicUnlock({:linear "tid"} tid: Tid)
 modifies mutex;
 {
-  assert mutex == Some(tid->val);
+  assert mutex == Some(tid);
   mutex := None();
 }
-yield procedure {:layer 1} Unlock(tid: Lval Tid)
+yield procedure {:layer 1} Unlock({:linear "tid"} tid: Tid)
 refines AtomicUnlock;
 preserves call YieldInv();
 preserves call YieldWait(tid);
@@ -70,13 +70,13 @@ preserves call YieldWait(tid);
   if (oldValue == 1) {
     call {:layer 1} mutex := Copy(None());
   } else {
-    call {:layer 1} inSlowPath := Copy(inSlowPath[tid->val := true]);
+    call {:layer 1} inSlowPath := Copy(inSlowPath[tid := true]);
     par YieldInv() | YieldWait(tid) | YieldSlowPath(tid);
     call Store(0);
     call {:layer 1} mutex := Copy(None());
     par YieldInv() | YieldWait(tid) | YieldSlowPath(tid);
     call Wake();
-    call {:layer 1} inSlowPath := Copy(inSlowPath[tid->val := false]);
+    call {:layer 1} inSlowPath := Copy(inSlowPath[tid := false]);
   }
 }
 
@@ -92,11 +92,11 @@ invariant (forall i: Tid :: futex->waiters[i] ==> inSlowPath[i]);
 invariant futex->word == 2 || futex->waiters == MapConst(false) || (exists i: Tid :: !futex->waiters[i] && inSlowPath[i]);
 invariant mutex == None() <==> futex->word == 0;
 
-yield invariant {:layer 1} YieldWait(tid: Lval Tid);
-invariant !futex->waiters[tid->val];
+yield invariant {:layer 1} YieldWait({:linear "tid"} tid: Tid);
+invariant !futex->waiters[tid];
 
-yield invariant {:layer 1} YieldSlowPath(tid: Lval Tid);
-invariant inSlowPath[tid->val];
+yield invariant {:layer 1} YieldSlowPath({:linear "tid"} tid: Tid);
+invariant inSlowPath[tid];
 
 /// Primitive atomic actions
 

Test/civl/samples/MutexOverFutex.bpl.expect

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

Test/civl/samples/bluetooth.bpl

@@ -40,10 +40,10 @@ invariant pendingIo == Size(usersInDriver->dom) + (if stoppingFlag then 0 else 1
 // user code
 
 yield procedure {:layer 2}
-User(i: int, {:layer 1,2} l: Lval Perm, {:layer 1,2} r: Lval Perm)
+User(i: int, {:layer 1,2} l: Lset Perm, {:layer 1,2} r: Lset Perm)
 preserves call Inv2();
 preserves call Inv1();
-requires {:layer 1, 2} l->val == Left(i) && r->val == Right(i);
+requires {:layer 1, 2} l->dom == MapOne(Left(i)) && r->dom == MapOne(Right(i));
 {
     while (*)
     invariant {:yields} true;
@@ -56,56 +56,57 @@ requires {:layer 1, 2} l->val == Left(i) && r->val == Right(i);
     }
 }
 
-atomic action {:layer 2} AtomicEnter#1(i: int, {:linear_in} l: Lval Perm, r: Lval Perm)
+atomic action {:layer 2} AtomicEnter#1(i: int, {:linear_in} l: Lset Perm, r: Lset Perm)
 modifies usersInDriver;
 {
     assume !stoppingFlag;
-    call Lval_Put(usersInDriver, l);
+    call Lset_Put(usersInDriver, l);
 }
 yield procedure {:layer 1}
-Enter#1(i: int, {:layer 1} {:linear_in} l: Lval Perm, {:layer 1} r: Lval Perm)
+Enter#1(i: int, {:layer 1} {:linear_in} l: Lset Perm, {:layer 1} r: Lset Perm)
 refines AtomicEnter#1;
 preserves call Inv1();
-requires {:layer 1} l->val == Left(i) && r->val == Right(i);
+requires {:layer 1} l->dom == MapOne(Left(i)) && r->dom == MapOne(Right(i));
 {
     call Enter();
     call {:layer 1} SizeLemma(usersInDriver->dom, Left(i));
-    call {:layer 1} Lval_Put(usersInDriver, l);
+    call {:layer 1} Lset_Put(usersInDriver, l);
 }
 
-left action {:layer 2} AtomicCheckAssert#1(i: int, r: Lval Perm)
+left action {:layer 2} AtomicCheckAssert#1(i: int, r: Lset Perm)
 {
-    assert r->val == Right(i) && usersInDriver->dom[Left(i)];
+    assert r->dom == MapOne(Right(i)) && usersInDriver->dom[Left(i)];
     assert !stopped;
 }
 yield procedure {:layer 1}
-CheckAssert#1(i: int, {:layer 1} r: Lval Perm)
+CheckAssert#1(i: int, {:layer 1} r: Lset Perm)
 refines AtomicCheckAssert#1;
 preserves call Inv1();
 {
     call CheckAssert();
 }
 
-left action {:layer 2} AtomicExit(i: int, {:linear_out} l: Lval Perm, r: Lval Perm)
+left action {:layer 2} AtomicExit(i: int, {:linear_out} l: Lset Perm, r: Lset Perm)
 modifies usersInDriver;
 {
-    assert l->val == Left(i) && r->val == Right(i);
-    call Lval_Split(usersInDriver, l);
+    assert l->dom == MapOne(Left(i)) && r->dom == MapOne(Right(i));
+    call Lset_Split(usersInDriver, l);
 }
 yield procedure {:layer 1}
-Exit(i: int, {:layer 1} {:linear_out} l: Lval Perm, {:layer 1} r: Lval Perm)
+Exit(i: int, {:layer 1} {:linear_out} l: Lset Perm, {:layer 1} r: Lset Perm)
 refines AtomicExit;
 preserves call Inv1();
 {
     call DeleteReference();
     call {:layer 1} SizeLemma(usersInDriver->dom, Left(i));
-    call {:layer 1} Lval_Split(usersInDriver, l);
+    call {:layer 1} Lset_Split(usersInDriver, l);
     call {:layer 1} SubsetSizeRelationLemma(MapConst(false), usersInDriver->dom);
 }
 
 // stopper code
+type {:linear "stopper"} X = int;
 
-yield procedure {:layer 2} Stopper(i: Lval int)
+yield procedure {:layer 2} Stopper({:linear "stopper"} i: int)
 refines AtomicSetStoppingFlag;
 preserves call Inv2();
 preserves call Inv1();
@@ -114,7 +115,7 @@ preserves call Inv1();
     call WaitAndStop();
 }
 
-yield procedure {:layer 1} Close(i: Lval int)
+yield procedure {:layer 1} Close({:linear "stopper"} i: int)
 refines AtomicSetStoppingFlag;
 preserves call Inv1();
 {
@@ -155,16 +156,16 @@ atomic action {:layer 1} AtomicCheckAssert()
 yield procedure {:layer 0} CheckAssert();
 refines AtomicCheckAssert;
 
-right action {:layer 1,3} AtomicSetStoppingFlag(i: Lval int)
+right action {:layer 1,3} AtomicSetStoppingFlag({:linear "stopper"} i: int)
 modifies stoppingFlag;
 {
     // The first assertion ensures that there is at most one stopper.
     // Otherwise AtomicSetStoppingFlag does not commute with itself.
-    assert i->val == 0;
+    assert i == 0;
     assert !stoppingFlag;
     stoppingFlag := true;
 }
-yield procedure {:layer 0} SetStoppingFlag(i: Lval int);
+yield procedure {:layer 0} SetStoppingFlag({:linear "stopper"} i: int);
 refines AtomicSetStoppingFlag;
 
 atomic action {:layer 1} AtomicDeleteReference()