More fine-grained state consolidation configuration

src/main/scala/Config.scala

@@ -906,14 +906,17 @@ object Config {
 
   object StateConsolidationMode extends Enumeration {
     type StateConsolidationMode = Value
-    val Minimal, Default, Retrying, MinimalRetrying, MoreCompleteExhale = Value
+    val Minimal, Default, Retrying, MinimalRetrying, MoreCompleteExhale, LastRetry, RetryingFailOnly, LastRetryFailOnly = Value
 
     private[Config] final def helpText: String = {
       s"""  ${Minimal.id}: Minimal work, many incompletenesses
          |  ${Default.id}: Most work, fewest incompletenesses
-         |  ${Retrying.id}: Similar to ${Default.id}, but less eager
+         |  ${Retrying.id}: Similar to ${Default.id}, but less eager (optional and failure-driven consolidation only on retry)
          |  ${MinimalRetrying.id}: Less eager and less complete than ${Default.id}
          |  ${MoreCompleteExhale.id}: Intended for use with --moreCompleteExhale
+         |  ${LastRetry.id}: Similar to ${Retrying.id}, but only on last retry
+         |  ${RetryingFailOnly.id}: Similar to ${Retrying.id}, but performs no optional consolidation at all.
+         |  ${LastRetryFailOnly.id}: Similar to ${LastRetry.id}, but performs no optional consolidation at all.
          |""".stripMargin
     }
 

src/main/scala/rules/Brancher.scala

@@ -146,7 +146,7 @@ object brancher extends BranchingRules {
             if (v.uniqueId != v0.uniqueId)
               v1.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract)
 
-            val result = fElse(v1.stateConsolidator.consolidateIfRetrying(s1, v1), v1)
+            val result = fElse(v1.stateConsolidator.consolidateOptionally(s1, v1), v1)
             if (wasElseExecutedOnDifferentVerifier) {
               v1.decider.resetProverOptions()
               v1.decider.setProverOptions(proverArgsOfElseBranchDecider)
@@ -186,7 +186,7 @@ object brancher extends BranchingRules {
             v1.decider.prover.comment(s"[then-branch: $cnt | $condition]")
             v1.decider.setCurrentBranchCondition(condition, conditionExp)
 
-            fThen(v1.stateConsolidator.consolidateIfRetrying(s1, v1), v1)
+            fThen(v1.stateConsolidator.consolidateOptionally(s1, v1), v1)
           })
         } else {
           Unreachable()

src/main/scala/rules/Evaluator.scala

@@ -861,7 +861,7 @@ object evaluator extends EvaluationRules {
                                          recordVisited = s3.recordVisited,
                                          permissionScalingFactor = s6.permissionScalingFactor)
                                    .decCycleCounter(predicate)
-                        val s10 = v5.stateConsolidator.consolidateIfRetrying(s9, v5)
+                        val s10 = v5.stateConsolidator.consolidateOptionally(s9, v5)
                         eval(s10, eIn, pve, v5)(QB)})})
                   })(join(v2.symbolConverter.toSort(eIn.typ), "joined_unfolding", s2.relevantQuantifiedVariables, v2))(Q)
                 case false =>
