Reset resource cache

viperproject · Nov 13, 2023 · ceca6c4 · ceca6c4
1 parent 5bfe0dc
commit ceca6c4
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 6 deletions.
diff --git a/src/main/scala/rules/MaskHeapSupport.scala b/src/main/scala/rules/MaskHeapSupport.scala
@@ -19,18 +19,25 @@ import viper.silicon.supporters.functions.NoopFunctionRecorder
 import viper.silicon.verifier.Verifier
 import viper.silver.verifier.{ErrorReason, PartialVerificationError}
 import viper.silver.ast
+import viper.silver.components.StatefulComponent
 import viper.silver.reporter.InternalWarningMessage
 import viper.silver.verifier.reasons.{InsufficientPermission, MagicWandChunkNotFound}
 
 import scala.collection.mutable.ListBuffer
 import scala.collection.{immutable, mutable}
 
-object maskHeapSupporter extends SymbolicExecutionRules {
+object maskHeapSupporter extends SymbolicExecutionRules with StatefulComponent {
 
   val assumeGoodMask = true
-  val simplifyOnConsume = !Verifier.config.prover.toOption.contains("Z3-API")
+  val simplifyOnConsume = false // !Verifier.config.prover.toOption.contains("Z3-API")
 
   val resCache = mutable.HashMap[(Seq[ast.Exp], ast.Program), Seq[Any]]()
+
+  override def start(): Unit = { }
+  override def stop(): Unit = {}
+  override def reset(): Unit = {
+    resCache.clear()
+  }
   def getResourceSeq(tlcs: Seq[ast.Exp], program: ast.Program): Seq[Any] = {
     val key = (tlcs, program)
     val current = resCache.get(key)
@@ -741,8 +748,6 @@ object maskHeapSupporter extends SymbolicExecutionRules {
     val qpMaskGet = HeapLookup(qpMask, argTerm)
     val qpMaskConstraint = Forall(formalQVars, qpMaskGet === conditionalizedPermissions, Seq(Trigger(qpMaskGet)), "qpMaskdef")
 
-    v.decider.assume(qpMaskConstraint)
-
     val resourceToFind = resource match {
       case mw: ast.MagicWand => MagicWandIdentifier(mw, s.program)
       case _ => resource
@@ -753,8 +758,7 @@ object maskHeapSupporter extends SymbolicExecutionRules {
       case r: ast.Resource => (s.h, findMaskHeapChunk(s.h, r))
     }
     val newMask =  MaskSum(currentChunk.mask, qpMask)
-    if (assumeGoodMask)
-      v.decider.assume(if (resource.isInstanceOf[ast.Field]) GoodFieldMask(newMask) else GoodMask(newMask))
+
 
     val newHeap = MergeHeaps(currentChunk.heap, currentChunk.mask, snapHeapMap(resource), qpMask)
     val (newChunk, fr0) = currentChunk.copy(newMask = newMask, v.decider, s.functionRecorder, newHeap = newHeap)
@@ -830,6 +834,11 @@ object maskHeapSupporter extends SymbolicExecutionRules {
         v.decider.assume(FunctionPreconditionTransformer.transform(receiverInjectivityCheck, s.program))
         v.decider.assert(receiverInjectivityCheck) {
           case true =>
+            v.decider.assume(qpMaskConstraint)
+
+            if (assumeGoodMask)
+              v.decider.assume(if (resource.isInstanceOf[ast.Field]) GoodFieldMask(newMask) else GoodMask(newMask))
+
             val ax = inverseFunctions.axiomInversesOfInvertibles
             val inv = inverseFunctions.copy(axiomInversesOfInvertibles = Forall(ax.vars, ax.body, effectiveTriggers))
 

diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala
@@ -23,6 +23,7 @@ import viper.silicon.interfaces._
 import viper.silicon.interfaces.decider.ProverLike
 import viper.silicon.logger.{MemberSymbExLogger, SymbExLogger}
 import viper.silicon.reporting.{MultiRunRecorders, condenseToViperResult}
+import viper.silicon.rules.maskHeapSupporter
 import viper.silicon.state._
 import viper.silicon.state.terms.{Decl, Sort, Term, sorts}
 import viper.silicon.supporters._
@@ -85,6 +86,7 @@ class DefaultMainVerifier(config: Config,
     fieldValueFunctionsContributor,
     heapFunctionsContributor,
     predSnapGenerator, predicateAndWandSnapFunctionsContributor,
+    maskHeapSupporter,
     functionsSupporter, predicateSupporter,
     _verificationPoolManager,
     MultiRunRecorders /* In lieu of a better place, include MultiRunRecorders singleton here */