Merge branch 'master' into meilers_discard_empty_triggers

src/main/scala/Config.scala

@@ -6,11 +6,12 @@
 
 package viper.silicon
 
-import java.nio.file.{Path, Paths}
+import java.nio.file.{Files, Path, Paths}
 import scala.collection.immutable.ArraySeq
 import scala.util.matching.Regex
 import scala.util.Properties._
 import org.rogach.scallop._
+import viper.silicon.Config.JoinMode.JoinMode
 import viper.silicon.Config.StateConsolidationMode.StateConsolidationMode
 import viper.silicon.decider.{Cvc5ProverStdIO, Z3ProverAPI, Z3ProverStdIO}
 import viper.silver.frontend.SilFrontendConfig
@@ -451,9 +452,15 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
   lazy val z3Exe: String = {
     val isWindows = System.getProperty("os.name").toLowerCase.startsWith("windows")
 
-    rawZ3Exe.toOption.getOrElse(
-      envOrNone(Z3ProverStdIO.exeEnvironmentalVariable)
-        .getOrElse("z3" + (if (isWindows) ".exe" else "")))
+    rawZ3Exe.toOption.getOrElse({
+      Option(System getenv Z3ProverStdIO.exeEnvironmentalVariable).getOrElse({
+        val filename = "z3" + (if (isWindows) ".exe" else "")
+        System.getenv("PATH").split(if (isWindows) ";" else ":").find(dirname => Files.exists(Paths.get(dirname, filename))) match {
+          case Some(dirname) => Paths.get(dirname, filename).toString
+          case None => filename
+        }
+      })
+    })
   }
 
   private val rawCvc5Exe = opt[String]("cvc5Exe",
@@ -662,11 +669,11 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
-  val moreJoins: ScallopOption[Boolean] = opt[Boolean]("moreJoins",
-    descr = "Enable more joins using a more complete implementation of state merging.",
-    default = Some(false),
+  val moreJoins: ScallopOption[JoinMode] = opt[JoinMode]("moreJoins",
+    descr = s"Decides when to join branches. Options are:\n${JoinMode.helpText}",
+    default = Some(JoinMode.Off),
     noshort = true
-  )
+  )(singleArgConverter(mode => JoinMode(mode.toInt)))
 
   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).",
@@ -895,18 +902,33 @@ object Config {
     case object MoreCompleteOnDemand extends ExhaleMode
   }
 
+  object JoinMode extends Enumeration {
+    type JoinMode = Value
+    val Off, Impure, All = Value
+
+    private[Config] final def helpText: String = {
+      s"""  ${Off.id} (off): No additional joins
+         |  ${Impure.id} (impure): Immediately join all branch on impure conditionals
+         |  ${All.id} (all): Join all branches when possible
+         |""".stripMargin
+    }
+  }
+
   case class ProverStateSaturationTimeout(timeout: Int, comment: String)
 
   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
-         |  ${MinimalRetrying.id}: Less eager and less complete than ${Default.id}
-         |  ${MoreCompleteExhale.id}: Intended for use with --moreCompleteExhale
+      s"""  ${Minimal.id} (minimal): Minimal work, many incompletenesses
+         |  ${Default.id} (default): Most work, fewest incompletenesses
+         |  ${Retrying.id} (retrying): Similar to ${Default.id}, but less eager (optional and failure-driven consolidation only on retry)
+         |  ${MinimalRetrying.id} (minimalRetrying): Less eager and less complete than ${Default.id}
+         |  ${MoreCompleteExhale.id} (moreCompleteExhale): Intended for use with --moreCompleteExhale / --exhaleMode=1
+         |  ${LastRetry.id} (lastRetry): Similar to ${Retrying.id}, but only on last retry
+         |  ${RetryingFailOnly.id} (retryingFailOnly): Similar to ${Retrying.id}, but performs no optional consolidation at all.
+         |  ${LastRetryFailOnly.id} (lastRetryFailOnly): Similar to ${LastRetry.id}, but performs no optional consolidation at all.
          |""".stripMargin
     }
 

src/main/scala/Silicon.scala

@@ -117,7 +117,9 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)]
     lifetimeState = LifetimeState.Configured
 
     _config = new Config(args)
-    _symbExLog = SymbExLogger.ofConfig(_config)
+    if (!config.exit) {
+      _symbExLog = SymbExLogger.ofConfig(_config)
+    }
   }
 
   def debugInfo(debugInfo: Seq[(String, Any)]): Unit = { this.debugInfo = debugInfo }
