Chalice: On unfolds, assume that for all locations from within the predicate the per-predicate mask is true.

1 files changed, 20 insertions, 13 deletions

diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala
index 11068156..bd94c71e 100644
--- a/Chalice/src/main/scala/Translator.scala
+++ b/Chalice/src/main/scala/Translator.scala
@@ -723,7 +723,7 @@ class Translator {
         isDefined(e) :::

         bassert(nonNull(o), s.pos, "The target of the fold statement might be null.") ::

         isDefined(perm) :::

-        ExhaleDuringUnfold(List((acc, ErrorMessage(s.pos, "unfold might fail because the predicate " + pred.predicate.FullName + " does not hold."))), "unfold", unfoldK, false) :::

+        ExhaleDuringUnfold(List((acc, ErrorMessage(s.pos, "unfold might fail because the predicate " + pred.predicate.FullName + " does not hold."))), "unfold", unfoldK, false, o, pred.predicate) :::

         etran.Inhale(List(definition), "unfold", false, unfoldK)

       case c@CallAsync(declaresLocal, token, obj, id, args) =>

         val formalThisV = new Variable("this", new Type(c.m.Parent))

@@ -1440,7 +1440,7 @@ class Translator {
 

   def Inhale(predicates: List[Expression], occasion: String, currentK: Expr): List[Boogie.Stmt] = etran.Inhale(predicates, occasion, false, currentK)

   def Exhale(predicates: List[(Expression, ErrorMessage)], occasion: String, currentK: Expr, exactchecking: Boolean): List[Boogie.Stmt] = etran.Exhale(predicates, occasion, false, currentK, exactchecking)

-  def ExhaleDuringUnfold(predicates: List[(Expression, ErrorMessage)], occasion: String, currentK: Expr, exactchecking: Boolean): List[Boogie.Stmt] = etran.ExhaleDuringUnfold(predicates, occasion, false, currentK, exactchecking)

+  def ExhaleDuringUnfold(predicates: List[(Expression, ErrorMessage)], occasion: String, currentK: Expr, exactchecking: Boolean, unfoldReceiver: Expr, unfoldPredicate: Predicate): List[Boogie.Stmt] = etran.ExhaleDuringUnfold(predicates, occasion, false, currentK, exactchecking, unfoldReceiver, unfoldPredicate)

   def InhaleWithChecking(predicates: List[Expression], occasion: String, currentK: Expr): List[Boogie.Stmt] = etran.Inhale(predicates, occasion, true, currentK)

   def ExhaleWithChecking(predicates: List[(Expression, ErrorMessage)], occasion: String, currentK: Expr, exactchecking: Boolean): List[Boogie.Stmt] = etran.Exhale(predicates, occasion, true, currentK, exactchecking)

 

@@ -1655,7 +1655,7 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
         BLocals(tmpGlobalsV) :::

         copyState(tmpGlobals, this) :::

         // exhale the predicate

-        tmpTranslator.ExhaleDuringUnfold(List((acc, ErrorMessage(unfolding.pos, "Unfolding might fail."))), "unfolding", false, unfoldingK, false) :::

+        tmpTranslator.ExhaleDuringUnfold(List((acc, ErrorMessage(unfolding.pos, "Unfolding might fail."))), "unfolding", false, unfoldingK, false, o, pred.predicate) :::

         // inhale the definition of the predicate

         tmpTranslator.Inhale(List(definition), "unfolding", false, unfoldingK) :::

         // update the predicate mask to indicate the predicates that are folded under 'pred'

@@ -2135,15 +2135,15 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
   def Exhale(predicates: List[(Expression, ErrorMessage)], occasion: String, check: Boolean, currentK: Expr, exactchecking: Boolean): List[Boogie.Stmt] = 

     Exhale(Mask, SecMask, predicates, occasion, check, currentK, exactchecking)

   /** Exhale as part of a unfold statement (just like a regular exhale, but no heap havocing) */

-  def ExhaleDuringUnfold(predicates: List[(Expression, ErrorMessage)], occasion: String, check: Boolean, currentK: Expr, exactchecking: Boolean): List[Boogie.Stmt] = 

-    Exhale(Mask, SecMask, predicates, occasion, check, currentK, exactchecking, false, -1, false, null, true)

+  def ExhaleDuringUnfold(predicates: List[(Expression, ErrorMessage)], occasion: String, check: Boolean, currentK: Expr, exactchecking: Boolean, unfoldReceiver: Expr, unfoldPredicate: Predicate): List[Boogie.Stmt] = 

+    ExhaleForUnfold(Mask, SecMask, predicates, occasion, check, currentK, exactchecking, false, -1, false, null, true, unfoldReceiver, unfoldPredicate)

   /** Regular exhale with specific mask/secmask */

   def Exhale(m: Expr, sm: Expr, predicates: List[(Expression, ErrorMessage)], occasion: String, check: Boolean, currentK: Expr, exactchecking: Boolean): List[Boogie.Stmt] = {

     Exhale(m, sm, predicates, occasion, check, currentK, exactchecking, false, -1, false, null, false)

   }

   /** Exhale that transfers permission to the secondary mask */

   def ExhaleAndTransferToSecMask(receiver: Expr, pred: Predicate, predicates: List[(Expression, ErrorMessage)], occasion: String, currentK: Expr, exactchecking: Boolean): List[Boogie.Stmt] = {

-    Exhale(receiver, pred, Mask, SecMask, predicates, occasion, false, currentK, exactchecking, true /* transfer to SecMask */, -1, false, null, false)

+    Exhale(receiver, pred, Mask, SecMask, predicates, occasion, false, currentK, exactchecking, true /* transfer to SecMask */, -1, false, null, false, null /* unfoldReceiver */, null /* unfoldPred */)

   }

   /** Remove permission from the secondary mask, and assume all assertions that

    * would get generated. Recursion is bouded by the parameter depth.

@@ -2207,9 +2207,12 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
   // previousReceivers is not needed, and thus null.

   // Assumption 4+5: duringUnfold can only be true if transferPermissionToSecMask

   // and isUpdatingSecMask are not.

+  // Assumption 6: duringUnfold <==> (unfoldReceiver != null && unfoldPredicate != null)

   def Exhale(m: Expr, sm: Expr, predicates: List[(Expression, ErrorMessage)], occasion: String, check: Boolean, currentK: Expr, exactchecking: Boolean, transferPermissionToSecMask: Boolean, recurseOnPredicatesDepth: Int, isUpdatingSecMask: Boolean, previousReceivers: Map[String,List[Expr]], duringUnfold: Boolean): List[Boogie.Stmt] =

-    Exhale(null, null, m, sm, predicates, occasion, check, currentK, exactchecking, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers, duringUnfold)

-  def Exhale(receiver: Expr, pred: Predicate, m: Expr, sm: Expr, predicates: List[(Expression, ErrorMessage)], occasion: String, check: Boolean, currentK: Expr, exactchecking: Boolean, transferPermissionToSecMask: Boolean, recurseOnPredicatesDepth: Int, isUpdatingSecMask: Boolean, previousReceivers: Map[String,List[Expr]], duringUnfold: Boolean): List[Boogie.Stmt] = {

+    Exhale(null, null, m, sm, predicates, occasion, check, currentK, exactchecking, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers, duringUnfold, null /* unfoldReceiver */, null /* unfoldPred */)

+  def ExhaleForUnfold(m: Expr, sm: Expr, predicates: List[(Expression, ErrorMessage)], occasion: String, check: Boolean, currentK: Expr, exactchecking: Boolean, transferPermissionToSecMask: Boolean, recurseOnPredicatesDepth: Int, isUpdatingSecMask: Boolean, previousReceivers: Map[String,List[Expr]], duringUnfold: Boolean, unfoldReceiver: Expr, unfoldPredicate: Predicate): List[Boogie.Stmt] =

+    Exhale(null, null, m, sm, predicates, occasion, check, currentK, exactchecking, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers, duringUnfold, unfoldReceiver, unfoldPredicate)

+  def Exhale(receiver: Expr, pred: Predicate, m: Expr, sm: Expr, predicates: List[(Expression, ErrorMessage)], occasion: String, check: Boolean, currentK: Expr, exactchecking: Boolean, transferPermissionToSecMask: Boolean, recurseOnPredicatesDepth: Int, isUpdatingSecMask: Boolean, previousReceivers: Map[String,List[Expr]], duringUnfold: Boolean, unfoldReceiver: Expr, unfoldPredicate: Predicate): List[Boogie.Stmt] = {

     assert ((isUpdatingSecMask && recurseOnPredicatesDepth >= 0) || (!isUpdatingSecMask && recurseOnPredicatesDepth == -1)) // check assumption 2

     assert (isUpdatingSecMask || (previousReceivers == null))

     assert (!(isUpdatingSecMask && duringUnfold))

@@ -2225,8 +2228,8 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
       em = m

       Nil

     }) :::

