renamed og to civl

1 files changed, 0 insertions, 324 deletions

diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
deleted file mode 100644
index 7fb0a081..00000000
--- a/Test/og/multiset.bpl
+++ /dev/null
@@ -1,324 +0,0 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-type X;

-

-const unique null : int;

-const unique nil: X;

-const unique done: X;

-

-var {:layer 0} elt : [int]int;

-var {:layer 0} valid : [int]bool;

-var {:layer 0} lock : [int]X;

-var {:layer 0} owner : [int]X;

-const max : int;

-

-function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

-function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

-{

-  MapConstBool(false)[x := true]

-}

-

-axiom (max > 0);

-

-procedure {:yields} {:layer 0} acquire(i : int, {:linear "tid"} tid: X);

-ensures {:right} |{ A: 

-                      assert 0 <= i && i < max;

-                      assert tid != nil && tid != done;

-                      assume lock[i] == nil;

-	              lock[i] := tid;

-                      return true;

-                    }|;

-

-

-procedure {:yields} {:layer 0} release(i : int, {:linear "tid"} tid: X);

-ensures {:left} |{ A: 

-                     assert 0 <= i && i < max;

-                     assert lock[i] == tid;

-                     assert tid != nil && tid != done; 

-	             lock[i] := nil;

-                     return true;

-                    }|;

-

-

-procedure {:yields} {:layer 0,1} getElt(j : int, {:linear "tid"} tid: X) returns (elt_j:int);

-ensures {:both} |{ A: 

-                     assert 0 <= j && j < max;

-                     assert lock[j] == tid;

-                     assert tid != nil && tid != done;

-	             elt_j := elt[j];

-                     return true;

-                    }|;

-

-

-procedure {:yields} {:layer 0,1} setElt(j : int, x : int, {:linear "tid"} tid: X);

-ensures {:both} |{ A: 

-                     assert x != null;

-                     assert owner[j] == nil;

-                     assert 0 <= j && j < max;

-                     assert lock[j] == tid;

-                     assert tid != nil && tid != done;

-	             elt[j] := x;

-                     owner[j] := tid;

-                     return true;

-                    }|;

-

-

-procedure {:yields} {:layer 0,2} setEltToNull(j : int, {:linear "tid"} tid: X);

-ensures {:left} |{ A: 

-                     assert owner[j] == tid;

-                     assert 0 <= j && j < max;

-                     assert lock[j] == tid;

-                     assert !valid[j];

-                     assert tid != nil  && tid != done;

-	             elt[j] := null;

-                     owner[j] := nil;

-                     return true;

-                    }|;

-

-procedure {:yields} {:layer 0,2} setValid(j : int, {:linear "tid"} tid: X);

-ensures {:both} |{ A: 

-                     assert 0 <= j && j < max;

-                     assert lock[j] == tid;

-                     assert tid != nil && tid != done;

-                     assert owner[j] == tid;

-	             valid[j] := true;

-                     owner[j] := done;

-                     return true;

-                    }|;

-

-procedure {:yields} {:layer 0,2} isEltThereAndValid(j : int, x : int, {:linear "tid"} tid: X) returns (fnd:bool);

-ensures {:both} |{ A: 

-                       assert 0 <= j && j < max;

-                       assert lock[j] == tid;

-                       assert tid != nil && tid != done;

-                       fnd := (elt[j] == x) && valid[j];

-                       return true;

-                    }|;

-

-procedure {:yields} {:layer 1,2} FindSlot(x : int, {:linear "tid"} tid: X) returns (r : int)