@@ -434,7 +436,6 @@ class SiliconRunnerInstance extends SiliconFrontend(StdIOReporter()) {
          *       the process to kill has no input/output data left in the
          *       corresponding streams.
          */
-      submitter.submit()
     }
 
     sys.exit(exitCode)

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(s1).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(s1).consolidateOptionally(s1, v1), v1)
           })
         } else {
           Unreachable()
@@ -244,7 +244,8 @@ object brancher extends BranchingRules {
       v.decider.prover.comment(s"Bulk-declaring functions")
       v.decider.declareAndRecordAsFreshFunctions(functionsOfElseBranchDecider, true)
       v.decider.prover.comment(s"Bulk-declaring macros")
-      v.decider.declareAndRecordAsFreshMacros(macrosOfElseBranchDecider, true)
+      // Declare macros without duplicates; we keep only the last occurrence of every declaration to avoid errors.
+      v.decider.declareAndRecordAsFreshMacros(macrosOfElseBranchDecider.reverse.distinct.reverse, true)
     }
     res
   }

src/main/scala/rules/ChunkSupporter.scala

@@ -190,7 +190,7 @@ object chunkSupporter extends ChunkSupportRules {
 
     // Try to merge the chunk into the heap by finding an alias.
     // In any case, property assumptions are added after the merge step.
-    val (fr1, h1) = v.stateConsolidator.merge(s.functionRecorder, h, ch, v)
+    val (fr1, h1) = v.stateConsolidator(s).merge(s.functionRecorder, h, ch, v)
     Q(s.copy(functionRecorder = fr1), h1, v)
   }
 

src/main/scala/rules/Consumer.scala

@@ -6,6 +6,8 @@
 
 package viper.silicon.rules
 
+import viper.silicon.Config.JoinMode
+
 import scala.collection.mutable
 import viper.silver.ast
 import viper.silver.ast.utility.QuantifiedPermissions.QuantifiedPermissionAssertion
@@ -183,7 +185,7 @@ object consumer extends ConsumptionRules {
       v.logger.debug("hR = " + s.reserveHeaps.map(v.stateFormatter.format).mkString("", ",\n     ", ""))
 
     val consumed = a match {
-      case imp @ ast.Implies(e0, a0) if !a.isPure && s.moreJoins =>
+      case imp @ ast.Implies(e0, a0) if !a.isPure && s.moreJoins.id >= JoinMode.Impure.id =>
         val impliesRecord = new ImpliesRecord(imp, s, v.decider.pcs, "consume")
         val uidImplies = v.symbExLog.openScope(impliesRecord)
         consumeConditionalTlcMoreJoins(s, h, e0, a0, None, uidImplies, pve, v)(Q)
@@ -203,7 +205,7 @@ object consumer extends ConsumptionRules {
               Q(s2, h, Unit, v2)
             }))
 
-      case ite @ ast.CondExp(e0, a1, a2) if !a.isPure && s.moreJoins =>
+      case ite @ ast.CondExp(e0, a1, a2) if !a.isPure && s.moreJoins.id >= JoinMode.Impure.id =>
         val condExpRecord = new CondExpRecord(ite, s, v.decider.pcs, "consume")
         val uidCondExp = v.symbExLog.openScope(condExpRecord)
         consumeConditionalTlcMoreJoins(s, h, e0, a1, Some(a2), uidCondExp, pve, v)(Q)
@@ -507,7 +509,7 @@ object consumer extends ConsumptionRules {
               // Asume that entry1.pcs is inverse of entry2.pcs
               Ite(And(entry1.pathConditions.branchConditions), entry1.data._2, entry2.data._2)
             )
-            (entry1.pathConditionAwareMerge(entry2, v1), mergedData)
+            (entry1.pathConditionAwareMergeWithoutConsolidation(entry2, v1), mergedData)
           case _ =>
             sys.error(s"Unexpected join data entries: $entries")
         }

src/main/scala/rules/Evaluator.scala

@@ -6,6 +6,7 @@
 
 package viper.silicon.rules
 
+import viper.silicon.Config.JoinMode
 import viper.silver.ast
 import viper.silver.verifier.{CounterexampleTransformer, PartialVerificationError, VerifierWarning}
 import viper.silver.verifier.errors.{ErrorWrapperWithExampleTransformer, PreconditionInAppFalse}
