Chalice: Alternative approach to frame known-folded locations; use quantification instead of explicit enumeration of locations.

2 files changed, 6 insertions, 2 deletions

diff --git a/Chalice/src/main/scala/Prelude.scala b/Chalice/src/main/scala/Prelude.scala
index 410a96ef..de7bc53b 100644
--- a/Chalice/src/main/scala/Prelude.scala
+++ b/Chalice/src/main/scala/Prelude.scala
@@ -194,6 +194,7 @@ function IsGoodExhalePredicateState(eh: HeapType, h: HeapType, pm: PMaskType) re
 {

   (forall<T> o: ref, f: Field T :: { eh[o, f] }  pm[o, f] ==> eh[o, f] == h[o, f])

 }

+function predicateMaskField<T>(f: Field T): Field PMaskType;

 function IsGoodExhaleState(eh: HeapType, h: HeapType,

                            m: MaskType, sm: MaskType) returns (bool)

 {

@@ -205,6 +206,8 @@ function IsGoodExhaleState(eh: HeapType, h: HeapType,
   (forall o: ref :: { h[o, forkK] } { eh[o, forkK] } h[o, forkK] == eh[o, forkK]) &&

   (forall o: ref :: { h[o, held] } { eh[o, held] } h[o, held] == eh[o, held]) &&

   (forall o: ref, f: Field int :: { eh[o, f], PredicateField(f) } PredicateField(f) ==> h[o, f] <= eh[o, f]) &&

+  (forall o: ref, f: Field int :: { h[o, predicateMaskField(f)], PredicateField(f) } { eh[o, predicateMaskField(f)], PredicateField(f) } PredicateField(f) && CanRead(m, sm, o, f) ==>

+      (forall<T> o2: ref, f2: Field T :: { h[o2, f2] } { eh[o2, f2] }  h[o, predicateMaskField(f)][o2, f2] ==> eh[o2, f2] == h[o2, f2])) &&

   (forall pmask: Field PMaskType, o: ref :: eh[o, pmask] == h[o, pmask])

 }"""

 }

diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala
index f09c37e7..f661e51c 100644
--- a/Chalice/src/main/scala/Translator.scala
+++ b/Chalice/src/main/scala/Translator.scala
@@ -414,8 +414,9 @@ class Translator {
     // const unique class.name: HeapType;

     Const(pred.FullName, true, FieldType(tint)) ::

     Const(pred.FullName+"#m", true, FieldType(tpmask)) ::

-    // axiom PredicateField(f);

     Axiom(PredicateField(pred.FullName)) ::

+    // axiom PredicateField(f);

+    Axiom(FunctionApp("predicateMaskField", List(VarExpr(pred.FullName))) ==@ VarExpr(pred.FullName + "#m")) ::

     // trigger function to unfold function definitions

     Boogie.Function("#" + pred.FullName + "#trigger", BVar("this", tref) :: Nil, BVar("$myresult", tbool)) ::

     // check definedness of predicate body

@@ -2515,7 +2516,7 @@ def buildTriggersCovering(vars : Set[Variable], functs : List[(Boogie.FunctionAp
     (if (!isUpdatingSecMask && !duringUnfold && !transferPermissionToSecMask)

       (m := em) ::

       bassume(IsGoodExhaleState(eh, Heap, m, sm)) ::

-      restoreFoldedLocations(m, Heap, eh) :::

+      //restoreFoldedLocations(m, Heap, eh) :::

       (Heap := eh) :: Nil

     else Nil) :::

     (if (isUpdatingSecMask) Nil else bassume(AreGoodMasks(m, sm)) :: Nil) :::