Skip to content

MCE annotation #724

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
marcoeilers merged 6 commits into from
May 31, 2023
Merged

MCE annotation #724

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
8d6209f
Reading exhaleMode annotation to set MCE locally. Also using new Warn…
marcoeilers May 27, 2023
38879f8
Updated Silver reference
marcoeilers May 27, 2023
658f293
Updated silver reference
marcoeilers May 27, 2023
67ecb96
Updated silver reference
marcoeilers May 31, 2023
1e3c903
Merge branch 'master' into meilers_mce_annotation
marcoeilers May 31, 2023
1856253
Supporting mce on demand via annotation
marcoeilers May 31, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion silver
Open in desktop
Submodule silver updated 5 files
+9 −0 src/main/scala/viper/silver/reporter/Message.scala
+12 −0 src/main/scala/viper/silver/reporter/Reporter.scala
+7 −0 src/main/scala/viper/silver/verifier/VerificationResult.scala
+66 −0 src/test/resources/all/annotation/annotationMCE.vpr
+3 −0 src/test/resources/all/annotation/annotationSuccess.vpr
8 changes: 4 additions & 4 deletions src/main/scala/rules/Evaluator.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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)
}
}
Expand Down
25 changes: 20 additions & 5 deletions src/main/scala/verifier/DefaultMainVerifier.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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

@jcp19 jcp19 May 31, 2023 •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does this mean that we wouldn't be able to annotate Viper to use moreCompleteExhale on demand for a method?

@marcoeilers marcoeilers May 31, 2023

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Right. Basically, MCE on demand is a global setting; if that's set, Silicon will always switch to MCE on retry. This annotation sets the default for the given method.

I could change that though.

@jcp19 jcp19 May 31, 2023

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In the router package in SCION, I have an example where I want the package to be verified with mce, except for a particular method where mceOnDemand is useful. With the current approach, I would need to set-up the mode as mce on demand and potentially have to annotate almost all methods with mce (which is fine, only a bit verbose). If adding the option for mce on demand requires only small changes to silicon, I would be grateful for that feature. Otherwise, I wouldn't bother changing it.

@marcoeilers marcoeilers May 31, 2023

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done.

case v =>
reporter report AnnotationWarning(s"Member ${member.name} has invalid exhaleMode annotation value $v. Annotation will be ignored.")

@jcp19 jcp19 May 31, 2023

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would reject this one via a consistency check instead of reporting a warning (I think it might be very easy for a front-end developer to miss the warning otherwise)

@marcoeilers marcoeilers May 31, 2023

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Mh I'm not sure. A consistency check is an AST-level check that's usually independent of the backend, right, and this is a backend-specific annotation. So we'd either need to build in checks regarding what a correct annotation is right into the AnnotationInfo AST node, which seems wrong to me, since annotations should in principle allow you to add all kinds of stuff in a flexible way. Or it wouldn't be a consistency check and we'd return an AnnotationError here instead, so you wouldn't be able to ignore it.
This might actually be something we should discuss with more people, since this will come up again and again.

@jcp19 jcp19 May 31, 2023 •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think you are right about reporting consistency errors for annotations. At first sight, reporting an AnnotationError here instead of AnnotationWarning sounds like the best option.

@marcoeilers marcoeilers May 31, 2023

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah I can see that. Actually the more I think about it the more a backend-specific consistency check would also make sense. But I think this is just something we need to discuss and decide once and for all, for annotations in general. I think it's not super clear what's best. IMO warnings could also make sense:

  • We at some point had the idea that it should always be sound to ignore an annotation.
  • We can't reliably flag errors for all potential problems here. E.g. we would detect @exhaleMode("nce") but not @exhaleNode("mce"). For the latter we can't flag an error (at most a warning), it's just an annotation we don't recognize, and we can't flag errors for all annotations we don't recognize since otherwise Carbon would have to reject all programs with Silicon-specific annotations.

So I'd suggest going with the warning for now and making sure we discuss this asap. Changing this to an error would be super quick and simple of course.

Verifier.config.exhaleMode == ExhaleMode.MoreComplete
}
case _ => Verifier.config.exhaleMode == ExhaleMode.MoreComplete
}

State(program = program,
functionData = functionData,
predicateData = predicateData,
Expand All @@ -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,
Expand Down
⚡