Chalice: add assumption that receivers of nested predicates are different

1 files changed, 27 insertions, 15 deletions

diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala
index 9817d9a3..9c3931f3 100644
--- a/Chalice/src/main/scala/Translator.scala
+++ b/Chalice/src/main/scala/Translator.scala
@@ -2002,34 +2002,43 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
     Exhale(Mask, SecMask, predicates, occasion, check, currentK, exactchecking)

   /** 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)

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

   }

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

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

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

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

   }

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

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

    */

   def UpdateSecMask(predicate: Predicate, receiver: Expr, version: Expr, perm: Permission, currentK: Expr): List[Stmt] = {

     val depth = etran.fpi.getRecursionBound(predicate)

-    UpdateSecMask(predicate, receiver, version, perm, currentK, depth)

+    UpdateSecMask(predicate, receiver, version, perm, currentK, depth, Map())

   }

-  def UpdateSecMask(predicate: Predicate, receiver: Expr, version: Expr, perm: Permission, currentK: Expr, depth: Int): List[Stmt] = {

+  def UpdateSecMask(predicate: Predicate, receiver: Expr, version: Expr, perm: Permission, currentK: Expr, depth: Int, previousReceivers: Map[String,List[Expr]]): List[Stmt] = {

     assert (depth >= 0)

     if (depth <= 0) return Nil

     

     val definition = scaleExpressionByPermission(SubstThis(DefinitionOf(predicate), BoogieExpr(receiver)), perm, NoPosition)

     val occasion = "update SecMask"

     

-    // for every folded predicate that matches (both receiver and version), update the secondary map

+    // condition: if any folded predicate matches (both receiver and version), update the secondary map

     val b = (for (fp <- etran.fpi.getFoldedPredicates(predicate)) yield {

       val conditions = (fp.conditions map (c => if (c._2) c._1 else !c._1)).foldLeft(true: Expr){ (a: Expr, b: Expr) => a && b }

       fp.version ==@ version && fp.receiver ==@ receiver && conditions

     }).foldLeft(false: Expr){ (a: Expr, b: Expr) => a || b }

+    

+    // add receiver to list of previous receivers

+    val newPreviousReceivers = previousReceivers + (predicate.FullName -> (receiver :: previousReceivers.getOrElse(predicate.FullName, Nil)))

+

+    // assumption that the current receiver is different from all previous ones

+    (for (r <- previousReceivers.getOrElse(predicate.FullName, Nil)) yield {

+      bassume(receiver !=@ r)

+    }) :::

+    // actually update the secondary mask

     Boogie.If(b,

       // asserts are converted to assumes, so error messages do not matter

-      assert2assume(Exhale(SecMask, SecMask, List((definition, ErrorMessage(NoPosition, ""))), occasion, false, currentK, false /* it should not important what we pass here */, false, depth-1, true)),

+      assert2assume(Exhale(SecMask, SecMask, List((definition, ErrorMessage(NoPosition, ""))), occasion, false, currentK, false /* it should not important what we pass here */, false, depth-1, true, newPreviousReceivers)),

       Nil) :: Nil

   }

   /** Most general form of exhale; implements all the specific versions above */

@@ -2040,8 +2049,11 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
   // is true, then the depth is important. It is initially set in the method

   // UpdateSecMask (because only there we have precise knowledge of what upper

   // bound we want to use).

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

+  // Assumption 3: Similarly, if isUpdatingSecMask is false, then the list

+  // previousReceivers is not needed, and thus 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]]): List[Boogie.Stmt] = {

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

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

     if (predicates.size == 0) return Nil;

     val (ehV, eh) = Boogie.NewBVar("exhaleHeap", theap, true)

     var (emV, em: Expr) = Boogie.NewBVar("exhaleMask", tmask, true)

@@ -2053,8 +2065,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)).flatten :::

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

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

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

     (if (!isUpdatingSecMask)

       (m := em) ::

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

@@ -2112,11 +2124,11 @@ 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): List[Boogie.Stmt] = desugar(p) match {

+  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]]): List[Boogie.Stmt] = desugar(p) match {

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

       val tmp = Access(pred, Full);

       tmp.pos = pred.pos;

-      ExhaleHelper(tmp, m, sm, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask)

+      ExhaleHelper(tmp, m, sm, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers)

     case AccessAll(obj, perm) => throw new InternalErrorException("should be desugared")

     case AccessSeq(s, None, perm) => throw new InternalErrorException("should be desugared")

     case acc@Access(e,perm) =>

@@ -2144,7 +2156,7 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
         // give up secondary permission to locations of the body of the predicate (also recursively)

         (if (e.isPredicate)

           (if (isUpdatingSecMask)

-            UpdateSecMask(e.predicate, trE, Heap.select(trE, memberName), perm, currentK, recurseOnPredicatesDepth)

+            UpdateSecMask(e.predicate, trE, Heap.select(trE, memberName), perm, currentK, recurseOnPredicatesDepth, previousReceivers)

           else

             UpdateSecMask(e.predicate, trE, Heap.select(trE, memberName), perm, currentK)

           )

@@ -2217,12 +2229,12 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
       else Nil)

     case Implies(e0,e1) =>

       (if(check && !onlyExactCheckingPermissions) isDefined(e0)(true) else Nil) :::

-      Boogie.If(Tr(e0), ExhaleHelper(e1, m, sm, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask), Nil)

+      Boogie.If(Tr(e0), ExhaleHelper(e1, m, sm, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers), Nil)

     case IfThenElse(con, then, els) =>

       (if(check) isDefined(con)(true) else Nil) :::

-      Boogie.If(Tr(con), ExhaleHelper(then, m, sm, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask), ExhaleHelper(els, m, sm, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask))

+      Boogie.If(Tr(con), ExhaleHelper(then, m, sm, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers), ExhaleHelper(els, m, sm, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers))

     case And(e0,e1) =>

-      ExhaleHelper(e0, m, sm, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask) ::: ExhaleHelper(e1, m, sm, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask)

+      ExhaleHelper(e0, m, sm, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers) ::: ExhaleHelper(e1, m, sm, eh, error, check, currentK, exactchecking, onlyExactCheckingPermissions, transferPermissionToSecMask, recurseOnPredicatesDepth, isUpdatingSecMask, previousReceivers)

     case holds@Holds(e) if !onlyExactCheckingPermissions => 

       (if(check) isDefined(e)(true) :::

       bassert(nonNull(Tr(e)), error.pos, error.message + " The target of the holds predicate at " + holds.pos + " might be null.") :: Nil else Nil) :::