Add refute statement (#776)

* Add refute statement

* Update src/main/java/viper/gobra/frontend/GobraLexer.java

Co-authored-by: João Pereira <[email protected]>

* Update src/main/java/viper/gobra/frontend/GobraParser.java

Co-authored-by: João Pereira <[email protected]>

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

Co-authored-by: João Pereira <[email protected]>

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

Co-authored-by: João Pereira <[email protected]>

* Inline plugin execution

* Remove unused imports

* Switch to frontend API for Silicon and Carbon

* Remove explicit call to mapVerificationResult in RefutePlugin

* Add tests for refute

* Fix termination transformer

* Remove refute transformer

* Clean up error transformations for closures

* Refine error message for refute errors

Co-authored-by: João Pereira <[email protected]>

* Remove unnecessary parentheses

Co-authored-by: João Pereira <[email protected]>

* Simplify documentation of TerminationDomainTransformer

Co-authored-by: João Pereira <[email protected]>

* Convert spaces to tabs

* Revert "Remove unnecessary parentheses"

This reverts commit aee8e53.

---------

Co-authored-by: João Pereira <[email protected]>

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/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

@@ -84,17 +84,18 @@ object BackendVerifier {
   /**
     * 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)
+    }
 
   @scala.annotation.elidable(scala.annotation.elidable.ASSERTION)
   private def checkAbstractViperErrors(errors: Seq[silver.verifier.AbstractError]): Unit = {

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

@@ -7,6 +7,7 @@
 package viper.gobra.backend
 
 import viper.carbon
+import viper.carbon.CarbonFrontendAPI
 import viper.gobra.util.GobraExecutionContext
 import viper.silver.ast.Program
 import viper.silver.reporter._
@@ -20,19 +21,18 @@ class Carbon(commandLineArguments: Seq[String]) extends ViperVerifier {
     // directly declaring the parameter implicit somehow does not work as the compiler is unable to spot the inheritance
     implicit val _executor: GobraExecutionContext = executor
     Future {
-      val backend: carbon.CarbonVerifier = carbon.CarbonVerifier(reporter, List("startedBy" -> s"Unit test ${this.getClass.getSimpleName}"))
-      backend.parseCommandLine(commandLineArguments ++ Seq("--ignoreFile", "dummy.sil"))
+      val carbonApi: carbon.CarbonFrontendAPI = new CarbonFrontendAPI(reporter)
 
       val startTime = System.currentTimeMillis()
-      backend.start()
-      val result = backend.verify(program)
-      backend.stop()
+      carbonApi.initialize(commandLineArguments ++ Seq("--ignoreFile", "dummy.sil"))
+      val result = carbonApi.verify(program)
+      carbonApi.stop()
 
       result match {
         case Success =>
-          reporter report OverallSuccessMessage(backend.name, System.currentTimeMillis() - startTime)
+          reporter report OverallSuccessMessage(carbonApi.verifier.name, System.currentTimeMillis() - startTime)
         case f@Failure(_) =>
-          reporter report OverallFailureMessage(backend.name, System.currentTimeMillis() - startTime, f)
+          reporter report OverallFailureMessage(carbonApi.verifier.name, System.currentTimeMillis() - startTime, f)
       }
 
       result

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

@@ -19,19 +19,19 @@ class Silicon(commandLineArguments: Seq[String]) extends ViperVerifier {
     // directly declaring the parameter implicit somehow does not work as the compiler is unable to spot the inheritance
     implicit val _executor: GobraExecutionContext = executor
     Future {
-      val backend: silicon.Silicon = silicon.Silicon.fromPartialCommandLineArguments(commandLineArguments, reporter)
+      val siliconApi: silicon.SiliconFrontendAPI = new silicon.SiliconFrontendAPI(reporter)
 
       val startTime = System.currentTimeMillis()
       try {
-        backend.start()
-        val result = backend.verify(program)
-        backend.stop()
+        siliconApi.initialize(commandLineArguments)
+        val result = siliconApi.verify(program)
+        siliconApi.stop()
 
         result match {
           case Success =>
-            reporter report OverallSuccessMessage(backend.name, System.currentTimeMillis() - startTime)
+            reporter report OverallSuccessMessage(siliconApi.verifier.name, System.currentTimeMillis() - startTime)
           case f@Failure(_) =>
-            reporter report OverallFailureMessage(backend.name, System.currentTimeMillis() - startTime, f)
+            reporter report OverallFailureMessage(siliconApi.verifier.name, System.currentTimeMillis() - startTime, f)
         }
 
         result

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,14 +12,17 @@ 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 {
 
   def translateWithTransformer(
                                 viperError: viper.silver.verifier.VerificationError,
                                 transformer: BackTranslator.ErrorTransformer
                               ): VerificationError = {
-    val gobraError = transformer.lift.apply(viperError).getOrElse{ UncaughtError(viperError) }
+    val gobraError = transformer.lift.apply(viperError).getOrElse {
+      UncaughtError(viperError)
+    }
     if (viperError.cached) gobraError.cached = true
     gobraError
   }
@@ -28,7 +31,9 @@ object DefaultErrorBackTranslator {
                                 viperReason: silver.verifier.ErrorReason,
                                 transformer: BackTranslator.ReasonTransformer
                               ): VerificationErrorReason = {
-    transformer.lift.apply(viperReason).getOrElse{ UncaughtReason(viperReason) }
+    transformer.lift.apply(viperReason).getOrElse {
+      UncaughtReason(viperReason)
+    }
   }
 
   def defaultTranslate(viperReason: silver.verifier.ErrorReason): VerificationErrorReason =
@@ -40,6 +45,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 +129,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, _) =>
@@ -153,35 +162,35 @@ class DefaultErrorBackTranslator(
         IfError(info) dueTo translate(reason)
       case vprerr.IfFailed(CertainSource(info), reason, _) =>
         IfError(info) dueTo translate(reason)
-       case termination.FunctionTerminationError(Source(info) , reason, _) =>
-         FunctionTerminationError(info) dueTo translate(reason)
-       case termination.MethodTerminationError(Source(info), reason, _) =>
-         MethodTerminationError(info) dueTo translate(reason)
-       case termination.LoopTerminationError(Source(info), reason, _) =>
-         LoopTerminationError(info) dueTo translate(reason)
+      case termination.FunctionTerminationError(Source(info), reason, _) =>
+        FunctionTerminationError(info) dueTo translate(reason)
+      case termination.MethodTerminationError(Source(info), reason, _) =>
+        MethodTerminationError(info) dueTo translate(reason)
+      case termination.LoopTerminationError(Source(info), reason, _) =>
+        LoopTerminationError(info) dueTo translate(reason)
     }
 
     val transformAnnotatedError: VerificationError => VerificationError = x => x.info match {
       case _ / (an: OverwriteErrorAnnotation) => an(x)
 
       case _ / OverflowCheckAnnotation =>
-        x.reasons.foldLeft(OverflowError(x.info): VerificationError){ case (err, reason) => err dueTo reason }
+        x.reasons.foldLeft(OverflowError(x.info): VerificationError) { case (err, reason) => err dueTo reason }
 
       case _ / AutoImplProofAnnotation(subT, superT) =>
         GeneratedImplementationProofError(subT, superT, x)
 
       case _ / MainPreNotEstablished =>
-        x.reasons.foldLeft(MainPreconditionNotEstablished(x.info): VerificationError){
+        x.reasons.foldLeft(MainPreconditionNotEstablished(x.info): VerificationError) {
           case (err, reason) => err dueTo reason
         }
 
       case _ / ImportPreNotEstablished =>
-        x.reasons.foldLeft(ImportPreconditionNotEstablished(x.info): VerificationError){
+        x.reasons.foldLeft(ImportPreconditionNotEstablished(x.info): VerificationError) {
           case (err, reason) => err dueTo reason
         }
 
       case _ / InsufficientPermissionToRangeExpressionAnnotation() =>
-        x.reasons.foldLeft(InsufficientPermissionToRangeExpressionError(x.info): VerificationError){ case (err, reason) => err dueTo reason }
+        x.reasons.foldLeft(InsufficientPermissionToRangeExpressionError(x.info): VerificationError) { case (err, reason) => err dueTo reason }
 
       case _ / LoopInvariantNotEstablishedAnnotation =>
         x.reasons.foldLeft(LoopInvariantEstablishmentError(x.info): VerificationError) { case (err, reason) => err dueTo reason }
@@ -192,11 +201,11 @@ class DefaultErrorBackTranslator(
     errorMapper.andThen(transformAnnotatedError)
   }
 
-  private val errorTransformer = backtrack.errorT.foldRight(defaultErrorTransformer){
+  private val errorTransformer = backtrack.errorT.foldRight(defaultErrorTransformer) {
     case (l, r) => l orElse r
   }
 
-  private val reasonTransformer = backtrack.reasonT.foldRight(DefaultErrorBackTranslator.defaultReasonTransformer){
+  private val reasonTransformer = backtrack.reasonT.foldRight(DefaultErrorBackTranslator.defaultReasonTransformer) {
     case (l, r) => l orElse r
   }
 

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

@@ -11,7 +11,7 @@ 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.{SourcePosition}
 
 sealed trait VerifierError {
   def position: Option[SourcePosition]
@@ -181,6 +181,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 is either unreachable or it always holds."
+}
+
 case class ExhaleError(info: Source.Verifier.Info) extends VerificationError {
   override def localId: String = "exhale_error"
   override def localMessage: String = "Exhale might fail"
@@ -396,6 +403,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, TerminationDomainTransformer, ViperTransformer}
 import viper.gobra.util.Violation
 import viper.silver.ast.{AbstractSourcePosition, SourcePosition}
 import viper.silver.ast.pretty.FastPrettyPrinter
@@ -38,7 +38,7 @@ object Translator {
 
     val transformers: Seq[ViperTransformer] = Seq(
       new AssumeTransformer,
-      new TerminationTransformer
+      new TerminationDomainTransformer
     )
 
     val transformedTask = transformers.foldLeft[Either[Vector[VerifierError], BackendVerifier.Task]](Right(task)) {

src/main/scala/viper/gobra/translator/encodings/closures/ClosureEncoding.scala

@@ -9,7 +9,7 @@ package viper.gobra.translator.encodings.closures
 import org.bitbucket.inkytonik.kiama.==>
 import viper.gobra.ast.{internal => in}
 import viper.gobra.reporting
-import viper.gobra.reporting.BackTranslator.ErrorTransformer
+import viper.gobra.reporting.BackTranslator.{ErrorTransformer, RichErrorMessage}
 import viper.gobra.reporting.Source
 import viper.gobra.theory.Addressability
 import viper.gobra.theory.Addressability.{Exclusive, Shared}
@@ -137,6 +137,7 @@ class ClosureEncoding extends LeafTypeEncoding {
     * inhale closureImplements$[spec]([closure], [params])
     */
   private def specImplementationProof(proof: in.SpecImplementationProof)(ctx: Context): CodeWriter[vpr.Stmt] = {
+    val (exhalePos, _, _) = proof.vprMeta
     val inhalePres = cl.seqns(proof.pres map (a => for {
           ass <- ctx.assertion(a)
         } yield vpr.Inhale(ass)()))
@@ -145,11 +146,10 @@ class ClosureEncoding extends LeafTypeEncoding {
         rest <- acc
         ass <- ctx.assertion (a)
       } yield vpr.And(rest, ass) ())
-    } yield vpr.Exhale(assertions)()
+    } yield vpr.Exhale(assertions)(exhalePos)
 
-    def isSubnode(sub: vpr.Node, n: vpr.Node): Boolean = (sub eq n) || n.subnodes.exists(n => isSubnode(sub, n))
     def failedExhale: ErrorTransformer = {
-      case errors.ExhaleFailed(offendingNode, reason, _) if isSubnode(offendingNode, exhalePosts.res) =>
+      case e@errors.ExhaleFailed(_, reason, _) if e causedBy exhalePosts.res =>
         val info = proof.vprMeta._2.asInstanceOf[Source.Verifier.Info]
         reason match {
           case reason: reasons.AssertionFalse => reporting.SpecImplementationPostconditionError(info, proof.spec.info.tag)