Add refute statement

src/main/antlr4/GobraLexer.g4

@@ -20,6 +20,7 @@ DECIMAL_FLOAT_LIT      : DECIMALS ('.'{_input.LA(1) != '.'}? DECIMALS? EXPONENT?
 TRUE        : 'true' -> mode(NLSEMI);
 FALSE       : 'false' -> mode(NLSEMI);
 ASSERT      : 'assert';
+REFUTE      : 'refute';
 ASSUME      : 'assume';
 INHALE      : 'inhale';
 EXHALE      : 'exhale';

src/main/antlr4/GobraParser.g4

@@ -60,7 +60,7 @@ ghostMember: implementationProof
 ghostStatement:
   GHOST statement  #explicitGhostStatement
   | fold_stmt=(FOLD | UNFOLD) predicateAccess #foldStatement
-  | kind=(ASSUME | ASSERT | INHALE | EXHALE) expression #proofStatement
+  | kind=(ASSUME | ASSERT | REFUTE | INHALE | EXHALE) expression #proofStatement
   | matchStmt #matchStmt_
   ;
 

src/main/java/viper/gobra/frontend/GobraParserBaseVisitor.java

@@ -1,4 +1,4 @@
-// Generated from src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
+// Generated from /mnt/c/Users/leasa/Documents/Git/gobra/src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
 package viper.gobra.frontend;
 import org.antlr.v4.runtime.tree.AbstractParseTreeVisitor;
 

src/main/java/viper/gobra/frontend/GobraParserVisitor.java

@@ -1,4 +1,4 @@
-// Generated from src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
+// Generated from /mnt/c/Users/leasa/Documents/Git/gobra/src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
 package viper.gobra.frontend;
 import org.antlr.v4.runtime.tree.ParseTreeVisitor;
 

src/main/scala/viper/gobra/ast/frontend/Ast.scala

@@ -969,6 +969,8 @@ case class PExplicitGhostStatement(actual: PStatement) extends PGhostStatement w
 
 case class PAssert(exp: PExpression) extends PGhostStatement
 
+case class PRefute(exp: PExpression) extends PGhostStatement
+
 case class PAssume(exp: PExpression) extends PGhostStatement
 
 case class PExhale(exp: PExpression) extends PGhostStatement

src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala

@@ -284,6 +284,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     case statement: PGhostStatement => statement match {
       case PExplicitGhostStatement(actual) => "ghost" <+> showStmt(actual)
       case PAssert(exp) => "assert" <+> showExpr(exp)
+      case PRefute(exp) => "refute" <+> showExpr(exp)
       case PAssume(exp) => "assume" <+> showExpr(exp)
       case PExhale(exp) => "exhale" <+> showExpr(exp)
       case PInhale(exp) => "inhale" <+> showExpr(exp)

src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala

@@ -341,6 +341,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
 
     case Return() => "return"
     case Assert(ass) => "assert" <+> showAss(ass)
+    case Refute(ass) => "refute" <+> showAss(ass)
     case Assume(ass) => "assume" <+> showAss(ass)
     case Inhale(ass) => "inhale" <+> showAss(ass)
     case Exhale(ass) => "exhale" <+> showAss(ass)
@@ -791,6 +792,7 @@ class ShortPrettyPrinter extends DefaultPrettyPrinter {
 
     case Return() => "return"
     case Assert(ass) => "assert" <+> showAss(ass)
+    case Refute(ass) => "refute" <+> showAss(ass)
     case Assume(ass) => "assume" <+> showAss(ass)
     case Inhale(ass) => "inhale" <+> showAss(ass)
     case Exhale(ass) => "exhale" <+> showAss(ass)

src/main/scala/viper/gobra/ast/internal/Program.scala

@@ -432,6 +432,7 @@ case class Defer(stmt: Deferrable)(val info: Source.Parser.Info) extends Stmt
 case class Return()(val info: Source.Parser.Info) extends Stmt
 
 case class Assert(ass: Assertion)(val info: Source.Parser.Info) extends Stmt
+case class Refute(ass: Assertion)(val info: Source.Parser.Info) extends Stmt
 case class Assume(ass: Assertion)(val info: Source.Parser.Info) extends Stmt
 case class Inhale(ass: Assertion)(val info: Source.Parser.Info) extends Stmt
 case class Exhale(ass: Assertion)(val info: Source.Parser.Info) extends Stmt

src/main/scala/viper/gobra/ast/internal/transform/OverflowChecksTransform.scala

@@ -135,7 +135,7 @@ object OverflowChecksTransform extends InternalTransform {
       Seqn(genOverflowChecksExprs(Vector(base, idx)) :+ m)(m.info)
 
     // explicitly matches remaining statements to detect non-exhaustive pattern matching if a new statement is added
-    case x@(_: Inhale | _: Exhale | _: Assert | _: Assume
+    case x@(_: Inhale | _: Exhale | _: Assert | _: Refute | _: Assume
             | _: Return | _: Fold | _: Unfold | _: PredExprFold | _: PredExprUnfold | _: Outline
             | _: SafeTypeAssertion | _: SafeReceive | _: Label | _: Initialization | _: PatternMatchStmt) => x
 

src/main/scala/viper/gobra/backend/BackendVerifier.scala

@@ -12,6 +12,8 @@ import viper.gobra.reporting.BackTranslator.BackTrackInfo
 import viper.gobra.reporting.{BackTranslator, BacktranslatingReporter, ChoppedProgressMessage}
 import viper.gobra.util.{ChopperUtil, GobraExecutionContext}
 import viper.silver
+import viper.silver.ast.Program
+import viper.silver.plugin.standard.refute.RefutePlugin
 import viper.silver.verifier.VerificationResult
 import viper.silver.{ast => vpr}
 
@@ -78,22 +80,31 @@ object BackendVerifier {
       }
     }
 
-    verificationResults.map(convertVerificationResult(_, task.backtrack))
+    verificationResults.map(convertVerificationResult(task.program, _, task.backtrack))
   }
 
   /**
     * Takes a Viper VerificationResult and converts it to a Gobra Result using the provided backtracking information
     */
-  def convertVerificationResult(result: VerificationResult, backTrackInfo: BackTrackInfo): Result = result match {
-    case silver.verifier.Success => Success
-    case failure: silver.verifier.Failure =>
-      val (verificationError, otherError) = failure.errors
-        .partition(_.isInstanceOf[silver.verifier.VerificationError])
-        .asInstanceOf[(Seq[silver.verifier.VerificationError], Seq[silver.verifier.AbstractError])]
+  def convertVerificationResult(result: VerificationResult, backTrackInfo: BackTrackInfo): Result =
+    result match {
+      case silver.verifier.Success => Success
+      case failure: silver.verifier.Failure =>
+        val (verificationError, otherError) = failure.errors
+          .partition(_.isInstanceOf[silver.verifier.VerificationError])
+          .asInstanceOf[(Seq[silver.verifier.VerificationError], Seq[silver.verifier.AbstractError])]
 
-      checkAbstractViperErrors(otherError)
+        checkAbstractViperErrors(otherError)
 
-      Failure(verificationError.toVector, backTrackInfo)
+        Failure(verificationError.toVector, backTrackInfo)
+    }
+
+
+  def convertVerificationResult(program: Program, result: VerificationResult, backTrackInfo: BackTrackInfo): Result = {
+    val refutePlugin = new RefutePlugin(null, null, null, null)
+    val transformedResult = refutePlugin.mapVerificationResult(program, result)
+
+    convertVerificationResult(transformedResult, backTrackInfo)
   }
 
   @scala.annotation.elidable(scala.annotation.elidable.ASSERTION)

src/main/scala/viper/gobra/frontend/Desugar.scala

@@ -4069,6 +4069,7 @@ object Desugar extends LazyLogging {
 
       stmt match {
         case PAssert(exp) => for {e <- goA(exp)} yield in.Assert(e)(src)
+        case PRefute(exp) => for {e <- goA(exp)} yield in.Refute(e)(src)
         case PAssume(exp) => for {e <- goA(exp)} yield in.Assume(e)(src)
         case PInhale(exp) => for {e <- goA(exp)} yield in.Inhale(e)(src)
         case PExhale(exp) => for {e <- goA(exp)} yield in.Exhale(e)(src)

src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala

@@ -2187,6 +2187,7 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
   override def visitProofStatement(ctx: ProofStatementContext): PGhostStatement = super.visitProofStatement(ctx) match {
     case Vector(kind : String, expr : PExpression) => kind match {
       case "assert" => PAssert(expr)
+      case "refute" => PRefute(expr)
       case "assume" => PAssume(expr)
       case "inhale" => PInhale(expr)
       case "exhale" => PExhale(expr)

src/main/scala/viper/gobra/frontend/info/implementation/typing/StmtTyping.scala

@@ -382,7 +382,7 @@ trait StmtTyping extends BaseTyping { this: TypeInfoImpl =>
 
     def validStatements(stmts: Vector[PStatement]): PropertyResult =
       PropertyResult.bigAnd(stmts.map {
-        case _: PUnfold | _: PFold | _: PAssert | _: PEmptyStmt => successProp
+        case _: PUnfold | _: PFold | _: PAssert | _: PRefute | _: PEmptyStmt => successProp
         case _: PAssume | _: PInhale | _: PExhale => failedProp("Assume, inhale, and exhale are forbidden in implementation proofs")
 
         case b: PBlock => validStatements(b.nonEmptyStmts)

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostStmtTyping.scala

@@ -17,6 +17,7 @@ trait GhostStmtTyping extends BaseTyping { this: TypeInfoImpl =>
   private[typing] def wellDefGhostStmt(stmt: PGhostStatement): Messages = stmt match {
     case n@PExplicitGhostStatement(s) => error(n, "ghost error: expected ghostifiable statement", !s.isInstanceOf[PGhostifiableStatement])
     case PAssert(exp) => assignableToSpec(exp)
+    case PRefute(exp) => assignableToSpec(exp)
     case PExhale(exp) => assignableToSpec(exp)
     case PAssume(exp) => assignableToSpec(exp) ++ isPureExpr(exp)
     case PInhale(exp) => assignableToSpec(exp)

src/main/scala/viper/gobra/reporting/DefaultErrorBackTranslator.scala

@@ -12,6 +12,7 @@ import viper.silver
 import viper.silver.ast.Not
 import viper.silver.verifier.{AbstractVerificationError, errors => vprerr, reasons => vprrea}
 import viper.silver.plugin.standard.termination
+import viper.silver.plugin.standard.{refute => vprrefute}
 
 object DefaultErrorBackTranslator {
 
@@ -40,6 +41,8 @@ object DefaultErrorBackTranslator {
         InsufficientPermissionError(info)
       case vprrea.AssertionFalse(CertainSource(info)) =>
         AssertionFalseError(info)
+      case vprrefute.RefutationTrue(CertainSource(info)) =>
+        RefutationTrueError(info)
       case vprrea.AssertionFalse(CertainSynthesized(info)) =>
         SynthesizedAssertionFalseReason(info)
       case vprrea.SeqIndexExceedsLength(CertainSource(node), CertainSource(index)) =>
@@ -122,6 +125,8 @@ class DefaultErrorBackTranslator(
         ForLoopError(info) dueTo translate(reason)
       case vprerr.AssertFailed(CertainSource(info), reason, _) =>
         AssertError(info) dueTo translate(reason)
+      case vprrefute.RefuteFailed(CertainSource(info), reason, _) =>
+        RefuteError(info) dueTo translate(reason)
       case vprerr.PostconditionViolated(CertainSource(info), _, reason, _) =>
         PostconditionError(info) dueTo translate(reason)
       case vprerr.FoldFailed(CertainSource(info), reason, _) =>

src/main/scala/viper/gobra/reporting/VerifierError.scala

@@ -11,7 +11,10 @@ import viper.gobra.ast.frontend.{PReceive, PSendStmt}
 import viper.gobra.reporting.Source.Verifier
 import viper.gobra.util.Constants
 import viper.gobra.util.Violation.violation
-import viper.silver.ast.SourcePosition
+import viper.silver.ast.{FalseLit, SourcePosition}
+import viper.silver.plugin.standard.refute.{Refute, RefuteError, RefuteErrorReason}
+import viper.silver.plugin.standard.smoke.SmokeDetectionInfo
+import viper.silver.verifier.{ErrorMessage, ErrorReason, errors, reasons}
 
 sealed trait VerifierError {
   def position: Option[SourcePosition]
@@ -181,6 +184,13 @@ case class AssertError(info: Source.Verifier.Info) extends VerificationError {
   override def localMessage: String = "Assert might fail"
 }
 
+case class RefuteError(info: Source.Verifier.Info) extends VerificationError {
+
+  override def localId: String = "refute_error"
+
+  override def localMessage: String = "Refute statement failed. Assertion holds in all cases or could not be reached"
+}
+
 case class ExhaleError(info: Source.Verifier.Info) extends VerificationError {
   override def localId: String = "exhale_error"
   override def localMessage: String = "Exhale might fail"
@@ -396,6 +406,13 @@ case class AssertionFalseError(info: Source.Verifier.Info) extends VerificationE
   override def message: String = s"Assertion ${info.origin.tag.trim} might not hold."
 }
 
+case class RefutationTrueError(info: Source.Verifier.Info) extends VerificationErrorReason {
+
+  override def id: String = "refutation_true_error"
+
+  override def message: String = s"Assertion ${info.origin.tag.trim} definitely holds."
+}
+
 case class SeqIndexExceedsLengthError(node: Source.Verifier.Info, index: Source.Verifier.Info) extends VerificationErrorReason {
   override def id: String = "seq_index_exceeds_length_error"
   override def message: String = s"Index ${index.origin.tag.trim} into ${node.origin.tag.trim} might exceed sequence length."

src/main/scala/viper/gobra/translator/Translator.scala

@@ -13,7 +13,7 @@ import viper.gobra.frontend.{Config, PackageInfo}
 import viper.gobra.reporting.{ConsistencyError, GeneratedViperMessage, TransformerFailureMessage, VerifierError}
 import viper.gobra.translator.context.DfltTranslatorConfig
 import viper.gobra.translator.encodings.programs.ProgramsImpl
-import viper.gobra.translator.transformers.{AssumeTransformer, TerminationTransformer, ViperTransformer}
+import viper.gobra.translator.transformers.{AssumeTransformer, RefuteTransformer, TerminationTransformer, ViperTransformer}
 import viper.gobra.util.Violation
 import viper.silver.ast.{AbstractSourcePosition, SourcePosition}
 import viper.silver.ast.pretty.FastPrettyPrinter
@@ -38,7 +38,8 @@ object Translator {
 
     val transformers: Seq[ViperTransformer] = Seq(
       new AssumeTransformer,
-      new TerminationTransformer
+      new TerminationTransformer,
+      new RefuteTransformer
     )
 
     val transformedTask = transformers.foldLeft[Either[Vector[VerifierError], BackendVerifier.Task]](Right(task)) {

src/main/scala/viper/gobra/translator/encodings/typeless/AssertionEncoding.scala

@@ -14,6 +14,7 @@ import viper.gobra.translator.util.ViperWriter.CodeWriter
 import viper.gobra.util.Violation
 import viper.gobra.translator.util.{ViperUtil => vu}
 import viper.silver.{ast => vpr}
+import viper.silver.plugin.standard.{refute => vprrefute}
 
 class AssertionEncoding extends Encoding {
 
@@ -90,6 +91,7 @@ class AssertionEncoding extends Encoding {
 
   override def statement(ctx: Context): in.Stmt ==> CodeWriter[vpr.Stmt] = {
     case n@ in.Assert(ass) => for {v <- ctx.assertion(ass)} yield withSrc(vpr.Assert(v), n)
+    case n@ in.Refute(ass) => for {v <- ctx.assertion(ass)} yield withSrc(vprrefute.Refute(v), n)
     case n@ in.Assume(ass) => for {v <- ctx.assertion(ass)} yield withSrc(vpr.Assume(v), n) // Assumes are later rewritten
     case n@ in.Inhale(ass) => for {v <- ctx.assertion(ass)} yield withSrc(vpr.Inhale(v), n)
     case n@ in.Exhale(ass) => for {v <- ctx.assertion(ass)} yield withSrc(vpr.Exhale(v), n)

src/main/scala/viper/gobra/translator/transformers/RefuteTransformer.scala

@@ -0,0 +1,38 @@
+// 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-2021 ETH Zurich.
+
+package viper.gobra.translator.transformers
+
+import viper.gobra.backend.BackendVerifier
+import viper.silver.plugin.SilverPlugin
+import viper.silver.plugin.standard.refute.RefutePlugin
+import viper.silver.verifier.AbstractError
+import viper.silver.{ast => vpr}
+
+class RefuteTransformer extends ViperTransformer {
+  override def transform(task: BackendVerifier.Task): Either[Seq[AbstractError], BackendVerifier.Task] = {
+    for {
+      transformedProg <- executeTerminationPlugin(task)
+    } yield transformedProg
+  }
+
+  private def executeTerminationPlugin(task: BackendVerifier.Task): Either[Seq[AbstractError], BackendVerifier.Task] = {
+    def applyPlugin(plugin: SilverPlugin, prog : vpr.Program): Either[Seq[AbstractError], vpr.Program] = {
+      val transformedProgram = plugin.beforeVerify(prog)
+      if (plugin.errors.isEmpty) {
+        Right(transformedProgram)
+      } else {
+        Left(plugin.errors)
+      }
+    }
+
+    val refutePlugin = new RefutePlugin(null, null, null, null)
+
+    for {
+      transformedProgram <- applyPlugin(refutePlugin, task.program)
+    } yield task.copy(program = transformedProgram)
+  }
+}