@@ -785,7 +786,7 @@ object evaluator extends EvaluationRules {
                                  * incomplete).
                                  */
                              smDomainNeeded = true,
-                             moreJoins = false)
+                             moreJoins = JoinMode.Off)
             consumes(s3, pres, _ => pvePre, v2)((s4, snap, v3) => {
               val snap1 = snap.convert(sorts.Snap)
               val preFApp = App(functionSupporter.preconditionVersion(v3.symbolConverter.toFunction(func)), snap1 :: tArgs)
@@ -861,7 +862,7 @@ object evaluator extends EvaluationRules {
                                          recordVisited = s3.recordVisited,
                                          permissionScalingFactor = s6.permissionScalingFactor)
                                    .decCycleCounter(predicate)
-                        val s10 = v5.stateConsolidator.consolidateIfRetrying(s9, v5)
+                        val s10 = v5.stateConsolidator(s9).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 +1150,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(s1).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/ExecutionFlowController.scala

@@ -126,7 +126,7 @@ object executionFlowController extends ExecutionFlowRules {
                                           * current branch turned out to be infeasible) */
         firstActionResult
       else {
-        val s0 = v.stateConsolidator.consolidate(s, v)
+        val s0 = v.stateConsolidator(s).consolidate(s, v)
 
         val comLog = new CommentRecord("Retry", s0, v.decider.pcs)
         val sepIdentifier = v.symbExLog.openScope(comLog)

src/main/scala/rules/Executor.scala

@@ -6,6 +6,8 @@
 
 package viper.silicon.rules
 
+import viper.silicon.Config.JoinMode
+
 import scala.annotation.unused
 import viper.silver.cfg.silver.SilverCfg
 import viper.silver.cfg.silver.SilverCfg.{SilverBlock, SilverEdge}
@@ -86,7 +88,7 @@ object executor extends ExecutionRules {
   def handleOutEdge(s: State, edge: SilverEdge, v: Verifier): State = {
     edge.kind match {
       case cfg.Kind.Out =>
-        val (fr1, h1) = v.stateConsolidator.merge(s.functionRecorder, s.h, s.invariantContexts.head, v)
+        val (fr1, h1) = v.stateConsolidator(s).merge(s.functionRecorder, s.h, s.invariantContexts.head, v)
         val s1 = s.copy(functionRecorder = fr1, h = h1,
           invariantContexts = s.invariantContexts.tail)
         s1
@@ -111,7 +113,7 @@ object executor extends ExecutionRules {
       case (Seq(), _) => Q(s, v)
       case (Seq(edge), _) => follow(s, edge, v, joinPoint)(Q)
       case (Seq(edge1, edge2), Some(newJoinPoint)) if
-          s.moreJoins &&
+          s.moreJoins.id >= JoinMode.All.id &&
           // Can't directly match type because of type erasure ...
           edge1.isInstanceOf[ConditionalEdge[ast.Stmt, ast.Exp]] &&
           edge2.isInstanceOf[ConditionalEdge[ast.Stmt, ast.Exp]] &&
@@ -387,6 +389,7 @@ object executor extends ExecutionRules {
               relevantChunks,
               Seq(`?r`),
               `?r` === tRcvr,
+              Some(Seq(tRcvr)),
               field,
               FullPerm,
               chunkOrderHeuristics,
@@ -517,15 +520,16 @@ object executor extends ExecutionRules {
       // Calling hack510() triggers a state consolidation.
       // See also Silicon issue #510.
       case ast.MethodCall(`hack510_method_name`, _, _) =>
-        val s1 = v.stateConsolidator.consolidate(s, v)
+        val s1 = v.stateConsolidator(s).consolidate(s, v)
         Q(s1, v)
 
       case call @ ast.MethodCall(methodName, eArgs, lhs) =>
         val meth = s.program.findMethod(methodName)
         val fargs = meth.formalArgs.map(_.localVar)
         val formalsToActuals: Map[ast.LocalVar, ast.Exp] = fargs.zip(eArgs).to(Map)
         val reasonTransformer = (n: viper.silver.verifier.errors.ErrorNode) => n.replace(formalsToActuals)
-        val pveCall = CallFailed(call).withReasonNodeTransformed(reasonTransformer)
+        val pveCall = CallFailed(call)
+        val pveCallTransformed = pveCall.withReasonNodeTransformed(reasonTransformer)
 
         val mcLog = new MethodCallRecord(call, s, v.decider.pcs)
         val sepIdentifier = v.symbExLog.openScope(mcLog)
@@ -549,7 +553,7 @@ object executor extends ExecutionRules {
             val outs = meth.formalReturns.map(_.localVar)
             val gOuts = Store(outs.map(x => (x, v2.decider.fresh(x))).toMap)
             val s4 = s3.copy(g = s3.g + gOuts, oldHeaps = s3.oldHeaps + (Verifier.PRE_STATE_LABEL -> magicWandSupporter.getEvalHeap(s1)))
-            produces(s4, freshSnap, meth.posts, _ => pveCall, v2)((s5, v3) => {
+            produces(s4, freshSnap, meth.posts, _ => pveCallTransformed, v2)((s5, v3) => {
               v3.symbExLog.closeScope(postCondId)
               v3.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract)
               val gLhs = Store(lhs.zip(outs)

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/Joiner.scala

@@ -19,7 +19,11 @@ case class JoinDataEntry[D](s: State, data: D, pathConditions: RecordedPathCondi
   // and the join data entries themselves provide information about the path conditions to State.merge.
   def pathConditionAwareMerge(other: JoinDataEntry[D], v: Verifier): State = {
     val res = State.merge(this.s, this.pathConditions, other.s, other.pathConditions)
-    v.stateConsolidator.consolidate(res, v)
+    v.stateConsolidator(s).consolidate(res, v)
+  }
+
+  def pathConditionAwareMergeWithoutConsolidation(other: JoinDataEntry[D], v: Verifier): State = {
+    State.merge(this.s, this.pathConditions, other.s, other.pathConditions)
   }
 }
 

src/main/scala/rules/MagicWandSupporter.scala

@@ -391,7 +391,7 @@ object magicWandSupporter extends SymbolicExecutionRules {
             val s3 = s2.copy(oldHeaps = s1.oldHeaps + (Verifier.MAGIC_WAND_LHS_STATE_LABEL -> magicWandSupporter.getEvalHeap(s1)))
             produce(s3.copy(conservingSnapshotGeneration = true), toSf(wandSnap.rhsSnapshot), wand.right, pve, v2)((s4, v3) => {
               val s5 = s4.copy(g = s1.g, conservingSnapshotGeneration = s3.conservingSnapshotGeneration)
-              val s6 = v3.stateConsolidator.consolidate(s5, v3).copy(oldHeaps = s1.oldHeaps)
+              val s6 = v3.stateConsolidator(s5).consolidate(s5, v3).copy(oldHeaps = s1.oldHeaps)
               Q(s6, v3)})})})}
 
   def transfer[CH <: Chunk]
@@ -422,7 +422,7 @@ object magicWandSupporter extends SymbolicExecutionRules {
       val s3 = s2.copy(conservedPcs = conservedPcs +: s2.conservedPcs.tail, reserveHeaps = s.reserveHeaps.head +: hs2)
 
       val usedChunks = chs2.flatten
-      val (fr4, hUsed) = v2.stateConsolidator.merge(s3.functionRecorder, s2.reserveHeaps.head, Heap(usedChunks), v2)
+      val (fr4, hUsed) = v2.stateConsolidator(s2).merge(s3.functionRecorder, s2.reserveHeaps.head, Heap(usedChunks), v2)
 
       val s4 = s3.copy(functionRecorder = fr4, reserveHeaps = hUsed +: s3.reserveHeaps.tail)
 
@@ -467,7 +467,7 @@ object magicWandSupporter extends SymbolicExecutionRules {
        * is consumed from hOps and permissions for the predicate are added to the state's
        * heap. After a statement is executed those permissions are transferred to hOps.
        */
-      val (fr, hOpsJoinUsed) = v.stateConsolidator.merge(newState.functionRecorder, newState.reserveHeaps(1), newState.h, v)
+      val (fr, hOpsJoinUsed) = v.stateConsolidator(newState).merge(newState.functionRecorder, newState.reserveHeaps(1), newState.h, v)
       newState.copy(functionRecorder = fr, h = Heap(),
           reserveHeaps = Heap() +: hOpsJoinUsed +: newState.reserveHeaps.drop(2))
     } else newState