Chalice: first try for unfolding

1 files changed, 38 insertions, 11 deletions

diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala
index 9c3931f3..a2106c14 100644
--- a/Chalice/src/main/scala/Translator.scala
+++ b/Chalice/src/main/scala/Translator.scala
@@ -1418,6 +1418,7 @@ class FoldedPredicatesInfo {
   /** Start again with the empty information about folded predicates. */

   def reset {

     foldedPredicates = List()

+    currentConditions = Set()

   }

   

   /** return a list of folded predicates that might match for predicate */

@@ -1560,16 +1561,22 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
         (if(checkTermination) { List(prove(NonEmptyMask(tmpGlobals.mask), func.pos, "The heap of the callee might not be strictly smaller than the heap of the caller.")) } else Nil)

       case unfolding@Unfolding(acc@Access(pred@MemberAccess(obj, f), perm), e) =>

         val (tmpGlobalsV, tmpGlobals) = etran.FreshGlobals("unfolding")

-        val tmpTranslator = new ExpressionTranslator(tmpGlobals, etran.oldEtran.globals, currentClass);

+        val tmpTranslator = new ExpressionTranslator(Globals(tmpGlobals.heap, tmpGlobals.mask, etran.SecMask, tmpGlobals.credits), etran.oldEtran.globals, currentClass);

         

-        val receiverOk = isDefined(obj) ::: prove(nonNull(Tr(obj)), obj.pos, "Receiver might be null.");

+        val (receiverV, receiver) = Boogie.NewBVar("predRec", tref, true)

+        val (versionV, version) = Boogie.NewBVar("predVer", tint, true)

+        

+        val trO = Tr(obj)

+        val receiverOk = isDefined(obj) ::: prove(nonNull(trO), obj.pos, "Receiver might be null.");

         val definition = scaleExpressionByPermission(SubstThis(DefinitionOf(pred.predicate), obj), perm, unfolding.pos)

         

         // pick new k

         val (unfoldingKV, unfoldingK) = Boogie.NewBVar("unfoldingK", tint, true)

         

-        Comment("unfolding") ::

+        val stmts = Comment("unfolding") ::

         BLocal(unfoldingKV) :: bassume(0 < unfoldingK && 1000*unfoldingK < percentPermission(1)) ::

+        BLocal(receiverV) :: (receiver := trO) ::

+        BLocal(versionV) :: (version := etran.Heap.select(trO, pred.predicate.FullName)) ::

         // check definedness

         receiverOk ::: isDefined(perm) :::

         // copy state into temporary variables

@@ -1578,9 +1585,16 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
         // exhale the predicate

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

         // inhale the definition of the predicate

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

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

         // check definedness of e in state where the predicate is unfolded

         tmpTranslator.isDefined(e)

+        

+        // record folded predicate

+        Thread.dumpStack()

+        println(FoldedPredicate(pred.predicate, receiver, version, etran.fpi.currentConditions))

+        etran.fpi.addFoldedPredicate(FoldedPredicate(pred.predicate, receiver, version, etran.fpi.currentConditions))

+        

+        stmts

       case Iff(e0,e1) =>

         isDefined(e0) ::: isDefined(e1)

       case Implies(e0,e1) =>

@@ -1819,6 +1833,16 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
   /**********************************************************************

   *****************          INHALE/EXHALE              *****************

   **********************************************************************/

+  

+  def InhaleAndTransferToSecMask(predicates: List[Expression], occasion: String, check: Boolean, currentK: Expr): List[Boogie.Stmt] = {

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

+    

+    Comment("inhale (" + occasion + ")") ::

+    (for (p <- predicates) yield Inhale(p, Heap, check, currentK, true)).flatten :::

+    bassume(AreGoodMasks(Mask, SecMask)) ::

+    bassume(wf(Heap, Mask, SecMask)) ::

+    Comment("end inhale")

+  }

 

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

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

@@ -1827,7 +1851,7 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
     Comment("inhale (" + occasion + ")") ::

     //BLocal(ihV) :: Boogie.Havoc(ih) ::

     //bassume(IsGoodInhaleState(ih, Heap, Mask, SecMask)) ::

-    (for (p <- predicates) yield Inhale(p, Heap, check, currentK)).flatten :::

+    (for (p <- predicates) yield Inhale(p, Heap, check, currentK, false)).flatten :::

     bassume(AreGoodMasks(Mask, SecMask)) ::

     bassume(wf(Heap, Mask, SecMask)) ::

     Comment("end inhale")

@@ -1853,7 +1877,7 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
     })

   }

 

