Merge pull request viperproject#724 from viperproject/meilers_mce_ann…

…otation MCE annotation
rvandoren · May 31, 2023 · 19b013b · 19b013b
2 parents 7a4c3e4 + 1856253
commit 19b013b
Show file tree

Hide file tree

Showing 4 changed files with 39 additions and 11 deletions.
diff --git a/silver b/silver
diff --git 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/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
@@ -32,8 +32,8 @@ import viper.silicon.utils.Counter
 import viper.silver.ast.{BackendType, Member}
 import viper.silver.ast.utility.rewriter.Traverse
 import viper.silver.cfg.silver.SilverCfg
-import viper.silver.reporter.{ConfigurationConfirmation, ExecutionTraceReport, Reporter, VerificationResultMessage, VerificationTerminationMessage, QuantifierChosenTriggersMessage, WarningsDuringTypechecking}
-import viper.silver.verifier.TypecheckerWarning
+import viper.silver.reporter.{AnnotationWarning, ConfigurationConfirmation, ExecutionTraceReport, QuantifierChosenTriggersMessage, Reporter, VerificationResultMessage, VerificationTerminationMessage, WarningsDuringVerification}
+import viper.silver.verifier.VerifierWarning
 
 /* TODO: Extract a suitable MainVerifier interface, probably including
  *         - def verificationPoolManager: VerificationPoolManager)
@@ -166,13 +166,13 @@ class DefaultMainVerifier(config: Config,
         case forall: ast.Forall if forall.isPure =>
           val res = viper.silicon.utils.ast.autoTrigger(forall, forall.autoTrigger)
           if (res.triggers.isEmpty)
-            reporter.report(WarningsDuringTypechecking(Seq(TypecheckerWarning("No triggers provided or inferred for quantifier.", res.pos))))
+            reporter.report(WarningsDuringVerification(Seq(VerifierWarning("No triggers provided or inferred for quantifier.", res.pos))))
           reporter report QuantifierChosenTriggersMessage(res, res.triggers)
           res
         case exists: ast.Exists =>
           val res = viper.silicon.utils.ast.autoTrigger(exists, exists.autoTrigger)
           if (res.triggers.isEmpty)
-            reporter.report(WarningsDuringTypechecking(Seq(TypecheckerWarning("No triggers provided or inferred for quantifier.", res.pos))))
+            reporter.report(WarningsDuringVerification(Seq(VerifierWarning("No triggers provided or inferred for quantifier.", res.pos))))
           reporter report QuantifierChosenTriggersMessage(res, res.triggers)
           res
       }, Traverse.BottomUp)
@@ -303,6 +303,21 @@ class DefaultMainVerifier(config: Config,
       case r => r
     }
 
+    val mce = member.info.getUniqueInfo[ast.AnnotationInfo] match {
+      case Some(ai) if ai.values.contains("exhaleMode") =>
+        ai.values("exhaleMode") match {
+          case Seq("0") | Seq("greedy") | Seq("2") | Seq("mceOnDemand") =>
+            if (Verifier.config.counterexample.isSupplied)
+              reporter report AnnotationWarning(s"Member ${member.name} has exhaleMode annotation that may interfere with counterexample generation.")
+            false
+          case Seq("1") | Seq("mce") | Seq("moreCompleteExhale") => true
+          case v =>
+            reporter report AnnotationWarning(s"Member ${member.name} has invalid exhaleMode annotation value $v. Annotation will be ignored.")
+            Verifier.config.exhaleMode == ExhaleMode.MoreComplete
+        }
+      case _ => Verifier.config.exhaleMode == ExhaleMode.MoreComplete
+    }
+
     State(program = program,
           functionData = functionData,
           predicateData = predicateData,
@@ -313,7 +328,7 @@ class DefaultMainVerifier(config: Config,
           predicateFormalVarMap = predSnapGenerator.formalVarMap,
           currentMember = Some(member),
           heapDependentTriggers = resourceTriggers,
-          moreCompleteExhale = Verifier.config.exhaleMode == ExhaleMode.MoreComplete)
+          moreCompleteExhale = mce)
   }
 
   private def createInitialState(@unused cfg: SilverCfg,
+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