Merge pull request #817 from viperproject/meilers_avoid_qp_wildcard_constraint_quantifier

Avoid using a quantifier for wildcard constraints for quantified resources

Author: marcoeilers

src/main/scala/rules/Executor.scala

@@ -387,6 +387,7 @@ object executor extends ExecutionRules {
               relevantChunks,
               Seq(`?r`),
               `?r` === tRcvr,
+              Some(Seq(tRcvr)),
               field,
               FullPerm,
               chunkOrderHeuristics,

src/main/scala/rules/QuantifiedChunkSupport.scala

@@ -1146,6 +1146,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                     relevantChunks,
                     formalQVars,
                     And(condOfInvOfLoc, And(imagesOfFormalQVars)),
+                    None,
                     resource,
                     rPerm,
                     chunkOrderHeuristics,
@@ -1192,6 +1193,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                   relevantChunks,
                   formalQVars,
                   And(condOfInvOfLoc, And(imagesOfFormalQVars)),
+                  None,
                   resource,
                   lossOfInvOfLoc,
                   chunkOrderHeuristics,
@@ -1259,6 +1261,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
           relevantChunks,
           codomainQVars,
           And(codomainQVars.zip(arguments).map { case (r, e) => r === e }),
+          Some(arguments),
           resource,
           rPerm,
           chunkOrderHeuristics,
@@ -1302,6 +1305,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
         relevantChunks,
         codomainQVars,
         And(codomainQVars.zip(arguments).map { case (r, e) => r === e }),
+        Some(arguments),
         resource,
         permissions,
         chunkOrderHeuristics,
@@ -1339,6 +1343,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                         relevantChunks: Seq[QuantifiedBasicChunk],
                         codomainQVars: Seq[Var], /* rs := r_1, ..., r_m */
                         condition: Term, // c(rs)
+                        optQVarValues: Option[Seq[Term]], /* optionally actual known values vs := v_1, ..., v_m for all codomainQVars
+                                                             (if we're consuming a single location), i.e., if condition is
+                                                             forall i :: r_i == v_i */
                         resource: ast.Resource, // field f: e_1(rs).f; or predicate P: P(es); or magic wand
                         perms: Term, // p(rs)
                         chunkOrderHeuristic: Seq[QuantifiedBasicChunk] => Seq[QuantifiedBasicChunk],
@@ -1409,7 +1416,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       else {
         val (permissionConstraint, depletedCheck) =
           createPermissionConstraintAndDepletedCheck(
-            codomainQVars, condition, perms,constrainPermissions, ithChunk, ithPTaken, v)
+            codomainQVars, condition, optQVarValues, perms, constrainPermissions, ithChunk, ithPTaken, v)
 
         if (constrainPermissions) {
           v.decider.prover.comment(s"Constrain original permissions $perms")
@@ -1459,6 +1466,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
 
   private def createPermissionConstraintAndDepletedCheck(codomainQVars: Seq[Var], /* rs := r_1, ..., r_m */
                                                          condition: Term, // c(rs)
+                                                         optQVarValues: Option[Seq[Term]], /* vs := v_1, ..., v_m  if c is r_1 == v_1 && ... */
                                                          perms: Term, // p(rs)
                                                          constrainPermissions: Boolean,
                                                          ithChunk: QuantifiedBasicChunk,
@@ -1499,8 +1507,14 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
             (quantifiedPermissionConstraint.map(_.instantiate(args)),
              quantifiedDepletedCheck.instantiate(args))
           case None =>
-            (quantifiedPermissionConstraint,
-             quantifiedDepletedCheck)
+            optQVarValues match {
+              case Some(values) =>
+                (quantifiedPermissionConstraint.map(_.instantiate(values)),
+                 quantifiedDepletedCheck)
+              case _ =>
+                (quantifiedPermissionConstraint,
+                  quantifiedDepletedCheck)
+            }
         }
 
     (permissionConstraint.getOrElse(True), depletedCheck)