-  def Inhale(p: Expression, ih: Boogie.Expr, check: Boolean, currentK: Expr): List[Boogie.Stmt] = desugar(p) match {

+  def Inhale(p: Expression, ih: Boogie.Expr, check: Boolean, currentK: Expr, transferToSecMask: Boolean): List[Boogie.Stmt] = desugar(p) match {

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

       val chk = (if (check) {

         isDefined(e)(true) ::: 

@@ -1861,7 +1885,7 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
       } else Nil)

       val tmp = Access(pred, Full);

       tmp.pos = pred.pos;

-      chk ::: Inhale(tmp, ih, check, currentK)

+      chk ::: Inhale(tmp, ih, check, currentK, transferToSecMask)

     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) =>

@@ -1877,6 +1901,9 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
       bassume(wf(Heap, Mask, SecMask)) ::

       (if(e.isPredicate) Nil else List(bassume(TypeInformation(new Boogie.MapSelect(Heap, trE, memberName), e.f.typ.typ)))) :::

       InhalePermission(perm, trE, memberName, currentK) :::

+      (if (transferToSecMask)

+        InhalePermission(perm, trE, memberName, currentK, SecMask)

+      else Nil) :::

       bassume(AreGoodMasks(Mask, SecMask)) ::

       bassume(IsGoodState(heapFragment(new Boogie.MapSelect(ih, trE, memberName)))) ::

       bassume(wf(Heap, Mask, SecMask)) ::

@@ -1936,12 +1963,12 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
       new Boogie.MapUpdate(Credits, trCh, new Boogie.MapSelect(Credits, trCh) + Tr(cr.N))

     case Implies(e0,e1) =>

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

-      Boogie.If(Tr(e0), Inhale(e1, ih, check, currentK), Nil)

+      Boogie.If(Tr(e0), Inhale(e1, ih, check, currentK, transferToSecMask), Nil)

     case IfThenElse(con, then, els) =>

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

-      Boogie.If(Tr(con), Inhale(then, ih, check, currentK), Inhale(els, ih, check, currentK))

+      Boogie.If(Tr(con), Inhale(then, ih, check, currentK, transferToSecMask), Inhale(els, ih, check, currentK, transferToSecMask))

     case And(e0,e1) =>

-      Inhale(e0, ih, check, currentK) ::: Inhale(e1, ih, check, currentK)

+      Inhale(e0, ih, check, currentK, transferToSecMask) ::: Inhale(e1, ih, check, currentK, transferToSecMask)

     case holds@Holds(e) =>

       val trE = Tr(e);

       (if(check)

@@ -1979,7 +2006,7 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
       bassume(AreGoodMasks(preEtran.Mask, preEtran.SecMask)) ::

       bassume(wf(preEtran.Heap, preEtran.Mask, preEtran.SecMask)) ::

       bassume(proofOrAssume) ::

-      preEtran.Inhale(e, ih, check, currentK) :::

+      preEtran.Inhale(e, ih, check, currentK, transferToSecMask) :::

       bassume(preEtran.Heap ==@ evalHeap) ::

       bassume(submask(preEtran.Mask, evalMask))

     case e => (if(check) isDefined(e)(true) else Nil) ::: bassume(Tr(e))