diff --git a/silver b/silver index ae4a12399..65ec3412b 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit ae4a12399cd0b42bedabf01be2cda93700244bd6 +Subproject commit 65ec3412bb9118a8c465462c94dab6d0d53da5f4 diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala index bdbc99db9..1d86690ea 100644 --- a/src/main/scala/Config.scala +++ b/src/main/scala/Config.scala @@ -431,6 +431,10 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") { noshort = true ) + lazy val outputProverLog: Boolean = { + enableTempDirectory.isSupplied || rawProverLogFile.isSupplied || rawZ3LogFile.isSupplied + } + private val rawZ3Exe = opt[String]("z3Exe", descr = (s"Z3 executable. The environment variable ${Z3ProverStdIO.exeEnvironmentalVariable}" + " can also be used to specify the path of the executable."), @@ -810,8 +814,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") { validateOpt(counterexample, moreCompleteExhale, exhaleModeOption) { case (Some(_), Some(false), None) | - (Some(_), Some(_), Some(ExhaleMode.Greedy)) | - (Some(_), Some(_), Some(ExhaleMode.MoreCompleteOnDemand)) => + (Some(_), Some(_), Some(ExhaleMode.Greedy)) => Left(s"Option ${counterexample.name} requires setting " + s"${exhaleModeOption.name} to 1 (more complete exhale)") case (_, Some(true), Some(m)) if m != ExhaleMode.MoreComplete => @@ -819,12 +822,6 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") { 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() - } - validateFileOpt(logConfig) validateFileOpt(setAxiomatizationFile) validateFileOpt(multisetAxiomatizationFile) diff --git a/src/main/scala/Silicon.scala b/src/main/scala/Silicon.scala index ebab80e34..a9b1001cf 100644 --- a/src/main/scala/Silicon.scala +++ b/src/main/scala/Silicon.scala @@ -14,7 +14,7 @@ import ch.qos.logback.classic.{Level, Logger} import com.typesafe.scalalogging.LazyLogging import org.slf4j.LoggerFactory import viper.silver.ast -import viper.silver.frontend.{DefaultStates, SilFrontend} +import viper.silver.frontend.{DefaultStates, MinimalViperFrontendAPI, SilFrontend, ViperFrontendAPI} import viper.silver.reporter._ import viper.silver.verifier.{AbstractVerificationError => SilAbstractVerificationError, Failure => SilFailure, Success => SilSuccess, TimeoutOccurred => SilTimeoutOccurred, VerificationResult => SilVerificationResult, Verifier => SilVerifier} import viper.silicon.interfaces.Failure @@ -377,6 +377,23 @@ class SiliconFrontend(override val reporter: Reporter, } } +/** + * Silicon "frontend" for use by actual Viper frontends. + * Performs consistency check and verification. + * See [[viper.silver.frontend.ViperFrontendAPI]] for usage information. + */ +class SiliconFrontendAPI(override val reporter: Reporter) + extends SiliconFrontend(reporter) with ViperFrontendAPI + +/** + * Silicon "frontend" for use by actual Viper frontends. + * Performs only verification (no consistency check). + * See [[viper.silver.frontend.ViperFrontendAPI]] for usage information. + */ +class MinimalSiliconFrontendAPI(override val reporter: Reporter) + extends SiliconFrontend(reporter) with MinimalViperFrontendAPI + + object SiliconRunner extends SiliconRunnerInstance { def main(args: Array[String]): Unit = { runMain(args) diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala index 29e284443..145fcceb0 100644 --- a/src/main/scala/decider/Decider.scala +++ b/src/main/scala/decider/Decider.scala @@ -382,7 +382,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => def statistics(): Map[String, String] = prover.statistics() - override def generateModel(): Unit = proverAssert(False, None) + override def generateModel(): Unit = proverAssert(False, Verifier.config.assertTimeout.toOption) override def getModel(): Model = prover.getModel() diff --git a/src/main/scala/decider/ProverStdIO.scala b/src/main/scala/decider/ProverStdIO.scala index 8cd2419ea..4bc4507a4 100644 --- a/src/main/scala/decider/ProverStdIO.scala +++ b/src/main/scala/decider/ProverStdIO.scala @@ -83,7 +83,7 @@ abstract class ProverStdIO(uniqueId: String, } pushPopScopeDepth = 0 lastTimeout = -1 - logfileWriter = if (!Verifier.config.enableTempDirectory()) null else viper.silver.utility.Common.PrintWriter(Verifier.config.proverLogFile(uniqueId).toFile) + logfileWriter = if (!Verifier.config.outputProverLog) null else viper.silver.utility.Common.PrintWriter(Verifier.config.proverLogFile(uniqueId).toFile) proverPath = getProverPath prover = createProverInstance() input = new BufferedReader(new InputStreamReader(prover.getInputStream)) diff --git a/src/main/scala/decider/Z3ProverAPI.scala b/src/main/scala/decider/Z3ProverAPI.scala index ed98ee7ba..d5b9dfe77 100644 --- a/src/main/scala/decider/Z3ProverAPI.scala +++ b/src/main/scala/decider/Z3ProverAPI.scala @@ -9,19 +9,17 @@ package viper.silicon.decider import com.typesafe.scalalogging.LazyLogging import viper.silicon.common.config.Version import viper.silicon.interfaces.decider.{Prover, Result, Sat, Unknown, Unsat} -import viper.silicon.state.{IdentifierFactory, State} -import viper.silicon.state.terms.{App, Decl, Fun, FunctionDecl, Implies, Ite, MacroDecl, Quantification, Sort, SortDecl, SortWrapperDecl, Term, Trigger, TriggerGenerator, sorts} +import viper.silicon.state.IdentifierFactory +import viper.silicon.state.terms.{App, Decl, Fun, FunctionDecl, Implies, MacroDecl, Not, Quantification, Sort, SortDecl, SortWrapperDecl, Term, TriggerGenerator, sorts} import viper.silicon.{Config, Map} import viper.silicon.verifier.Verifier import viper.silver.reporter.{InternalWarningMessage, Reporter} import viper.silver.verifier.{MapEntry, ModelEntry, ModelParser, ValueEntry, DefaultDependency => SilDefaultDependency, Model => ViperModel} -import java.io.PrintWriter import java.nio.file.Path import scala.collection.mutable import com.microsoft.z3._ import com.microsoft.z3.enumerations.Z3_param_kind -import viper.silicon.decider.Z3ProverAPI.oldVersionOnlyParams import viper.silicon.reporting.ExternalToolError import scala.jdk.CollectionConverters.MapHasAsJava @@ -64,7 +62,6 @@ object Z3ProverAPI { "smt.qi.eager_threshold" -> 100.0, ) val allParams = boolParams ++ intParams ++ stringParams ++ doubleParams - val oldVersionOnlyParams = Set("smt.arith.solver") } @@ -122,26 +119,21 @@ class Z3ProverAPI(uniqueId: String, s } - val useOldVersionParams = version() <= Version("4.8.7.0") Z3ProverAPI.boolParams.foreach{ case (k, v) => - if (useOldVersionParams || !oldVersionOnlyParams.contains(k)) - params.add(removeSmtPrefix(k), v) + params.add(removeSmtPrefix(k), v) } Z3ProverAPI.intParams.foreach{ case (k, v) => - if (useOldVersionParams || !oldVersionOnlyParams.contains(k)) - params.add(removeSmtPrefix(k), v) + params.add(removeSmtPrefix(k), v) } Z3ProverAPI.doubleParams.foreach{ case (k, v) => - if (useOldVersionParams || !oldVersionOnlyParams.contains(k)) - params.add(removeSmtPrefix(k), v) + params.add(removeSmtPrefix(k), v) } Z3ProverAPI.stringParams.foreach{ case (k, v) => - if (useOldVersionParams || !oldVersionOnlyParams.contains(k)) - params.add(removeSmtPrefix(k), v) + params.add(removeSmtPrefix(k), v) } val userProvidedArgs = Verifier.config.proverConfigArgs prover = ctx.mkSolver() @@ -256,19 +248,24 @@ class Z3ProverAPI(uniqueId: String, // When used via API, Z3 completely discards assumptions that contain invalid triggers (whereas it just ignores // the invalid trigger when used via stdio). Thus, to make sure our assumption is not discarded, we manually // walk through all quantifiers and remove invalid terms inside the trigger. - triggerGenerator.setCustomIsForbiddenInTrigger(triggerGenerator.advancedIsForbiddenInTrigger) - val cleanTerm = term.transform{ - case q@Quantification(_, _, _, triggers, _, _, _) if triggers.nonEmpty => - val goodTriggers = triggers.filterNot(trig => trig.p.exists(ptrn => ptrn.shallowCollect{ - case t => triggerGenerator.isForbiddenInTrigger(t) - }.nonEmpty)) - q.copy(triggers = goodTriggers) - }() + val cleanTerm = cleanTriggers(term) prover.add(termConverter.convert(cleanTerm).asInstanceOf[BoolExpr]) reporter.report(InternalWarningMessage("Z3 error: " + e.getMessage)) } } + def cleanTriggers(term: Term): Term = { + triggerGenerator.setCustomIsForbiddenInTrigger(triggerGenerator.advancedIsForbiddenInTrigger) + val cleanTerm = term.transform { + case q@Quantification(_, _, _, triggers, _, _, _) if triggers.nonEmpty => + val goodTriggers = triggers.filterNot(trig => trig.p.exists(ptrn => ptrn.shallowCollect { + case t => triggerGenerator.isForbiddenInTrigger(t) + }.nonEmpty)) + q.copy(triggers = goodTriggers) + }() + cleanTerm + } + def assert(goal: Term, timeout: Option[Int]): Boolean = { endPreamblePhase() @@ -279,7 +276,14 @@ class Z3ProverAPI(uniqueId: String, } result } catch { - case e: Z3Exception => throw ExternalToolError("Prover", "Z3 error: " + e.getMessage) + case e: Z3Exception => { + val cleanGoal = cleanTriggers(goal) + if (cleanGoal == goal) { + throw ExternalToolError("Prover", "Z3 error: " + e.getMessage) + } else { + assert(cleanGoal, timeout) + } + } } } @@ -320,8 +324,13 @@ class Z3ProverAPI(uniqueId: String, protected def retrieveAndSaveModel(): Unit = { if (Verifier.config.counterexample.toOption.isDefined) { - val model = prover.getModel - lastModel = model + try { + val model = prover.getModel + lastModel = model + } catch { + case _: Z3Exception => + lastModel = null + } } } @@ -337,7 +346,7 @@ class Z3ProverAPI(uniqueId: String, val guard = fresh("grd", Nil, sorts.Bool) val guardApp = App(guard, Nil) - val goalImplication = Implies(guardApp, goal) + val goalImplication = Implies(guardApp, Not(goal)) prover.add(termConverter.convertTerm(goalImplication).asInstanceOf[BoolExpr]) @@ -451,7 +460,11 @@ class Z3ProverAPI(uniqueId: String, for (constDecl <- lastModel.getConstDecls){ val constInterp = lastModel.getConstInterp(constDecl) val constName = constDecl.getName.toString - val entry = fastparse.parse(constInterp.toString, ModelParser.value(_)).get.value + val constInterpString = constInterp match { + case rn: RatNum => s"(/ ${rn.getBigIntNumerator} ${rn.getBigIntDenominator})" + case _ => constInterp.toString + } + val entry = fastparse.parse(constInterpString, ModelParser.value(_)).get.value entries.update(constName, entry) } for (funcDecl <- lastModel.getFuncDecls) { diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index fe8dfe0b5..d8688acc8 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -7,7 +7,7 @@ package viper.silicon.rules import viper.silver.ast -import viper.silver.verifier.{CounterexampleTransformer, PartialVerificationError, TypecheckerWarning} +import viper.silver.verifier.{CounterexampleTransformer, PartialVerificationError, VerifierWarning} import viper.silver.verifier.errors.{ErrorWrapperWithExampleTransformer, PreconditionInAppFalse} import viper.silver.verifier.reasons._ import viper.silicon.common.collections.immutable.InsertionOrderedSet @@ -23,8 +23,8 @@ import viper.silicon.verifier.Verifier import viper.silicon.{Map, TriggerSets} import viper.silicon.interfaces.state.{ChunkIdentifer, NonQuantifiedChunk} import viper.silicon.logger.records.data.{CondExpRecord, EvaluateRecord, ImpliesRecord} -import viper.silver.reporter.WarningsDuringTypechecking -import viper.silver.ast.WeightedQuantifier +import viper.silver.reporter.{AnnotationWarning, WarningsDuringVerification} +import viper.silver.ast.{AnnotationInfo, WeightedQuantifier} /* TODO: With the current design w.r.t. parallelism, eval should never "move" an execution * to a different verifier. Hence, consider not passing the verifier to continuations @@ -290,8 +290,12 @@ object evaluator extends EvaluationRules { evalInOldState(s, lbl, e0, pve, v)(Q)} case ast.Let(x, e0, e1) => - eval(s, e0, pve, v)((s1, t0, v1) => - eval(s1.copy(g = s1.g + (x.localVar, t0)), e1, pve, v1)(Q)) + eval(s, e0, pve, v)((s1, t0, v1) => { + val t = v1.decider.appliedFresh("letvar", v1.symbolConverter.toSort(x.typ), s1.relevantQuantifiedVariables) + v1.decider.assume(t === t0) + val newFuncRec = s1.functionRecorder.recordFreshSnapshot(t.applicable.asInstanceOf[Function]) + eval(s1.copy(g = s1.g + (x.localVar, t0), functionRecorder = newFuncRec), e1, pve, v1)(Q) + }) /* Strict evaluation of AND */ case ast.And(e0, e1) if Verifier.config.disableShortCircuitingEvaluations() => @@ -642,9 +646,25 @@ object evaluator extends EvaluationRules { (exists, Exists, exists.triggers) case _: ast.ForPerm => sys.error(s"Unexpected quantified expression $sourceQuant") } - val quantWeight = sourceQuant.info match { - case w: WeightedQuantifier => Some(w.weight) - case _ => None + val quantWeight = sourceQuant.info.getUniqueInfo[WeightedQuantifier] match { + case Some(w) => + if (w.weight >= 0) { + Some(w.weight) + } else { + v.reporter.report(AnnotationWarning(s"Invalid quantifier weight annotation: ${w}")) + None + } + case None => sourceQuant.info.getUniqueInfo[AnnotationInfo] match { + case Some(ai) if ai.values.contains("weight") => + ai.values("weight") match { + case Seq(w) if w.toIntOption.exists(w => w >= 0) => + Some(w.toInt) + case s => + v.reporter.report(AnnotationWarning(s"Invalid quantifier weight annotation: ${s}")) + None + } + case _ => None + } } val body = eQuant.exp @@ -1345,8 +1365,8 @@ object evaluator extends EvaluationRules { Q(s, cachedTriggerTerms ++ remainingTriggerTerms, v) case _ => for (e <- remainingTriggerExpressions) - v.reporter.report(WarningsDuringTypechecking(Seq( - TypecheckerWarning(s"Might not be able to use trigger $e, since it is not evaluated while evaluating the body of the quantifier", e.pos)))) + v.reporter.report(WarningsDuringVerification(Seq( + VerifierWarning(s"Might not be able to use trigger $e, since it is not evaluated while evaluating the body of the quantifier", e.pos)))) Q(s, cachedTriggerTerms, v) } } @@ -1396,13 +1416,15 @@ object evaluator extends EvaluationRules { triggerAxioms = triggerAxioms ++ axioms smDefs = smDefs ++ smDef case pa: ast.PredicateAccess if s.heapDependentTriggers.contains(pa.loc(s.program)) => - val (axioms, trigs, _) = generatePredicateTrigger(pa, s, pve, v) + val (axioms, trigs, _, smDef) = generatePredicateTrigger(pa, s, pve, v) triggers = triggers ++ trigs triggerAxioms = triggerAxioms ++ axioms + smDefs = smDefs ++ smDef case wand: ast.MagicWand if s.heapDependentTriggers.contains(MagicWandIdentifier(wand, s.program)) => - val (axioms, trigs, _) = generateWandTrigger(wand, s, pve, v) + val (axioms, trigs, _, smDef) = generateWandTrigger(wand, s, pve, v) triggers = triggers ++ trigs triggerAxioms = triggerAxioms ++ axioms + smDefs = smDefs ++ smDef case e => evalTrigger(s, Seq(e), pve, v)((_, t, _) => { triggers = triggers ++ t Success() @@ -1482,7 +1504,11 @@ object evaluator extends EvaluationRules { } /* TODO: Try to unify with generateFieldTrigger above, or at least with generateWandTrigger below */ - private def generatePredicateTrigger(pa: ast.PredicateAccess, s: State, pve: PartialVerificationError, v: Verifier): (Seq[Term], Seq[Term], PredicateTrigger) = { + private def generatePredicateTrigger(pa: ast.PredicateAccess, + s: State, + pve: PartialVerificationError, + v: Verifier) + : (Seq[Term], Seq[Term], PredicateTrigger, Seq[SnapshotMapDefinition]) = { var axioms = Seq.empty[Term] var triggers = Seq.empty[Term] var mostRecentTrig: PredicateTrigger = null @@ -1504,11 +1530,15 @@ object evaluator extends EvaluationRules { Success() }) - (axioms, triggers, mostRecentTrig) + (axioms, triggers, mostRecentTrig, Seq(smDef1)) } /* TODO: See comments for generatePredicateTrigger above */ - private def generateWandTrigger(wand: ast.MagicWand, s: State, pve: PartialVerificationError, v: Verifier): (Seq[Term], Seq[Term], PredicateTrigger) = { + private def generateWandTrigger(wand: ast.MagicWand, + s: State, + pve: PartialVerificationError, + v: Verifier) + : (Seq[Term], Seq[Term], PredicateTrigger, Seq[SnapshotMapDefinition]) = { var axioms = Seq.empty[Term] var triggers = Seq.empty[Term] var mostRecentTrig: PredicateTrigger = null @@ -1532,7 +1562,7 @@ object evaluator extends EvaluationRules { Success() }) - (axioms, triggers, mostRecentTrig) + (axioms, triggers, mostRecentTrig, Seq(smDef1)) } /* Evaluate a sequence of expressions in Order diff --git a/src/main/scala/rules/ExecutionFlowController.scala b/src/main/scala/rules/ExecutionFlowController.scala index 05cab4941..6a2d28513 100644 --- a/src/main/scala/rules/ExecutionFlowController.scala +++ b/src/main/scala/rules/ExecutionFlowController.scala @@ -6,6 +6,7 @@ package viper.silicon.rules +import viper.silver.ast import viper.silicon.Config.ExhaleMode import viper.silicon.interfaces._ import viper.silicon.logger.records.data.CommentRecord @@ -129,7 +130,19 @@ object executionFlowController extends ExecutionFlowRules { val comLog = new CommentRecord("Retry", s0, v.decider.pcs) val sepIdentifier = v.symbExLog.openScope(comLog) - val temporaryMCE = Verifier.config.exhaleMode != ExhaleMode.Greedy + val temporaryMCE = s0.currentMember.map(_.info.getUniqueInfo[ast.AnnotationInfo]) match { + case Some(Some(ai)) if ai.values.contains("exhaleMode") => + ai.values("exhaleMode") match { + case Seq("0") | Seq("greedy") => + false + case Seq("1") | Seq("mce") | Seq("moreCompleteExhale") | Seq("2") | Seq("mceOnDemand") => true + case _ => + // Invalid annotation was already reported when creating the initial state. + Verifier.config.exhaleMode != ExhaleMode.Greedy + } + case _ => 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, moreCompleteExhale = s0.moreCompleteExhale), r, v1) diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index 24d2c602d..69fe5e98a 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -203,9 +203,9 @@ object executor extends ExecutionRules { v1.decider.freshFunctions /* [BRANCH-PARALLELISATION] */) v1.decider.prover.comment("Loop head block: Check well-definedness of edge conditions") edgeConditions.foldLeft(Success(): VerificationResult) { - case (fatalResult: FatalResult, _) => fatalResult + case (result, _) if !result.continueVerification => result case (intermediateResult, eCond) => - intermediateResult && executionFlowController.locally(s1, v1)((s2, v2) => { + intermediateResult combine executionFlowController.locally(s1, v1)((s2, v2) => { eval(s2, eCond, WhileFailed(eCond), v2)((_, _, _) => Success())})}})}) && executionFlowController.locally(s, v)((s0, v0) => { @@ -213,10 +213,10 @@ object executor extends ExecutionRules { consumes(s0, invs, LoopInvariantNotEstablished, v0)((sLeftover, _, v1) => { v1.decider.prover.comment("Loop head block: Execute statements of loop head block (in invariant state)") phase1data.foldLeft(Success(): VerificationResult) { - case (fatalResult: FatalResult, _) => fatalResult + case (result, _) if !result.continueVerification => result case (intermediateResult, (s1, pcs, ff1)) => /* [BRANCH-PARALLELISATION] ff1 */ val s2 = s1.copy(invariantContexts = sLeftover.h +: s1.invariantContexts) - intermediateResult && executionFlowController.locally(s2, v1)((s3, v2) => { + intermediateResult combine executionFlowController.locally(s2, v1)((s3, v2) => { v2.decider.declareAndRecordAsFreshFunctions(ff1 -- v2.decider.freshFunctions) /* [BRANCH-PARALLELISATION] */ v2.decider.assume(pcs.assumptions) v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract) @@ -313,7 +313,7 @@ object executor extends ExecutionRules { val (relevantChunks, otherChunks) = quantifiedChunkSupporter.splitHeap[QuantifiedFieldChunk](s2.h, BasicChunkIdentifier(field.name)) val hints = quantifiedChunkSupporter.extractHints(None, Seq(tRcvr)) - val chunkOrderHeuristics = quantifiedChunkSupporter.hintBasedChunkOrderHeuristic(hints) + val chunkOrderHeuristics = quantifiedChunkSupporter.singleReceiverChunkOrderHeuristic(Seq(tRcvr), hints, v2) val s2p = if (s2.heapDependentTriggers.contains(field)){ val (smDef1, smCache1) = quantifiedChunkSupporter.summarisingSnapshotMap( diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 54dd22f76..4393d857c 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -1231,8 +1231,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { case Some(heuristics) => heuristics case None => - quantifiedChunkSupporter.hintBasedChunkOrderHeuristic( - quantifiedChunkSupporter.extractHints(None, arguments)) + quantifiedChunkSupporter.singleReceiverChunkOrderHeuristic(arguments, + quantifiedChunkSupporter.extractHints(None, arguments), v) } if (s.exhaleExt) { @@ -1362,9 +1362,12 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { // ME: When using Z3 via API, it is beneficial to not use macros, since macro-terms will *always* be different // (leading to new terms that have to be translated), whereas without macros, we can usually use a term // that already exists. + // ME: Update: Actually, it seems better to use macros even with the API since Silicon terms can grow so large + // that e.g. the instantiate call in createPermissionConstraintAndDepletedCheck takes forever, before even + // converting to a Z3 term. // During function verification, we should not define macros, since they could contain resullt, which is not // defined elsewhere. - val declareMacro = s.functionRecorder == NoopFunctionRecorder && !Verifier.config.useFlyweight + val declareMacro = s.functionRecorder == NoopFunctionRecorder // && !Verifier.config.useFlyweight val permsProvided = ch.perm val permsTaken = if (declareMacro) { @@ -1734,6 +1737,38 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { matchingChunks ++ otherChunks } + def singleReceiverChunkOrderHeuristic(receiver: Seq[Term], hints: Seq[Term], v: Verifier) + : Seq[QuantifiedBasicChunk] => Seq[QuantifiedBasicChunk] = { + // Heuristic that emulates greedy Silicon behavior for consuming single-receiver permissions. + // First: Find singleton chunks that have the same receiver syntactically. + // If so, consider those first, then all others. + // Second: If nothing matches syntactically, try to find a chunk that matches the receiver using the decider. + // If that's the case, consider that chunk first, then all others. + // Third: As a fallback, use the standard hint based heuristics. + val fallback = hintBasedChunkOrderHeuristic(hints) + + (chunks: Seq[QuantifiedBasicChunk]) => { + val (syntacticMatches, others) = chunks.partition(c => c.singletonArguments.contains(receiver)) + if (syntacticMatches.nonEmpty) { + syntacticMatches ++ others + } else { + val greedyMatch = chunks.find(c => c.singletonArguments match { + case Some(args) if args.length == receiver.length => + args.zip(receiver).forall(ts => v.decider.check(ts._1 === ts._2, Verifier.config.checkTimeout())) + case _ => + false + }).toSeq + if (greedyMatch.nonEmpty) { + greedyMatch ++ chunks.diff(greedyMatch) + } else { + // It doesn't seem to be any of the singletons. Use the fallback on the non-singletons. + val (qpChunks, singletons) = chunks.partition(_.singletonArguments.isEmpty) + fallback(qpChunks) ++ singletons + } + } + } + } + def extractHints(cond: Option[Term], arguments: Seq[Term]): Seq[Term] = { var hints = arguments.flatMap { diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index 56a3f29e3..b56238772 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -168,7 +168,7 @@ object State { `recordVisited1`, `visited1`, `methodCfg1`, `invariantContexts1`, constrainableARPs2, - `quantifiedVariables1`, + quantifiedVariables2, `retrying1`, `underJoin1`, functionRecorder2, @@ -187,6 +187,7 @@ object State { val triggerExp3 = triggerExp1 && triggerExp2 val possibleTriggers3 = possibleTriggers1 ++ possibleTriggers2 val constrainableARPs3 = constrainableARPs1 ++ constrainableARPs2 + val quantifiedVariables3 = (quantifiedVariables1 ++ quantifiedVariables2).distinct val smCache3 = smCache1.union(smCache2) val pmCache3 = pmCache1 ++ pmCache2 @@ -198,6 +199,7 @@ object State { possibleTriggers = possibleTriggers3, triggerExp = triggerExp3, constrainableARPs = constrainableARPs3, + quantifiedVariables = quantifiedVariables3, ssCache = ssCache3, smCache = smCache3, pmCache = pmCache3, diff --git a/src/main/scala/state/Terms.scala b/src/main/scala/state/Terms.scala index 86e4ee5aa..3c2d341a0 100644 --- a/src/main/scala/state/Terms.scala +++ b/src/main/scala/state/Terms.scala @@ -2479,7 +2479,7 @@ object Let extends CondFlyweightTermFactory[(Map[Var, Term], Term), Let] { def apply(v: Var, t: Term, body: Term): Term = apply(Map(v -> t), body) def apply(vs: Seq[Var], ts: Seq[Term], body: Term): Term = apply(toMap(vs zip ts), body) - override def apply(v0: (Map[Var, Term], Term)) = { + override def apply(v0: (Map[Var, Term], Term)): Term = { val (bindings, body) = v0 if (bindings.isEmpty) body else createIfNonExistent(v0) diff --git a/src/main/scala/supporters/BuiltinDomainsContributor.scala b/src/main/scala/supporters/BuiltinDomainsContributor.scala index 21594f49d..f181a298a 100644 --- a/src/main/scala/supporters/BuiltinDomainsContributor.scala +++ b/src/main/scala/supporters/BuiltinDomainsContributor.scala @@ -17,7 +17,6 @@ import viper.silicon.interfaces.PreambleContributor import viper.silicon.interfaces.decider.ProverLike import viper.silicon.state.DefaultSymbolConverter import viper.silicon.state.terms._ -import viper.silver.ast.LineCol abstract class BuiltinDomainsContributor extends PreambleContributor[Sort, DomainFun, Term] { type BuiltinDomainType <: ast.GenericType @@ -194,23 +193,14 @@ private object utils { } val fp = new viper.silver.parser.FastParser() - val lc = new LineCol(fp) - fp.parse(content, fromPath) match { - case fastparse.Parsed.Success(parsedProgram: viper.silver.parser.PProgram, _) => - assert(parsedProgram.errors.isEmpty, s"Unexpected parsing errors: ${parsedProgram.errors}") - - val resolver = viper.silver.parser.Resolver(parsedProgram) - val resolved = resolver.run.get - val translator = viper.silver.parser.Translator(resolved) - val program = translator.translate.get - - program - - case fastparse.Parsed.Failure(msg, index, _) => - val (line, col) = lc.getPos(index) - sys.error(s"Failure: $msg, at ${viper.silver.ast.FilePosition(fromPath, line, col)}") - //? val pos = extra.input.prettyIndex(index).split(":").map(_.toInt) - //? sys.error(s"Failure: $msg, at ${viper.silver.ast.FilePosition(fromPath, pos(0), pos(1))}") - } + val parsedProgram = fp.parse(content, fromPath) + assert(parsedProgram.errors.isEmpty, s"Unexpected parsing errors: ${parsedProgram.errors}") + + val resolver = viper.silver.parser.Resolver(parsedProgram) + val resolved = resolver.run.get + val translator = viper.silver.parser.Translator(resolved) + val program = translator.translate.get + + program } } diff --git a/src/main/scala/supporters/Domains.scala b/src/main/scala/supporters/Domains.scala index 131ebb696..192cb10f6 100644 --- a/src/main/scala/supporters/Domains.scala +++ b/src/main/scala/supporters/Domains.scala @@ -12,9 +12,9 @@ import viper.silicon.common.collections.immutable.MultiMap._ import viper.silicon.toMap import viper.silicon.interfaces.PreambleContributor import viper.silicon.interfaces.decider.ProverLike -import viper.silicon.state.{SymbolConverter, terms} +import viper.silicon.state.{FunctionPreconditionTransformer, SymbolConverter, terms} import viper.silicon.state.terms.{Distinct, DomainFun, Sort, Term} -import viper.silver.ast.{NamedDomainAxiom} +import viper.silver.ast.NamedDomainAxiom trait DomainsContributor[SO, SY, AX, UA] extends PreambleContributor[SO, SY, AX] { def uniquenessAssumptionsAfterAnalysis: Iterable[UA] @@ -100,7 +100,8 @@ class DefaultDomainsContributor(symbolConverter: SymbolConverter, domain.axioms foreach (axiom => { val tAx = domainTranslator.translateAxiom(axiom, symbolConverter.toSort) - collectedAxioms += tAx + val tAxPres = FunctionPreconditionTransformer.transform(tAx, program) + collectedAxioms += terms.And(tAxPres, tAx) }) }) } diff --git a/src/main/scala/supporters/ExpressionTranslator.scala b/src/main/scala/supporters/ExpressionTranslator.scala index 353dac8c1..22077d182 100644 --- a/src/main/scala/supporters/ExpressionTranslator.scala +++ b/src/main/scala/supporters/ExpressionTranslator.scala @@ -10,7 +10,7 @@ import viper.silver.ast import viper.silicon.rules.functionSupporter import viper.silicon.state.Identifier import viper.silicon.state.terms._ -import viper.silver.ast.WeightedQuantifier +import viper.silver.ast.{AnnotationInfo, WeightedQuantifier} trait ExpressionTranslator { /* TODO: Shares a lot of code with DefaultEvaluator. Unfortunately, it doesn't seem to be easy to @@ -97,10 +97,25 @@ trait ExpressionTranslator { case other => other } ))) - - val weight = sourceQuant.info match { - case w: WeightedQuantifier => Some(w.weight) - case _ => None + val weight = sourceQuant.info.getUniqueInfo[WeightedQuantifier] match { + case Some(w) => + if (w.weight >= 0) { + Some(w.weight) + } else { + // TODO: We would like to emit a warning here, but don't have a reporter available. + None + } + case None => sourceQuant.info.getUniqueInfo[AnnotationInfo] match { + case Some(ai) if ai.values.contains("weight") => + ai.values("weight") match { + case Seq(w) if w.toIntOption.exists(w => w >= 0) => + Some(w.toInt) + case s => + // TODO: We would like to emit a warning here, but don't have a reporter available. + None + } + case _ => None + } } Quantification(qantOp, @@ -147,7 +162,7 @@ trait ExpressionTranslator { val df = Fun(id, inSorts, outSort) App(df, tArgs) - case bfa@ast.BackendFuncApp(func, args) => + case bfa@ast.BackendFuncApp(_, args) => val tArgs = args map f val inSorts = tArgs map (_.sort) val outSort = toSort(bfa.typ) @@ -155,6 +170,15 @@ trait ExpressionTranslator { val sf = SMTFun(id, inSorts, outSort) App(sf, tArgs) + case fa@ast.FuncApp(name, args) => + // We are assuming here that only functions with empty preconditions are used. + val tArgs = Unit +: (args map f) + val inSorts = tArgs map (_.sort) + val outSort = toSort(fa.typ) + val id = Identifier(name) + val df = HeapDepFun(id, inSorts, outSort) + App(df, tArgs) + /* Permissions */ case _: ast.FullPerm => FullPerm diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index e78253f3f..a99cbb17e 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/src/main/scala/supporters/MethodSupporter.scala @@ -72,6 +72,7 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif new java.io.File(s"${Verifier.config.tempDirectory()}/${method.name}.dot")) } + errorsReportedSoFar.set(0) val result = /* Combined the well-formedness check and the execution of the body, which are two separate * rules in Smans' paper. diff --git a/src/main/scala/supporters/functions/FunctionData.scala b/src/main/scala/supporters/functions/FunctionData.scala index 8629a2168..7e0b3cab2 100644 --- a/src/main/scala/supporters/functions/FunctionData.scala +++ b/src/main/scala/supporters/functions/FunctionData.scala @@ -266,17 +266,22 @@ class FunctionData(val programFunction: ast.Function, Forall(arguments, body, allTriggers)}) } - lazy val preconditionPropagationAxiom: Seq[Term] = { + lazy val bodyPreconditionPropagationAxiom: Seq[Term] = { val pre = preconditionFunctionApplication val bodyPreconditions = if (programFunction.body.isDefined) optBody.map(translatedBody => { val body = Implies(pre, FunctionPreconditionTransformer.transform(translatedBody, program)) Forall(arguments, body, Seq(Trigger(functionApplication))) }) else None + bodyPreconditions.toSeq + } + + lazy val postPreconditionPropagationAxiom: Seq[Term] = { + val pre = preconditionFunctionApplication val postPreconditions = if (programFunction.posts.nonEmpty) { val bodyBindings: Map[Var, Term] = Map(formalResult -> limitedFunctionApplication) val bodies = translatedPosts.map(tPost => Let(bodyBindings, Implies(pre, FunctionPreconditionTransformer.transform(tPost, program)))) bodies.map(b => Forall(arguments, b, Seq(Trigger(limitedFunctionApplication)))) } else Seq() - bodyPreconditions.toSeq ++ postPreconditions + postPreconditions } } diff --git a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala index 71a2117dd..32d15c436 100644 --- a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala +++ b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala @@ -172,10 +172,10 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver emitAndRecordFunctionAxioms(data.limitedAxiom) emitAndRecordFunctionAxioms(data.triggerAxiom) emitAndRecordFunctionAxioms(data.postAxiom.toSeq: _*) + emitAndRecordFunctionAxioms(data.postPreconditionPropagationAxiom: _*) this.postConditionAxioms = this.postConditionAxioms ++ data.postAxiom.toSeq if (function.body.isEmpty) { - emitAndRecordFunctionAxioms(data.preconditionPropagationAxiom.toSeq: _*) result1 } else { /* Phase 2: Verify the function's postcondition */ @@ -186,7 +186,7 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver data.verificationFailures = data.verificationFailures :+ fatalResult case _ => emitAndRecordFunctionAxioms(data.definitionalAxiom.toSeq: _*) - emitAndRecordFunctionAxioms(data.preconditionPropagationAxiom.toSeq: _*) + emitAndRecordFunctionAxioms(data.bodyPreconditionPropagationAxiom: _*) } result1 && result2 diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index 3a4af84bc..4e3809788 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -32,8 +32,8 @@ import viper.silicon.utils.Counter import viper.silver.ast.{BackendType, Member} import viper.silver.ast.utility.rewriter.Traverse import viper.silver.cfg.silver.SilverCfg -import viper.silver.reporter.{ConfigurationConfirmation, ExecutionTraceReport, Reporter, VerificationResultMessage, VerificationTerminationMessage, QuantifierChosenTriggersMessage, WarningsDuringTypechecking} -import viper.silver.verifier.TypecheckerWarning +import viper.silver.reporter.{AnnotationWarning, ConfigurationConfirmation, ExecutionTraceReport, QuantifierChosenTriggersMessage, Reporter, VerificationResultMessage, VerificationTerminationMessage, WarningsDuringVerification} +import viper.silver.verifier.VerifierWarning /* TODO: Extract a suitable MainVerifier interface, probably including * - def verificationPoolManager: VerificationPoolManager) @@ -166,13 +166,13 @@ class DefaultMainVerifier(config: Config, case forall: ast.Forall if forall.isPure => val res = viper.silicon.utils.ast.autoTrigger(forall, forall.autoTrigger) if (res.triggers.isEmpty) - reporter.report(WarningsDuringTypechecking(Seq(TypecheckerWarning("No triggers provided or inferred for quantifier.", res.pos)))) + reporter.report(WarningsDuringVerification(Seq(VerifierWarning("No triggers provided or inferred for quantifier.", res.pos)))) reporter report QuantifierChosenTriggersMessage(res, res.triggers) res case exists: ast.Exists => val res = viper.silicon.utils.ast.autoTrigger(exists, exists.autoTrigger) if (res.triggers.isEmpty) - reporter.report(WarningsDuringTypechecking(Seq(TypecheckerWarning("No triggers provided or inferred for quantifier.", res.pos)))) + reporter.report(WarningsDuringVerification(Seq(VerifierWarning("No triggers provided or inferred for quantifier.", res.pos)))) reporter report QuantifierChosenTriggersMessage(res, res.triggers) res }, Traverse.BottomUp) @@ -303,6 +303,21 @@ class DefaultMainVerifier(config: Config, case r => r } + val mce = member.info.getUniqueInfo[ast.AnnotationInfo] match { + case Some(ai) if ai.values.contains("exhaleMode") => + ai.values("exhaleMode") match { + case Seq("0") | Seq("greedy") | Seq("2") | Seq("mceOnDemand") => + if (Verifier.config.counterexample.isSupplied) + reporter report AnnotationWarning(s"Member ${member.name} has exhaleMode annotation that may interfere with counterexample generation.") + false + case Seq("1") | Seq("mce") | Seq("moreCompleteExhale") => true + case v => + reporter report AnnotationWarning(s"Member ${member.name} has invalid exhaleMode annotation value $v. Annotation will be ignored.") + Verifier.config.exhaleMode == ExhaleMode.MoreComplete + } + case _ => Verifier.config.exhaleMode == ExhaleMode.MoreComplete + } + State(program = program, functionData = functionData, predicateData = predicateData, @@ -313,7 +328,7 @@ class DefaultMainVerifier(config: Config, predicateFormalVarMap = predSnapGenerator.formalVarMap, currentMember = Some(member), heapDependentTriggers = resourceTriggers, - moreCompleteExhale = Verifier.config.exhaleMode == ExhaleMode.MoreComplete) + moreCompleteExhale = mce) } private def createInitialState(@unused cfg: SilverCfg, diff --git a/src/test/scala/SiliconQuantifierWeightTests.scala b/src/test/scala/SiliconQuantifierWeightTests.scala index a2e89b2f7..7382ff87f 100644 --- a/src/test/scala/SiliconQuantifierWeightTests.scala +++ b/src/test/scala/SiliconQuantifierWeightTests.scala @@ -11,7 +11,7 @@ import viper.silicon.state.DefaultSymbolConverter import viper.silicon.state.terms.Term import viper.silicon.supporters.ExpressionTranslator import viper.silver.ast -import viper.silver.ast.{AnonymousDomainAxiom, Bool, Domain, DomainFunc, DomainFuncApp, EqCmp, Exists, Forall, Int, IntLit, LocalVar, LocalVarDecl, Method, Program, Seqn, Trigger, TrueLit, WeightedQuantifier} +import viper.silver.ast.{AnnotationInfo, AnonymousDomainAxiom, Bool, Domain, DomainFunc, DomainFuncApp, EqCmp, Exists, Forall, Int, IntLit, LocalVar, LocalVarDecl, Method, Program, Seqn, Trigger, TrueLit, WeightedQuantifier} import viper.silver.reporter.NoopReporter import viper.silver.verifier.{Failure, Success} @@ -46,6 +46,32 @@ class SiliconQuantifierWeightTests extends AnyFunSuite { assert(rendered.contains(":weight 12")) } + test("The weight annotation is part of the translation of a Forall") { + val expr = Forall( + Seq(LocalVarDecl("x", Int)()), + Seq(), + TrueLit()() + )( + info = AnnotationInfo(Map("weight" -> Seq("12"))) + ) + val term = translator.translateExpr(expr) + val rendered = termConverter.convert(term) + assert(rendered.contains(":weight 12")) + } + + test("The weight annotation is ignored for negative values") { + val expr = Forall( + Seq(LocalVarDecl("x", Int)()), + Seq(), + TrueLit()() + )( + info = AnnotationInfo(Map("weight" -> Seq("-12"))) + ) + val term = translator.translateExpr(expr) + val rendered = termConverter.convert(term) + assert(!rendered.contains(":weight")) + } + test("The weight is part of the translation of an Exists") { val expr = Exists( Seq(LocalVarDecl("x", Int)()),