[Civl] eliminate use of Lset (#844)

boogie-org · Jan 28, 2024 · aa88c55 · aa88c55
1 parent a3c0ea8
commit aa88c55
Show file tree

Hide file tree

Showing 11 changed files with 115 additions and 184 deletions.
diff --git a/Test/civl/regression-tests/linear-test.bpl b/Test/civl/regression-tests/linear-test.bpl
@@ -7,12 +7,3 @@ yield procedure {:layer 1} foo1({:linear "A"} x: int, {:linear "A"} y: int)
 {
     assert {:layer 1} x != y;
 }
-
-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);
-{
-    var {:layer 1} v: Lset int;
-    y := x;
-    call {:layer 1} v := Lset_Get(y, i);
-    assert {:layer 1} IsDisjoint(y->dom, i);
-}
diff --git a/Test/civl/regression-tests/linear-test.bpl.expect b/Test/civl/regression-tests/linear-test.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 2 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/civl/regression-tests/linear_types.bpl b/Test/civl/regression-tests/linear_types.bpl
diff --git a/Test/civl/regression-tests/linear_types_error.bpl b/Test/civl/regression-tests/linear_types_error.bpl
diff --git a/Test/civl/regression-tests/linear_types_error.bpl.expect b/Test/civl/regression-tests/linear_types_error.bpl.expect
diff --git a/Test/civl/samples/alloc-mem.bpl b/Test/civl/samples/alloc-mem.bpl
@@ -1,15 +1,19 @@
 // RUN: %parallel-boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-function {:inline} PoolInv(unallocated:[int]bool, pool:Lset int) : (bool)
+type {:linear "mem"} X = int;
+function {:inline}{:linear "mem"} SetCollector(x: Set int): [int]bool { x->val }
+function {:inline}{:linear "mem"} MapCollector(x: Map int int): [int]bool { SetCollector(x->dom) }
+
+function {:inline} PoolInv(unallocated:[int]bool, pool:Set int) : (bool)
 {
-  (forall x:int :: unallocated[x] ==> Lset_Contains(pool, x))
+  (forall x:int :: unallocated[x] ==> Set_Contains(pool, x))
 }
 
 yield procedure {:layer 2} Main ()
 preserves call Yield();
 {
-  var {:layer 1,2} l:Lmap int int;
+  var {:layer 1,2} {:linear "mem"} l:Map int int;
   var i:int;
   while (*)
     invariant {:yields} true;
@@ -20,13 +24,13 @@ preserves call Yield();
   }
 }
 
-yield procedure {:layer 2} Thread ({:layer 1,2} {:linear_in} local_in:Lmap int int, i:int)
+yield procedure {:layer 2} Thread ({:layer 1,2} {:linear_in "mem"} local_in:Map int int, i:int)
 preserves call Yield();
-requires {:layer 1,2} Map_Contains(local_in->val, i);
+requires {:layer 1,2} Map_Contains(local_in, i);
 {
   var y, o:int;
-  var {:layer 1,2} local:Lmap int int;
-  var {:layer 1,2} l:Lmap int int;
+  var {:layer 1,2} {:linear "mem"} local:Map int int;
+  var {:layer 1,2} {:linear "mem"} l:Map int int;
 
   call local := Write(local_in, i, 42);
   call o := Read(local, i);
@@ -43,56 +47,55 @@ requires {:layer 1,2} Map_Contains(local_in->val, i);
   }
 }
 
-right action {:layer 2} atomic_Alloc() returns (l:Lmap int int, i:int)
+right action {:layer 2} atomic_Alloc() returns ({:linear "mem"} l:Map int int, i:int)
 modifies pool;
 {
-  assume Lset_Contains(pool, i);
+  assume Set_Contains(pool, i);
   call l, pool := AllocLinear(i, pool);
 }
 
 yield procedure {:layer 1}
-Alloc() returns ({:layer 1} l:Lmap int int, i:int)
+Alloc() returns ({:layer 1} {:linear "mem"} l:Map int int, i:int)
 refines atomic_Alloc;
 preserves call Yield();
-ensures {:layer 1} Map_Contains(l->val, i);
+ensures {:layer 1} Map_Contains(l, i);
 {
   call i := PickAddr();
   call {:layer 1} l, pool := AllocLinear(i, pool);
 }
 
-left action {:layer 2} atomic_Free({:linear_in} l:Lmap int int, i:int)
+left action {:layer 2} atomic_Free({:linear_in "mem"} l:Map int int, i:int)
 modifies pool;
 {
-  var t:Lset int;
-  assert Map_Contains(l->val, i);
-  call t := Lmap_Free(l);
-  call Lset_Put(pool, t);
+  assert Map_Contains(l, i);
+  pool := Set_Union(pool, l->dom);
 }
 
-yield procedure {:layer 1} Free({:layer 1} {:linear_in} l:Lmap int int, i:int)
+yield procedure {:layer 1} Free({:layer 1} {:linear_in "mem"} l:Map int int, i:int)
 refines atomic_Free;
