Chalice: Four new interesting Chalice examples (added to test suite with the correct reference output). The example FictionallyDisjointCells.chalice is due to Yannis Kassios. Small fix to test script.

8 files changed, 218 insertions, 0 deletions

diff --git a/Chalice/tests/examples/BackgroundComputation.chalice b/Chalice/tests/examples/BackgroundComputation.chalice
new file mode 100644
index 00000000..e8168183
--- /dev/null
+++ b/Chalice/tests/examples/BackgroundComputation.chalice
@@ -0,0 +1,38 @@
+class C {

+  var x: int;

+  

+  method main()

+    requires acc(x);

+    ensures acc(x);

+  {

+    // start long-running processing

+    fork tk := processing();

+    

+    /* do some computation itself */

+    

+    // finish

+    call finish(tk);

+  }

+  

+  method finish(tk: token<C.processing>)

+    requires acc(x,100-rd(tk));

+    requires acc(tk.joinable) && tk.joinable && tk != null;

+    requires eval(tk.fork this.processing(), true);

+    ensures acc(x);

+  {

+    var res: int;

+    join res := tk;

+    

+    // final write to x (requires full permission)

+    this.x := res - 1;

+  }

+  

+  method processing() returns (res: int)

+    requires rd(x);

+    ensures rd(x);

+  {

+    res := 1;

+    /* do some computation */

+  }

+  

+}

diff --git a/Chalice/tests/examples/BackgroundComputation.output.txt b/Chalice/tests/examples/BackgroundComputation.output.txt
new file mode 100644
index 00000000..c139677a
--- /dev/null
+++ b/Chalice/tests/examples/BackgroundComputation.output.txt
@@ -0,0 +1,4 @@
+Verification of BackgroundComputation.chalice using parameters="" 

+

+

+Boogie program verifier finished with 7 verified, 0 errors

diff --git a/Chalice/tests/examples/FictionallyDisjointCells.chalice b/Chalice/tests/examples/FictionallyDisjointCells.chalice
new file mode 100644
index 00000000..d26dedbb
--- /dev/null
+++ b/Chalice/tests/examples/FictionallyDisjointCells.chalice
@@ -0,0 +1,75 @@
+class Cell

+{

+    var inner: InnerCell;

+    

+    predicate inv

+    {

+        acc(inner) && inner!=null && rd(inner.value,1) && rd*(inner.mu) && rd*(this.mu)

+    }

+    

+    method CellConstructor()

+        requires acc(inner) && acc(this.mu)

+        ensures inv && get()==0;

+    {

+        inner := new InnerCell;

+        call inner.InnerCellConstructor(0)

+        share inner;

+        fold inv;

+    }

+    

+    method CellConstructor2(other: Cell)

+        requires acc(inner) && acc(this.mu)

+        requires other != null && other.inv;

+        requires unfolding other.inv in waitlevel << other.inner.mu

+        ensures inv && other.inv && get()==other.get();

+    {

+        unfold other.inv;

+        inner := other.inner;

+        acquire inner;

+        inner.refCount := inner.refCount+1;

+        release inner;

+        fold other.inv;

+        fold inv;

+    }

+    

+    function get():int

+        requires inv;

+    { unfolding inv in inner.value }

+    

+    method set(x:int)

+        requires inv;

+        requires unfolding inv in waitlevel << inner.mu

+        ensures inv && get()==x;

+    {

+        var old_in: InnerCell;

+        unfold inv;

+        old_in := inner;

+        acquire old_in;

+        if (inner.refCount==1) { inner.value:=x; }

+        else

+        {

+            inner.refCount := inner.refCount-1;

+            inner := new InnerCell;

+            call inner.InnerCellConstructor(x)

+            share inner;

+        }

+        release old_in;

+        fold inv;

+    }

+}

+

+class InnerCell

+{

+    var value: int;

+    var refCount: int;

+    

+    invariant acc(refCount) && refCount > 0 && acc(value,100-rd(refCount));

+    

+    method InnerCellConstructor(val: int)

+        requires acc(refCount) && acc(value)

+        ensures acc(refCount) && acc(value) && refCount==1 && value == val;

+    {

+        refCount := 1;

+        value := val

+    }

+}

diff --git a/Chalice/tests/examples/FictionallyDisjointCells.output.txt b/Chalice/tests/examples/FictionallyDisjointCells.output.txt
new file mode 100644
index 00000000..1dc7a7b1
--- /dev/null
+++ b/Chalice/tests/examples/FictionallyDisjointCells.output.txt
@@ -0,0 +1,4 @@
+Verification of FictionallyDisjointCells.chalice using parameters="" 

