Implementing exhaleExt for quantified permissions

src/main/scala/viper/carbon/boogie/boogie.scala

@@ -263,6 +263,13 @@ object MaybeForall {
     else Forall(vars, triggers, exp)
   }
 }
+
+object MaybeExists {
+  def apply(vars: Seq[LocalVarDecl], triggers: Seq[Trigger], exp: Exp) = {
+    if (vars.isEmpty) exp
+    else Exists(vars, triggers, exp)
+  }
+}
 case class Exists(vars: Seq[LocalVarDecl], triggers: Seq[Trigger], exp: Exp, weight: Option[Int] = None) extends QuantifiedExp
 case class Trigger(exps: Seq[Exp]) extends Node
 

src/main/scala/viper/carbon/modules/HeapModule.scala

@@ -183,6 +183,9 @@ trait HeapModule extends Module with CarbonStateComponent {
   // adds permission to field e to the secondary mask of the wand
   def addPermissionToWMask(wMask: Exp, e: sil.Exp): Stmt
 
+  // adds all locations that have positive permission in the given mask to the secondary mask of the wand
+  def addPermissionToWMaskQuant(wMask: Exp, takeMask: Exp): Stmt
+
   // If expression evaluates to true then resultHeap is the sum of of heap1, where mask1 is defined,
   // and heap2, where mask2 is defined.
   def sumHeap(resultHeap: Exp, heap1: Exp, mask1: Exp, heap2: Exp, mask2: Exp): Exp

src/main/scala/viper/carbon/modules/PermModule.scala

@@ -42,6 +42,8 @@ trait PermModule extends Module with CarbonStateComponent {
    */
   def permissionPositive(permission: Exp, zeroOK : Boolean = false): Exp
 
+  def permissionZero(permission: Exp): Exp
+
   def conservativeIsPositivePerm(e: sil.Exp): Boolean
 
   /**
@@ -107,6 +109,8 @@ trait PermModule extends Module with CarbonStateComponent {
 
   def currentPermission(rcv:Exp, loc:Exp):Exp
 
+  def currentPermission(mask: Exp, rcv: Exp, location: Exp): Exp
+
   /**these methods are for experimental purposes, not yet finalized **/
   /*def beginSumMask : Stmt
 
@@ -137,6 +141,8 @@ trait PermModule extends Module with CarbonStateComponent {
     */
   def sumMask(resultMask: Seq[Exp], summandMask1: Seq[Exp], summandMask2: Seq[Exp]) : Exp
 
+  def minMask(mask1: Seq[Exp], mask2: Seq[Exp]): Exp
+
     /** returns a mask and the returned statement ensures that the mask  has non-zero permission at rcv.loc and zero
       * permission at all other location
       * this should only be used temporarily, i.e. if there are two calls to this then the previous tempMask returned
@@ -162,4 +168,14 @@ trait PermModule extends Module with CarbonStateComponent {
 
   def assumePermUpperBounds(doAssume: Boolean): Stmt
 
+  def hasSomePerm(mask: Exp, vars: Seq[LocalVarDecl], rcv: Exp, fld: Exp): Exp
+
+  def subtractMask(op1: Exp, op2: Exp, target: Var): Stmt
+
+  def goodMask(msk: Exp): Exp
+
+  def addQPFunctions(qvars: Seq[LocalVarDecl], argumentDecls: Seq[LocalVarDecl]):(Seq[Func],Func,Func)
+
+  def validateTriggers(vars:Seq[LocalVarDecl], triggers:Seq[Trigger]):Seq[Trigger]
+
 }

src/main/scala/viper/carbon/modules/TransferEntity.scala

@@ -6,10 +6,9 @@
 
 package viper.carbon.modules
 
-import viper.carbon.boogie.Exp
+import viper.carbon.boogie.{Exp, LocalVar}
 import viper.silver.ast.LocationAccess
 import viper.silver.verifier.{PartialVerificationError, VerificationError, reasons}
-
 import viper.silver.{ast => sil}
 
 sealed trait TransferableEntity {
@@ -39,11 +38,19 @@ object TransferableAccessPred {
 }
 
 case class TransferableFieldAccessPred(rcv: Exp, loc:Exp, transferAmount: Exp,originalSILExp: sil.AccessPredicate) extends TransferableAccessPred
+case class QuantifiedTransferableFieldAccessPred(qvars: Seq[LocalVar], cond: Exp, rcv: Exp, loc:Exp, transferAmount: Exp, originalSILExp: sil.AccessPredicate) extends TransferableAccessPred
 
 case class TransferablePredAccessPred(rcv: Exp, loc:Exp, transferAmount: Exp,originalSILExp: sil.AccessPredicate) extends TransferableAccessPred
+case class QuantifiedTransferablePredAccessPred(qvars: Seq[LocalVar], cond: Exp, rcv: Exp, loc:Exp, transferAmount: Exp,originalSILExp: sil.AccessPredicate) extends TransferableAccessPred
 
 case class TransferableWand(rcv:Exp, loc: Exp, transferAmount: Exp,originalSILExp: sil.MagicWand) extends TransferableEntity {
   override def transferError(error: PartialVerificationError): VerificationError = {
     error.dueTo(reasons.MagicWandChunkNotFound(originalSILExp))
   }
 }
+
+case class QuantifiedTransferableWand(qvars: Seq[LocalVar], cond: Exp, rcv:Exp, loc: Exp, transferAmount: Exp,originalSILExp: sil.MagicWand) extends TransferableEntity {
+  override def transferError(error: PartialVerificationError): VerificationError = {
+    error.dueTo(reasons.MagicWandChunkNotFound(originalSILExp))
+  }
+}

src/main/scala/viper/carbon/modules/components/TransferComponent.scala

@@ -32,11 +32,15 @@ trait TransferComponent extends Component {
    */
   def transferAdd(e:TransferableEntity, cond: Exp): Stmt
 
+  def transferAddQuant(toAddMask: Exp, cond: Exp): Stmt
+
   /**
    *
    * @param e
    * @param cond all assumptions and assertions should be wrapped inside an if statement with condition cond
    * @return  statement which removes the expression e to the current state (for example permissions, wand)
    */
   def transferRemove(e:TransferableEntity, cond:Exp): Stmt
+
+  def transferRemoveQuant(toRemoveMask: Exp, cond: Exp): Stmt
 }

src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala

@@ -694,6 +694,23 @@ class DefaultHeapModule(val verifier: Verifier)
         Statements.EmptyStmt
     }
   }
