Sound MoreCompleteExhale on demand

src/main/scala/Config.scala

@@ -82,6 +82,18 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     val argType: ArgType.V = org.rogach.scallop.ArgType.LIST
   }
 
+  private val exhaleModeConverter: ValueConverter[ExhaleMode] = new ValueConverter[ExhaleMode] {
+    def parse(s: List[(String, List[String])]): Either[String, Option[ExhaleMode]] = s match {
+      case (_, "0" :: Nil) :: Nil => Right(Some(ExhaleMode.Greedy))
+      case (_, "1" :: Nil) :: Nil => Right(Some(ExhaleMode.MoreComplete))
+      case (_, "2" :: Nil) :: Nil => Right(Some(ExhaleMode.MoreCompleteOnDemand))
+      case Nil => Right(None)
+      case _ => Left(s"unexpected arguments")
+    }
+
+    val argType: ArgType.V = org.rogach.scallop.ArgType.LIST
+  }
+
   private val saturationTimeoutWeightsConverter: ValueConverter[ProverSaturationTimeoutWeights] = new ValueConverter[ProverSaturationTimeoutWeights] {
     def parse(s: List[(String, List[String])]): Either[String, Option[ProverSaturationTimeoutWeights]] = s match {
       case Seq((_, Seq(rawString))) =>
@@ -623,12 +635,30 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     case _ => opt
   }
 
-  val enableMoreCompleteExhale: ScallopOption[Boolean] = opt[Boolean]("enableMoreCompleteExhale",
-    descr = "Enable a more complete exhale version.",
+  // DEPRECATED and replaced by exhaleMode.
+  val moreCompleteExhale: ScallopOption[Boolean] = opt[Boolean]("enableMoreCompleteExhale",
+    descr =  "Warning: This option is deprecated. "
+           + "Please use 'exhaleMode' instead. "
+           + "Enables a more complete exhale version.",
     default = Some(false),
     noshort = true
   )
 
+  val exhaleModeOption: ScallopOption[ExhaleMode] = opt[ExhaleMode]("exhaleMode",
+    descr = "Exhale mode. Options are 0 (greedy, default), 1 (more complete exhale), 2 (more complete exhale on demand).",
+    default = None,
+    noshort = true
+  )(exhaleModeConverter)
+
+  lazy val exhaleMode: ExhaleMode = {
+    if (exhaleModeOption.isDefined)
+      exhaleModeOption()
+    else if (moreCompleteExhale())
+      ExhaleMode.MoreComplete
+    else
+      ExhaleMode.Greedy
+  }
+
   val numberOfErrorsToReport: ScallopOption[Int] = opt[Int]("numberOfErrorsToReport",
     descr = "Number of errors per member before the verifier stops. If this number is set to 0, all errors are reported.",
     default = Some(1),
@@ -763,18 +793,23 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
       sys.error(s"Unexpected combination: $other")
   }
 
+  validateOpt(counterexample, moreCompleteExhale, exhaleModeOption) {
+    case (Some(_), Some(false), None) |
+         (Some(_), Some(_), Some(ExhaleMode.Greedy)) |
+         (Some(_), Some(_), Some(ExhaleMode.MoreCompleteOnDemand)) =>
+      Left(s"Option ${counterexample.name} requires setting "
+        + s"${exhaleModeOption.name} to 1 (more complete exhale)")
+    case (_, Some(true), Some(m)) if m != ExhaleMode.MoreComplete =>
+      Left(s"Contradictory values given for options ${moreCompleteExhale.name} and ${exhaleModeOption.name}")
+    case _ => Right(())
+  }
+
   validateOpt(assertionMode, parallelizeBranches) {
     case (Some(AssertionMode.SoftConstraints), Some(true)) =>
       Left(s"Assertion mode SoftConstraints is not supported in combination with ${parallelizeBranches.name}")
     case _ => Right()
   }
 
-  validateOpt(counterexample, enableMoreCompleteExhale) {
-    case (Some(_), Some(false)) => Left(  s"Option ${counterexample.name} requires setting "
-                                        + s"flag ${enableMoreCompleteExhale.name}")
-    case _ => Right(())
-  }
-
   validateFileOpt(logConfig)
   validateFileOpt(setAxiomatizationFile)
   validateFileOpt(multisetAxiomatizationFile)
@@ -810,6 +845,13 @@ object Config {
     case object SoftConstraints extends AssertionMode
   }
 
+  sealed trait ExhaleMode
+  object ExhaleMode {
+    case object Greedy extends ExhaleMode
+    case object MoreComplete extends ExhaleMode
+    case object MoreCompleteOnDemand extends ExhaleMode
+  }
+
   case class ProverStateSaturationTimeout(timeout: Int, comment: String)
 
   object StateConsolidationMode extends Enumeration {

src/main/scala/rules/ChunkSupporter.scala

@@ -109,7 +109,7 @@ object chunkSupporter extends ChunkSupportRules {
     } else {
       executionFlowController.tryOrFail2[Heap, Option[Term]](s.copy(h = h), v)((s1, v1, QS) =>
         // 2022-05-07 MHS: MoreCompleteExhale isn't yet integrated into function verification, hence the limitation to method verification
-        if (s.isMethodVerification && Verifier.config.enableMoreCompleteExhale()) {
+        if (s.isMethodVerification && s1.moreCompleteExhale) {
           moreCompleteExhaleSupporter.consumeComplete(s1, s1.h, resource, args, perms, ve, v1)((s2, h2, snap2, v2) => {
             QS(s2.copy(h = s.h), h2, snap2, v2)
           })
@@ -206,7 +206,7 @@ object chunkSupporter extends ChunkSupportRules {
 
     executionFlowController.tryOrFail2[Heap, Term](s.copy(h = h), v)((s1, v1, QS) => {
       val lookupFunction =
-        if (s.isMethodVerification && Verifier.config.enableMoreCompleteExhale()) moreCompleteExhaleSupporter.lookupComplete _
+        if (s.isMethodVerification && s1.moreCompleteExhale) moreCompleteExhaleSupporter.lookupComplete _
         else lookupGreedy _
       lookupFunction(s1, s1.h, resource, args, ve, v1)((s2, tSnap, v2) =>
         QS(s2.copy(h = s.h), s2.h, tSnap, v2))

src/main/scala/rules/Evaluator.scala

@@ -675,8 +675,7 @@ object evaluator extends EvaluationRules {
 
       case fapp @ ast.FuncApp(funcName, eArgs) =>
         val func = s.program.findFunction(funcName)
-        val s0 = s.copy(hackIssue387DisablePermissionConsumption = Verifier.config.enableMoreCompleteExhale())
-        evals2(s0, eArgs, Nil, _ => pve, v)((s1, tArgs, v1) => {
+        evals2(s, eArgs, Nil, _ => pve, v)((s1, tArgs, v1) => {
 //          bookkeeper.functionApplications += 1
           val joinFunctionArgs = tArgs //++ c2a.quantifiedVariables.filterNot(tArgs.contains)
           /* TODO: Does it matter that the above filterNot does not filter out quantified

src/main/scala/rules/ExecutionFlowController.scala

@@ -6,6 +6,7 @@
 
 package viper.silicon.rules
 
+import viper.silicon.Config.ExhaleMode
 import viper.silicon.interfaces._
 import viper.silicon.logger.records.data.CommentRecord
 import viper.silicon.state.State
@@ -128,9 +129,10 @@ object executionFlowController extends ExecutionFlowRules {
 
         val comLog = new CommentRecord("Retry", s0, v.decider.pcs)
         val sepIdentifier = v.symbExLog.openScope(comLog)
-        action(s0.copy(retrying = true, retryLevel = s.retryLevel), v, (s1, r, v1) => {
+        val temporaryMCE = Verifier.config.exhaleMode != ExhaleMode.Greedy
+        action(s0.copy(retrying = true, retryLevel = s.retryLevel, moreCompleteExhale = temporaryMCE), v, (s1, r, v1) => {
           v1.symbExLog.closeScope(sepIdentifier)
-          Q(s1.copy(retrying = false), r, v1)
+          Q(s1.copy(retrying = false, moreCompleteExhale = s0.moreCompleteExhale), r, v1)
         })
       }
 

src/main/scala/rules/MoreCompleteExhaleSupporter.scala

@@ -170,7 +170,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
                      (Q: (State, Heap, Option[Term], Verifier) => VerificationResult)
                      : VerificationResult = {
 
-    if (s.functionRecorder == NoopFunctionRecorder && !s.hackIssue387DisablePermissionConsumption)
+    if (!s.hackIssue387DisablePermissionConsumption)
       actualConsumeComplete(s, h, resource, args, perms, ve, v)(Q)
     else
       summariseHeapAndAssertReadAccess(s, h, resource, args, ve, v)(Q)
@@ -224,7 +224,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
       }
     } else {
       if (!terms.utils.consumeExactRead(perms, s.constrainableARPs)) {
-        actualConsumeCompleteConstrainable(s, relevantChunks, args, perms, ve, v)((s1, updatedChunks, optSnap, v2) => {
+        actualConsumeCompleteConstrainable(s, relevantChunks, resource, args, perms, ve, v)((s1, updatedChunks, optSnap, v2) => {
           Q(s1, Heap(updatedChunks ++ otherChunks), optSnap, v2)})
       } else {
         var pNeeded = perms
@@ -281,35 +281,39 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
 
         val s0 = s.copy(functionRecorder = currentFunctionRecorder)
 
-        summarise(s0, relevantChunks.toSeq, resource, args, v)((s1, snap, _, _, v1) =>
+        summarise(s0, relevantChunks.toSeq, resource, args, v)((s1, snap, _, _, v1) => {
+          val condSnap = if (v1.decider.check(Greater(perms, NoPerm()), Verifier.config.checkTimeout())) {
+            snap
+          } else {
+            Ite(Greater(perms, NoPerm()), snap.convert(sorts.Snap), Unit)
+          }
           if (!moreNeeded) {
-            Q(s1, newHeap, Some(snap), v1)
+            Q(s1, newHeap, Some(condSnap), v1)
           } else {
             v1.decider.assert(pNeeded === NoPerm()) {
               case true =>
-                Q(s1, newHeap, Some(snap), v1)
+                Q(s1, newHeap, Some(condSnap), v1)
               case false =>
                 createFailure(ve, v1, s1)
             }
-          })
+          }})
       }
     }
   }
 
   private def actualConsumeCompleteConstrainable(s: State,
                                                  relevantChunks: ListBuffer[NonQuantifiedChunk],
+                                                 resource: ast.Resource,
                                                  args: Seq[Term],
                                                  perms: Term, // Expected to be constrainable. Will be assumed to equal the consumed permission amount.
                                                  ve: VerificationError,
                                                  v: Verifier)
                                                 (Q: (State, ListBuffer[NonQuantifiedChunk], Option[Term], Verifier) => VerificationResult)
                                                 : VerificationResult = {
 
-    assert(s.functionRecorder == NoopFunctionRecorder)
-
     var totalPermSum: Term = NoPerm()
     var totalPermTaken: Term = NoPerm()
-    val snap: Term = v.decider.fresh(sorts.Snap)
+    var newFr = s.functionRecorder
 
     val updatedChunks =
       relevantChunks map (ch => {
@@ -319,12 +323,13 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
         totalPermSum = PermPlus(totalPermSum, Ite(eq, ch.perm, NoPerm()))
         totalPermTaken = PermPlus(totalPermTaken, permTaken)
 
-        v.decider.assume(Seq(
-          IsValidPermVar(permTaken),
+        val constraint = And(IsValidPermVar(permTaken),
           PermAtMost(permTaken, ch.perm),
-          Implies(Not(eq), permTaken === NoPerm()),
-          Implies(permTaken !== NoPerm(), snap === ch.snap.convert(sorts.Snap))
-        ))
+          Implies(Not(eq), permTaken === NoPerm())
+        )
+
+        v.decider.assume(constraint)
+        newFr = newFr.recordArp(permTaken, constraint)
 
         ch.withPerm(PermMinus(ch.perm, permTaken))
       })
@@ -339,7 +344,8 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
     v.decider.assert(totalPermTaken !== NoPerm()) {
       case true =>
         v.decider.assume(perms === totalPermTaken)
-        Q(s, updatedChunks, Some(snap), v)
+        summarise(s, relevantChunks.toSeq, resource, args, v)((s2, snap, _, _, v1) =>
+          Q(s2, updatedChunks, Some(snap), v1))
       case false =>
         createFailure(ve, v, s)
     }

src/main/scala/state/State.scala

@@ -67,7 +67,8 @@ final case class State(g: Store = Store(),
                        isMethodVerification: Boolean = false,
                        retryLevel: Int = 0,
                        /* ast.Field, ast.Predicate, or MagicWandIdentifier */
-                       heapDependentTriggers: InsertionOrderedSet[Any] = InsertionOrderedSet.empty)
+                       heapDependentTriggers: InsertionOrderedSet[Any] = InsertionOrderedSet.empty,
+                       moreCompleteExhale: Boolean = false)
     extends Mergeable[State] {
 
   def incCycleCounter(m: ast.Predicate) =
@@ -147,7 +148,8 @@ object State {
                  reserveHeaps1, reserveCfgs1, conservedPcs1, recordPcs1, exhaleExt1,
                  ssCache1, hackIssue387DisablePermissionConsumption1,
                  qpFields1, qpPredicates1, qpMagicWands1, smCache1, pmCache1, smDomainNeeded1,
-                 predicateSnapMap1, predicateFormalVarMap1, hack, retryLevel, useHeapTriggers) =>
+                 predicateSnapMap1, predicateFormalVarMap1, hack, retryLevel, useHeapTriggers,
+                 moreCompleteExhale) =>
 
         /* Decompose state s2: most values must match those of s1 */
         s2 match {
@@ -171,7 +173,8 @@ object State {
                      `reserveHeaps1`, `reserveCfgs1`, `conservedPcs1`, `recordPcs1`, `exhaleExt1`,
                      ssCache2, `hackIssue387DisablePermissionConsumption1`,
                      `qpFields1`, `qpPredicates1`, `qpMagicWands1`, smCache2, pmCache2, `smDomainNeeded1`,
-                     `predicateSnapMap1`, `predicateFormalVarMap1`, `hack`, `retryLevel`, `useHeapTriggers`) =>
+                     `predicateSnapMap1`, `predicateFormalVarMap1`, `hack`, `retryLevel`, `useHeapTriggers`,
+                     moreCompleteExhale2) =>
 
             val functionRecorder3 = functionRecorder1.merge(functionRecorder2)
             val triggerExp3 = triggerExp1 && triggerExp2
@@ -182,14 +185,16 @@ object State {
             val pmCache3 = pmCache1 ++ pmCache2
 
             val ssCache3 = ssCache1 ++ ssCache2
+            val moreCompleteExhale3 = moreCompleteExhale || moreCompleteExhale2
 
             s1.copy(functionRecorder = functionRecorder3,
                     possibleTriggers = possibleTriggers3,
                     triggerExp = triggerExp3,
                     constrainableARPs = constrainableARPs3,
                     ssCache = ssCache3,
                     smCache = smCache3,
-                    pmCache = pmCache3)
+                    pmCache = pmCache3,
+                    moreCompleteExhale = moreCompleteExhale3)
 
           case _ =>
             val err = new StringBuilder()

src/main/scala/verifier/DefaultMainVerifier.scala

@@ -6,6 +6,8 @@
 
 package viper.silicon.verifier
 
+import viper.silicon.Config.ExhaleMode
+
 import java.text.SimpleDateFormat
 import java.util.concurrent._
 import scala.annotation.unused
@@ -307,7 +309,8 @@ class DefaultMainVerifier(config: Config,
           predicateSnapMap = predSnapGenerator.snapMap,
           predicateFormalVarMap = predSnapGenerator.formalVarMap,
           isMethodVerification = member.isInstanceOf[ast.Member],
-          heapDependentTriggers = resourceTriggers)
+          heapDependentTriggers = resourceTriggers,
+          moreCompleteExhale = Verifier.config.exhaleMode == ExhaleMode.MoreComplete)
   }
 
   private def createInitialState(@unused cfg: SilverCfg,
@@ -326,7 +329,8 @@ class DefaultMainVerifier(config: Config,
       qpPredicates = quantifiedPredicates,
       qpMagicWands = quantifiedMagicWands,
       predicateSnapMap = predSnapGenerator.snapMap,
-      predicateFormalVarMap = predSnapGenerator.formalVarMap)
+      predicateFormalVarMap = predSnapGenerator.formalVarMap,
+      moreCompleteExhale = Verifier.config.exhaleMode == ExhaleMode.MoreComplete)
   }
 
   private def excludeMethod(method: ast.Method) = (

src/test/resources/moreCompleteExhale/0523.vpr

@@ -0,0 +1,37 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+function req(x: Ref): Bool
+  requires acc(x.f, 2/1)
+{ true }
+
+method test(x: Ref) {
+  inhale acc(x.f)
+  //:: ExpectedOutput(application.precondition:insufficient.permission)
+  assert req(x) // Fails only without --enableMoreCompleteExhale (and should fail)
+  assert false  // Fails even with --enableMoreCompleteExhale (and should fail)
+}
+
+
+
+/////// Example from issue 594
+
+field val$_Int: Int
+
+function getter_pkg_F(param_pkg_V0: Ref): Int
+  requires acc(SomePredicate_pkg_F(param_pkg_V0), write)
+{
+  (unfolding acc(SomePredicate_pkg_F(param_pkg_V0), write) in param_pkg_V0.val$_Int)
+}
+
+predicate SomePredicate_pkg_F(param_pkg_V0: Ref) {
+  true && acc(param_pkg_V0.val$_Int, write)
+}
+
+method client2_pkg_F(param_pkg_V0: Ref) returns (res_pkg_V0: Int)
+  requires acc(SomePredicate_pkg_F(param_pkg_V0), 1 / 2)
+  ensures acc(SomePredicate_pkg_F(param_pkg_V0), 1 / 2)
+  //:: ExpectedOutput(application.precondition:insufficient.permission)
+  ensures res_pkg_V0 == getter_pkg_F(param_pkg_V0)

src/test/scala/SiliconTestsMoreCompleteExhale.scala

@@ -11,5 +11,5 @@ class SiliconTestsMoreCompleteExhale extends SiliconTests {
 
  override val commandLineArguments: Seq[String] = Seq(
     "--timeout", "300" /* seconds */,
-    "--enableMoreCompleteExhale")
+    "--exhaleMode=1")
 }