Skip to content

Commit

Permalink
Add refute statement
Browse files Browse the repository at this point in the history
  • Loading branch information
bruggerl committed Jul 1, 2024
1 parent cc1fb72 commit 86878b2
Show file tree
Hide file tree
Showing 21 changed files with 1,811 additions and 1,719 deletions.
1 change: 1 addition & 0 deletions src/main/antlr4/GobraLexer.g4
Original file line number Diff line number Diff line change
Expand Up @@ -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';
Expand Down
2 changes: 1 addition & 1 deletion src/main/antlr4/GobraParser.g4
Original file line number Diff line number Diff line change
Expand Up @@ -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_
;

Expand Down
2,305 changes: 1,155 additions & 1,150 deletions src/main/java/viper/gobra/frontend/GobraLexer.java

Large diffs are not rendered by default.

1,107 changes: 555 additions & 552 deletions src/main/java/viper/gobra/frontend/GobraParser.java

Large diffs are not rendered by default.

Original file line number Diff line number Diff line change
@@ -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;

Expand Down
2 changes: 1 addition & 1 deletion src/main/java/viper/gobra/frontend/GobraParserVisitor.java
Original file line number Diff line number Diff line change
@@ -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;

Expand Down
2 changes: 2 additions & 0 deletions src/main/scala/viper/gobra/ast/frontend/Ast.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
2 changes: 2 additions & 0 deletions src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand Down
1 change: 1 addition & 0 deletions src/main/scala/viper/gobra/ast/internal/Program.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
29 changes: 20 additions & 9 deletions src/main/scala/viper/gobra/backend/BackendVerifier.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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}

Expand Down Expand Up @@ -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)
Expand Down
1 change: 1 addition & 0 deletions src/main/scala/viper/gobra/frontend/Desugar.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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 {

Expand Down Expand Up @@ -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)) =>
Expand Down Expand Up @@ -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, _) =>
Expand Down
19 changes: 18 additions & 1 deletion src/main/scala/viper/gobra/reporting/VerifierError.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down Expand Up @@ -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"
Expand Down Expand Up @@ -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."
Expand Down
5 changes: 3 additions & 2 deletions src/main/scala/viper/gobra/translator/Translator.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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)) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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 {

Expand Down Expand Up @@ -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)
Expand Down
Original file line number Diff line number Diff line change
@@ -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)
}
}

0 comments on commit 86878b2

Please sign in to comment.