+
+  override def addPermissionToWMaskQuant(wMaskField: Exp, takeMask: Exp): Stmt = {
+    if(usingOldState) { sys.error("Updating wand mask while using old state") }
+    // TODO: for transferred predicate instances, the locations in the predicates' footprints
+    // (i.e., their secondary masks) are not propagated to the wand mask here, in contrast to
+    // the non-quantified case in addPermissionToWMask.
+    val newPMask = LocalVar(Identifier("newPMask"), pmaskType)
+    val obj = LocalVarDecl(Identifier("o")(axiomNamespace), refType)
+    val field = LocalVarDecl(Identifier("f")(axiomNamespace), fieldType)
+    val pm1 = lookup(wandMask(wMaskField), obj.l, field.l, true)
+    val pm2 = lookup(newPMask, obj.l, field.l, true)
+    val transferredPerm = permModule.currentPermission(takeMask, obj.l, field.l)
+    Havoc(newPMask) ++
+      Assume(Forall(Seq(obj, field), Seq(Trigger(pm2)), (pm1 || permModule.permissionPositive(transferredPerm)) ==> pm2)) ++
+      curHeapAssignUpdatePredWandMask(wMaskField, newPMask)
+  }
+
   /**
    * Adds the permissions from the body of a predicate to its permission mask.
    */