Merge pull request #666 from viperproject/meilers_qp_finite_domains

marcoeilers · web-flow · commit 062a11cf27fd · 2022-11-25T18:59:42.000+01:00
Adjusting the QP encoding to deal with quantification over finite types
diff --git a/silver b/silver
@@ -1 +1 @@
-Subproject commit d978f88eb363440390ca3baa62ce56ad3fadc42c
+Subproject commit 41b7353ac09cfc39d7b8f2b67e1a2c5487bcae35
diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala
@@ -32,10 +32,13 @@ case class InverseFunctions(condition: Term,
                             additionalArguments: Vector[Var],
                             axiomInversesOfInvertibles: Quantification,
                             axiomInvertiblesOfInverses: Quantification,
-                            qvarsToInverses: Map[Var, Function]) {
+                            qvarsToInverses: Map[Var, Function],
+                            qvarsToImages: Map[Var, Function]) {
 
   val inverses: Iterable[Function] = qvarsToInverses.values
 
+  val images: Iterable[Function] = qvarsToImages.values
+
   val definitionalAxioms: Vector[Quantification] =
     Vector(axiomInversesOfInvertibles, axiomInvertiblesOfInverses)
 
@@ -93,6 +96,8 @@ trait QuantifiedChunkSupport extends SymbolicExecutionRules {
   /** Creates `n` fresh (partial) inverse functions `inv_i` that invert an `n`-ary
     * function `fct`, where `n == qvars.length`, and returns the inverse functions as
     * well as the definitional axioms.
+    * If the types of the quantified variables could be finite, additionally creates n fresh
+    * boolean functions `img_i` denoting the domain of the respective inverse functions.
     *
     * Let
     *   - `x_1: T_1`, ..., `x_n: T_n` denote the quantified variables (argument `qvars`)
@@ -103,18 +108,21 @@ trait QuantifiedChunkSupport extends SymbolicExecutionRules {
     *     the partial inverses are defined
     *
     * The following definitional axioms will be returned, in addition to the fresh
-    * inverse functions `inv_1`, ..., `inv_n`:
+    * inverse functions `inv_1`, ..., `inv_n` and the respective image functions:
     *
     *   forall x_1: T_1, ..., x_n: T_n :: {fct(x_1, ..., x_n)}
     *     c(x_1, ..., x_n) ==>
-    *          inv_1(fct(x_1, ..., x_n)) == x_1
+    *          inv_1(fct(x_1, ..., x_n)) == x_1 && img_1(fct(x_1, ..., x_n))
     *       && ...
-    *       && inv_n(fct(x_1, ..., x_n)) == x_n
+    *       && inv_n(fct(x_1, ..., x_n)) == x_n && img_n(fct(x_1, ..., x_n))
     *
     *   forall r: R :: {inv_1(r), ..., inv_n(r)}
-    *     c(inv_1(r), ..., inv_n(r)) ==>
+    *     c(inv_1(r), ..., inv_n(r)) && img_1(r) && ... && img_n(r) ==>
     *       fct(inv_1(r), ..., inv_n(r)) == r
     *
+    *  For all i where x_i is of type Ref or Int, we do not generate the img_i constraints in
+    *  either axiom, since those types are known to have the same cardinality as Ref.
+    *
     * @param qvars Quantified variables that occur in the invertible function and for
     *              which partial inverse functions are to be defined..
     * @param condition A condition (containing the quantified variables) determining
@@ -125,7 +133,10 @@ trait QuantifiedChunkSupport extends SymbolicExecutionRules {
     * @param additionalInvArgs Additional arguments on which `inv` depends (typically
     *                          quantified variables bound by some surrounding scope).
     *                          Currently omitted from the axioms shown above.
-    * @return The generated partial inverse functions and corresponding definitional axioms.
+    * @return The generated partial inverse functions and corresponding definitional axioms, and
+    *         the images of the given codomain variables (returned separately, since nothing else
+    *         in the returned InverseFunctions object references or contains the codomain
+    *         variables, and thus they only have meaning for the caller).
     */
   def getFreshInverseFunctions(qvars: Seq[Var],
                                condition: Term,
@@ -135,7 +146,7 @@ trait QuantifiedChunkSupport extends SymbolicExecutionRules {
                                userProvidedTriggers: Option[Seq[Trigger]],
                                qidPrefix: String,
                                v: Verifier)
-                              : InverseFunctions
+                              : (InverseFunctions, Seq[Term])
 
   def injectivityAxiom(qvars: Seq[Var],
                        condition: Term,
@@ -247,7 +258,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                             program: ast.Program)
                            : (QuantifiedBasicChunk, InverseFunctions) = {
 
-    val inverseFunctions =
+    val (inverseFunctions, imagesOfCodomain) =
       getFreshInverseFunctions(
         qvars,
         And(condition, IsPositive(permissions)),
@@ -262,7 +273,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
 
     val conditionalizedPermissions =
       Ite(
-        condition.replace(qvarsToInversesOfCodomain),
+        And(And(imagesOfCodomain), condition.replace(qvarsToInversesOfCodomain)),
         permissions.replace(qvarsToInversesOfCodomain),
         NoPerm())
 
@@ -1014,7 +1025,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
              (Q: (State, Heap, Term, Verifier) => VerificationResult)
              : VerificationResult = {
 
-    val inverseFunctions =
+    val (inverseFunctions, imagesOfFormalQVars) =
       quantifiedChunkSupporter.getFreshInverseFunctions(
         qvars,
         And(tCond, IsPositive(tPerm)),
@@ -1124,13 +1135,13 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                     s2,
                     relevantChunks,
                     formalQVars,
-                    condOfInvOfLoc,
+                    And(condOfInvOfLoc, And(imagesOfFormalQVars)),
                     resource,
                     rPerm,
                     chunkOrderHeuristics,
                     v2)
                 val optSmDomainDefinitionCondition2 =
-                    if (s3.smDomainNeeded) Some(And(condOfInvOfLoc, IsPositive(lossOfInvOfLoc)))
+                    if (s3.smDomainNeeded) Some(And(condOfInvOfLoc, IsPositive(lossOfInvOfLoc), And(imagesOfFormalQVars)))
                     else None
                   val (smDef2, smCache2) =
                     quantifiedChunkSupporter.summarisingSnapshotMap(
@@ -1170,7 +1181,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                   s.copy(smCache = smCache1),
                   relevantChunks,
                   formalQVars,
-                  condOfInvOfLoc,
+                  And(condOfInvOfLoc, And(imagesOfFormalQVars)),
                   resource,
                   lossOfInvOfLoc,
                   chunkOrderHeuristics,
@@ -1180,7 +1191,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                 case (Complete(), s2, remainingChunks) =>
                   val h3 = Heap(remainingChunks ++ otherChunks)
                   val optSmDomainDefinitionCondition2 =
-                    if (s2.smDomainNeeded) Some(And(condOfInvOfLoc, IsPositive(lossOfInvOfLoc)))
+                    if (s2.smDomainNeeded) Some(And(condOfInvOfLoc, IsPositive(lossOfInvOfLoc), And(And(imagesOfFormalQVars))))
                     else None
                   val (smDef2, smCache2) =
                     quantifiedChunkSupporter.summarisingSnapshotMap(
@@ -1577,7 +1588,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                                userProvidedTriggers: Option[Seq[Trigger]],
                                qidPrefix: String,
                                v: Verifier)
-                              : InverseFunctions = {
+                              : (InverseFunctions, Seq[Term]) = {
 
     assert(
       invertibles.length == codomainQVars.length,
@@ -1593,6 +1604,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
     val qvarsWithIndices = qvars.zipWithIndex
 
     val inverseFunctions = Array.ofDim[Function](qvars.length) /* inv_i */
+    val imageFunctions = Array.ofDim[Function](qvars.length) /* img_i */
+    val imagesOfFcts = Array.ofDim[Term](qvars.length) // /* img_i(f_1(xs), ..., f_m(xs)) */
+    val imagesOfCodomains = Array.ofDim[Term](qvars.length) /* img_i(rs) */
     val inversesOfFcts = Array.ofDim[Term](qvars.length)       /* inv_i(f_1(xs), ..., f_m(xs)) */
     val inversesOfCodomains = Array.ofDim[Term](qvars.length)  /* inv_i(rs) */
 
@@ -1603,6 +1617,20 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       inverseFunctions(idx) = fun
       inversesOfFcts(idx) = inv(invertibles)
       inversesOfCodomains(idx) = inv(codomainQVars)
+
+      if (qvar.sort != sorts.Int && qvar.sort != sorts.Ref) {
+        // Types known to be infinite, thus there is no need to constrain the domain using image functions.
+        val imgFun = v.decider.fresh("img", (additionalInvArgs map (_.sort)) ++ invertibles.map(_.sort), sorts.Bool)
+        val img = (ts: Seq[Term]) => App(imgFun, additionalInvArgs ++ ts)
+
+        imageFunctions(idx) = imgFun
+        imagesOfFcts(idx) = img(invertibles)
+        imagesOfCodomains(idx) = img(codomainQVars)
+      } else {
+        // imageFunctions(idx) remains null, will be filtered out later.
+        imagesOfFcts(idx) = True()
+        imagesOfCodomains(idx) = True()
+      }
     }
 
     /* f_1(inv_1(rs), ..., inv_n(rs)), ...,  f_m(inv_1(rs), ..., inv_n(rs)) */
@@ -1614,14 +1642,15 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       condition.replace(qvars, ArraySeq.unsafeWrapArray(inversesOfCodomains))
 
     /* c(xs) ==>
-     *       inv_1(f_1(xs), ..., f_m(xs)) == x_1
+     *       inv_1(f_1(xs), ..., f_m(xs)) == x_1 && img_1(f_1(xs), ..., f_m(xs)) &&
      *   &&  ...
-     *   &&  inv_n(f_1(xs), ..., f_m(xs)) == x_n
+     *   &&  inv_n(f_1(xs), ..., f_m(xs)) == x_n && img_n(f_1(xs), ..., f_m(xs))
      */
     val axInvsOfFctsBody =
       Implies(
         condition,
-        And(qvarsWithIndices map { case (qvar, idx) => inversesOfFcts(idx) === qvar }))
+        And(And(qvarsWithIndices map { case (qvar, idx) => inversesOfFcts(idx) === qvar }),
+            And(qvarsWithIndices map { case (_, idx) => imagesOfFcts(idx) })))
 
     val axInvsOfFct =
       userProvidedTriggers match {
@@ -1644,12 +1673,12 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
             s"$qidPrefix-invOfFct")
       }
 
-    /* c(inv_1(rs), ..., inv_n(rs)) ==>
+    /* c(inv_1(rs), ..., inv_n(rs)) && img_1(rs) && ... && img_n(rs) ==>
      *    f_1(inv_1(rs), ..., inv_n(rs)) == r_1
      */
     val axFctsOfInvsBody =
       Implies(
-        conditionOfInverses,
+        And(And(imagesOfCodomains), conditionOfInverses),
         And(
           fctsOfInversesOfCodomain
             .zip(codomainQVars)
@@ -1669,13 +1698,16 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
         isGlobal = true,
         v.axiomRewriter)
 
-    InverseFunctions(
+    val res = InverseFunctions(
       condition,
       invertibles,
       additionalInvArgs.toVector,
       axInvsOfFct,
       axFctsOfInvs,
-      qvars.zip(inverseFunctions).to(Map))
+      qvars.zip(inverseFunctions).to(Map),
+      qvars.zip(imageFunctions).filter(_._2 != null).to(Map)
+    )
+    (res, imagesOfCodomains)
   }
 
   def hintBasedChunkOrderHeuristic(hints: Seq[Term])
diff --git a/src/main/scala/supporters/functions/FunctionData.scala b/src/main/scala/supporters/functions/FunctionData.scala
@@ -124,7 +124,7 @@ class FunctionData(val programFunction: ast.Function,
     freshSymbolsAcrossAllPhases ++= freshPathSymbols map FunctionDecl
     freshSymbolsAcrossAllPhases ++= freshArps.map(pair => FunctionDecl(pair._1))
     freshSymbolsAcrossAllPhases ++= freshSnapshots map FunctionDecl
-    freshSymbolsAcrossAllPhases ++= freshFieldInvs.flatMap(_.inverses map FunctionDecl)
+    freshSymbolsAcrossAllPhases ++= freshFieldInvs.flatMap(i => (i.inverses ++ i.images) map FunctionDecl)
     freshSymbolsAcrossAllPhases ++= freshMacros
 
     freshSymbolsAcrossAllPhases ++= freshFvfsAndDomains map (fvfDef =>
