From 8d6209fd187a91e57e86751e369a457838d574cc Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sat, 27 May 2023 14:39:14 +0200 Subject: [PATCH 1/5] 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 2/5] 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 3/5] 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 67ecb967019013f307220eb3aae421683827bc80 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 31 May 2023 18:44:34 +0200 Subject: [PATCH 4/5] 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 5/5] 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