1 files changed, 232 insertions, 0 deletions
diff --git a/Chalice/tests/permission-model/basic.chalice b/Chalice/tests/permission-model/basic.chalice
new file mode 100644
index 00000000..53443a49
--- /dev/null
+++ b/Chalice/tests/permission-model/basic.chalice
@@ -0,0 +1,232 @@
+class Cell {
+  var x: int;
+  
+  // dispose a read permission to x
+  method dispose_rd()
+    requires rd(x);
+    ensures true;
+  {
+  }
+  
+  // return read permission
+  method void()
+    requires rd(x);
+    ensures rd(x);
+  {
+  }
+  
+  // multiple calls to method that destroys rd(x)
+  method a1()
+    requires rd(x);
+    ensures true;
+  {
+    call dispose_rd();
+    call dispose_rd();
+  }
+  
+  // call to method that destroys rd(x) really removes permission
+  method a2()
+    requires rd(x);
+    ensures rd(x);
+  {
+    call dispose_rd();
+    // ERROR: should fail to verify postcondition
+  }
+  
+  // forking and method calls of dispose_rd
+  method a3()
+    requires rd(x);
+    ensures true;
+  {
+    fork dispose_rd();
+    call dispose_rd();
+    fork dispose_rd();
+    call dispose_rd();
+  }
+  
+  // forking and method calls of dispose_rd
+  method a4()
+    requires rd(x);
+    ensures rd(x);
+  {
+    fork dispose_rd();
+    // ERROR: should fail to verify postcondition
+  }
+  
+  // forking and method calls of dispose_rd
+  method a5()
+    requires rd(x);
+    ensures rd(x,1);
+  {
+    fork dispose_rd();
+    // OK: giving away an epsilon permission however should work
+  }
+  
+  // forking and method calls of dispose_rd
+  method a6()
+    requires rd(x);
+    ensures rd*(x);
+  {
+    fork dispose_rd();
+    // OK: giving away a 'undefined' read permission however should work
+  }
+  
+  // multiple forks of dispose_rd
+  method a7()
+    requires rd(x);
+    ensures true;
+  {
+    fork dispose_rd();
+    fork dispose_rd();
+    fork dispose_rd();
+    fork dispose_rd();
+    fork dispose_rd();
+    fork dispose_rd();
+  }
+  
+  // joining to regain permission
+  method a8(a: int)
+    requires rd(x);
+    ensures rd(x)
+  {
+    fork tk := void();
+    join tk;
+  }
+  
+  // joining to regain permission
+  method a9(a: int)
+    requires rd(x);
+    ensures rd(x)
+  {
+    fork tk := dispose_rd();
+    join tk;
+    // ERROR: should fail to verify postcondition
+  }
+  
+  // joining to regain permission
+  method a10(a: int)
+    requires rd(x);
+    ensures a == 3 ==> rd(x)
+  {
+    fork tk := void();
+    if (3 == a) {
+      join tk;
+    }
+  }
+  
+  // finite loop of method calls, preserving rd(x)
+  method a11()
+    requires rd(x);
+    ensures rd(x);
+  {
+    var i: int;
+    i := 0;
+    while (i < 1000)
+      invariant rd(x);
+    {
+      call void();
+      i := i+1;
+    }
+  }
+  
+  // forking dispose_rd in a loop (using rd(x,*) to denote unknown read permission)
+  method a12(a: int)
+    requires rd(x);
+    ensures rd*(x);
+  {
+    var i: int;
+    i := 0;
+    while (i < a)
+      invariant rd*(x);
+    {
+      fork dispose_rd();
+      i := i+1;
+    }
+  }
+  
+  // forking dispose_rd in a loop (using rd(x,*) to denote unknown read permission)
+  method a13(a: int)
+    requires rd(x);
+    ensures rd(x);
+  {
+    var i: int;
+    i := 0;
+    while (i < a)
+      invariant rd*(x);
+    {
+      fork dispose_rd();
+      i := i+1;
+    }
+    // ERROR: should fail to verify postcondition
+  }
+  
+  // calling dispose_rd in a loop (using rd(x,*) to denote unknown read permission)
+  method a14()
+    requires rd(x);
+    ensures true;
+  {
+    call dispose_rd();
+    
+    var i: int;
+    i := 0;
+    while (i < 1000)
+      invariant rd*(x);
+    {
+      call dispose_rd();
+      i := i+1;
+    }
+  }
+  
+  // return unknown permission
+  method a15()
+    requires rd(x);
+    ensures rd*(x);
+  {
+    call dispose_rd();
+  }
+  
+  // rd in loop invariant
+  method a16()
+    requires rd(x);
+    ensures rd*(x);
+  {
+    call dispose_rd();
+    
+    var i: int;
+    i := 0;
+    while (i < 1000)
+      invariant acc(x,rd);
+    {
+      call void();
+      i := i+1;
+    }
+  }
+  
+  // rd in method contracts
+  method a17()
+    requires acc(x,rd);
+  {
+    call dispose_rd();
+    call a17();
+  }
+  
+  // multiple rd in method contracts
+  method a18()
+    requires rd(x);
+    ensures rd(x)
+  {
+    call a18a()
+    call a18b()
+  }
+  method a18a()
+    requires acc(x,2*rd);
+    ensures acc(x,rd+rd);
+  {
+  }
+  method a18b()
+    requires acc(x,rd+rd);
+    ensures acc(x,rd*2);
+  {
+  }
+  
+}