-requires {:layer 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; 

-ensures {:layer 1} Inv(valid, elt, owner);

-ensures {:right}  |{   A: assert tid != nil && tid != done; 

-                          assert x != null; 

-			  goto B, C;

-                       B: assume (0 <= r && r < max); 

-                                            assume elt[r] == null; 

-                                            assume owner[r] == nil;

-					    assume !valid[r];

-                                            elt[r] := x; 

-                                            owner[r] := tid;

-                                            return true;

-                       C: assume (r == -1); return true; 

-                   }|;

-{

-	var j : int;

-	var elt_j : int;

-        

-        par Yield1();

-

-	j := 0;

-	while(j < max)

-        invariant {:layer 1} Inv(valid, elt, owner);

-	invariant {:layer 1} 0 <= j;

-	{

-                call acquire(j, tid);

-                call elt_j := getElt(j, tid);

-		if(elt_j == null)

-		{

-                        call setElt(j, x, tid);

-			call release(j, tid);

-			r := j;

-

-                        par Yield1();

-			return;		

-		}

-		call release(j,tid);

-

-                par Yield1();

-

-		j := j + 1;	

-	}

-	r := -1;

-

-        par Yield1();

-	return;

-}

-

-procedure {:yields} {:layer 2} Insert(x : int, {:linear "tid"} tid: X) returns (result : bool) 

-requires {:layer 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; 

-ensures {:layer 1} Inv(valid, elt, owner);

-requires {:layer 2} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; 

-ensures {:layer 2} Inv(valid, elt, owner);

-ensures {:atomic}  |{ var r:int;

-                        A: goto B, C;

-                        B: assume (0 <= r && r < max); 

-                           assume valid[r] == false; 

-                           assume elt[r] == null; 

-                           assume owner[r] == nil; 

-                           elt[r] := x; valid[r] := true; owner[r] := done;

-                           result := true; return true;

-                        C: result := false; return true; 

-                      }|;

- {

-        var i: int;

-        par Yield12();

-        call i := FindSlot(x, tid);

-        

-	if(i == -1)

-	{

-		result := false;

-                par Yield12();

-		return;

-	}

-        par Yield1();

-        assert {:layer 1} i != -1;

-        assert {:layer 2} i != -1;

-	call acquire(i, tid);

-        assert {:layer 2} elt[i] == x;

-	assert {:layer 2}  valid[i] == false;

-        call setValid(i, tid);   

-	call release(i, tid);

-	result := true; 

-        par Yield12();

-	return;

-}

-

-procedure {:yields} {:layer 2} InsertPair(x : int, y : int, {:linear "tid"} tid: X) returns (result : bool)

-requires {:layer 1} Inv(valid, elt, owner) && x != null && y != null && tid != nil && tid != done; 

-ensures {:layer 1} Inv(valid, elt, owner);

-requires {:layer 2} Inv(valid, elt, owner) && x != null && y != null && tid != nil && tid != done; 

-ensures {:layer 2} Inv(valid, elt, owner);

-ensures {:atomic}  |{ var rx:int;

-                        var ry:int;

-                        A: goto B, C;

-                        B: assume (0 <= rx && rx < max && 0 <= ry && ry < max && rx != ry); 

-                           assume valid[rx] == false; 

-                           assume valid[ry] == false; 

-                           assume elt[rx] == null; 

-                           assume elt[rx] == null; 

-                           elt[rx] := x; 

-                           elt[ry] := y; 

-                           valid[rx] := true; 

-                           valid[ry] := true;

-                           owner[rx] := done;

-                           owner[ry] := done; 

-                           result := true; return true;

-                        C: result := false; return true; 

-                      }|;

- {

-        var i : int; 

-        var j : int;

-        par Yield12();

-

-        call i := FindSlot(x, tid);

-        

-	if (i == -1)

-	{

-	 	result := false;

-                par Yield12();

-		return;

-	}

-

-        par Yield1();

-        call j := FindSlot(y, tid);

-        

-	if(j == -1)

-	{

-                par Yield1();

-                call acquire(i,tid);  

-                call setEltToNull(i, tid);

-                call release(i,tid);  

-		result := false;

-                par Yield12();

-		return;

-	}

-

-        par Yield1();

-        assert {:layer 2} i != -1 && j != -1;

-	call acquire(i, tid);

-	call acquire(j, tid);

-        assert {:layer 2} elt[i] == x;

-        assert {:layer 2} elt[j] == y;

-	assert {:layer 2}  valid[i] == false;

-	assert {:layer 2}  valid[j] == false;

-        call setValid(i, tid);   

-        call setValid(j, tid);   

-	call release(j, tid);

-	call release(i, tid);

-	result := true; 

-        par Yield12();

-	return;

-}

-

-procedure {:yields} {:layer 2} LookUp(x : int, {:linear "tid"} tid: X, old_valid:[int]bool, old_elt:[int]int) returns (found : bool)

-requires {:layer 1} {:layer 2} old_valid == valid && old_elt == elt;

-requires {:layer 1} {:layer 2} Inv(valid, elt, owner);

-requires {:layer 1} {:layer 2} (tid != nil && tid != done);

-ensures {:layer 1} {:layer 2} Inv(valid, elt, owner);

-ensures {:atomic}  |{ A: assert tid != nil && tid != done; 

-                          assert x != null;

-                          assume found ==> (exists ii:int :: 0 <= ii && ii < max && valid[ii] && elt[ii] == x);

-			  assume !found ==> (forall ii:int :: 0 <= ii && ii < max ==> !(old_valid[ii] && old_elt[ii] == x));

-                          return true;

-                    }|;

-{

-	var j : int;

-	var isThere : bool;

-        

-        par Yield12() | YieldLookUp(old_valid, old_elt);

-

-	j := 0;

-

-	while(j < max)

-        invariant {:layer 1} {:layer 2} Inv(valid, elt, owner);

-        invariant {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < j ==> !(old_valid[ii] && old_elt[ii] == x));

-	invariant {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);

-	invariant {:layer 1} {:layer 2} 0 <= j;

-	{

-                call acquire(j, tid);

-                call isThere := isEltThereAndValid(j, x, tid);

-		if(isThere)

-		{

-			 call release(j, tid);

-                         found := true; 

-                         par Yield12() | YieldLookUp(old_valid, old_elt);

-		 	 return;		

-		}

-		call release(j,tid);

-                par Yield12() | YieldLookUp(old_valid, old_elt);

-		j := j + 1;	

-	}

-	found := false;

-

-        par Yield12() | YieldLookUp(old_valid, old_elt);

-	return;

-}

-

-procedure {:yields} {:layer 1} Yield1()

-requires {:layer 1} Inv(valid, elt, owner);

-ensures {:layer 1} Inv(valid, elt, owner);

-{

-	yield;

-	assert {:layer 1} Inv(valid, elt, owner);

-}

-

-procedure {:yields} {:layer 2} Yield12()

-requires {:layer 1} {:layer 2} Inv(valid, elt, owner);

-ensures {:layer 1} {:layer 2} Inv(valid, elt, owner);

-{

-        yield;

-        assert {:layer 1} {:layer 2} Inv(valid, elt, owner);

-}

-

-function {:inline} Inv(valid: [int]bool, elt: [int]int, owner: [int]X): (bool)

-{

-   (forall i:int :: 0 <= i && i < max ==> (elt[i] == null <==> (!valid[i] && owner[i] == nil)))

-}

-

-procedure {:yields} {:layer 2} YieldLookUp(old_valid: [int]bool, old_elt: [int]int)

-requires {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);

-ensures {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);

-{

-    yield;

-    assert {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);

-}