-requires {:layer 1} Map_Contains(l->val, i);
+requires {:layer 1} Map_Contains(l, i);
 preserves call Yield();
 {
   call {:layer 1} pool := FreeLinear(l, i, pool);
   call ReturnAddr(i);
 }
 
-both action {:layer 2} atomic_Read (l:Lmap int int, i:int) returns (o:int)
+both action {:layer 2} atomic_Read ({:linear "mem"} l:Map int int, i:int) returns (o:int)
 {
-  assert Map_Contains(l->val, i);
-  o := l->val->val[i];
+  assert Map_Contains(l, i);
+  o := l->val[i];
 }
 
-both action {:layer 2} atomic_Write ({:linear_in} l:Lmap int int, i:int, o:int) returns (l':Lmap int int)
+both action {:layer 2} atomic_Write ({:linear_in "mem"} l:Map int int, i:int, o:int)
+  returns ({:linear "mem"} l':Map int int)
 {
-  assert Map_Contains(l->val, i);
+  assert Map_Contains(l, i);
   l' := l;
-  l'->val->val[i] := o;
+  l'->val[i] := o;
 }
 
 yield procedure {:layer 1}
-Read ({:layer 1} l:Lmap int int, i:int) returns (o:int)
+Read ({:layer 1} {:linear "mem"} l:Map int int, i:int) returns (o:int)
 refines atomic_Read;
 requires call YieldMem(l, i);
 ensures call Yield();
@@ -101,50 +104,49 @@ ensures call Yield();
 }
 
 yield procedure {:layer 1}
-Write ({:layer 1} {:linear_in} l:Lmap int int, i:int, o:int) returns ({:layer 1} l':Lmap int int)
+Write ({:layer 1} {:linear_in "mem"} l:Map int int, i:int, o:int)
+  returns ({:layer 1} {:linear "mem"} l':Map int int)
 refines atomic_Write;
 requires call Yield();
-requires {:layer 1} Map_Contains(l->val, i);
+requires {:layer 1} Map_Contains(l, i);
 ensures call YieldMem(l', i);
 {
   call WriteLow(i, o);
   call {:layer 1} l' := WriteLinear(l, i, o);
 }
 
-pure action AllocLinear (i:int, {:linear_in} pool:Lset int) returns (l:Lmap int int, pool':Lset int)
+pure action AllocLinear (i:int, {:linear_in "mem"} pool:Set int)
+  returns ({:linear "mem"} l:Map int int, {:linear "mem"} pool':Set int)
 {
   var m:[int]int;
-  var t:Lset int;
-  assert Lset_Contains(pool, i);
-  pool' := pool;
-  call t := Lset_Get(pool', MapOne(i));
-  call l := Lmap_Create(t, m);
+  assert Set_Contains(pool, i);
+  pool' := Set_Remove(pool, i);
+  l := Map(Set_Singleton(i), m);
 }
 
-pure action FreeLinear ({:linear_in} l:Lmap int int, i:int, {:linear_in} pool:Lset int) returns (pool':Lset int)
+pure action FreeLinear ({:linear_in "mem"} l:Map int int, i:int, {:linear_in "mem"} pool:Set int)
+  returns ({:linear "mem"} pool':Set int)
 {
-  var t: Lset int;
-  assert Map_Contains(l->val, i);
-  call t := Lmap_Free(l);
-  pool' := pool;
-  call Lset_Put(pool', t);
+  assert Map_Contains(l, i);
+  pool' := Set_Union(pool, l->dom);
 }
 
-pure action WriteLinear ({:layer 1} {:linear_in} l:Lmap int int, i:int, o:int) returns ({:layer 1} l':Lmap int int)
+pure action WriteLinear ({:layer 1} {:linear_in "mem"} l:Map int int, i:int, o:int)
+  returns ({:layer 1} {:linear "mem"} l':Map int int)
 {
-  assert Map_Contains(l->val, i);
+  assert Map_Contains(l, i);
   l' := l;
-  l'->val->val[i] := o;
+  l'->val[i] := o;
 }
 
 yield invariant {:layer 1} Yield ();
 invariant PoolInv(unallocated, pool);
 
-yield invariant {:layer 1} YieldMem ({:layer 1} l:Lmap int int, i:int);
+yield invariant {:layer 1} YieldMem ({:layer 1} {:linear "mem"} l:Map int int, i:int);
 invariant PoolInv(unallocated, pool);
-invariant Map_Contains(l->val, i) && Map_At(l->val, i) == mem[i];
+invariant Map_Contains(l, i) && Map_At(l, i) == mem[i];
 
-var {:layer 1, 2} pool:Lset int;
+var {:layer 1, 2} {:linear "mem"} pool:Set int;
 var {:layer 0, 1} mem:[int]int;
 var {:layer 0, 1} unallocated:[int]bool;
 

diff --git a/Test/civl/samples/alloc-mem.bpl.expect b/Test/civl/samples/alloc-mem.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 13 verified, 0 errors
+Boogie program verifier finished with 20 verified, 0 errors