Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add refute statement #776

Merged
merged 18 commits into from
Jul 10, 2024
Merged
Show file tree
Hide file tree
Changes from 13 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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,303 changes: 1,154 additions & 1,149 deletions src/main/java/viper/gobra/frontend/GobraLexer.java

Large diffs are not rendered by default.

1,105 changes: 554 additions & 551 deletions src/main/java/viper/gobra/frontend/GobraParser.java

Large diffs are not rendered by default.

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
19 changes: 10 additions & 9 deletions src/main/scala/viper/gobra/backend/BackendVerifier.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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 = {
Expand Down
14 changes: 7 additions & 7 deletions src/main/scala/viper/gobra/backend/Carbon.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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._
Expand All @@ -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
Expand Down
12 changes: 6 additions & 6 deletions src/main/scala/viper/gobra/backend/Silicon.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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
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,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
}
Expand All @@ -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 =
Expand All @@ -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)) =>
Expand Down Expand Up @@ -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, _) =>
Expand Down Expand Up @@ -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 }
Expand All @@ -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
}

Expand Down
16 changes: 15 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,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]
Expand Down Expand Up @@ -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 holds in all cases or could not be reached"
bruggerl marked this conversation as resolved.
Show resolved Hide resolved
}

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 +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."
Expand Down
4 changes: 2 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, TerminationDomainTransformer, ViperTransformer}
import viper.gobra.util.Violation
import viper.silver.ast.{AbstractSourcePosition, SourcePosition}
import viper.silver.ast.pretty.FastPrettyPrinter
Expand All @@ -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)) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down Expand Up @@ -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)()))
Expand All @@ -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)
Expand Down
Loading
Loading