Always use image functions for QPs

src/main/scala/rules/HavocSupporter.scala

@@ -26,7 +26,7 @@ object havocSupporter extends SymbolicExecutionRules {
   // should replace the snapshot. Different data is needed for `havoc` and `havocall`.
   // For more information, see `replacementCond`.
   sealed trait HavocHelperData
-  case class HavocallData(inverseFunctions: InverseFunctions) extends HavocHelperData
+  case class HavocallData(inverseFunctions: InverseFunctions, codomainQVars: Seq[Var], imagesOfCodomain: Seq[Term]) extends HavocHelperData
   case class HavocOneData(args: Seq[Term]) extends HavocHelperData
 
   /** Execute the statement `havoc c ==> R`, where c is a conditional expression and
@@ -130,8 +130,7 @@ object havocSupporter extends SymbolicExecutionRules {
           case false => createFailure(pve dueTo notInjectiveReason, v, s1)
           case true =>
             // Generate the inverse axioms
-            // TODO: Second return value (imagesOfCodomain) currently not used — OK?
-            val (inverseFunctions, _) = quantifiedChunkSupporter.getFreshInverseFunctions(
+            val (inverseFunctions, imagesOfCodomain) = quantifiedChunkSupporter.getFreshInverseFunctions(
               qvars = tVars,
               condition = tCond,
               invertibles = tArgs,
@@ -149,9 +148,9 @@ object havocSupporter extends SymbolicExecutionRules {
             // the HavocHelperData inside of a HavocAllData case.
             val newChunks =
               if (usesQPChunks(s1, resource))
-                havocQuantifiedResource(s1, tCond, resource, HavocallData(inverseFunctions), v1)
+                havocQuantifiedResource(s1, tCond, resource, HavocallData(inverseFunctions, codomainQVars, imagesOfCodomain), v1)
               else
-                havocNonQuantifiedResource(s1, tCond, resource, HavocallData(inverseFunctions), v1)
+                havocNonQuantifiedResource(s1, tCond, resource, HavocallData(inverseFunctions, codomainQVars, imagesOfCodomain), v1)
 
             Q(s1.copy(h = Heap(newChunks)), v1)
         }
@@ -291,9 +290,9 @@ object havocSupporter extends SymbolicExecutionRules {
       case HavocOneData(args) =>
         val eqs = And(chunkArgs.zip(args).map{ case (t1, t2) => t1 === t2 })
         And(lhs, eqs)
-      case HavocallData(inverseFunctions) =>
+      case HavocallData(inverseFunctions, codomainQVars, imagesOfCodomain) =>
         val replaceMap = inverseFunctions.qvarsToInversesOf(chunkArgs)
-        lhs.replace(replaceMap)
+        And(lhs.replace(replaceMap), And(imagesOfCodomain.map(_.replace(codomainQVars, chunkArgs))))
     }
   }
 

src/main/scala/rules/QuantifiedChunkSupport.scala

@@ -1114,6 +1114,10 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
             val qvarsToInvOfLoc = inverseFunctions.qvarsToInversesOf(formalQVars)
             val condOfInvOfLoc = tCond.replace(qvarsToInvOfLoc)
             val lossOfInvOfLoc = loss.replace(qvarsToInvOfLoc)
+            val argsOfInvOfLoc = tArgs.map(a => a.replace(qvarsToInvOfLoc))
+            // ME: We include the following condition to make sure the arguments are contained in the condition (and
+            // can trigger other quantifiers) even if neither tCond not loss term mention the arguments.
+            val argumentsMatch = And(formalQVars.zip(argsOfInvOfLoc).map(va => va._1 === va._2))
 
             v.decider.prover.comment("Definitional axioms for inverse functions")
             v.decider.assume(inverseFunctions.definitionalAxioms.map(a => FunctionPreconditionTransformer.transform(a, s.program)))
@@ -1145,7 +1149,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                     s2,
                     relevantChunks,
                     formalQVars,
-                    And(condOfInvOfLoc, And(imagesOfFormalQVars)),
+                    And(condOfInvOfLoc, And(imagesOfFormalQVars), argumentsMatch),
                     None,
                     resource,
                     rPerm,
@@ -1161,7 +1165,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                   case Complete() => rPerm
                   case Incomplete(remaining) => PermMinus(rPerm, remaining)
                 }
-                val (consumedChunk, _) = quantifiedChunkSupporter.createQuantifiedChunk(
+                val (consumedChunk, inverseFunctions) = quantifiedChunkSupporter.createQuantifiedChunk(
                   qvars,
                   condOfInvOfLoc,
                   resource,
@@ -1175,6 +1179,11 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                   v2,
                   s.program
                 )
+                v.decider.assume(FunctionPreconditionTransformer.transform(inverseFunctions.axiomInvertiblesOfInverses, s3.program))
+                v.decider.assume(inverseFunctions.axiomInvertiblesOfInverses)
+                val substitutedAxiomInversesOfInvertibles = inverseFunctions.axiomInversesOfInvertibles.replace(formalQVars, tArgs)
+                v.decider.assume(FunctionPreconditionTransformer.transform(substitutedAxiomInversesOfInvertibles, s3.program))
+                v.decider.assume(substitutedAxiomInversesOfInvertibles)
                 val h2 = Heap(remainingChunks ++ otherChunks)
                 val s4 = s3.copy(smCache = smCache2,
                                  constrainableARPs = s.constrainableARPs)
@@ -1192,7 +1201,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                   s.copy(smCache = smCache1),
                   relevantChunks,
                   formalQVars,
-                  And(condOfInvOfLoc, And(imagesOfFormalQVars)),
+                  And(condOfInvOfLoc, And(imagesOfFormalQVars), argumentsMatch),
                   None,
                   resource,
                   lossOfInvOfLoc,
@@ -1664,19 +1673,12 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       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)
+      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
-      }
+      imageFunctions(idx) = imgFun
+      imagesOfFcts(idx) = img(invertibles)
+      imagesOfCodomains(idx) = img(codomainQVars)
     }
 
     /* f_1(inv_1(rs), ..., inv_n(rs)), ...,  f_m(inv_1(rs), ..., inv_n(rs)) */