Chalice: copy concrete values for every permission in coupling invariants of "this"

2 files changed, 39 insertions, 8 deletions

diff --git a/Chalice/refinements/Counter.chalice b/Chalice/refinements/Counter.chalice
index e0c0c7df..16cd8473 100644
--- a/Chalice/refinements/Counter.chalice
+++ b/Chalice/refinements/Counter.chalice
@@ -21,6 +21,13 @@ class Counter0 {
   {    
     x := x - 1;  
   }
+
+  method magic() returns (c: Cell)
+    requires acc(x);
+    ensures acc(x) && acc(c.n)
+  {
+    var c [acc(c.n)]
+  }
 }
 
 class Counter1 refines Counter0 {
@@ -53,15 +60,17 @@ the spec of Counter1 uses the abstract field x which disappears at the concrete
 I'm not sure what a good solution to this problem...
 */
 
-class Counter2 refines Counter1 {
+class Counter2 refines Counter0 {
   var a: Cell;
   var b: Cell;
-  replaces y, z by acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n;
+  replaces x by acc(a) && acc(b) && acc(a.n) && acc(b.n) && x == a.n - b.n;
   
   refines init() 
   {    
-    this.a := new Cell {n := 0};
-    this.b := new Cell {n := 0};    
+    this.a := new Cell;
+    this.b := new Cell;
+    this.a.n := 0;
+    this.b.n := 0;
   }
 
   refines inc() 
@@ -74,4 +83,16 @@ class Counter2 refines Counter1 {
     this.b.n := this.b.n + 1;
   }
 }
+
+class Client {
+  method main() 
+  {
+    var c := new Counter0;
+    call c.init();
+    call c.inc();
+    call c.inc();
+    call c.dec();
+    assert c.x == 1;
+  }
+}
   
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 5b9e442f..0c23db04 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -1111,14 +1111,24 @@ class Translator {
     }} :::

     {

       val (v,ve) = NewBVar("this", tref, true)

-      // TODO: we only preserve concrete fields of "this" at the moment       

       // TODO: check for mask coupling

+      // TODO: we only inhale concrete values for "This"

+

+      def copy(e: Expression):List[Stmt] = e match {

+        case And(a,b) => copy(a) ::: copy(b)

+        case Implies(a,b) => Boogie.If(absTran.Tr(a), copy(b), Nil)

+        case Access(ma, _) if ! ma.isPredicate => absTran.Heap.store(absTran.Tr(ma.e), new VarExpr(ma.f.FullName), conTran.Heap.select(absTran.Tr(ma.e), ma.f.FullName))

+        case _: PermissionExpr => throw new Exception("not implemented")

+        case _ => Nil

+      }

 

+      // copy variables in the coupling invariants to the abstract heap (to preserve their values across refinement blocks and establish invariant)

+      (for (ci <- currentClass.CouplingInvariants)

+        yield Boogie.If((ci.fields.map(f => absTran.CanRead(new VarExpr("this"), f.FullName)).reduceLeft(_ || _)),

+          copy(ci.e), Nil)) :::

       // assert equality on shared globals (except those that are replaced)

       (for (f <- currentClass.refines.Fields; if ! currentClass.CouplingInvariants.exists(_.fields.contains(f)))

-        yield bassert((absTran.Heap.select(ve, f.FullName) ==@ conTran.Heap.select(ve, f.FullName)).forall(v), r.pos, "Refinement may change value of field " + f.FullName)) :::         

-      // copy new globals from concrete to abstract heap (to preserve their values across refinement blocks and establish invariant)

-      (for (f <- currentClass.DeclaredFields) yield absTran.Heap.store(VarExpr("this"), VarExpr(f.FullName), conTran.Heap.select(VarExpr("this"), f.FullName)))

+        yield bassert((absTran.Heap.select(ve, f.FullName) ==@ conTran.Heap.select(ve, f.FullName)).forall(v), r.pos, "Refinement may change value of field " + f.FullName)) 

     } :::

     Comment("end of refinement block")

   }