@@ -1149,7 +1149,7 @@ object evaluator extends EvaluationRules {
 
     val h = s.oldHeaps(label)
     val s1 = s.copy(h = h, partiallyConsumedHeap = None)
-    val s2 = v.stateConsolidator.consolidateIfRetrying(s1, v)
+    val s2 = v.stateConsolidator.consolidateOptionally(s1, v)
     val possibleTriggersBefore: Map[ast.Exp, Term] = if (s.recordPossibleTriggers) s.possibleTriggers else Map.empty
 
     eval(s2, e, pve, v)((s3, t, v1) => {

src/main/scala/rules/StateConsolidator.scala

@@ -22,7 +22,7 @@ import viper.silver.ast
 
 trait StateConsolidationRules extends SymbolicExecutionRules {
   def consolidate(s: State, v: Verifier): State
-  def consolidateIfRetrying(s: State, v: Verifier): State
+  def consolidateOptionally(s: State, v: Verifier): State
   def merge(fr: FunctionRecorder, h: Heap, newH: Heap, v: Verifier): (FunctionRecorder, Heap)
   def merge(fr: FunctionRecorder, h: Heap, ch: NonQuantifiedChunk, v: Verifier): (FunctionRecorder, Heap)
 
@@ -37,7 +37,7 @@ trait StateConsolidationRules extends SymbolicExecutionRules {
   */
 class MinimalStateConsolidator extends StateConsolidationRules {
   def consolidate(s: State, @unused v: Verifier): State = s
-  def consolidateIfRetrying(s: State, @unused v: Verifier): State = s
+  def consolidateOptionally(s: State, @unused v: Verifier): State = s
 
   def merge(fr: FunctionRecorder, h: Heap, newH: Heap, v: Verifier): (FunctionRecorder, Heap) =
     (fr, Heap(h.values ++ newH.values))
@@ -117,7 +117,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol
     s2
   }
 
-  def consolidateIfRetrying(s: State, v: Verifier): State =
+  def consolidateOptionally(s: State, v: Verifier): State =
     if (s.retrying) consolidate(s, v)
     else s
 
@@ -298,7 +298,35 @@ class RetryingStateConsolidator(config: Config) extends DefaultStateConsolidator
     else s
   }
 
-  override def consolidateIfRetrying(s: State, v: Verifier): State = consolidate(s, v)
+  override def consolidateOptionally(s: State, v: Verifier): State = consolidate(s, v)
+}
+
+/** A variant of [[RetryingStateConsolidator]] that differs only in that optional state consolidations (i.e.,
+  * ones not triggered by a verification failure) are not performed at all.
+  */
+class RetryingFailOnlyStateConsolidator(config: Config) extends RetryingStateConsolidator(config) {
+  override def consolidateOptionally(s: State, v: Verifier): State = s
+}
+
+/** A variant of [[DefaultStateConsolidator]]:
+  *   - Merging heaps and assuming QP permission bounds is equally complete
+  *   - State consolidation is equally complete, but only performed when Silicon is retrying
+  *     an assertion/operation for the last time.
+  */
+class LastRetryStateConsolidator(config: Config) extends DefaultStateConsolidator(config) {
+  override def consolidate(s: State, v: Verifier): State = {
+    if (s.isLastRetry) super.consolidate(s, v)
+    else s
+  }
+
+  override def consolidateOptionally(s: State, v: Verifier): State = consolidate(s, v)
+}
+
+/** A variant of [[LastRetryStateConsolidator]] that differs only in that optional state consolidations (i.e.,
+  * ones not triggered by a verification failure) are not performed at all.
+  */
+class LastRetryFailOnlyStateConsolidator(config: Config) extends LastRetryStateConsolidator(config) {
+  override def consolidateOptionally(s: State, v: Verifier): State = s
 }
 
 /** A variant of [[RetryingStateConsolidator]] and [[MinimalStateConsolidator]]:

src/main/scala/verifier/BaseVerifier.scala

@@ -17,7 +17,7 @@ import viper.silicon.state._
 import viper.silicon.state.terms.{AxiomRewriter, TriggerGenerator}
 import viper.silicon.supporters._
 import viper.silicon.reporting.DefaultStateFormatter
-import viper.silicon.rules.{DefaultStateConsolidator, MinimalRetryingStateConsolidator, MinimalStateConsolidator, MoreComplexExhaleStateConsolidator, RetryingStateConsolidator, StateConsolidationRules}
+import viper.silicon.rules.{DefaultStateConsolidator, LastRetryFailOnlyStateConsolidator, LastRetryStateConsolidator, MinimalRetryingStateConsolidator, MinimalStateConsolidator, MoreComplexExhaleStateConsolidator, RetryingFailOnlyStateConsolidator, RetryingStateConsolidator, StateConsolidationRules}
 import viper.silicon.utils.Counter
 
 import scala.collection.mutable
@@ -66,6 +66,9 @@ abstract class BaseVerifier(val config: Config,
       case Retrying => new RetryingStateConsolidator(config)
       case MinimalRetrying => new MinimalRetryingStateConsolidator(config)
       case MoreCompleteExhale => new MoreComplexExhaleStateConsolidator(config)
+      case LastRetry => new LastRetryStateConsolidator(config)
+      case RetryingFailOnly => new RetryingFailOnlyStateConsolidator(config)
+      case LastRetryFailOnly => new LastRetryFailOnlyStateConsolidator(config)
     }
   }