From 9fc9067726387f2d08855486558e52d9c00e768c Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Tue, 24 Jun 2025 12:29:48 +0200 Subject: [PATCH] Renamed proverArgs annotation, cleaned up annotation handling code, enabled proverConfigArgs annotation for functions --- silver | 2 +- src/main/scala/rules/Brancher.scala | 14 +-- .../scala/rules/ExecutionFlowController.scala | 19 ++-- .../supporters/AnnotationSupporter.scala | 106 ++++++++++++++++++ .../scala/supporters/MethodSupporter.scala | 17 +-- .../functions/FunctionVerificationUnit.scala | 7 +- src/main/scala/verifier/BaseVerifier.scala | 22 +--- .../scala/verifier/DefaultMainVerifier.scala | 45 ++------ 8 files changed, 141 insertions(+), 91 deletions(-) create mode 100644 src/main/scala/supporters/AnnotationSupporter.scala diff --git a/silver b/silver index 4093accb3..f49194125 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 4093accb3069e0fa13edfb14207e12d3e535168e +Subproject commit f49194125dd3a5edc5d1ecbd689864a474b9c66c diff --git a/src/main/scala/rules/Brancher.scala b/src/main/scala/rules/Brancher.scala index fc2422b49..3c1cf3240 100644 --- a/src/main/scala/rules/Brancher.scala +++ b/src/main/scala/rules/Brancher.scala @@ -88,10 +88,10 @@ object brancher extends BranchingRules { val uidBranchPoint = v.symbExLog.insertBranchPoint(2, Some(condition), Some(conditionExp._1)) var functionsOfCurrentDecider: Set[FunctionDecl] = null var macrosOfCurrentDecider: Vector[MacroDecl] = null - var proverArgsOfCurrentDecider: viper.silicon.Map[String, String] = null + var proverConfigArgsOfCurrentDecider: viper.silicon.Map[String, String] = null var wasElseExecutedOnDifferentVerifier = false var functionsOfElseBranchDecider: Set[FunctionDecl] = null - var proverArgsOfElseBranchDecider: viper.silicon.Map[String, String] = null + var proverConfigArgsOfElseBranchDecider: viper.silicon.Map[String, String] = null var macrosOfElseBranchDecider: Seq[MacroDecl] = null var pcsForElseBranch: PathConditionStack = null var noOfErrors = 0 @@ -109,7 +109,7 @@ object brancher extends BranchingRules { if (parallelizeElseBranch){ functionsOfCurrentDecider = v.decider.freshFunctions macrosOfCurrentDecider = v.decider.freshMacros - proverArgsOfCurrentDecider = v.decider.getProverOptions() + proverConfigArgsOfCurrentDecider = v.decider.getProverOptions() pcsForElseBranch = v.decider.pcs.duplicate() noOfErrors = v.errorsReportedSoFar.get() } @@ -127,9 +127,9 @@ object brancher extends BranchingRules { val newMacros = macrosOfCurrentDecider.filter(m => !v0FreshMacros.contains(m)) v0.decider.prover.comment(s"[Shifting execution from ${v.uniqueId} to ${v0.uniqueId}]") - proverArgsOfElseBranchDecider = v0.decider.getProverOptions() + proverConfigArgsOfElseBranchDecider = v0.decider.getProverOptions() v0.decider.resetProverOptions() - v0.decider.setProverOptions(proverArgsOfCurrentDecider) + v0.decider.setProverOptions(proverConfigArgsOfCurrentDecider) v0.decider.prover.comment(s"Bulk-declaring functions") v0.decider.declareAndRecordAsFreshFunctions(newFunctions) v0.decider.prover.comment(s"Bulk-declaring macros") @@ -159,7 +159,7 @@ object brancher extends BranchingRules { val result = fElse(v1.stateConsolidator(s1).consolidateOptionally(s1, v1), v1) if (wasElseExecutedOnDifferentVerifier) { v1.decider.resetProverOptions() - v1.decider.setProverOptions(proverArgsOfElseBranchDecider) + v1.decider.setProverOptions(proverConfigArgsOfElseBranchDecider) if (s.underJoin) { functionsOfElseBranchDecider = v1.decider.freshFunctions -- functionsOfElseBranchdDeciderBefore macrosOfElseBranchDecider = v1.decider.freshMacros.drop(nMacrosOfElseBranchDeciderBefore) @@ -226,7 +226,7 @@ object brancher extends BranchingRules { v.errorsReportedSoFar.set(noOfErrorsAfterThenBranch) v.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract) v.decider.resetProverOptions() - v.decider.setProverOptions(proverArgsOfCurrentDecider) + v.decider.setProverOptions(proverConfigArgsOfCurrentDecider) } } else { rs = elseBranchFuture.get() diff --git a/src/main/scala/rules/ExecutionFlowController.scala b/src/main/scala/rules/ExecutionFlowController.scala index 8cc287d0f..96d4a4de7 100644 --- a/src/main/scala/rules/ExecutionFlowController.scala +++ b/src/main/scala/rules/ExecutionFlowController.scala @@ -11,6 +11,7 @@ import viper.silicon.Config.ExhaleMode import viper.silicon.interfaces._ import viper.silicon.logger.records.data.CommentRecord import viper.silicon.state.State +import viper.silicon.supporters.AnnotationSupporter import viper.silicon.verifier.Verifier trait ExecutionFlowRules extends SymbolicExecutionRules { @@ -130,17 +131,13 @@ object executionFlowController extends ExecutionFlowRules { val comLog = new CommentRecord("Retry", s0, v.decider.pcs) val sepIdentifier = v.symbExLog.openScope(comLog) - 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 + val temporaryMCE = s0.currentMember.flatMap(AnnotationSupporter.getExhaleMode(_, v.reporter)) match { + case Some(ExhaleMode.Greedy) => + false + case Some(ExhaleMode.MoreComplete) | Some(ExhaleMode.MoreCompleteOnDemand) => + true + case _ => + Verifier.config.exhaleMode != ExhaleMode.Greedy } action(s0.copy(retrying = true, retryLevel = s.retryLevel, moreCompleteExhale = temporaryMCE), v, (s1, r, v1) => { diff --git a/src/main/scala/supporters/AnnotationSupporter.scala b/src/main/scala/supporters/AnnotationSupporter.scala new file mode 100644 index 000000000..5b12cdfac --- /dev/null +++ b/src/main/scala/supporters/AnnotationSupporter.scala @@ -0,0 +1,106 @@ +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. +// +// Copyright (c) 2011-2025 ETH Zurich. + +package viper.silicon.supporters + +import viper.silicon.Config.JoinMode.JoinMode +import viper.silicon.Config.StateConsolidationMode._ +import viper.silicon.Config.{ExhaleMode, JoinMode, StateConsolidationMode} +import viper.silicon.{Map, toMap} +import viper.silver.ast +import viper.silver.reporter.{AnnotationWarning, Reporter} + +object AnnotationSupporter { + val proverConfigAnnotation = "proverConfigArgs" + val exhaleModeAnnotation = "exhaleMode" + val joinModeAnnotation = "moreJoins" + val stateConsolidationModeAnnotation = "stateConsolidationMode" + + def getProverConfigArgs(member: ast.Member, reporter: Reporter): Map[String, String] = { + member.info.getUniqueInfo[ast.AnnotationInfo] match { + case Some(ai) if ai.values.contains(proverConfigAnnotation) => + toMap(ai.values(proverConfigAnnotation).flatMap(o => { + val index = o.indexOf("=") + if (index == -1) { + reporter report AnnotationWarning(s"Invalid ${proverConfigAnnotation} annotation ${o} on member ${member.name}. " + + s"Required format for each option is optionName=value.") + None + } else { + val (name, value) = (o.take(index), o.drop(index + 1)) + Some((name, value)) + } + })) + case _ => + Map.empty + } + } + + def getExhaleMode(member: ast.Member, reporter: Reporter): Option[ExhaleMode] = { + member.info.getUniqueInfo[ast.AnnotationInfo] match { + case Some(ai) if ai.values.contains(exhaleModeAnnotation) => + ai.values(exhaleModeAnnotation) match { + case Seq("0") | Seq("greedy") => + Some(ExhaleMode.Greedy) + case Seq("1") | Seq("mce") | Seq("moreCompleteExhale") => Some(ExhaleMode.MoreComplete) + case Seq("2") | Seq("mceOnDemand") => + Some(ExhaleMode.MoreCompleteOnDemand) + case v => + reporter report AnnotationWarning(s"Member ${member.name} has invalid ${exhaleModeAnnotation} annotation value $v. Annotation will be ignored.") + None + } + case _ => None + } + } + + def getJoinMode(member: ast.Member, reporter: Reporter): Option[JoinMode] = { + member.info.getUniqueInfo[ast.AnnotationInfo] match { + case Some(ai) if ai.values.contains(joinModeAnnotation) => + ai.values(joinModeAnnotation) match { + case Seq() | Seq("all") => Some(JoinMode.All) + case Seq("off") => Some(JoinMode.Off) + case Seq("impure") => Some(JoinMode.Impure) + case Seq(vl) => + try { + Some(JoinMode(vl.toInt)) + } catch { + case _: NumberFormatException => + reporter report AnnotationWarning(s"Member ${member.name} has invalid ${joinModeAnnotation} annotation value $vl. Annotation will be ignored.") + None + } + case v => + reporter report AnnotationWarning(s"Member ${member.name} has invalid ${joinModeAnnotation} annotation value $v. Annotation will be ignored.") + None + } + case _ => None + } + } + + def getStateConsolidationMode(member: ast.Member, reporter: Reporter): Option[StateConsolidationMode] = { + member.info.getUniqueInfo[ast.AnnotationInfo] match { + case Some(ai) if ai.values.contains(stateConsolidationModeAnnotation) => + val modeAnnotation = ai.values(stateConsolidationModeAnnotation) + try { + val mode = modeAnnotation match { + case Seq("minimal") => Minimal + case Seq("default") => Default + case Seq("retrying") => Retrying + case Seq("minimalRetrying") => MinimalRetrying + case Seq("moreCompleteExhale") => MoreCompleteExhale + case Seq("lastRetry") => LastRetry + case Seq("retryingFailOnly") => RetryingFailOnly + case Seq("lastRetryFailOnly") => LastRetryFailOnly + case Seq(v) => StateConsolidationMode(v.toInt) + } + Some(mode) + } catch { + case _ => + reporter report AnnotationWarning(s"Member ${member.name} has invalid ${stateConsolidationModeAnnotation} annotation value. Annotation will be ignored.") + None + } + case _ => None + } + } +} diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index 9b483ff4a..9e74b9e44 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/src/main/scala/supporters/MethodSupporter.scala @@ -46,22 +46,7 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif logger.debug("\n\n" + "-" * 10 + " METHOD " + method.name + "-" * 10 + "\n") decider.prover.comment("%s %s %s".format("-" * 10, method.name, "-" * 10)) - val proverOptions: Map[String, String] = method.info.getUniqueInfo[ast.AnnotationInfo] match { - case Some(ai) if ai.values.contains("proverArgs") => - toMap(ai.values("proverArgs").flatMap(o => { - val index = o.indexOf("=") - if (index == -1) { - reporter report AnnotationWarning(s"Invalid proverArgs annotation ${o} on method ${method.name}. " + - s"Required format for each option is optionName=value.") - None - } else { - val (name, value) = (o.take(index), o.drop(index + 1)) - Some((name, value)) - } - })) - case _ => - Map.empty - } + val proverOptions: Map[String, String] = AnnotationSupporter.getProverConfigArgs(method, reporter) v.decider.setProverOptions(proverOptions) openSymbExLogger(method) diff --git a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala index 8e83c0973..b877b511f 100644 --- a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala +++ b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala @@ -22,7 +22,7 @@ import viper.silicon.state.terms.predef.`?s` import viper.silicon.common.collections.immutable.InsertionOrderedSet import viper.silicon.decider.Decider import viper.silicon.rules.{consumer, evaluator, executionFlowController, producer} -import viper.silicon.supporters.PredicateData +import viper.silicon.supporters.{AnnotationSupporter, PredicateData} import viper.silicon.utils.ast.{BigAnd, simplifyVariableName} import viper.silicon.verifier.{Verifier, VerifierComponent} import viper.silicon.utils.{freshSnap, toSf} @@ -150,6 +150,9 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver logger.debug(s"\n\n$comment\n") decider.prover.comment(comment) + val proverOptions: Map[String, String] = AnnotationSupporter.getProverConfigArgs(function, reporter) + v.decider.setProverOptions(proverOptions) + openSymbExLogger(function) val data = functionData(function) @@ -157,6 +160,8 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver decider.prover.declare(ConstDecl(data.formalResult)) val res = Seq(handleFunction(sInit, function)) + + v.decider.resetProverOptions() symbExLog.closeMemberScope() res } diff --git a/src/main/scala/verifier/BaseVerifier.scala b/src/main/scala/verifier/BaseVerifier.scala index 36820148f..7c1cf2081 100644 --- a/src/main/scala/verifier/BaseVerifier.scala +++ b/src/main/scala/verifier/BaseVerifier.scala @@ -73,26 +73,8 @@ abstract class BaseVerifier(val config: Config, val mode = s.currentMember match { case Some(member) => - member.info.getUniqueInfo[ast.AnnotationInfo] match { - case Some(ai) if ai.values.contains("stateConsolidationMode") => - val modeAnnotation = ai.values("stateConsolidationMode") - try { - modeAnnotation match { - case Seq("minimal") => Minimal - case Seq("default") => Default - case Seq("retrying") => Retrying - case Seq("minimalRetrying") => MinimalRetrying - case Seq("moreCompleteExhale") => MoreCompleteExhale - case Seq("lastRetry") => LastRetry - case Seq("retryingFailOnly") => RetryingFailOnly - case Seq("lastRetryFailOnly") => LastRetryFailOnly - case Seq(v) => StateConsolidationMode(v.toInt) - } - } catch { - case _ => - reporter report AnnotationWarning(s"Member ${member.name} has invalid stateConsolidationMode annotation value. Annotation will be ignored.") - config.stateConsolidationMode() - } + AnnotationSupporter.getStateConsolidationMode(member, reporter) match { + case Some(mode) => mode case _ => config.stateConsolidationMode() } case None => config.stateConsolidationMode() diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index e9450aa9c..a7b5a7911 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -26,7 +26,7 @@ import viper.silicon.logger.{MemberSymbExLogger, SymbExLogger} import viper.silicon.reporting.{MultiRunRecorders, condenseToViperResult} import viper.silicon.state._ import viper.silicon.state.terms.{Decl, Sort, Term, sorts} -import viper.silicon.supporters.{DefaultDomainsContributor, DefaultMapsContributor, DefaultMultisetsContributor, DefaultPredicateVerificationUnitProvider, DefaultSequencesContributor, DefaultSetsContributor, MagicWandSnapFunctionsContributor, PredicateData} +import viper.silicon.supporters.{AnnotationSupporter, DefaultDomainsContributor, DefaultMapsContributor, DefaultMultisetsContributor, DefaultPredicateVerificationUnitProvider, DefaultSequencesContributor, DefaultSetsContributor, MagicWandSnapFunctionsContributor, PredicateData} import viper.silicon.supporters.qps._ import viper.silicon.supporters.functions.{DefaultFunctionVerificationUnitProvider, FunctionData} import viper.silicon.utils.Counter @@ -321,40 +321,15 @@ class DefaultMainVerifier(config: Config, case r => r } - val mce = member.info.getUniqueInfo[ast.AnnotationInfo] match { - case Some(ai) if ai.values.contains("exhaleMode") => - ai.values("exhaleMode") match { - case Seq("0") | Seq("greedy") | Seq("2") | Seq("mceOnDemand") => - if (Verifier.config.counterexample.isSupplied) - reporter report AnnotationWarning(s"Member ${member.name} has exhaleMode annotation that may interfere with counterexample generation.") - false - case Seq("1") | Seq("mce") | Seq("moreCompleteExhale") => true - case v => - reporter report AnnotationWarning(s"Member ${member.name} has invalid exhaleMode annotation value $v. Annotation will be ignored.") - Verifier.config.exhaleMode == ExhaleMode.MoreComplete - } - case _ => Verifier.config.exhaleMode == ExhaleMode.MoreComplete - } - val moreJoinsAnnotated = member.info.getUniqueInfo[ast.AnnotationInfo] match { - case Some(ai) if ai.values.contains("moreJoins") => - ai.values("moreJoins") match { - case Seq() | Seq("all") => Some(JoinMode.All) - case Seq("off") => Some(JoinMode.Off) - case Seq("impure") => Some(JoinMode.Impure) - case Seq(vl) => - try { - Some(JoinMode(vl.toInt)) - } catch { - case _: NumberFormatException => - reporter report AnnotationWarning(s"Member ${member.name} has invalid moreJoins annotation value $vl. Annotation will be ignored.") - None - } - case v => - reporter report AnnotationWarning(s"Member ${member.name} has invalid moreJoins annotation value $v. Annotation will be ignored.") - None - } - case _ => None + val mce = AnnotationSupporter.getExhaleMode(member, reporter) match { + case Some(ExhaleMode.MoreComplete) => true + case Some(ExhaleMode.Greedy) | Some(ExhaleMode.MoreCompleteOnDemand) => + if (Verifier.config.counterexample.isSupplied) + reporter report AnnotationWarning(s"Member ${member.name} has exhaleMode annotation that may interfere with counterexample generation.") + false + case None => Verifier.config.exhaleMode == ExhaleMode.MoreComplete } + val moreJoinsAnnotated = AnnotationSupporter.getJoinMode(member, reporter) val moreJoins = if (member.isInstanceOf[ast.Method]) { moreJoinsAnnotated.getOrElse(Verifier.config.moreJoins.getOrElse(JoinMode.Off)) } else { @@ -452,7 +427,7 @@ class DefaultMainVerifier(config: Config, if (smt2ConfigOptions.nonEmpty) { // One can pass options to the prover. This allows to check whether they have been received. - val msg = s"Additional prover configuration options are '${config.proverConfigArgs}'" + val msg = s"Additional prover configuration options are '${config.proverConfigArgs.mkString(", ")}'" reporter report ConfigurationConfirmation(msg) logger info msg preambleReader.emitPreamble(smt2ConfigOptions, sink, true)