From 1e642a3d540c72fcfcea44a2a53ed879fe67200c Mon Sep 17 00:00:00 2001 From: Lea Salome Brugger Date: Mon, 8 Jan 2024 15:40:59 +0100 Subject: [PATCH 1/4] Add unreachable statement --- .../smoke/UnreachableASTExtension.scala | 19 +++++++++++++++++++ .../smoke/UnreachablePASTExtension.scala | 19 +++++++++++++++++++ 2 files changed, 38 insertions(+) create mode 100644 src/main/scala/viper/silver/plugin/standard/smoke/UnreachableASTExtension.scala create mode 100644 src/main/scala/viper/silver/plugin/standard/smoke/UnreachablePASTExtension.scala diff --git a/src/main/scala/viper/silver/plugin/standard/smoke/UnreachableASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/smoke/UnreachableASTExtension.scala new file mode 100644 index 000000000..4ca3d226a --- /dev/null +++ b/src/main/scala/viper/silver/plugin/standard/smoke/UnreachableASTExtension.scala @@ -0,0 +1,19 @@ +// 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.smoke + +import viper.silver.ast._ +import viper.silver.ast.pretty.FastPrettyPrinter.text +import viper.silver.ast.pretty.PrettyPrintPrimitives + +case class Unreachable()(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends ExtensionStmt { + + override lazy val prettyPrint: PrettyPrintPrimitives#Cont = text("unreachable") + + override def extensionSubnodes: Seq[Node] = Seq() +} + diff --git a/src/main/scala/viper/silver/plugin/standard/smoke/UnreachablePASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/smoke/UnreachablePASTExtension.scala new file mode 100644 index 000000000..2b1e996c1 --- /dev/null +++ b/src/main/scala/viper/silver/plugin/standard/smoke/UnreachablePASTExtension.scala @@ -0,0 +1,19 @@ +// 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.smoke + +import viper.silver.ast.{Position, Stmt} +import viper.silver.parser._ + +case class PUnreachable()(val pos: (Position, Position)) extends PExtender with PStmt { + override val getSubnodes: Seq[PNode] = Seq() + override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = { + None + } + + override def translateStmt(t: Translator): Stmt = Unreachable()(t.liftPos(this)) +} From cb8caaeb85ee0730e28cb6eeb113b7721010f2f5 Mon Sep 17 00:00:00 2001 From: Lea Salome Brugger Date: Mon, 8 Jan 2024 15:41:34 +0100 Subject: [PATCH 2/4] Implement smoke detection --- .../plugin/standard/refute/RefuteErrors.scala | 6 +- .../plugin/standard/refute/RefutePlugin.scala | 2 +- .../standard/smoke/SmokeDetectionPlugin.scala | 235 ++++++++++++++++++ 3 files changed, 241 insertions(+), 2 deletions(-) create mode 100644 src/main/scala/viper/silver/plugin/standard/smoke/SmokeDetectionPlugin.scala diff --git a/src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala b/src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala index e3642b52a..8901fb213 100644 --- a/src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala +++ b/src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala @@ -6,6 +6,8 @@ package viper.silver.plugin.standard.refute +import viper.silver.ast.FalseLit +import viper.silver.plugin.standard.smoke.SmokeDetectionInfo import viper.silver.verifier._ sealed abstract class RefuteError extends ExtensionAbstractVerificationError @@ -13,7 +15,9 @@ sealed abstract class RefuteErrorReason extends ExtensionAbstractErrorReason case class RefuteFailed(override val offendingNode: Refute, override val reason: ErrorReason, override val cached: Boolean = false) extends RefuteError { override val id = "refute.failed" - override val text = "Refute holds in all cases or could not be reached (e.g. see Silicon `numberOfErrorsToReport`)." + override val text: String = if (offendingNode.exp.isInstanceOf[FalseLit] && offendingNode.info.getUniqueInfo[SmokeDetectionInfo].isDefined) + "Smoke detection: False could be proven here (which should never hold)." else + "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) diff --git a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala index 131fb58cc..268608e66 100644 --- a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala +++ b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala @@ -56,7 +56,7 @@ class RefutePlugin(@unused reporter: viper.silver.reporter.Reporter, If(nonDetLocalVarDecl.localVar, Seqn(Seq( Assert(exp)(r.pos, RefuteInfo(r)), - Inhale(BoolLit(false)(r.pos))(r.pos) + Inhale(BoolLit(false)(r.pos))(r.pos, Synthesized) ), Seq())(r.pos), Seqn(Seq(), Seq())(r.pos))(r.pos) ), diff --git a/src/main/scala/viper/silver/plugin/standard/smoke/SmokeDetectionPlugin.scala b/src/main/scala/viper/silver/plugin/standard/smoke/SmokeDetectionPlugin.scala new file mode 100644 index 000000000..354418315 --- /dev/null +++ b/src/main/scala/viper/silver/plugin/standard/smoke/SmokeDetectionPlugin.scala @@ -0,0 +1,235 @@ +package viper.silver.plugin.standard.smoke + +import fastparse.P +import viper.silver.ast._ +import viper.silver.ast.utility.ViperStrategy +import viper.silver.cfg.silver.SilverCfg +import viper.silver.cfg.silver.SilverCfg.SilverBlock +import viper.silver.parser.FastParser +import viper.silver.plugin.standard.refute.Refute +import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin} + +import scala.annotation.unused +import scala.collection.mutable.ListBuffer + +class SmokeDetectionPlugin(@unused reporter: viper.silver.reporter.Reporter, + @unused logger: ch.qos.logback.classic.Logger, + @unused config: viper.silver.frontend.SilFrontendConfig, + fp: FastParser) extends SilverPlugin with ParserPluginTemplate { + + import fp.{FP, ParserExtension, keyword} + + /** Keyword used to define `unreachable` statement. */ + private val unreachableKeyword: String = "unreachable" + + /** Parser for `unreachable` statements. */ + def unreachable[$: P]: P[PUnreachable] = + FP(keyword(unreachableKeyword)).map { case (pos, _) => PUnreachable()(pos) } + + /** Add `unreachable` to the parser. */ + override def beforeParse(input: String, isImported: Boolean): String = { + // Add new keyword + ParserExtension.addNewKeywords(Set[String](unreachableKeyword)) + // Add new parser to the precondition + ParserExtension.addNewStmtAtEnd(unreachable(_)) + input + } + + override def beforeVerify(input: Program): Program = { + var refuteId = 0 + + // Add `refute false` at end of each method body + val transformedMethods = input.methods.map(method => { + val bodyWithRefute = if (method.body.isEmpty) method.body else + Option(Seqn(method.body.toSeq :+ refuteFalse(method.pos, refuteId), Seq())(method.pos)) + + Method(method.name, method.formalArgs, method.formalReturns, method.pres, + method.posts, bodyWithRefute)(method.pos, method.info, method.errT) + }) + + // Add `refute false` after each inhale, at end of each loop body, at end of each if/else branch and before each goto + val methodsWithRefutes = transformedMethods.map(method => { + ViperStrategy.Slim({ + case i@Inhale(expr) if i.info.getUniqueInfo[Synthesized.type].isEmpty => + refuteId += 1 + appendRefuteFalse(Inhale(expr)(i.pos, Synthesized), i.pos, refuteId) + case w@While(cond, invs, body) => + refuteId += 1 + While(cond, invs, appendRefuteFalse(body, body.pos, refuteId))(w.pos) + case i@If(cond, thn, els) => + var thnWithRefute: Seqn = thn + var elsWithRefute: Seqn = els + + if (thn.ss.nonEmpty) { + refuteId += 1 + thnWithRefute = appendRefuteFalse(thn, thn.pos, refuteId) + } + + if (els.ss.nonEmpty) { + refuteId += 1 + elsWithRefute = appendRefuteFalse(els, els.pos, refuteId) + } + + If(cond, thnWithRefute, elsWithRefute)(i.pos) + case g@Goto(target) if g.info.getUniqueInfo[Synthesized.type].isEmpty => + refuteId += 1 + Seqn(Seq(refuteFalse(g.pos, refuteId), Goto(target)(g.pos, Synthesized)), Seq())(g.pos) + }).execute[Method](method) + }) + + // Remove all `refute false` statements which are inside of control-flow branch marked as unreachable + val methodsWithoutUnreachableRefutes = methodsWithRefutes.map(method => { + val cfg = method.toCfg(simplify = false) + val result = collectRefutesToKeep(cfg) + + ViperStrategy.Slim({ + case r@Refute(_) => + val info = r.info.getUniqueInfo[SmokeDetectionInfo] + + if (info.isDefined && + !result._1.contains(info.get.id) && // not marked reachable + result._2.contains(info.get.id)) { // actually considered when traversing CFG + Seqn(Seq(), Seq())(r.pos) // remove refute statement + } else { + r + } + case u@Unreachable() => + Seqn(Seq(), Seq())(u.pos) + }).execute[Method](method) + }) + + Program(input.domains, input.fields, input.functions, input.predicates, methodsWithoutUnreachableRefutes, + input.extensions)(input.pos, input.info, input.errT) + } + + /** + * Construct a [[Seqn]] consisting of `stmt` followed by a `refute false` statement with position `pos`. + * The `Refute` instance will have the ID `refuteId`. + * + * @param stmt the statement at the beginning of the sequence + * @param pos the position of the resulting [[Seqn]] instance + * @param refuteId the ID of the `refute false` statement at the end of the sequence + * @return a [[Seqn]] instance consisting of `stmt` and a `refute false` statement + */ + private def appendRefuteFalse(stmt: Stmt, pos: Position, refuteId: Int): Seqn = { + Seqn(Seq(stmt, refuteFalse(pos, refuteId)), Seq())(pos) + } + + /** + * Construct a `refute false` statement with position `pos` and ID `id`. + * + * @param pos the position of the resulting [[Refute]] instance + * @param id the ID of the `refute false` statement + * @return a [[Refute]] instance with with the `exp` set to `false` and the given position and ID + */ + private def refuteFalse(pos: Position, id: Int): Refute = { + Refute(FalseLit()(pos))(pos, SmokeDetectionInfo(id)) + } + + /** + * Construct a list of the IDs of all `refute false` statements that are not marked unreachable. + * + * @param cfg the control-flow graph of a method + * @return a list of the IDs of the reachable `refute false` statements and a list of the IDs of the `refute false` + * statements that were encountered when traversing the control-flow graph + */ + private def collectRefutesToKeep(cfg: SilverCfg): (List[Int], List[Int]) = { + val refutesToKeep = ListBuffer[Int]() + val seenRefutes = ListBuffer[Int]() + collectRefutesToKeepUntilExit(cfg, cfg.entry, cfg.exit.toSeq, ListBuffer[SilverBlock](), + refutesToKeep, seenRefutes, unreachable = false) + (refutesToKeep.toList, seenRefutes.toList) + } + + /** + * Recursively construct a list of the IDs of all `refute false` statements that are not marked as unreachable on the + * path from the node `current` to one of the nodes in `exits` in the control-flow graph `cfg`. + * + * @param cfg the control-flow graph + * @param current the currently considered node in the control-flow graph + * @param exits a list of potential exit nodes of the currently considered subgraph + * @param seen a list of all nodes of the control-flow graph that have already been visited + * @param refutesToKeep the list of the IDs of all `refute false` statements which are not on an unreachable path + * @param seenRefutes the list of the IDs of all `refute false` statements that were already considered + * @param unreachable indicates whether the current node is on a path marked as unreachable + * @return `true` if some part of the path from the `current` node to one of the `exits` is unreachable, otherwise `false` + */ + private def collectRefutesToKeepUntilExit(cfg: SilverCfg, + current: SilverBlock, + exits: Seq[SilverBlock], + seen: ListBuffer[SilverBlock], + refutesToKeep: ListBuffer[Int], + seenRefutes: ListBuffer[Int], + unreachable: Boolean): Boolean = { + seen += current + val elements = current.elements + + var unreachableSuccessors = unreachable + + for (elem <- elements) { + val leftElem = elem.left.getOrElse(null) + + leftElem match { + case _: Unreachable => + // Encountered `unreachable` statement -> successors of current node are unreachable + unreachableSuccessors = true + case refute: Refute if refute.exp.isInstanceOf[FalseLit] => + // Encountered `refute false` statement -> add ID to list if it is reachable + val info = refute.info.getUniqueInfo[SmokeDetectionInfo] + + if (info.isDefined) { + val id = info.get.id + + if (!unreachableSuccessors) { + refutesToKeep += id + } + + seenRefutes += id + } + case _ => + } + } + + if (exits.contains(current)) { + // Considered whole path + return unreachableSuccessors + } + + val successors = cfg.successors(current).filter(s => !seen.contains(s)) + val joinPointMap = cfg.joinPoints + + if (joinPointMap.contains(current)) { + // Current node is branch point + val joinPoint = joinPointMap(current) + val joinPointPredecessors = cfg.predecessors(joinPoint) + var allBranchesUnreachable = true + + for (elem <- successors) { + val unreachableBranch = collectRefutesToKeepUntilExit(cfg, elem, joinPointPredecessors, seen, + refutesToKeep, seenRefutes, unreachableSuccessors) + if (!unreachableBranch) { + allBranchesUnreachable = false + } + } + + // If all paths from the branch point to the join point contain an `unreachable` statement, the code following + // the joint point (including the join point) is also unreachable. + return collectRefutesToKeepUntilExit(cfg, joinPoint, exits, seen, refutesToKeep, seenRefutes, allBranchesUnreachable) + } + + // Current node is no branch point -> collect Refute IDs for successor node + successors.forall(s => collectRefutesToKeepUntilExit(cfg, s, exits, seen, refutesToKeep, seenRefutes, unreachableSuccessors)) + } +} + +/** + * An info used to mark AST nodes (more specifically, `refute false` statements) as used in smoke detection, + * also assigning a unique identifier to it. + * + * @param id the ID of the node + */ +case class SmokeDetectionInfo(id: Int) extends Info { + override def comment: Seq[String] = Seq(s"`refute false` #$id") + + override def isCached: Boolean = false +} From c0156dc3ffacba1d46affc0d69d739bbaf830782 Mon Sep 17 00:00:00 2001 From: Lea Salome Brugger Date: Mon, 8 Jan 2024 15:42:12 +0100 Subject: [PATCH 3/4] Add frontend option to enable smoke detection --- .../silver/frontend/SilFrontEndConfig.scala | 7 +++ .../viper/silver/frontend/SilFrontend.scala | 58 ++++++++++++------- 2 files changed, 43 insertions(+), 22 deletions(-) diff --git a/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala b/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala index b837c5aed..4dd374f3a 100644 --- a/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala +++ b/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala @@ -82,6 +82,13 @@ abstract class SilFrontendConfig(args: Seq[String], private var projectName: Str hidden = true ) + val enableSmokeDetection = opt[Boolean]("enableSmokeDetection", + descr = "Enable smoke detection (if enabled, refute false statements are inserted in the code in order to detect unsound specifications).", + default = Some(false), + noshort = true, + hidden = false + ) + val disableDefaultPlugins = opt[Boolean]("disableDefaultPlugins", descr = "Deactivate all default plugins.", default = Some(false), diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala index a2ee386f0..5ce0cefa2 100644 --- a/src/main/scala/viper/silver/frontend/SilFrontend.scala +++ b/src/main/scala/viper/silver/frontend/SilFrontend.scala @@ -31,20 +31,21 @@ trait SilFrontend extends DefaultFrontend { */ object ApplicationExitReason extends Enumeration { type PreVerificationFailureReasons = Value - val UNKNOWN_EXIT_REASON = Value(-2) - val NOTHING_TO_BE_DONE = Value(-1) - val VERIFICATION_SUCCEEDED = Value( 0) // POSIX standard - val VERIFICATION_FAILED = Value( 1) - val COMMAND_LINE_ARGS_PARSE_FAILED = Value( 2) - val ISSUE_WITH_PLUGINS = Value( 3) - val SYSTEM_DEPENDENCY_UNSATISFIED = Value( 4) + val UNKNOWN_EXIT_REASON = Value(-2) + val NOTHING_TO_BE_DONE = Value(-1) + val VERIFICATION_SUCCEEDED = Value(0) // POSIX standard + val VERIFICATION_FAILED = Value(1) + val COMMAND_LINE_ARGS_PARSE_FAILED = Value(2) + val ISSUE_WITH_PLUGINS = Value(3) + val SYSTEM_DEPENDENCY_UNSATISFIED = Value(4) } protected var _appExitReason: ApplicationExitReason.Value = ApplicationExitReason.UNKNOWN_EXIT_REASON + def appExitCode: Int = _appExitReason.id protected def specifyAppExitCode(): Unit = { - if ( _state >= DefaultStates.Verification ) { + if (_state >= DefaultStates.Verification) { _appExitReason = result match { case Success => ApplicationExitReason.VERIFICATION_SUCCEEDED case Failure(_) => ApplicationExitReason.VERIFICATION_FAILED @@ -55,7 +56,10 @@ trait SilFrontend extends DefaultFrontend { def resetPlugins(): Unit = { val pluginsArg: Option[String] = if (_config != null) { // concat defined plugins and default plugins - val list = _config.plugin.toOption ++ (if (_config.disableDefaultPlugins()) Seq() else defaultPlugins) + val list = (if (_config.enableSmokeDetection()) Set(smokeDetectionPlugin, refutePlugin) else Set()) ++ + (if (_config.disableDefaultPlugins()) Set() else defaultPlugins) ++ + _config.plugin.toOption.toSet + if (list.isEmpty) { None } else { @@ -75,12 +79,13 @@ trait SilFrontend extends DefaultFrontend { def createVerifier(fullCmd: String): Verifier /** Configures the verifier by passing it the command line arguments ''args''. - * Returns the verifier's effective configuration. - */ + * Returns the verifier's effective configuration. + */ def configureVerifier(args: Seq[String]): SilFrontendConfig /** The Viper verifier to be used for verification (after it has been initialized). */ def verifier: Verifier = _ver + protected var _ver: Verifier = _ override protected type ParsingResult = PProgram @@ -88,8 +93,12 @@ trait SilFrontend extends DefaultFrontend { /** The current configuration. */ protected var _config: SilFrontendConfig = _ + def config: SilFrontendConfig = _config + private val refutePlugin: String = "viper.silver.plugin.standard.refute.RefutePlugin" + private val smokeDetectionPlugin: String = "viper.silver.plugin.standard.smoke.SmokeDetectionPlugin" + /** * Default plugins are always activated and are run as last plugins. * All default plugins can be excluded from the plugins by providing the --disableDefaultPlugins flag @@ -97,9 +106,10 @@ 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" + "viper.silver.plugin.standard.predicateinstance.PredicateInstancePlugin", + refutePlugin ) + /** For testing of plugin import feature */ def defaultPluginCount: Int = defaultPlugins.size @@ -116,6 +126,7 @@ trait SilFrontend extends DefaultFrontend { def plugins: SilverPluginManager = _plugins protected var _startTime: Long = _ + def startTime: Time = _startTime def getTime: Long = System.currentTimeMillis() - _startTime @@ -124,13 +135,13 @@ trait SilFrontend extends DefaultFrontend { Consistency.resetMessages() } - def setVerifier(verifier:Verifier): Unit = { + def setVerifier(verifier: Verifier): Unit = { _ver = verifier } def prepare(args: Seq[String]): Boolean = { - reporter report CopyrightReport(_ver.signature)//${_ver.copyright}") // we agreed on 11/03/19 to drop the copyright + reporter report CopyrightReport(_ver.signature) //${_ver.copyright}") // we agreed on 11/03/19 to drop the copyright /* Parse command line arguments and populate _config */ parseCommandLine(args) @@ -189,16 +200,16 @@ trait SilFrontend extends DefaultFrontend { finish() } catch { - case MissingDependencyException(msg) => - println("Missing dependency exception: " + msg) - reporter report MissingDependencyReport(msg) + case MissingDependencyException(msg) => + println("Missing dependency exception: " + msg) + reporter report MissingDependencyReport(msg) } } override def reset(input: Path): Unit = { super.reset(input) - if(_config != null) { + if (_config != null) { resetPlugins() } } @@ -224,7 +235,7 @@ trait SilFrontend extends DefaultFrontend { } override def verification(): Unit = { - def filter(input: Program): Result[Program] = { + def filter(input: Program): Result[Program] = { plugins.beforeMethodFilter(input) match { case Some(inputPlugin) => // Filter methods according to command-line arguments. @@ -277,7 +288,10 @@ trait SilFrontend extends DefaultFrontend { val result = fp.parse(inputPlugin, file, Some(plugins)) if (result.errors.forall(p => p.isInstanceOf[ParseWarning])) { reporter report WarningsDuringParsing(result.errors) - Succ({result.initProperties(); result}) + Succ({ + result.initProperties(); + result + }) } else Fail(result.errors) case None => Fail(plugins.errors) @@ -326,7 +340,7 @@ trait SilFrontend extends DefaultFrontend { } } - def doConsistencyCheck(input: Program): Result[Program]= { + def doConsistencyCheck(input: Program): Result[Program] = { var errors = input.checkTransitively if (backendTypeFormat.isDefined) errors = errors ++ Consistency.checkBackendTypes(input, backendTypeFormat.get) From 3f0198a42cf3fe747e9bcc7be3722117dc086545 Mon Sep 17 00:00:00 2001 From: Lea Salome Brugger Date: Mon, 8 Jan 2024 15:42:39 +0100 Subject: [PATCH 4/4] Add tests for smoke detection plugin --- src/test/resources/smoke/axiom.vpr | 10 +++++++ src/test/resources/smoke/if.vpr | 19 +++++++++++++ .../resources/smoke/infinite_loop-goto.vpr | 6 +++++ .../resources/smoke/infinite_loop-while.vpr | 7 +++++ src/test/resources/smoke/inhale-1.vpr | 5 ++++ src/test/resources/smoke/inhale-2.vpr | 8 ++++++ src/test/resources/smoke/inhale-3.vpr | 9 +++++++ src/test/resources/smoke/loop.vpr | 14 ++++++++++ src/test/resources/smoke/method-abstract.vpr | 2 ++ src/test/resources/smoke/method.vpr | 5 ++++ src/test/resources/smoke/unreachable-1.vpr | 5 ++++ src/test/resources/smoke/unreachable-2.vpr | 27 +++++++++++++++++++ src/test/resources/smoke/unreachable-3.vpr | 25 +++++++++++++++++ 13 files changed, 142 insertions(+) create mode 100644 src/test/resources/smoke/axiom.vpr create mode 100644 src/test/resources/smoke/if.vpr create mode 100644 src/test/resources/smoke/infinite_loop-goto.vpr create mode 100644 src/test/resources/smoke/infinite_loop-while.vpr create mode 100644 src/test/resources/smoke/inhale-1.vpr create mode 100644 src/test/resources/smoke/inhale-2.vpr create mode 100644 src/test/resources/smoke/inhale-3.vpr create mode 100644 src/test/resources/smoke/loop.vpr create mode 100644 src/test/resources/smoke/method-abstract.vpr create mode 100644 src/test/resources/smoke/method.vpr create mode 100644 src/test/resources/smoke/unreachable-1.vpr create mode 100644 src/test/resources/smoke/unreachable-2.vpr create mode 100644 src/test/resources/smoke/unreachable-3.vpr diff --git a/src/test/resources/smoke/axiom.vpr b/src/test/resources/smoke/axiom.vpr new file mode 100644 index 000000000..f64540a88 --- /dev/null +++ b/src/test/resources/smoke/axiom.vpr @@ -0,0 +1,10 @@ +domain Foo { + axiom unsound { + false + } +} + +//:: ExpectedOutput(refute.failed:refutation.true) +method test() +{ +} \ No newline at end of file diff --git a/src/test/resources/smoke/if.vpr b/src/test/resources/smoke/if.vpr new file mode 100644 index 000000000..6100607e5 --- /dev/null +++ b/src/test/resources/smoke/if.vpr @@ -0,0 +1,19 @@ +//:: ExpectedOutput(refute.failed:refutation.true) +method x() + ensures false +{ + //:: ExpectedOutput(refute.failed:refutation.true) + assume 0 == 1 +} + +method test() +{ + var b: Bool + + //:: ExpectedOutput(refute.failed:refutation.true) + if (b) { + x() + } else { + + } +} \ No newline at end of file diff --git a/src/test/resources/smoke/infinite_loop-goto.vpr b/src/test/resources/smoke/infinite_loop-goto.vpr new file mode 100644 index 000000000..0d65bbed1 --- /dev/null +++ b/src/test/resources/smoke/infinite_loop-goto.vpr @@ -0,0 +1,6 @@ +//:: ExpectedOutput(refute.failed:refutation.true) +method test() +{ + label l0 + goto l0 +} \ No newline at end of file diff --git a/src/test/resources/smoke/infinite_loop-while.vpr b/src/test/resources/smoke/infinite_loop-while.vpr new file mode 100644 index 000000000..8ad276ebb --- /dev/null +++ b/src/test/resources/smoke/infinite_loop-while.vpr @@ -0,0 +1,7 @@ +//:: ExpectedOutput(refute.failed:refutation.true) +method test() +{ + while (true) + { + } +} \ No newline at end of file diff --git a/src/test/resources/smoke/inhale-1.vpr b/src/test/resources/smoke/inhale-1.vpr new file mode 100644 index 000000000..c13c46221 --- /dev/null +++ b/src/test/resources/smoke/inhale-1.vpr @@ -0,0 +1,5 @@ +//:: ExpectedOutput(refute.failed:refutation.true) +method test() { + //:: ExpectedOutput(refute.failed:refutation.true) + assume false +} \ No newline at end of file diff --git a/src/test/resources/smoke/inhale-2.vpr b/src/test/resources/smoke/inhale-2.vpr new file mode 100644 index 000000000..8693bab84 --- /dev/null +++ b/src/test/resources/smoke/inhale-2.vpr @@ -0,0 +1,8 @@ +//:: ExpectedOutput(refute.failed:refutation.true) +method test() returns (res: Int) + ensures res == 1 +{ + res := 2 + //:: ExpectedOutput(refute.failed:refutation.true) + assume res == 1 +} \ No newline at end of file diff --git a/src/test/resources/smoke/inhale-3.vpr b/src/test/resources/smoke/inhale-3.vpr new file mode 100644 index 000000000..4768933d5 --- /dev/null +++ b/src/test/resources/smoke/inhale-3.vpr @@ -0,0 +1,9 @@ +field x: Int + +//:: ExpectedOutput(refute.failed:refutation.true) +method test(a: Ref) +{ + inhale acc(a.x) + //:: ExpectedOutput(refute.failed:refutation.true) + inhale acc(a.x) +} \ No newline at end of file diff --git a/src/test/resources/smoke/loop.vpr b/src/test/resources/smoke/loop.vpr new file mode 100644 index 000000000..c146a4a19 --- /dev/null +++ b/src/test/resources/smoke/loop.vpr @@ -0,0 +1,14 @@ +function foo(): Bool +{ + false +} + +method test(a: Bool) +{ + + //:: ExpectedOutput(refute.failed:refutation.true) + while (a) { + //:: ExpectedOutput(refute.failed:refutation.true) + assume foo() + } +} \ No newline at end of file diff --git a/src/test/resources/smoke/method-abstract.vpr b/src/test/resources/smoke/method-abstract.vpr new file mode 100644 index 000000000..fd7e53272 --- /dev/null +++ b/src/test/resources/smoke/method-abstract.vpr @@ -0,0 +1,2 @@ +method abstract() + requires false \ No newline at end of file diff --git a/src/test/resources/smoke/method.vpr b/src/test/resources/smoke/method.vpr new file mode 100644 index 000000000..aabe0f71d --- /dev/null +++ b/src/test/resources/smoke/method.vpr @@ -0,0 +1,5 @@ +//:: ExpectedOutput(refute.failed:refutation.true) +method test() + requires false +{ +} \ No newline at end of file diff --git a/src/test/resources/smoke/unreachable-1.vpr b/src/test/resources/smoke/unreachable-1.vpr new file mode 100644 index 000000000..0929248d3 --- /dev/null +++ b/src/test/resources/smoke/unreachable-1.vpr @@ -0,0 +1,5 @@ +method test() + requires false +{ + unreachable +} \ No newline at end of file diff --git a/src/test/resources/smoke/unreachable-2.vpr b/src/test/resources/smoke/unreachable-2.vpr new file mode 100644 index 000000000..38d530909 --- /dev/null +++ b/src/test/resources/smoke/unreachable-2.vpr @@ -0,0 +1,27 @@ +method test7(a: Bool) + requires !a +{ + + if (a) { + unreachable + assume false + } + + if (a) { + unreachable + while (a) { + assume false + + if (a) { + assume false + } + } + } + + while (a) { + unreachable + if (a) { + assume false + } + } +} \ No newline at end of file diff --git a/src/test/resources/smoke/unreachable-3.vpr b/src/test/resources/smoke/unreachable-3.vpr new file mode 100644 index 000000000..48b116f78 --- /dev/null +++ b/src/test/resources/smoke/unreachable-3.vpr @@ -0,0 +1,25 @@ +method test(a: Bool) + requires !a +{ + if (a) { + unreachable + } + + + var x: Int := 1 + + if (a) { + //:: ExpectedOutput(refute.failed:refutation.true) + assume false + unreachable + x := 0 + + if (x == 1) { + assume false + + if (x == 1) { + assume false + } + } + } +} \ No newline at end of file