@@ -12,6 +12,7 @@ import viper.silver.ast._
1212import viper .silver .parser .FastParserCompanion .whitespace
1313import viper .silver .parser .FastParser
1414import viper .silver .plugin .{ParserPluginTemplate , SilverPlugin }
15+ import viper .silver .reporter .Entity
1516import viper .silver .verifier ._
1617import viper .silver .verifier .errors .AssertFailed
1718
@@ -27,8 +28,6 @@ class RefutePlugin(@unused reporter: viper.silver.reporter.Reporter,
2728 /** Keyword used to define refute statements. */
2829 private val refuteKeyword : String = " refute"
2930
30- private var refuteAsserts : Map [Position , Refute ] = Map ()
31-
3231 /** Parser for refute statements. */
3332 def refute [_ : P ]: P [PRefute ] =
3433 FP (keyword(refuteKeyword) ~/ exp).map{ case (pos, e) => PRefute (e)(pos) }
@@ -46,40 +45,62 @@ class RefutePlugin(@unused reporter: viper.silver.reporter.Reporter,
4645 * Remove refute statements from the AST and add them as non-det asserts.
4746 * The ⭐ is nice since such a variable name cannot be parsed, but will it cause issues?
4847 */
49- override def beforeVerify (input : Program ): Program =
50- ViperStrategy .Slim ({
51- case r@ Refute (exp) => {
52- this .refuteAsserts += (r.pos -> r)
53- Seqn (Seq (
54- If (LocalVar (s " __plugin_refute_nondet ${this .refuteAsserts.size}" , Bool )(r.pos),
55- Seqn (Seq (
56- Assert (exp)(r.pos, RefuteInfo ),
57- Inhale (BoolLit (false )(r.pos))(r.pos)
58- ), Seq ())(r.pos),
59- Seqn (Seq (), Seq ())(r.pos))(r.pos)
48+ override def beforeVerify (input : Program ): Program = {
49+ val transformedMethods = input.methods.map(method => {
50+ var refutesInMethod = 0
51+ ViperStrategy .Slim ({
52+ case r@ Refute (exp) =>
53+ refutesInMethod += 1
54+ val nonDetLocalVarDecl = LocalVarDecl (s " __plugin_refute_nondet $refutesInMethod" , Bool )(r.pos)
55+ Seqn (Seq (
56+ If (nonDetLocalVarDecl.localVar,
57+ Seqn (Seq (
58+ Assert (exp)(r.pos, RefuteInfo (r)),
59+ Inhale (BoolLit (false )(r.pos))(r.pos)
60+ ), Seq ())(r.pos),
61+ Seqn (Seq (), Seq ())(r.pos))(r.pos)
6062 ),
61- Seq (LocalVarDecl (s " __plugin_refute_nondet ${this .refuteAsserts.size}" , Bool )(r.pos))
62- )(r.pos)
63- }
64- }).recurseFunc({
65- case Method (_, _, _, _, _, body) => Seq (body)
66- }).execute(input)
63+ Seq (nonDetLocalVarDecl)
64+ )(r.pos)
65+ }).recurseFunc({
66+ case Method (_, _, _, _, _, body) => Seq (body)
67+ }).execute[Method ](method)
68+ })
69+ Program (input.domains, input.fields, input.functions, input.predicates, transformedMethods, input.extensions)(input.pos, input.info, input.errT)
70+ }
71+
72+ /** Remove refutation related errors for the current entity and add refuteAsserts in this entity that didn't report an error. */
73+ override def mapEntityVerificationResult (entity : Entity , input : VerificationResult ): VerificationResult =
74+ mapVerificationResultsForNode(entity, input)
6775
68- /** Remove refutation related errors and add refuteAsserts that didn't report an error. */
69- override def mapVerificationResult (input : VerificationResult ): VerificationResult = {
70- val errors : Seq [AbstractError ] = (input match {
71- case Success => Seq ()
72- case Failure (errors) => {
73- errors.filter {
74- case AssertFailed (a, _, _) if a.info == RefuteInfo => {
75- this .refuteAsserts -= a.pos
76- false
77- }
78- case _ => true
79- }
76+ /** Remove refutation related errors (for all entities) and add refuteAsserts (for all entities) that didn't report an error. */
77+ override def mapVerificationResult (program : Program , input : VerificationResult ): VerificationResult =
78+ mapVerificationResultsForNode(program, input)
79+
80+ private def mapVerificationResultsForNode (n : Node , input : VerificationResult ): VerificationResult = {
81+ val (refutesForWhichErrorOccurred, otherErrors) = input match {
82+ case Success => (Seq .empty, Seq .empty)
83+ case Failure (errors) => errors.partitionMap {
84+ case AssertFailed (NodeWithInfo (RefuteInfo (r)), _, _) => Left ((r, r.pos))
85+ case err => Right (err)
8086 }
81- }) ++ this .refuteAsserts.map(r => RefuteFailed (r._2, RefutationTrue (r._2.exp)))
82- if (errors.length == 0 ) Success
87+ }
88+ val refutesContainedInNode = n.collect {
89+ case NodeWithInfo (RefuteInfo (r)) => (r, r.pos)
90+ }
91+ // note that we include positional information in `refutesForWhichErrorOccurred` and `refutesContainedInNode` such
92+ // that we do not miss errors just because the same refute statement occurs multiple times
93+ val refutesForWhichNoErrorOccurred = refutesContainedInNode.filterNot(refutesForWhichErrorOccurred.contains(_))
94+ val missingErrorsInNode = refutesForWhichNoErrorOccurred.map{
95+ case (refute, _) => RefuteFailed (refute, RefutationTrue (refute.exp))
96+ }
97+
98+ val errors = otherErrors ++ missingErrorsInNode
99+ if (errors.isEmpty) Success
83100 else Failure (errors)
84101 }
85102}
103+
104+ object NodeWithInfo {
105+ def unapply (node : Node ) : Option [Info ] = Some (node.meta._2)
106+ }
0 commit comments