Add refutation support (#583)

* Add refutation plugin

Author: JonasAlaif

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

@@ -367,40 +367,48 @@ trait Info {
 
 /** A default `Info` that is empty. */
 case object NoInfo extends Info {
-  lazy val comment = Nil
-  lazy val isCached = false
+  override val comment = Nil
+  override val isCached = false
 }
 
 /** A simple `Info` that contains a list of comments. */
 case class SimpleInfo(comment: Seq[String]) extends Info {
-  lazy val isCached = false
+  override val isCached = false
 }
 
 /** An `Info` instance for labelling a quantifier as auto-triggered. */
 case object AutoTriggered extends Info {
-  lazy val comment = Nil
-  lazy val isCached = false
+  override val comment = Nil
+  override val isCached = false
 }
 
 /** An `Info` instance for labelling a pre-verified AST node (e.g., via caching). */
 case object Cached extends Info {
-  lazy val comment = Nil
-  lazy val isCached = true
+  override val comment = Nil
+  override val isCached = true
 }
 
 /** An `Info` instance for labelling a node as synthesized. A synthesized node is one that
   * was not present in the original program that was passed to a Viper backend, such as nodes that
   * originate from an AST transformation.
   */
 case object Synthesized extends Info {
-  lazy val comment = Nil
-  lazy val isCached = false
+  override val comment = Nil
+  override 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.
+*/
+abstract class FailureExpectedInfo extends Info {
+  override val comment = Nil
+  override 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
-  lazy val isCached = head.isCached || tail.isCached
+  override val comment = head.comment ++ tail.comment
+  override val isCached = head.isCached || tail.isCached
 }
 
 /** Build a `ConsInfo` instance out of two `Info`s, unless the latter is `NoInfo` (which can be dropped) */

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 `FailureExpectedInfo` info that tells us that this assert is a refute. */
+case object RefuteInfo extends FailureExpectedInfo
+
+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,27 @@
+// 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 = "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(s"__plugin_refute_nondet${this.refuteAsserts.size}", 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(s"__plugin_refute_nondet${this.refuteAsserts.size}", 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/plugin/standard/termination/TerminationPlugin.scala

@@ -28,7 +28,7 @@ class TerminationPlugin(reporter: viper.silver.reporter.Reporter,
   /**
    * Keyword used to define decreases clauses
    */
-  private val DecreasesKeyword: String = "decreases"
+  private val decreasesKeyword: String = "decreases"
 
   /**
    * Parser for decreases clauses with following possibilities.
@@ -40,7 +40,7 @@ class TerminationPlugin(reporter: viper.silver.reporter.Reporter,
    * decreases *
    */
   def decreases[_: P]: P[PDecreasesClause] =
-    P(keyword(DecreasesKeyword) ~/ (decreasesWildcard | decreasesStar | decreasesTuple) ~ ";".?)
+    P(keyword(decreasesKeyword) ~/ (decreasesWildcard | decreasesStar | decreasesTuple) ~ ";".?)
   def decreasesTuple[_: P]: P[PDecreasesTuple] =
     FP(exp.rep(sep = ",") ~/ condition.?).map { case (pos, (a, c)) => PDecreasesTuple(a, c)(pos) }
   def decreasesWildcard[_: P]: P[PDecreasesWildcard] = FP("_" ~/ condition.?).map{ case (pos, c) => PDecreasesWildcard(c)(pos) }
@@ -53,7 +53,7 @@ class TerminationPlugin(reporter: viper.silver.reporter.Reporter,
    */
   override def beforeParse(input: String, isImported: Boolean): String = {
     // Add new keyword
-    ParserExtension.addNewKeywords(Set[String](DecreasesKeyword))
+    ParserExtension.addNewKeywords(Set[String](decreasesKeyword))
     // Add new parser to the precondition
     ParserExtension.addNewPreCondition(decreases(_))
     // Add new parser to the postcondition

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

@@ -153,6 +153,12 @@ 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 `FailureExpectedInfo` info tags
+  def isExpected: Boolean = offendingNode match {
+    case i: Infoed => i.info.getUniqueInfo[FailureExpectedInfo].isDefined
+    case _ => false
+  }
 }
 
 trait VerificationError extends AbstractError with ErrorMessage {

src/test/resources/refute/complex.vpr

@@ -0,0 +1,36 @@
+field f: Int
+
+function foo(x:Ref): Bool
+    requires acc(x.f) { x.f == x.f }
+
+method bar(y: Int)
+    requires y > 10
+{
+    var x: Ref
+    inhale acc(x.f)
+    label l
+    while (x.f > y)
+        invariant acc(x.f) && (old[l](x.f >= y) ==> x.f >= y)
+    {
+        refute x.f < y
+        x.f := x.f - 1
+        //:: ExpectedOutput(refute.failed:refutation.true)
+        refute foo(x)
+    }
+    refute x.f == y
+    
+    var z: Int
+    if (z > 10) {
+        z := z+1
+    } else {
+        z := z-1
+    }
+    if (z < -10) {
+        z := z+1
+    } else {
+        z := z-1
+    }
+    refute z == 10
+    //:: ExpectedOutput(refute.failed:refutation.true)
+    refute z < 9 || z > 10
+}

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
+    }
+}