+

+

+Boogie program verifier finished with 12 verified, 0 errors

diff --git a/Chalice/tests/examples/TreeOfWorker.chalice b/Chalice/tests/examples/TreeOfWorker.chalice
new file mode 100644
index 00000000..6483f884
--- /dev/null
+++ b/Chalice/tests/examples/TreeOfWorker.chalice
@@ -0,0 +1,29 @@
+class Node {

+  var l: Node

+  var r: Node

+  

+  method work(data: Data)

+    requires rd(data.f)

+    requires valid

+    ensures rd(data.f)

+    ensures valid

+  {

+    var tkl: token<Node.work>

+    var tkr: token<Node.work>

+    

+    unfold valid

+    if (l != null) { fork tkl := l.work(data) }

+    if (r != null) { fork tkr := r.work(data) }

+    /* .. perform work on this node (using the global data: data.f) */

+    if (l != null) { join tkl }

+    if (r != null) { join tkr }

+    fold valid

+  }

+  

+  predicate valid {

+    acc(l) && acc(r) &&

+    (l != null ==> l.valid) &&

+    (r != null ==> r.valid)

+  }

+}

+class Data { var f: int; }

diff --git a/Chalice/tests/examples/TreeOfWorker.output.txt b/Chalice/tests/examples/TreeOfWorker.output.txt
new file mode 100644
index 00000000..4dc67e3c
--- /dev/null
+++ b/Chalice/tests/examples/TreeOfWorker.output.txt
@@ -0,0 +1,4 @@
+Verification of TreeOfWorker.chalice using parameters="" 

+

+

+Boogie program verifier finished with 5 verified, 0 errors

diff --git a/Chalice/tests/examples/UnboundedThreads.chalice b/Chalice/tests/examples/UnboundedThreads.chalice
new file mode 100644
index 00000000..c52bb10a
--- /dev/null
+++ b/Chalice/tests/examples/UnboundedThreads.chalice
@@ -0,0 +1,59 @@
+class C {

+  

+  var f: int;

+  

+  method main(n: int)

+    requires n > 0 && acc(this.f)

+    ensures acc(this.f)

+  {

+    // fork all threads, and join them afterwards

+    call work(n);

+    

+    this.f := 100; // we want a full permission in the end

+  }

+

+  method work(n: int)

+    requires rd(this.f,n)

+    ensures rd(this.f,n)

+  {

+    var tks:seq<token<C.m>> := nil<token<C.m>>;

+    

+    // first loop; fork all threads

+    var i := 0;

+    while (i < n)

+      invariant i <= n && |tks| == i;

+      invariant i < n ==> rd(this.f,n-i);

+      invariant acc(tks[*].joinable);

+      invariant forall k in [0..|tks|] :: tks[k] != null && tks[k].joinable;

+      invariant forall k in [0..|tks|] :: eval(tks[k].fork this.m(), true);

+      invariant forall k,j in [0..|tks|] :: k < j ==> tks[k] != tks[j];

+    {

+      fork tk := m();

+      tks := tks ++ [tk];

+      i := i+1;

+    }

+    

+    // second loop; join all threads

+    i := n;

+    while (i > 0)

+      invariant i >= 0 && |tks| == i;

+      invariant i < n ==> rd(this.f,n-i); // BUG: the eval construct inside the quantification does not give us the information needed to proof this invariant, see http://boogie.codeplex.com/workitem/10187

+      invariant acc(tks[*].joinable);

+      invariant forall k in [0..|tks|] :: tks[k] != null && tks[k].joinable;

+      invariant forall k in [0..|tks|] :: eval(tks[k].fork this.m(), true);

+      invariant forall k,j in [0..|tks|] :: k < j ==> tks[k] != tks[j];

+    {

+      var tk: token<C.m>;

+      tk := tks[i-1];

+      join tk;

+      i := i-1;

+      tks := tks[0..i];

+    }

+  }

+  

+  method m()

+    requires rd(this.f,1);

+    ensures rd(this.f,1);

+  { /* do some computation */ }

+

+}

diff --git a/Chalice/tests/examples/UnboundedThreads.output.txt b/Chalice/tests/examples/UnboundedThreads.output.txt
new file mode 100644
index 00000000..efd70a6d
--- /dev/null
+++ b/Chalice/tests/examples/UnboundedThreads.output.txt
@@ -0,0 +1,5 @@
+Verification of UnboundedThreads.chalice using parameters="" 

+

+  40.17: The loop invariant at 40.17 might not be preserved by the loop. Insufficient epsilons at 40.27  for C.f.

+

+Boogie program verifier finished with 6 verified, 1 error