Add refutation support

src/main/scala/viper/silver/ast/Ast.scala

@@ -397,6 +397,14 @@ case object Synthesized extends Info {
   lazy val isCached = false
 }
 
+/** An `Info` instance for labelling an AST node which is expected to fail verification.
+ * This is used by Silicon to avoid stopping verification.
+*/
+class ExpectFail extends Info {
+  lazy val comment = Nil
+  lazy val isCached = false
+}
+
 /** An `Info` instance for composing multiple `Info`s together */
 case class ConsInfo(head: Info, tail: Info) extends Info {
   lazy val comment = head.comment ++ tail.comment

src/main/scala/viper/silver/frontend/SilFrontend.scala

@@ -83,6 +83,7 @@ trait SilFrontend extends DefaultFrontend {
   private val defaultPlugins: Seq[String] = Seq(
     "viper.silver.plugin.standard.adt.AdtPlugin",
     "viper.silver.plugin.standard.termination.TerminationPlugin",
+    "viper.silver.plugin.standard.refute.RefutePlugin",
     "viper.silver.plugin.standard.predicateinstance.PredicateInstancePlugin"
   )
   /** For testing of plugin import feature */

src/main/scala/viper/silver/plugin/standard/refute/RefuteASTExtension.scala

@@ -0,0 +1,20 @@
+// 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-2022 ETH Zurich.
+
+package viper.silver.plugin.standard.refute
+
+import viper.silver.ast._
+import viper.silver.ast.pretty.FastPrettyPrinter.{ContOps, text, toParenDoc}
+import viper.silver.ast.pretty.PrettyPrintPrimitives
+
+/** An `ExpectFail` info that tells us that this assert is a refute. */
+case object RefuteInfo extends ExpectFail
+
+case class Refute(exp: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends ExtensionStmt {
+  override lazy val prettyPrint: PrettyPrintPrimitives#Cont = text("refute") <+> toParenDoc(exp)
+
+  override val extensionSubnodes: Seq[Node] = Seq(exp)
+}

src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala

@@ -0,0 +1,29 @@
+// 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-2022 ETH Zurich.
+
+package viper.silver.plugin.standard.refute
+
+import viper.silver.verifier._
+
+case class RefuteFailed(override val offendingNode: Refute,
+                                    override val reason: ErrorReason,
+                                    override val cached: Boolean = false) extends AbstractVerificationError {
+  override val id = "refute.failed"
+  override val text = s"Refute holds in all cases or could not be reached (e.g. see Silicon `numberOfErrorsToReport`)."
+
+  override def withNode(offendingNode: errors.ErrorNode = this.offendingNode): RefuteFailed =
+    RefuteFailed(this.offendingNode, this.reason, this.cached)
+
+  override def withReason(r: ErrorReason): RefuteFailed = RefuteFailed(offendingNode, r, cached)
+}
+
+case class RefutationTrue(offendingNode: reasons.ErrorNode) extends AbstractErrorReason {
+  override val id: String = "refutation.true"
+
+  override val readableMessage: String = s"Assertion $offendingNode definitely holds."
+
+  override def withNode(offendingNode: reasons.ErrorNode): ErrorMessage = RefutationTrue(offendingNode)
+}

src/main/scala/viper/silver/plugin/standard/refute/RefutePASTExtension.scala

@@ -0,0 +1,22 @@
+// 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-2022 ETH Zurich.
+
+package viper.silver.plugin.standard.refute
+
+import viper.silver.ast.{Position, Stmt}
+import viper.silver.parser.TypeHelper.Bool
+import viper.silver.parser._
+
+case class PRefute(e: PExp)(val pos: (Position, Position)) extends PExtender with PStmt {
+  override val getSubnodes: Seq[PNode] = Seq(e)
+
+  override def typecheck(t: TypeChecker, n: NameAnalyser):Option[Seq[String]] = {
+    t.check(e, Bool)
+    None
+  }
+
+  override def translateStmt(t: Translator): Stmt = Refute(t.exp(e))(t.liftPos(this))
+}

src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala

@@ -0,0 +1,78 @@
+// 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-2022 ETH Zurich.
+
+package viper.silver.plugin.standard.refute
+
+import fastparse.P
+import viper.silver.ast.utility.ViperStrategy
+import viper.silver.ast._
+import viper.silver.parser.FastParser.{FP, exp, keyword, whitespace}
+import viper.silver.parser.ParserExtension
+import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin}
+import viper.silver.verifier._
+import viper.silver.verifier.errors.AssertFailed
+
+class RefutePlugin extends SilverPlugin with ParserPluginTemplate {
+
+  /** Keyword used to define refute statements. */
+  private val RefuteKeyword: String = "refute"
+
+  private var RefuteAsserts: Map[Position, Refute] = Map()
+
+  /** Parser for refute statements. */
+  def refute[_: P]: P[PRefute] =
+    FP(keyword(RefuteKeyword) ~/ exp).map{ case (pos, e) => PRefute(e)(pos) }
+
+  /** Add refute to the parser. */
+  override def beforeParse(input: String, isImported: Boolean): String = {
+    // Add new keyword
+    ParserExtension.addNewKeywords(Set[String](RefuteKeyword))
+    // Add new parser to the precondition
+    ParserExtension.addNewStmtAtEnd(refute(_))
+    input
+  }
+
+  /**
+   * Remove refute statements from the AST and add them as non-det asserts.
+   * The ⭐ is nice since such a variable name cannot be parsed, but will it cause issues?
+   */
+  override def beforeVerify(input: Program): Program = 
+    ViperStrategy.Slim({
+      case r@Refute(exp) => {
+        this.RefuteAsserts += (r.pos -> r)
+        Seqn(Seq(
+          If(LocalVar("⭐", Bool)(r.pos),
+            Seqn(Seq(
+              Assert(exp)(r.pos, RefuteInfo),
+              Inhale(BoolLit(false)(r.pos))(r.pos)
+            ), Seq())(r.pos),
+            Seqn(Seq(), Seq())(r.pos))(r.pos)
+          ),
+          Seq(LocalVarDecl("⭐", Bool)(r.pos))
+        )(r.pos)
+      }
+    }).recurseFunc({
+      case Method(_, _, _, _, _, body) => Seq(body)
+    }).execute(input)
+
+  /** Remove refutation related errors and add RefuteAsserts that didn't report an error. */
+  override def mapVerificationResult(input: VerificationResult): VerificationResult = {
+    val errors: Seq[AbstractError] = (input match {
+      case Success => Seq()
+      case Failure(errors) => {
+        errors.filter {
+          case AssertFailed(a, _, _) if a.info == RefuteInfo => {
+            this.RefuteAsserts -= a.pos
+            false
+          }
+          case _ => true
+        }
+      }
+    }) ++ this.RefuteAsserts.map(r => RefuteFailed(r._2, RefutationTrue(r._2.exp)))
+    if (errors.length == 0) Success
+    else Failure(errors)
+  }
+}

src/main/scala/viper/silver/verifier/VerificationError.scala

@@ -153,6 +153,10 @@ trait ErrorMessage {
 
   // Should consider refactoring as a transformer, if/once we make the error message structure recursive
   def withNode(offendingNode: errors.ErrorNode = this.offendingNode) : ErrorMessage
+
+  // Check if the offendingNode contains any `ExpectFail` info tags
+  def isExpected: Boolean = if (!offendingNode.isInstanceOf[Infoed]) false
+    else offendingNode.asInstanceOf[Infoed].info.getUniqueInfo[ExpectFail].isDefined
 }
 
 trait VerificationError extends AbstractError with ErrorMessage {

src/test/resources/refute/simple.vpr

@@ -0,0 +1,18 @@
+method foo(x: Int) returns (r: Int)
+    requires x > 10
+{
+    refute !(x > 0)
+    //:: ExpectedOutput(refute.failed:refutation.true)
+    refute x > 0
+    refute false
+    //:: ExpectedOutput(refute.failed:refutation.true)
+    refute true
+    refute false
+    if (x > 0) {
+        r := x
+    } else {
+        //:: ExpectedOutput(refute.failed:refutation.true)
+        refute false
+        r := 0
+    }
+}