From 418318765039e55da9f7f7c50d0a004f3f860a65 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 2 May 2023 20:05:24 +0200 Subject: [PATCH 01/74] Merge states with different quantified variables --- src/main/scala/state/State.scala | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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, From af87319a734bdc8a8dd5fc7a2187d4c078d7a91b Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Thu, 4 May 2023 12:38:36 +0000 Subject: [PATCH 02/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index ae4a12399..5bdd26c4a 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit ae4a12399cd0b42bedabf01be2cda93700244bd6 +Subproject commit 5bdd26c4ad32c0048cc3a1bb2393dbbf882f71e5 From 26fdba5a168fd72be030a1bc25158afd41b61650 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Thu, 4 May 2023 13:22:37 +0000 Subject: [PATCH 03/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 5bdd26c4a..ff39eef9d 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 5bdd26c4ad32c0048cc3a1bb2393dbbf882f71e5 +Subproject commit ff39eef9deb4cc7c49570003a285539d9269b904 From 415be3afcc1d295c8f7d986eacc0e7e8c7408e19 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Fri, 5 May 2023 23:54:20 +0000 Subject: [PATCH 04/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index ff39eef9d..fc5c95d50 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit ff39eef9deb4cc7c49570003a285539d9269b904 +Subproject commit fc5c95d50c539c89b4e436b7ef1b1be02f048a34 From ab8f0bb1e8d575aa5bf6c507ddcf42da38d9678a Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Fri, 12 May 2023 11:32:34 +0000 Subject: [PATCH 05/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index fc5c95d50..92082072a 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit fc5c95d50c539c89b4e436b7ef1b1be02f048a34 +Subproject commit 92082072a41f25e87b65549e38d934818ea81234 From d9c762ac7f058c4f1e2f725b54f35d7541d66bde Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Fri, 12 May 2023 16:03:46 +0000 Subject: [PATCH 06/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 92082072a..035769d2e 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 92082072a41f25e87b65549e38d934818ea81234 +Subproject commit 035769d2eb280e38e283ab22fffb1e1d6eed5c17 From a5a0957aa5b204c9b1602a8d30a6c879c7a3bbc1 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Sat, 13 May 2023 14:46:16 +0000 Subject: [PATCH 07/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 035769d2e..2e0c91e43 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 035769d2eb280e38e283ab22fffb1e1d6eed5c17 +Subproject commit 2e0c91e439b5b71e96883800f3b248dc490586ae From 1dc0a2b3d564de02f6f9bda5093f1814e9d33d71 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 15 May 2023 14:06:59 +0200 Subject: [PATCH 08/74] Correctly translating calls to non-domain functions without preconditions from domain axioms --- src/main/scala/supporters/Domains.scala | 7 ++++--- src/main/scala/supporters/ExpressionTranslator.scala | 11 ++++++++++- 2 files changed, 14 insertions(+), 4 deletions(-) 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..608621cbe 100644 --- a/src/main/scala/supporters/ExpressionTranslator.scala +++ b/src/main/scala/supporters/ExpressionTranslator.scala @@ -147,7 +147,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 +155,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 From 988b8e10ca5171b5840c3bc37e61f34ca9d59c8e Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 15 May 2023 14:07:10 +0200 Subject: [PATCH 09/74] Updating silver --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 2e0c91e43..5a706439b 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 2e0c91e439b5b71e96883800f3b248dc490586ae +Subproject commit 5a706439b72a4868728bfbbc16c3b88b2a76ea62 From 235075bbfc6e3797b7b86846a90bd872d17e961b Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 15 May 2023 19:47:49 +0200 Subject: [PATCH 10/74] enabling logging when proverLogFile is set --- src/main/scala/Config.scala | 4 ++++ src/main/scala/decider/ProverStdIO.scala | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala index 41c31f442..c05e0d738 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."), 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)) From d7db3717ca36ca1420f4cc97236df5a7bace2970 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Mon, 15 May 2023 21:03:08 +0200 Subject: [PATCH 11/74] Fix silver's issue #688 (#718) * Fix Silver's issue #688 * use the correct verifier instance * use func. recorder --- src/main/scala/rules/Evaluator.scala | 8 ++++++-- src/main/scala/state/Terms.scala | 2 +- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index fe8dfe0b5..9bded4793 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -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.fresh(v1.symbolConverter.toSort(x.typ)) + v1.decider.assume(t === t0) + val newFuncRec = s1.functionRecorder.recordFreshSnapshot(t) + eval(s1.copy(g = s1.g + (x.localVar, t), functionRecorder = newFuncRec), e1, pve, v1)(Q) + }) /* Strict evaluation of AND */ case ast.And(e0, e1) if Verifier.config.disableShortCircuitingEvaluations() => diff --git a/src/main/scala/state/Terms.scala b/src/main/scala/state/Terms.scala index bcda3f8f3..5caefeb45 100644 --- a/src/main/scala/state/Terms.scala +++ b/src/main/scala/state/Terms.scala @@ -2447,7 +2447,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) From 0f14c67207fb205f1aefc83af53712f2409dd809 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Mon, 15 May 2023 19:41:18 +0000 Subject: [PATCH 12/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 2e0c91e43..dc8f0c95a 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 2e0c91e439b5b71e96883800f3b248dc490586ae +Subproject commit dc8f0c95abde16e1c37f48b2b45755ec85740a80 From 151f2218ff1c1da474d8acb5b613de705e749a8c Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Mon, 15 May 2023 21:41:46 +0000 Subject: [PATCH 13/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index dc8f0c95a..73ac16a10 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit dc8f0c95abde16e1c37f48b2b45755ec85740a80 +Subproject commit 73ac16a10c381ce42f9084bcbafeb80f0cbd3e23 From 35cc587bf0837707b6c47293597962ca7804ba4e Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 17 May 2023 00:15:55 +0200 Subject: [PATCH 14/74] Handling non-existent CEs and fractions correctly in CEs from Z3 via API --- src/main/scala/decider/Z3ProverAPI.scala | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/src/main/scala/decider/Z3ProverAPI.scala b/src/main/scala/decider/Z3ProverAPI.scala index ed98ee7ba..febf77bea 100644 --- a/src/main/scala/decider/Z3ProverAPI.scala +++ b/src/main/scala/decider/Z3ProverAPI.scala @@ -320,8 +320,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 + } } } @@ -451,7 +456,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) { From a048045d593bdb2be4686ce37b723bfb927c06d1 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Wed, 17 May 2023 10:12:21 +0000 Subject: [PATCH 15/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 73ac16a10..4e5845e9a 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 73ac16a10c381ce42f9084bcbafeb80f0cbd3e23 +Subproject commit 4e5845e9a8fa72407b09c088f2f3a670b18ecda1 From 413034fb5640f2ab3f988462d9a99c5ed97424b2 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Wed, 17 May 2023 11:25:37 +0000 Subject: [PATCH 16/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 4e5845e9a..ce2b99959 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 4e5845e9a8fa72407b09c088f2f3a670b18ecda1 +Subproject commit ce2b99959d631c8226da27391e55395ca890a436 From b7dea27fdde1233e206769c9242ba38ba30bc92d Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Wed, 17 May 2023 14:03:25 +0000 Subject: [PATCH 17/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index ce2b99959..ae28573b8 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit ce2b99959d631c8226da27391e55395ca890a436 +Subproject commit ae28573b8031898e71c7b1e5071ef1afc4b9d1ca From 29b4b5b13b02b79f60bcdd0e0cd27fcc77c85148 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Wed, 17 May 2023 16:14:19 +0000 Subject: [PATCH 18/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index ae28573b8..c352aa54d 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit ae28573b8031898e71c7b1e5071ef1afc4b9d1ca +Subproject commit c352aa54dc5a67229ea81f0d7c1602b74eaa7d69 From fd51ab6fba10db51858924575a3f51e385c6d577 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 19 May 2023 14:15:25 +0200 Subject: [PATCH 19/74] fix tiny incompletness (#722) --- src/main/scala/rules/Evaluator.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 9bded4793..7d79e8494 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -294,7 +294,7 @@ object evaluator extends EvaluationRules { val t = v1.decider.fresh(v1.symbolConverter.toSort(x.typ)) v1.decider.assume(t === t0) val newFuncRec = s1.functionRecorder.recordFreshSnapshot(t) - eval(s1.copy(g = s1.g + (x.localVar, t), functionRecorder = newFuncRec), e1, pve, v1)(Q) + eval(s1.copy(g = s1.g + (x.localVar, t0), functionRecorder = newFuncRec), e1, pve, v1)(Q) }) /* Strict evaluation of AND */ From 8d6209fd187a91e57e86751e369a457838d574cc Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sat, 27 May 2023 14:39:14 +0200 Subject: [PATCH 20/74] Reading exhaleMode annotation to set MCE locally. Also using new WarningsDuringVerification message in some places since it fits better --- src/main/scala/rules/Evaluator.scala | 8 +++--- .../scala/verifier/DefaultMainVerifier.scala | 25 +++++++++++++++---- 2 files changed, 24 insertions(+), 9 deletions(-) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 7d79e8494..b1124bf0b 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,7 +23,7 @@ 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.reporter.WarningsDuringVerification import viper.silver.ast.WeightedQuantifier /* TODO: With the current design w.r.t. parallelism, eval should never "move" an execution @@ -1349,8 +1349,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) } } diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index 3a4af84bc..a4fccac94 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") => + 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, From 38879f896eb73e946e57e044671b77e2ad52b6e8 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sat, 27 May 2023 14:41:34 +0200 Subject: [PATCH 21/74] Updated Silver reference --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index c352aa54d..554e54966 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit c352aa54dc5a67229ea81f0d7c1602b74eaa7d69 +Subproject commit 554e54966d3192cb9038939a3fc65bd77389c839 From 658f293ce7360697db005c5e27cad800f0370c6a Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sat, 27 May 2023 15:02:05 +0200 Subject: [PATCH 22/74] Updated silver reference --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 554e54966..32de02384 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 554e54966d3192cb9038939a3fc65bd77389c839 +Subproject commit 32de023845e5e997e080c703bb70329bb97fd95b From 4b27af5bbc70986884c676ffeebd63b47c1b6707 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 31 May 2023 13:52:47 +0200 Subject: [PATCH 23/74] @weight() annotation for quantifiers --- src/main/scala/rules/Evaluator.scala | 26 +++++++++++++++---- .../supporters/ExpressionTranslator.scala | 24 ++++++++++++++--- .../scala/SiliconQuantifierWeightTests.scala | 15 ++++++++++- 3 files changed, 55 insertions(+), 10 deletions(-) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index b1124bf0b..3fd6cf7c0 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -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.WarningsDuringVerification -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 @@ -646,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) => Some(w.weight) + case None => sourceQuant.info.getUniqueInfo[AnnotationInfo] match { + case Some(ai) if ai.values.contains("weight") => + ai.values("weight") match { + case Seq(w) => + try { + Some(w.toInt) + } catch { + case _: NumberFormatException => + v.reporter.report(AnnotationWarning(s"Invalid quantifier weight annotation: ${w}")) + None + } + case s => + v.reporter.report(AnnotationWarning(s"Invalid quantifier weight annotation: ${s}")) + None + } + case _ => None + } } val body = eQuant.exp diff --git a/src/main/scala/supporters/ExpressionTranslator.scala b/src/main/scala/supporters/ExpressionTranslator.scala index 353dac8c1..399cbb384 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 @@ -98,9 +98,25 @@ trait ExpressionTranslator { } ))) - val weight = sourceQuant.info match { - case w: WeightedQuantifier => Some(w.weight) - case _ => None + val weight = sourceQuant.info.getUniqueInfo[WeightedQuantifier] match { + case Some(w) => Some(w.weight) + case None => sourceQuant.info.getUniqueInfo[AnnotationInfo] match { + case Some(ai) if ai.values.contains("weight") => + ai.values("weight") match { + case Seq(w) => + try { + Some(w.toInt) + } catch { + case _: NumberFormatException => + // TODO: We would like to emit a warning here, but don't have a reporter available. + None + } + case s => + // TODO: We would like to emit a warning here. + None + } + case _ => None + } } Quantification(qantOp, diff --git a/src/test/scala/SiliconQuantifierWeightTests.scala b/src/test/scala/SiliconQuantifierWeightTests.scala index a2e89b2f7..6bf3e020e 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,19 @@ 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 is part of the translation of an Exists") { val expr = Exists( Seq(LocalVarDecl("x", Int)()), From 20a00265adc252d27c3b4111930497e6dcff83fa Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Wed, 31 May 2023 12:55:51 +0000 Subject: [PATCH 24/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index c352aa54d..c112143ef 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit c352aa54dc5a67229ea81f0d7c1602b74eaa7d69 +Subproject commit c112143ef84e98438556952ded5874e9b19e9d00 From 7a4c3e49c7c532a510abe94203c7b43e4761cf36 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Wed, 31 May 2023 16:26:55 +0000 Subject: [PATCH 25/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index c112143ef..d3825138a 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit c112143ef84e98438556952ded5874e9b19e9d00 +Subproject commit d3825138af396da6aa870ba1cf64b280dded5b3f From 67ecb967019013f307220eb3aae421683827bc80 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 31 May 2023 18:44:34 +0200 Subject: [PATCH 26/74] Updated silver reference --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 32de02384..77b5fd129 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 32de023845e5e997e080c703bb70329bb97fd95b +Subproject commit 77b5fd12969d833c5e7aa6f231a1f92262939ff9 From 1856253356acfcc7be02e4e0f2ae2b200894b6be Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 31 May 2023 19:36:04 +0200 Subject: [PATCH 27/74] Supporting mce on demand via annotation --- .../scala/rules/ExecutionFlowController.scala | 15 ++++++++++++++- src/main/scala/verifier/DefaultMainVerifier.scala | 2 +- 2 files changed, 15 insertions(+), 2 deletions(-) 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/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index a4fccac94..4e3809788 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -306,7 +306,7 @@ class DefaultMainVerifier(config: Config, 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") => + 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 From 49ae470f95013324d612ff5c1848082cf2681870 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 31 May 2023 20:21:07 +0200 Subject: [PATCH 28/74] Filtering negative weights --- src/main/scala/rules/Evaluator.scala | 18 ++++++++-------- .../supporters/ExpressionTranslator.scala | 21 +++++++++---------- .../scala/SiliconQuantifierWeightTests.scala | 13 ++++++++++++ 3 files changed, 32 insertions(+), 20 deletions(-) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 3fd6cf7c0..45d4fe43c 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -647,18 +647,18 @@ object evaluator extends EvaluationRules { case _: ast.ForPerm => sys.error(s"Unexpected quantified expression $sourceQuant") } val quantWeight = sourceQuant.info.getUniqueInfo[WeightedQuantifier] match { - case Some(w) => Some(w.weight) + 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) => - try { - Some(w.toInt) - } catch { - case _: NumberFormatException => - v.reporter.report(AnnotationWarning(s"Invalid quantifier weight annotation: ${w}")) - None - } + 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 diff --git a/src/main/scala/supporters/ExpressionTranslator.scala b/src/main/scala/supporters/ExpressionTranslator.scala index 399cbb384..b8356e0b7 100644 --- a/src/main/scala/supporters/ExpressionTranslator.scala +++ b/src/main/scala/supporters/ExpressionTranslator.scala @@ -97,22 +97,21 @@ trait ExpressionTranslator { case other => other } ))) - val weight = sourceQuant.info.getUniqueInfo[WeightedQuantifier] match { - case Some(w) => Some(w.weight) + 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) => - try { - Some(w.toInt) - } catch { - case _: NumberFormatException => - // TODO: We would like to emit a warning here, but don't have a reporter available. - None - } + case Seq(w) if w.toIntOption.exists(w => w >= 0) => + Some(w.toInt) case s => - // TODO: We would like to emit a warning here. + // TODO: We would like to emit a warning here, but don't have a reporter available. None } case _ => None diff --git a/src/test/scala/SiliconQuantifierWeightTests.scala b/src/test/scala/SiliconQuantifierWeightTests.scala index 6bf3e020e..7382ff87f 100644 --- a/src/test/scala/SiliconQuantifierWeightTests.scala +++ b/src/test/scala/SiliconQuantifierWeightTests.scala @@ -59,6 +59,19 @@ class SiliconQuantifierWeightTests extends AnyFunSuite { 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)()), From 535fec2b62a0ec8b271a51a8524aba65f807a7e1 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Wed, 31 May 2023 23:37:08 +0000 Subject: [PATCH 29/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 77b5fd129..cf6123bdf 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 77b5fd12969d833c5e7aa6f231a1f92262939ff9 +Subproject commit cf6123bdfb83436507f8066e1d7544b2982aef36 From 0b89740aa9c8c30a9acd7e023b463a3c34fe18c0 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 6 Jun 2023 14:17:59 +0200 Subject: [PATCH 30/74] Alternative heuristics for consumeSingle that emulate greedy behavior --- .../scala/rules/QuantifiedChunkSupport.scala | 36 +++++++++++++++++-- 1 file changed, 33 insertions(+), 3 deletions(-) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 857bacb02..a01928083 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) { @@ -1364,7 +1364,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { // that already exists. // 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 && ch.singletonArguments.isEmpty val permsProvided = ch.perm val permsTaken = if (declareMacro) { @@ -1734,6 +1734,36 @@ 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 { + fallback(chunks) + } + } + } + } + def extractHints(cond: Option[Term], arguments: Seq[Term]): Seq[Term] = { var hints = arguments.flatMap { From 92be50726f41303d88650822a57cb2d87a909c1a Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 6 Jun 2023 15:39:42 +0200 Subject: [PATCH 31/74] Using better hints also in Executor --- src/main/scala/rules/Executor.scala | 2 +- src/main/scala/rules/QuantifiedChunkSupport.scala | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index 24d2c602d..b9ef20052 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -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 a01928083..d1f6102df 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -1364,7 +1364,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { // that already exists. // 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 && ch.singletonArguments.isEmpty + val declareMacro = s.functionRecorder == NoopFunctionRecorder && !Verifier.config.useFlyweight val permsProvided = ch.perm val permsTaken = if (declareMacro) { From 9979303da6d1b18974fdce9db63251940eea8253 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 6 Jun 2023 16:36:40 +0200 Subject: [PATCH 32/74] Re-enabling macros with API --- src/main/scala/rules/QuantifiedChunkSupport.scala | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 857bacb02..c1a03b2d4 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -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) { From d1af9179555cdf84bf983a21d35cf889766b19db Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Tue, 6 Jun 2023 19:17:58 +0000 Subject: [PATCH 33/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index cf6123bdf..496dcdc3f 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit cf6123bdfb83436507f8066e1d7544b2982aef36 +Subproject commit 496dcdc3fac518c68d70f8e160307500ec2ffd00 From 18c6cec8cd9bbefd2ab8bed53717fdd372abf227 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Wed, 14 Jun 2023 18:17:46 +0000 Subject: [PATCH 34/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 541b5604f..b51e0dcb0 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 541b5604f9046b03a820cbc117ea2e086e3e7d95 +Subproject commit b51e0dcb04f00ed747b27f8991be766d3da97946 From 56ae917d60f4e579c1be60700bdfd845e62fda50 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Sat, 17 Jun 2023 18:53:51 +0000 Subject: [PATCH 35/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index b51e0dcb0..0e92e921c 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit b51e0dcb04f00ed747b27f8991be766d3da97946 +Subproject commit 0e92e921cfadb937ad16e61c956e2570db06da99 From b1ba4d9c7dbf790cd2fde986fda14c6b7ef0d04f Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 27 Jun 2023 11:14:17 +0200 Subject: [PATCH 36/74] No longer ignoring assertTimeout for generating model / reasonUnknown --- src/main/scala/decider/Decider.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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() From 873d273968a1615bf518f78551f90596c9851b1d Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 27 Jun 2023 11:18:57 +0200 Subject: [PATCH 37/74] Removing parameter difference depending on Z3 version --- src/main/scala/decider/Z3ProverAPI.scala | 20 ++++++-------------- 1 file changed, 6 insertions(+), 14 deletions(-) diff --git a/src/main/scala/decider/Z3ProverAPI.scala b/src/main/scala/decider/Z3ProverAPI.scala index febf77bea..acb19c4bc 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, 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() From bca3ce67f77621001b37aaee86afb3dff73c643d Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 27 Jun 2023 17:24:10 +0200 Subject: [PATCH 38/74] Fixing SC mode, enabling it with parallel branches, cleaning up triggers on assert --- src/main/scala/Config.scala | 6 ----- src/main/scala/decider/Z3ProverAPI.scala | 34 ++++++++++++++++-------- 2 files changed, 23 insertions(+), 17 deletions(-) diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala index c05e0d738..141efe9a4 100644 --- a/src/main/scala/Config.scala +++ b/src/main/scala/Config.scala @@ -816,12 +816,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/decider/Z3ProverAPI.scala b/src/main/scala/decider/Z3ProverAPI.scala index acb19c4bc..d5b9dfe77 100644 --- a/src/main/scala/decider/Z3ProverAPI.scala +++ b/src/main/scala/decider/Z3ProverAPI.scala @@ -10,7 +10,7 @@ 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 -import viper.silicon.state.terms.{App, Decl, Fun, FunctionDecl, Implies, MacroDecl, Quantification, Sort, SortDecl, SortWrapperDecl, Term, TriggerGenerator, sorts} +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} @@ -248,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() @@ -271,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) + } + } } } @@ -334,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]) From 442ed9c38039a328a3ab3aeff2473b5b8de53f55 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Fri, 30 Jun 2023 13:45:42 +0000 Subject: [PATCH 39/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 0e92e921c..86d3ab977 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 0e92e921cfadb937ad16e61c956e2570db06da99 +Subproject commit 86d3ab977d87956b2d0edd224552b458f970846b From 694756f30a63dcf8b6022e5881a0a9245febb37e Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 3 Jul 2023 20:02:13 +0200 Subject: [PATCH 40/74] Fixing unsound assumption about helper variable inside quantifiers --- src/main/scala/rules/Evaluator.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 45d4fe43c..610cc514e 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -291,9 +291,9 @@ object evaluator extends EvaluationRules { case ast.Let(x, e0, e1) => eval(s, e0, pve, v)((s1, t0, v1) => { - val t = v1.decider.fresh(v1.symbolConverter.toSort(x.typ)) + val t = v1.decider.appliedFresh("letvar", v1.symbolConverter.toSort(x.typ), s1.relevantQuantifiedVariables) v1.decider.assume(t === t0) - val newFuncRec = s1.functionRecorder.recordFreshSnapshot(t) + val newFuncRec = s1.functionRecorder.recordFreshSnapshot(t.applicable.asInstanceOf[Function]) eval(s1.copy(g = s1.g + (x.localVar, t0), functionRecorder = newFuncRec), e1, pve, v1)(Q) }) From df48ee05359e28f1e30620535c3102daba04e76a Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Wed, 5 Jul 2023 12:05:27 +0000 Subject: [PATCH 41/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 86d3ab977..cf425b809 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 86d3ab977d87956b2d0edd224552b458f970846b +Subproject commit cf425b809e97c362a3f82deb6aa003b4ab220139 From 133dec153414608d03cb5cc595e73fd43c7c18b6 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Wed, 5 Jul 2023 13:13:04 +0000 Subject: [PATCH 42/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index cf425b809..e2f0b3717 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit cf425b809e97c362a3f82deb6aa003b4ab220139 +Subproject commit e2f0b37172c3e5a13cf149eb59461833ef30a24c From 971dc6940f4de4d8510dfdafd8bbe7124a7dc988 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Thu, 6 Jul 2023 00:38:35 +0000 Subject: [PATCH 43/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index e2f0b3717..64016f1e8 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit e2f0b37172c3e5a13cf149eb59461833ef30a24c +Subproject commit 64016f1e87e4c23754d5692d46a7612a2777ccf8 From 259efc171fabdd988f4f2bf2d183f1d6ec396ed5 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Sat, 8 Jul 2023 17:43:20 +0000 Subject: [PATCH 44/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 64016f1e8..2e9bffcea 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 64016f1e87e4c23754d5692d46a7612a2777ccf8 +Subproject commit 2e9bffceaff9822cdbcb0fdaa9d0c31b9a185d85 From 0dde9079b7788186dc625e9f02a1e548782b4a18 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= Date: Wed, 12 Jul 2023 17:18:11 +0200 Subject: [PATCH 45/74] Improve language flexibility (#727) Update to be compatible with new parser output --- silver | 2 +- .../BuiltinDomainsContributor.scala | 28 ++++++------------- 2 files changed, 10 insertions(+), 20 deletions(-) diff --git a/silver b/silver index 2e9bffcea..b3015e07c 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 2e9bffceaff9822cdbcb0fdaa9d0c31b9a185d85 +Subproject commit b3015e07ce05b02f6d9ec8f00595c20c8aca88a2 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 } } From 0879362f5e13954d98bfa7d4bfee60ca70fd0fbe Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Wed, 12 Jul 2023 15:38:14 +0000 Subject: [PATCH 46/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index b3015e07c..3f39bbce1 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit b3015e07ce05b02f6d9ec8f00595c20c8aca88a2 +Subproject commit 3f39bbce12befe78a4aaf9a44b53e1e84a31bcf9 From 74489bb7cba1281ad281f32c98c2eaf83bf73f02 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Wed, 12 Jul 2023 17:19:59 +0000 Subject: [PATCH 47/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 3f39bbce1..5babb1818 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 3f39bbce12befe78a4aaf9a44b53e1e84a31bcf9 +Subproject commit 5babb181850f3a700f1d57a1db8f6c21ad50238f From 2c777b51771708140079aa90c6261e82191219fe Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Thu, 13 Jul 2023 13:33:15 +0000 Subject: [PATCH 48/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 5babb1818..d769c1e85 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 5babb181850f3a700f1d57a1db8f6c21ad50238f +Subproject commit d769c1e85ac1bc6d34228f9a60f4e0d82ab3c3c1 From 01c5ab5afa8e7be16dca4c6277f397ac65782318 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Thu, 13 Jul 2023 20:25:32 +0000 Subject: [PATCH 49/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index d769c1e85..a28b06fde 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit d769c1e85ac1bc6d34228f9a60f4e0d82ab3c3c1 +Subproject commit a28b06fdee4947b49e1765fb3596e7bf44a0d757 From 3b3b4befb716fc9df4606909ff25162a5c8563a8 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Mon, 17 Jul 2023 09:57:25 +0000 Subject: [PATCH 50/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index a28b06fde..c2c1b1183 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit a28b06fdee4947b49e1765fb3596e7bf44a0d757 +Subproject commit c2c1b1183e19a71a5793a7503aae452c77512b2d From 064be39d20d092bd5b057178fe7b7983d71d4875 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Wed, 19 Jul 2023 14:04:54 +0000 Subject: [PATCH 51/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index c2c1b1183..cafd01198 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit c2c1b1183e19a71a5793a7503aae452c77512b2d +Subproject commit cafd01198d92fb5941e8444df26500d6c41d135a From 8e3190bc05a110e636aa3882504165de23ab2e19 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Thu, 20 Jul 2023 19:10:52 +0000 Subject: [PATCH 52/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index cafd01198..7f1385bfc 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit cafd01198d92fb5941e8444df26500d6c41d135a +Subproject commit 7f1385bfc648e3e8296e60d1d7fc46aeaade3261 From e1d9cd5b4ae0a1a3a2c2a7f34d42ad7265e14110 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 27 Jul 2023 00:46:09 +0200 Subject: [PATCH 53/74] Allowing counterexamples wiht MCE on demand option --- src/main/scala/Config.scala | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala index 141efe9a4..068bcc03e 100644 --- a/src/main/scala/Config.scala +++ b/src/main/scala/Config.scala @@ -807,8 +807,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 => From 7fe4d9f0919dca2b503fff9967eb1e0c4ba748b3 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Wed, 2 Aug 2023 01:56:36 +0000 Subject: [PATCH 54/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 7f1385bfc..87f83ec95 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 7f1385bfc648e3e8296e60d1d7fc46aeaade3261 +Subproject commit 87f83ec957c78062837f85547d326c90efb3eaad From 7251bc6ddc657ee00bc2997d6fc3672ef46c70f5 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Thu, 3 Aug 2023 14:34:55 +0000 Subject: [PATCH 55/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 87f83ec95..9f5b214fb 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 87f83ec957c78062837f85547d326c90efb3eaad +Subproject commit 9f5b214fb27c7aba0f48901a02f80704915ea536 From c9a680043d39175f19c7c112a08c46bcd5429bf5 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Fri, 4 Aug 2023 14:49:13 +0000 Subject: [PATCH 56/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 9f5b214fb..04df2df94 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 9f5b214fb27c7aba0f48901a02f80704915ea536 +Subproject commit 04df2df94858240769c851e2a1aba43c35976232 From e07b53607720d114883df8d9cb68dd1ac4982eb0 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 14 Aug 2023 12:58:03 +0200 Subject: [PATCH 57/74] Don't always stop verification on FatalResult (fixes issue #740) --- src/main/scala/rules/Executor.scala | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index 24d2c602d..d15793a22 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) From eebbc61e6faaa62cb7d69c6185f566eb5f361fa9 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 14 Aug 2023 13:03:42 +0200 Subject: [PATCH 58/74] Added test in silver --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 9f5b214fb..f03ccf8f2 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 9f5b214fb27c7aba0f48901a02f80704915ea536 +Subproject commit f03ccf8f28f0dc733dbda162b4c17b98132952c9 From fb0f19e7e5fd64c1810b94227402b24770107115 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Mon, 14 Aug 2023 18:23:00 +0000 Subject: [PATCH 59/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 04df2df94..501f1ecef 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 04df2df94858240769c851e2a1aba43c35976232 +Subproject commit 501f1ecefb156db539de9ec68f5673f5ca3f4817 From 2885c620b89d6e6c4eb2ea51c635931f85739a87 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Mon, 14 Aug 2023 19:42:24 +0000 Subject: [PATCH 60/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 18e73c604..c3cf35a73 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 18e73c604d22db62261902ef8b0daa6a0bcd754f +Subproject commit c3cf35a73a1292d0b3c9f60039ca691c5b874ca6 From 246f0193cdef2555145fa9a1dda0e5fc93e779dd Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 15 Aug 2023 00:32:10 +0200 Subject: [PATCH 61/74] Silicon frontend classes for API usage --- silver | 2 +- src/main/scala/Silicon.scala | 21 ++++++++++++++++++++- 2 files changed, 21 insertions(+), 2 deletions(-) diff --git a/silver b/silver index 04df2df94..afaf4523a 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 04df2df94858240769c851e2a1aba43c35976232 +Subproject commit afaf4523a8429873c4f160713a22764162b12b21 diff --git a/src/main/scala/Silicon.scala b/src/main/scala/Silicon.scala index ebab80e34..987ae59f1 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,25 @@ 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, + override implicit val logger: Logger = ViperStdOutLogger("SiliconFrontendAPI", "INFO").get) + extends SiliconFrontend(reporter, logger) 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, + override implicit val logger: Logger = ViperStdOutLogger("MinimalSiliconFrontendAPI", "INFO").get) + extends SiliconFrontend(reporter, logger) with MinimalViperFrontendAPI + + object SiliconRunner extends SiliconRunnerInstance { def main(args: Array[String]): Unit = { runMain(args) From 184af09e0cdf8adbf5e982d58cb81bf0e65297f9 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 17 Aug 2023 13:30:37 +0200 Subject: [PATCH 62/74] Removed superfluous logger arguments --- src/main/scala/Silicon.scala | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/main/scala/Silicon.scala b/src/main/scala/Silicon.scala index 987ae59f1..a9b1001cf 100644 --- a/src/main/scala/Silicon.scala +++ b/src/main/scala/Silicon.scala @@ -382,18 +382,16 @@ class SiliconFrontend(override val reporter: Reporter, * Performs consistency check and verification. * See [[viper.silver.frontend.ViperFrontendAPI]] for usage information. */ -class SiliconFrontendAPI(override val reporter: Reporter, - override implicit val logger: Logger = ViperStdOutLogger("SiliconFrontendAPI", "INFO").get) - extends SiliconFrontend(reporter, logger) with ViperFrontendAPI +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, - override implicit val logger: Logger = ViperStdOutLogger("MinimalSiliconFrontendAPI", "INFO").get) - extends SiliconFrontend(reporter, logger) with MinimalViperFrontendAPI +class MinimalSiliconFrontendAPI(override val reporter: Reporter) + extends SiliconFrontend(reporter) with MinimalViperFrontendAPI object SiliconRunner extends SiliconRunnerInstance { From c2b3f1635abbb504e0fa200f594b5b4401f52789 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Thu, 17 Aug 2023 15:46:08 +0000 Subject: [PATCH 63/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index c3cf35a73..8bd26f55d 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit c3cf35a73a1292d0b3c9f60039ca691c5b874ca6 +Subproject commit 8bd26f55d8b60e5e3a7bc09d6e52b996265a6dc4 From 8fdb9d50b91d3db58d2302ce84f64e2efb8a6e41 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 17 Aug 2023 17:48:32 +0200 Subject: [PATCH 64/74] Updating silver --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index afaf4523a..8bd26f55d 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit afaf4523a8429873c4f160713a22764162b12b21 +Subproject commit 8bd26f55d8b60e5e3a7bc09d6e52b996265a6dc4 From cb319dee9508059f8c8f93f064294230ee413fce Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Thu, 17 Aug 2023 17:54:48 +0000 Subject: [PATCH 65/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 8bd26f55d..c5ce6cd1a 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 8bd26f55d8b60e5e3a7bc09d6e52b996265a6dc4 +Subproject commit c5ce6cd1a12c778bd254c2f7d10ba44654f08378 From d4c8d849278dd2f4e96ec6d85d13a93a89bb1163 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Mon, 21 Aug 2023 15:36:49 +0000 Subject: [PATCH 66/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index c5ce6cd1a..0f16c1f02 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit c5ce6cd1a12c778bd254c2f7d10ba44654f08378 +Subproject commit 0f16c1f025a67de84f1ba7511aa19e19ae8e59eb From da038b8232dbfdbda221d621e3eb4355cefd335e Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 21 Aug 2023 22:41:13 +0200 Subject: [PATCH 67/74] Fixing issue #744 --- silver | 2 +- src/main/scala/supporters/functions/FunctionData.scala | 9 +++++++-- .../supporters/functions/FunctionVerificationUnit.scala | 4 ++-- 3 files changed, 10 insertions(+), 5 deletions(-) diff --git a/silver b/silver index 0f16c1f02..c7d57c2e0 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 0f16c1f025a67de84f1ba7511aa19e19ae8e59eb +Subproject commit c7d57c2e09eaec9279827098c93ec3a400e42702 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 From 084d7178c95a0ac4e0e3d5c869dd04b09397ce5e Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Mon, 21 Aug 2023 22:18:31 +0000 Subject: [PATCH 68/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index c7d57c2e0..56b74d1ab 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit c7d57c2e09eaec9279827098c93ec3a400e42702 +Subproject commit 56b74d1abcf7cfe4f9268f8df1bf015a736fd30c From 854b84c06cdb7e85d27540a782a849f5d880889c Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 22 Aug 2023 17:35:22 +0200 Subject: [PATCH 69/74] Reset the number of errors before verifying a new method --- src/main/scala/supporters/MethodSupporter.scala | 1 + 1 file changed, 1 insertion(+) 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. From fa5810e6d30237fc1ec05e1b13dbfc3ba2d2a906 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Fri, 25 Aug 2023 15:14:08 +0000 Subject: [PATCH 70/74] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 56b74d1ab..65ec3412b 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 56b74d1abcf7cfe4f9268f8df1bf015a736fd30c +Subproject commit 65ec3412bb9118a8c465462c94dab6d0d53da5f4 From 9b62b97765ffc2db805e3be4853515268ba55cda Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 12 Sep 2023 00:57:50 +0200 Subject: [PATCH 71/74] De-prioritize singleton chunks when we know none of them definitely fits --- src/main/scala/rules/QuantifiedChunkSupport.scala | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 09f1dca3b..67211833f 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -1761,7 +1761,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { if (greedyMatch.nonEmpty) { greedyMatch ++ chunks.diff(greedyMatch) } else { - fallback(chunks) + // 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 } } } From 67fc9a33c535de7184c8a9255736202e8816ba75 Mon Sep 17 00:00:00 2001 From: Dspil Date: Fri, 15 Sep 2023 17:35:51 +0200 Subject: [PATCH 72/74] benchmarking mods --- src/main/scala/rules/Brancher.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/scala/rules/Brancher.scala b/src/main/scala/rules/Brancher.scala index 625ca4918..0597ff5d2 100644 --- a/src/main/scala/rules/Brancher.scala +++ b/src/main/scala/rules/Brancher.scala @@ -56,13 +56,13 @@ object brancher extends BranchingRules { /* True if the then-branch is to be explored */ val executeThenBranch = ( skipPathFeasibilityCheck - || !v.decider.check(negatedCondition, Verifier.config.checkTimeout())) + ||{v.decider.prover.comment("branching!!!") ; !v.decider.check(negatedCondition, Verifier.config.checkTimeout())} || true) /* False if the then-branch is to be explored */ val executeElseBranch = ( !executeThenBranch /* Assumes that ast least one branch is feasible */ || skipPathFeasibilityCheck - || !v.decider.check(condition, Verifier.config.checkTimeout())) + || {v.decider.prover.comment("branching!!!") ; !v.decider.check(condition, Verifier.config.checkTimeout())} || true) val parallelizeElseBranch = s.parallelizeBranches && !s.underJoin && executeThenBranch && executeElseBranch From 1982e7358a3c29e36a270a0e88db080a4516aaa0 Mon Sep 17 00:00:00 2001 From: Dspil Date: Fri, 15 Sep 2023 17:38:34 +0200 Subject: [PATCH 73/74] Revert "benchmarking mods" This reverts commit 67fc9a33c535de7184c8a9255736202e8816ba75. --- src/main/scala/rules/Brancher.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/scala/rules/Brancher.scala b/src/main/scala/rules/Brancher.scala index 0597ff5d2..625ca4918 100644 --- a/src/main/scala/rules/Brancher.scala +++ b/src/main/scala/rules/Brancher.scala @@ -56,13 +56,13 @@ object brancher extends BranchingRules { /* True if the then-branch is to be explored */ val executeThenBranch = ( skipPathFeasibilityCheck - ||{v.decider.prover.comment("branching!!!") ; !v.decider.check(negatedCondition, Verifier.config.checkTimeout())} || true) + || !v.decider.check(negatedCondition, Verifier.config.checkTimeout())) /* False if the then-branch is to be explored */ val executeElseBranch = ( !executeThenBranch /* Assumes that ast least one branch is feasible */ || skipPathFeasibilityCheck - || {v.decider.prover.comment("branching!!!") ; !v.decider.check(condition, Verifier.config.checkTimeout())} || true) + || !v.decider.check(condition, Verifier.config.checkTimeout())) val parallelizeElseBranch = s.parallelizeBranches && !s.underJoin && executeThenBranch && executeElseBranch From 9069f59626d820e605456d5d09816587e2d49b6e Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 22 Sep 2023 13:43:49 +0200 Subject: [PATCH 74/74] Fixing unknown function error by recording snapshot masks --- src/main/scala/rules/Evaluator.scala | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 610cc514e..d8688acc8 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -1416,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() @@ -1502,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 @@ -1524,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 @@ -1552,7 +1562,7 @@ object evaluator extends EvaluationRules { Success() }) - (axioms, triggers, mostRecentTrig) + (axioms, triggers, mostRecentTrig, Seq(smDef1)) } /* Evaluate a sequence of expressions in Order