-    (for (p <- predicates) yield ExhaleHelper(p._1, em, sm, eh, p._2, check, currentK, exactchecking, false, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers, duringUnfold)).flatten :::

-    (for (p <- predicates) yield ExhaleHelper(p._1, em, sm, eh, p._2, check, currentK, exactchecking, true, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers, duringUnfold)).flatten :::

+    (for (p <- predicates) yield ExhaleHelper(p._1, em, sm, eh, Heap, p._2, check, currentK, exactchecking, false, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers, duringUnfold, unfoldReceiver, unfoldPredicate)).flatten :::

+    (for (p <- predicates) yield ExhaleHelper(p._1, em, sm, eh, Heap, p._2, check, currentK, exactchecking, true, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers, duringUnfold, unfoldReceiver, unfoldPredicate)).flatten :::

     (if (!isUpdatingSecMask && !duringUnfold && !transferPermissionToSecMask)

       (m := em) ::

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

@@ -2347,8 +2350,8 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
     }

   }

   

-  def ExhaleHelper(p: Expression, m: Boogie.Expr, sm: Boogie.Expr, eh: Boogie.Expr, error: ErrorMessage, check: Boolean, currentK: Expr, exactchecking: Boolean, onlyExactCheckingPermissions: Boolean, transferPermissionToSecMask: Boolean, recurseOnPredicatesDepth: Int, isUpdatingSecMask: Boolean, previousReceivers: Map[String,List[Expr]], duringUnfold: Boolean): List[Boogie.Stmt] = {

-    val LocalExhaleHelper = (expr: Expression) => ExhaleHelper(expr, m, sm, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers, duringUnfold)

+  def ExhaleHelper(p: Expression, m: Boogie.Expr, sm: Boogie.Expr, eh: Boogie.Expr, h: Boogie.Expr, error: ErrorMessage, check: Boolean, currentK: Expr, exactchecking: Boolean, onlyExactCheckingPermissions: Boolean, transferPermissionToSecMask: Boolean, recurseOnPredicatesDepth: Int, isUpdatingSecMask: Boolean, previousReceivers: Map[String,List[Expr]], duringUnfold: Boolean, unfoldReceiver: Expr, unfoldPredicate: Predicate): List[Boogie.Stmt] = {

+    val LocalExhaleHelper = (expr: Expression) => ExhaleHelper(expr, m, sm, eh, h, error, check, currentK, exactchecking, onlyExactCheckingPermissions, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers, duringUnfold, unfoldReceiver, unfoldPredicate)

     desugar(p) match {

     case pred@MemberAccess(e, p) if pred.isPredicate =>

       val tmp = Access(pred, Full);

@@ -2381,7 +2384,11 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
               BLocal(newVersV) :: Boogie.Havoc(newVers) :: (Heap.select(trE, memberName) := newVers) ::

               bassume(oldVers < Heap.select(trE, memberName)) :: Nil

             }),

-            Nil) :: Nil

+            Nil) :::

+            (if (duringUnfold)

+              // assume that the mask of the predicate we are inhaling contains this location

+              bassume(h.select(unfoldReceiver, unfoldPredicate.FullName+"#m").select(trE, memberName)) :: Nil

+            else Nil)

         else Nil) :::

         bassume(wf(Heap, m, sm)) :::

         (if (m != Mask || sm != SecMask) bassume(wf(Heap, Mask, SecMask)) :: Nil else Nil)