diff --git a/silver b/silver index b9f72722..4833685a 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit b9f7272234d6c2a2b84e140979d1b282c74ecba1 +Subproject commit 4833685a51d8f3c4e2793103db4121d9e71e0109 diff --git a/src/main/scala/branchTree/BranchTree.scala b/src/main/scala/branchTree/BranchTree.scala new file mode 100644 index 00000000..7204ac3a --- /dev/null +++ b/src/main/scala/branchTree/BranchTree.scala @@ -0,0 +1,297 @@ +package viper.silicon.branchTree + +import viper.silicon.common.io.PrintWriter +import viper.silicon.verifier.Verifier +import viper.silver.ast +import viper.silver.ast.Exp + +import scala.annotation.tailrec + +class BranchTree extends viper.silver.verifier.errors.BranchTree { + + private def incrementIfFatal(currBranchResultFatal: Int, isResultFatal: Boolean) : Int = + if (isResultFatal) Math.max(currBranchResultFatal,0)+1 else currBranchResultFatal + + protected[branchTree] def extend(branchConditions : Seq[Exp], isResultFatal: Boolean) : Unit = { + (this, branchConditions) match { + case (b:Branch, bcs) if bcs.nonEmpty => + var currBranch = b + var negated = branchConditions.head match { + case _: ast.Not => true + case _ => false + } + var tail = branchConditions.tail + var next = true + while (tail.nonEmpty && next) { + next = false + val headExp = tail.head match { + case ast.Not(exp) => exp + case _ => tail.head + } + (currBranch.left, currBranch.right) match { + case (lb@Branch(exp,_,_,_,_),_) if headExp.toString == exp.toString && negated => + currBranch.leftResFatalCount = incrementIfFatal(currBranch.leftResFatalCount,isResultFatal) + currBranch = lb + next = true + case (_,rb@Branch(exp,_,_,_,_)) if headExp.toString == exp.toString && !negated => + currBranch.rightResFatalCount = incrementIfFatal(currBranch.rightResFatalCount,isResultFatal) + currBranch = rb + next = true + case _ => + } + if (next) { + negated = tail.head match { + case _: ast.Not => true + case _ => false + } + tail = tail.tail + } + } + val errorCount = if (isResultFatal) 1 else -1 + val subTree = BranchTree.generate(Vector((tail, isResultFatal)))// -1 for successful result + if (negated) { + currBranch.left = subTree.get + currBranch.leftResFatalCount = errorCount + } else { + currBranch.right = subTree.get + currBranch.rightResFatalCount = errorCount + } + case _=> + } + } + + + private def even(n: Int) = (n & 1) == 0 + private def buildTreeStrRec(fatalCount: Int) : (Vector[String], Int, Int) = { + this match { + case Leaf if fatalCount == -1 => (Vector("✔"), 0, 0) + case Leaf if fatalCount > 0 => (Vector("Error"), 2, 2) // ✘ + case _ : Branch => this.buildTreeStr() + case _ => (Vector("?"), 0, 0) + } + } + private def buildTreeStr() : (Vector[String], Int, Int) = { + this match { + case Branch(exp, left, right, leftErrCount, rightErrCount) => + val expStr = exp.toString + val expStrLen = expStr.length + + var boxMiddle = "│ " + expStr + (if (even(expStr.length)) " " else "") + " │" + val boxLen = boxMiddle.length + val halfBoxLen = boxLen / 2 + + var (leftStrVec, _, prevLeftRightBoxLen) = left.buildTreeStrRec(leftErrCount) + var (rightStrVec, prevRightLeftBoxLen, _) = right.buildTreeStrRec(rightErrCount) + + val halfExpStrLen = expStrLen / 2 + val leftBoxLen = leftStrVec.head.length + val rightBoxLen = rightStrVec.head.length + + var leftFiller = halfBoxLen - leftBoxLen + if (leftFiller > 0) { + leftStrVec = leftStrVec.map(str => " " * leftFiller + str) + leftFiller = 0 + } else { + leftFiller = -leftFiller + } + + var rightFiller = halfBoxLen - rightBoxLen + if (rightFiller > 0) { + rightStrVec = rightStrVec.map(str => str + " " * rightFiller) + rightFiller = 0 + } else { + rightFiller = -rightFiller + } + + val boxTop = " " * leftFiller + "┌─" + ("─" * halfExpStrLen) + "┴" + ("─" * halfExpStrLen) + "─┐" + " " * rightFiller + boxMiddle = " " * leftFiller + boxMiddle + " " * rightFiller + val boxBottom = " " * leftFiller + "└─" + "─" * halfExpStrLen + "┬" + "─" * halfExpStrLen + "─┘" + " " * rightFiller + + leftStrVec = leftStrVec.map(str => str + " ") + leftStrVec +:= " " * (leftFiller+halfExpStrLen-prevLeftRightBoxLen) + "F┌" + "─" * prevLeftRightBoxLen + "┴" + rightStrVec +:= "─" * prevRightLeftBoxLen + "┐T" + " " * (rightFiller+halfExpStrLen-prevRightLeftBoxLen) + + if (leftStrVec.length > rightStrVec.length){ + for(_ <- 0 to leftStrVec.length - rightStrVec.length) + { + rightStrVec :+= " "*rightStrVec.head.length + } + } else { + for(_ <- 0 to rightStrVec.length - leftStrVec.length) + { + leftStrVec :+= " "*leftStrVec.head.length + } + } + (boxTop +: boxMiddle +: boxBottom +: (leftStrVec zip rightStrVec).map(t => t._1 + t._2), leftFiller + halfBoxLen, rightFiller + halfBoxLen) + case _ => (Vector.empty, -1, -1) // Should not happen + } + } + + + private def fill(vec : Vector[String], filler :Int): Vector[String] = { + vec.grouped(4) + .flatMap(elems => { + Vector( + " "*filler + elems(0) + " "*filler, + " "*filler + elems(1) + "─"*filler, + " "*filler + elems(2) + " "*filler, + " "*filler + elems(3) + " "*filler + ) + }).toVector + } + private def buildPathStr() : String = { + var currTree : BranchTree = this + var maxBoxLen = 5 // for 'Error' + var path = Vector[String]() + var side = Vector[String]() + while (currTree != Leaf) { + currTree match { + case b@Branch(e, l, r, lc, rc) => + val expStr = e.toString + val halfExpStrLen = expStr.length / 2 + val (pathTaken, pathNotTaken) = if (b.isRightFatal) ("T", "F") else ("F","T") + + val boxTop = "┌─" + ("─" * halfExpStrLen) + "┴" + ("─" * halfExpStrLen) + s"─┐ $pathNotTaken " + val boxMiddle = "│ " + expStr + (if (even(expStr.length)) " " else "") + " ├──" + val boxBottom = "└─" + "─" * halfExpStrLen + "┬" + "─" * halfExpStrLen + "─┘ " + val conDown = " " * (halfExpStrLen+2) + s"│$pathTaken " + " " * halfExpStrLen + var box = Vector(boxTop, boxMiddle, boxBottom, conDown) + + val boxLen = boxMiddle.length-2 + val filler = Math.abs(maxBoxLen - boxLen) / 2 + if (maxBoxLen > boxLen) box = fill(box, filler) else path = fill(path, filler) + maxBoxLen = Math.max(maxBoxLen, boxLen) + + (if(b.isRightFatal) lc else rc) match { + case -1 => side ++= Vector("\n"," ✔\n","\n","\n") + case 0 => side ++= Vector("\n"," ?\n","\n","\n") + case _ => side ++= Vector("\n"," Error\n","\n","\n") + } + + path ++= box + currTree = if (b.isRightFatal) r else l // influenced by order of verification results (true branch results before left) + case _ => currTree = Leaf + } + } + val filler = maxBoxLen/2 + val combined = path.zip(side).map(t => t._1+t._2) + ((" "*filler + "│" + " "*filler + "\n") +: combined :+ (" "*(filler-2)+"Error\n")) + .reduce((str, s) => str + s) + } + + def getErrorCount: Int = { + this match { + case Branch(_,_,_,lf,rf) => Math.max(lf,0) + Math.max(rf,0) + case _ => 0 + } + } + + def prettyPrint() : String = { + if (Verifier.config.numberOfErrorsToReport() == 1 || this.getErrorCount == 1) { + this.buildPathStr() + } else { + this.buildTreeStr()._1.reduce((str, s) => str + "\n" + s) + "\n" + } + } + + private def leafToDotNodeContent(fatalCount : Int): String = { + fatalCount match { + case -1 => "label=\"✔\",shape=\"octagon\",style=\"filled\", fillcolor=\"palegreen\"" + case 1 => "label=\"Error\",shape=\"octagon\",style=\"filled\", fillcolor=\"lightsalmon\"" + case _ => "label=\"?\",shape=\"octagon\",style=\"filled\", fillcolor=\"lightgoldenrodyellow\"" + } + } + private def writeDotFileRec(writer: java.io.PrintWriter, visitedCount : Int = 0) : Int = { + this match { + case Branch(exp,left,right,leftResFatalCount,rightResFatalCount) => + val parentIdn = s"B$visitedCount" + writer.write(s" $parentIdn[shape=\"square\",label=\"${exp.toString}\"];\n") + val newVisitedCountLeft = visitedCount + 1 + val visitedCountLeft = left match { + case _ : Branch => + val leftBranchIdn = s"B$newVisitedCountLeft" + val visitedCountLeft_ = left.writeDotFileRec(writer, newVisitedCountLeft) + writer.write(s" $parentIdn -> $leftBranchIdn[label=\"F\"];\n") + visitedCountLeft_ + case Leaf => + val leftLeafIdn = s"B$newVisitedCountLeft" + writer.write(s" $leftLeafIdn[${leafToDotNodeContent(leftResFatalCount)}];\n") + writer.write(s" $parentIdn -> $leftLeafIdn [label=\"F\"];\n") + newVisitedCountLeft + } + val newVisitedCountRight = visitedCountLeft + 1 + val visitedCountRight = right match { + case _ : Branch => + val rightBranchIdn = s"B$newVisitedCountRight" + val visitedCountRight_ = right.writeDotFileRec(writer, newVisitedCountRight) + writer.write(s" $parentIdn -> $rightBranchIdn[label=\"T\"];\n") + visitedCountRight_ + case Leaf => + val rightLeafIdn = s"B$newVisitedCountRight" + writer.write(s" $rightLeafIdn[${leafToDotNodeContent(rightResFatalCount)}];\n") + writer.write(s" $parentIdn -> $rightLeafIdn [label=\"T\"];\n") + newVisitedCountRight + } + visitedCountRight + case _ => 0 + } + } + + def toDotFile(): Unit = { + val writer = PrintWriter(new java.io.File(BranchTree.DotFilePath),append=true) + writer.write("digraph {\n") + this.writeDotFileRec(writer) + writer.write("}\n") + writer.close() + } +} + +object BranchTree { + val DotFilePath = s"${System.getProperty("user.dir")}/${Verifier.config.tempDirectory()}/BranchTree.dot" + + @tailrec + private def generatePathRec(expressions: Seq[Exp], errorCount: Int, result: BranchTree): BranchTree = { + expressions.length match { + case 0 => result + case _ => + val lastExp = expressions.last + lastExp match { + case ast.Not(exp) => + generatePathRec(expressions.init, errorCount, Branch(exp, result, Leaf, errorCount, 0)) + case _ => + generatePathRec(expressions.init, errorCount, Branch(lastExp, Leaf, result, 0, errorCount)) + } + } + } + + @tailrec + private def generateRec(exploredPaths: Vector[(Seq[Exp], Boolean)], result: BranchTree): BranchTree = { // result.instanceOf[Branch] must hold + exploredPaths.length match { + case 0 => result + case _ => + val (expressions, isResultFatal) = exploredPaths.head + result.extend(expressions, isResultFatal) + generateRec(exploredPaths.tail, result) + } + } + + def generate(exploredPaths: Vector[(Seq[Exp], Boolean)]): Option[BranchTree] = { + exploredPaths.length match { + case 0 => None + case _ => + val (expressions, isResultFatal) = exploredPaths.head + val path = generatePathRec(expressions, if (isResultFatal) 1 else -1, Leaf) // -1 or distinguishing successful from no result at leaves + Some(generateRec(exploredPaths.tail, path)) + } + } +} + +object Leaf extends BranchTree +case class Branch(var exp : Exp, + var left: BranchTree, + var right: BranchTree, + protected[branchTree] var leftResFatalCount: Int, + protected[branchTree] var rightResFatalCount: Int) extends BranchTree { + def isLeftFatal : Boolean = leftResFatalCount > 0 + def isRightFatal : Boolean = rightResFatalCount > 0 +} \ No newline at end of file diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala index fbf93b06..6b2a90b8 100644 --- a/src/main/scala/decider/Decider.scala +++ b/src/main/scala/decider/Decider.scala @@ -18,7 +18,7 @@ import viper.silicon.state.terms.{Term, _} import viper.silicon.utils.ast.{extractPTypeFromExp, simplifyVariableName} import viper.silicon.verifier.{Verifier, VerifierComponent} import viper.silver.ast -import viper.silver.ast.{LocalVarWithVersion, NoPosition} +import viper.silver.ast.{Exp, LocalVarWithVersion, NoPosition} import viper.silver.components.StatefulComponent import viper.silver.parser.{PKw, PPrimitiv, PReserved, PType} import viper.silver.reporter.{ConfigurationConfirmation, InternalWarningMessage} @@ -129,7 +129,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => private var _proverOptions: Map[String, String] = Map.empty private var _proverResetOptions: Map[String, String] = Map.empty private val _debuggerAssumedTerms: mutable.Set[Term] = mutable.Set.empty - + def functionDecls: Set[FunctionDecl] = _declaredFreshFunctions def macroDecls: Vector[MacroDecl] = _declaredFreshMacros @@ -256,6 +256,16 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => def setPathConditionMark(): Mark = pathConditions.mark() + def getBranchConditionsExp(): Seq[Exp] = { + this.pcs.branchConditionExps.map(_._1) + .filterNot(e => e.isInstanceOf[viper.silver.ast.TrueLit]) /* remove "true" bcs introduced by viper.silicon.utils.ast.BigAnd */ + .sortBy(_.pos match { + /* Order branchconditions according to source position */ + case pos: viper.silver.ast.HasLineColumn => (pos.line, pos.column) + case _ => (-1, -1) + }) + } + /* Assuming facts */ def startDebugSubExp(): Unit = { diff --git a/src/main/scala/decider/PathConditions.scala b/src/main/scala/decider/PathConditions.scala index de38c28c..01783861 100644 --- a/src/main/scala/decider/PathConditions.scala +++ b/src/main/scala/decider/PathConditions.scala @@ -13,7 +13,7 @@ import viper.silicon.state.terms._ import viper.silicon.utils.Counter import viper.silicon.verifier.Verifier import viper.silver.ast -import viper.silver.ast.TrueLit +import viper.silver.ast.{Exp, TrueLit} /* * Interfaces */ @@ -61,6 +61,7 @@ trait RecordedPathConditions { trait PathConditionStack extends RecordedPathConditions { def setCurrentBranchCondition(condition: Term, conditionExp: (ast.Exp, Option[ast.Exp])): Unit + def getBranchConditionsExp(): Seq[Exp] def add(assumption: Term): Unit def addDefinition(assumption: Term): Unit def add(declaration: Decl): Unit @@ -459,6 +460,16 @@ private[decider] class LayeredPathConditionStack layers.head.branchConditionExp = conditionExp } + def getBranchConditionsExp(): Seq[Exp] = { + branchConditionExps.map(_._1) + .filterNot(e => e.isInstanceOf[viper.silver.ast.TrueLit]) /* remove "true" bcs introduced by viper.silicon.utils.ast.BigAnd */ + .sortBy(_.pos match { + /* Order branchconditions according to source position */ + case pos: viper.silver.ast.HasLineColumn => (pos.line, pos.column) + case _ => (-1, -1) + }) + } + def startDebugSubExp(): Unit = { layers.head.startDebugSubExp() } diff --git a/src/main/scala/interfaces/Verification.scala b/src/main/scala/interfaces/Verification.scala index ad52d3bf..caa71711 100644 --- a/src/main/scala/interfaces/Verification.scala +++ b/src/main/scala/interfaces/Verification.scala @@ -14,7 +14,7 @@ import viper.silicon.state.terms.{FunctionDecl, MacroDecl, Term} import viper.silicon.state.{State, Store} import viper.silicon.verifier.Verifier import viper.silver.ast -import viper.silver.ast.Program +import viper.silver.ast.{Exp, Program} import viper.silver.verifier._ /* @@ -28,9 +28,19 @@ import viper.silver.verifier._ /* TODO: Make VerificationResult immutable */ sealed abstract class VerificationResult { var previous: Vector[VerificationResult] = Vector() //Sets had problems with equality + var exploredBranchPaths: Vector[(Seq[Exp],Boolean)] = Vector() val continueVerification: Boolean = true var isReported: Boolean = false + def getExploredBranchPaths(r: VerificationResult = this) : Vector[(Seq[Exp], Boolean)] = { + r.exploredBranchPaths ++ r.previous.flatMap(x => x.previous.length match { + case 0 => x.exploredBranchPaths + case _ => + val recRes = x.previous.flatMap(getExploredBranchPaths) + x.exploredBranchPaths ++ recRes + }) + } + def isFatal: Boolean def &&(other: => VerificationResult): VerificationResult @@ -61,7 +71,6 @@ sealed abstract class VerificationResult { } this } - } } @@ -100,7 +109,6 @@ case class Failure/*[ST <: Store[ST], S <: State[ST, H, S]]*/ (message: VerificationError, override val continueVerification: Boolean = true) extends FatalResult { - override lazy val toString: String = message.readableMessage } diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index fd3e34b9..8231a78c 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -589,7 +589,6 @@ object consumer extends ConsumptionRules { ) } - private def evalAndAssert(s: State, e: ast.Exp, returnSnap: Boolean, pve: PartialVerificationError, v: Verifier) (Q: (State, Option[Term], Verifier) => VerificationResult) : VerificationResult = { @@ -620,7 +619,9 @@ object consumer extends ConsumptionRules { v2.decider.assert(termToAssert) { case true => v2.decider.assume(t, Option.when(withExp)(e), eNew) - QS(s3, v2) + val r = QS(s3, v2) + r.exploredBranchPaths +:= (v.decider.pcs.getBranchConditionsExp(),false) + r case false => val failure = createFailure(pve dueTo AssertionFalse(e), v2, s3, termToAssert, eNew) if (s3.retryLevel == 0 && v2.reportFurtherErrors()){ diff --git a/src/main/scala/rules/SymbolicExecutionRules.scala b/src/main/scala/rules/SymbolicExecutionRules.scala index 6f18728d..d8ce63f0 100644 --- a/src/main/scala/rules/SymbolicExecutionRules.scala +++ b/src/main/scala/rules/SymbolicExecutionRules.scala @@ -84,15 +84,7 @@ trait SymbolicExecutionRules { None } - val branchconditions = if (Verifier.config.enableBranchconditionReporting()) { - v.decider.pcs.branchConditionExps.map(_._1) - .filterNot(e => e.isInstanceOf[viper.silver.ast.TrueLit]) /* remove "true" bcs introduced by viper.silicon.utils.ast.BigAnd */ - .sortBy(_.pos match { - /* Order branchconditions according to source position */ - case pos: viper.silver.ast.HasLineColumn => (pos.line, pos.column) - case _ => (-1, -1) - }) - } else Seq() + val branchConditions = v.decider.pcs.getBranchConditionsExp() if (Verifier.config.enableDebugging()){ val assumptions = v.decider.pcs.assumptionExps @@ -100,10 +92,12 @@ trait SymbolicExecutionRules { counterexample, reasonUnknown, Some(s), Some(v), v.decider.prover.getAllEmits(), v.decider.prover.preambleAssumptions, v.decider.macroDecls, v.decider.functionDecls, assumptions, failedAssert, failedAssertExp.get)) } else { - res.failureContexts = Seq(SiliconFailureContext(branchconditions, counterexample, reasonUnknown)) + val branchConditionsReported = if (Verifier.config.enableBranchconditionReporting()) branchConditions else Seq() + res.failureContexts = Seq(SiliconFailureContext(branchConditionsReported, counterexample, reasonUnknown)) } - Failure(res, v.reportFurtherErrors()) - + val f = Failure(res, v.reportFurtherErrors()) + f.exploredBranchPaths +:= (branchConditions, true) + f } } diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index 9b483ff4..604ce311 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/src/main/scala/supporters/MethodSupporter.scala @@ -12,6 +12,7 @@ import viper.silver.components.StatefulComponent import viper.silver.verifier.errors._ import viper.silicon.interfaces._ import viper.silicon.decider.Decider +import viper.silicon.branchTree.{Branch, BranchTree} import viper.silicon.logger.records.data.WellformednessCheckRecord import viper.silicon.rules.{consumer, executionFlowController, executor, producer} import viper.silicon.state.{Heap, State, Store} @@ -20,6 +21,7 @@ import viper.silicon.verifier.{Verifier, VerifierComponent} import viper.silicon.utils.freshSnap import viper.silver.reporter.AnnotationWarning import viper.silicon.{Map, toMap} +import viper.silver.verifier.reasons.BranchFails /* TODO: Consider changing the DefaultMethodVerificationUnitProvider into a SymbolicExecutionRule */ @@ -117,7 +119,25 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif v.decider.resetProverOptions() symbExLog.closeMemberScope() - Seq(result) + + BranchTree.generate(result.getExploredBranchPaths()) match { + case Some(branchTree : Branch) if branchTree.getErrorCount > 0 => + val method = s.currentMember.get.asInstanceOf[ast.Method] + Seq(result, Failure( + BranchFailed( + method, + BranchFails( + method, + branchTree, + Seq(BeamInfo(branchTree.exp, + branchTree.isLeftFatal, + branchTree.isRightFatal) + ) + ) + ) + )) + case _=> Seq(result) + } } /* Lifetime */ diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index b395ed21..84df895b 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -630,4 +630,4 @@ class DefaultMainVerifier(config: Config, */ private def extractAllVerificationResults(res: VerificationResult): Seq[VerificationResult] = res :: res.previous.toList -} +} \ No newline at end of file diff --git a/src/test/resources/branchTreeTests/allPathsCorrect.vpr b/src/test/resources/branchTreeTests/allPathsCorrect.vpr new file mode 100644 index 00000000..f00c6ff1 --- /dev/null +++ b/src/test/resources/branchTreeTests/allPathsCorrect.vpr @@ -0,0 +1,10 @@ +define P(z) z == true + +method foo(b: Bool) returns (z: Bool) +ensures P(z) { + if (b) { + z := true + } else { + z := true + } +} \ No newline at end of file diff --git a/src/test/resources/branchTreeTests/default/allPathsCorrect_expected b/src/test/resources/branchTreeTests/default/allPathsCorrect_expected new file mode 100644 index 00000000..49263a9e --- /dev/null +++ b/src/test/resources/branchTreeTests/default/allPathsCorrect_expected @@ -0,0 +1 @@ +Verification successful. \ No newline at end of file diff --git a/src/test/resources/branchTreeTests/default/firstPathFails_expected b/src/test/resources/branchTreeTests/default/firstPathFails_expected new file mode 100644 index 00000000..118145ee --- /dev/null +++ b/src/test/resources/branchTreeTests/default/firstPathFails_expected @@ -0,0 +1,10 @@ + │ + ┌─┴─┐ F + │ a ├──── ? + └─┬─┘ + │T +┌───┴───┐ F +│ bcde ├── ? +└───┬───┘ + │T + Error diff --git a/src/test/resources/branchTreeTests/default/lastPathFails_expected b/src/test/resources/branchTreeTests/default/lastPathFails_expected new file mode 100644 index 00000000..abf6886c --- /dev/null +++ b/src/test/resources/branchTreeTests/default/lastPathFails_expected @@ -0,0 +1,10 @@ + │ +┌─┴─┐ T +│ a ├── ✔ +└─┬─┘ + │F +┌─┴─┐ T +│ c ├── ✔ +└─┬─┘ + │F +Error diff --git a/src/test/resources/branchTreeTests/default/multipleMethods_expected b/src/test/resources/branchTreeTests/default/multipleMethods_expected new file mode 100644 index 00000000..360dffef --- /dev/null +++ b/src/test/resources/branchTreeTests/default/multipleMethods_expected @@ -0,0 +1,21 @@ + │ + ┌─┴─┐ F + │ a ├──── ? + └─┬─┘ + │T +┌───┴───┐ F +│ bcde ├── ? +└───┬───┘ + │T + Error + + │ +┌─┴─┐ T +│ a ├── ✔ +└─┬─┘ + │F +┌─┴─┐ T +│ c ├── ✔ +└─┬─┘ + │F +Error diff --git a/src/test/resources/branchTreeTests/default/noBranches_expected b/src/test/resources/branchTreeTests/default/noBranches_expected new file mode 100644 index 00000000..49263a9e --- /dev/null +++ b/src/test/resources/branchTreeTests/default/noBranches_expected @@ -0,0 +1 @@ +Verification successful. \ No newline at end of file diff --git a/src/test/resources/branchTreeTests/default/onlyIf_expected b/src/test/resources/branchTreeTests/default/onlyIf_expected new file mode 100644 index 00000000..2035a798 --- /dev/null +++ b/src/test/resources/branchTreeTests/default/onlyIf_expected @@ -0,0 +1,6 @@ + │ +┌─┴─┐ F +│ d ├── ? +└─┬─┘ + │T +Error diff --git a/src/test/resources/branchTreeTests/default/while_expected b/src/test/resources/branchTreeTests/default/while_expected new file mode 100644 index 00000000..3b4a031d --- /dev/null +++ b/src/test/resources/branchTreeTests/default/while_expected @@ -0,0 +1,6 @@ + │ +┌─┴─┐ T +│ a ├── ? +└─┬─┘ + │F +Error diff --git a/src/test/resources/branchTreeTests/firstPathFails.vpr b/src/test/resources/branchTreeTests/firstPathFails.vpr new file mode 100644 index 00000000..e896a90f --- /dev/null +++ b/src/test/resources/branchTreeTests/firstPathFails.vpr @@ -0,0 +1,19 @@ +define P(z) z == true + +method foo(a: Bool, bcde: Bool, c: Bool) returns (z: Bool) +requires a ==> c +ensures P(z) { + if (a) { + if (bcde) { + z := !(bcde && a) // failure + } else { + z := (bcde && !a) + } + } else { + if (c) { + z := !(c && a) + } else { + z := !(!c && !a) + } + } +} \ No newline at end of file diff --git a/src/test/resources/branchTreeTests/lastPathFails.vpr b/src/test/resources/branchTreeTests/lastPathFails.vpr new file mode 100644 index 00000000..a1618e5d --- /dev/null +++ b/src/test/resources/branchTreeTests/lastPathFails.vpr @@ -0,0 +1,19 @@ +define P(z) z == true + +method foo(a: Bool, bcde: Bool, c: Bool) returns (z: Bool) +requires a ==> c +ensures P(z) { + if (a) { + if (bcde) { + z := (bcde && a) + } else { + z := !(bcde && !a) + } + } else { + if (c) { + z := !(c && a) + } else { + z := !(!c && !a) // failure + } + } +} \ No newline at end of file diff --git a/src/test/resources/branchTreeTests/multipleMethods.vpr b/src/test/resources/branchTreeTests/multipleMethods.vpr new file mode 100644 index 00000000..f527fed0 --- /dev/null +++ b/src/test/resources/branchTreeTests/multipleMethods.vpr @@ -0,0 +1,37 @@ +define P(z) z == true + +method foo(a: Bool, bcde: Bool, c: Bool) returns (z: Bool) +requires a ==> c +ensures P(z) { + if (a) { + if (bcde) { + z := !(bcde && a) // failure + } else { + z := (bcde && !a) + } + } else { + if (c) { + z := !(c && a) + } else { + z := !(!c && !a) + } + } +} + +method bar(a: Bool, bcde: Bool, c: Bool) returns (z: Bool) +requires a ==> c +ensures P(z) { + if (a) { + if (bcde) { + z := (bcde && a) + } else { + z := !(bcde && !a) + } + } else { + if (c) { + z := !(c && a) + } else { + z := !(!c && !a) // failure + } + } +} \ No newline at end of file diff --git a/src/test/resources/branchTreeTests/noBranches.vpr b/src/test/resources/branchTreeTests/noBranches.vpr new file mode 100644 index 00000000..7ae9e52e --- /dev/null +++ b/src/test/resources/branchTreeTests/noBranches.vpr @@ -0,0 +1,6 @@ +define P(z) z == true + +method foo(b: Bool) returns (z: Bool) +ensures P(z) { + z := true +} \ No newline at end of file diff --git a/src/test/resources/branchTreeTests/onlyIf.vpr b/src/test/resources/branchTreeTests/onlyIf.vpr new file mode 100644 index 00000000..6f8c13eb --- /dev/null +++ b/src/test/resources/branchTreeTests/onlyIf.vpr @@ -0,0 +1,14 @@ +define P(z) z == true + +method foo(a: Int, b: Int, d: Bool) returns (z: Bool) +ensures P(z) { + var a_ : Int := a + var b_ : Int := b + if (d) { + a_ := 3 + b_ := 3 + } + var c: Int + c := a_ / b_ + z := c > 1 +} \ No newline at end of file diff --git a/src/test/resources/branchTreeTests/reportAllErrors/allPathsCorrect_expected b/src/test/resources/branchTreeTests/reportAllErrors/allPathsCorrect_expected new file mode 100644 index 00000000..49263a9e --- /dev/null +++ b/src/test/resources/branchTreeTests/reportAllErrors/allPathsCorrect_expected @@ -0,0 +1 @@ +Verification successful. \ No newline at end of file diff --git a/src/test/resources/branchTreeTests/reportAllErrors/firstPathFails_expected b/src/test/resources/branchTreeTests/reportAllErrors/firstPathFails_expected new file mode 100644 index 00000000..ef79e48e --- /dev/null +++ b/src/test/resources/branchTreeTests/reportAllErrors/firstPathFails_expected @@ -0,0 +1,9 @@ + ┌─┴─┐ + │ a │ + └─┬─┘ + F┌──┴─────┐T + ┌─┴─┐ ┌───┴───┐ + │ c │ │ bcde │ + └─┬─┘ └───┬───┘ + F┌──┴┐T F┌──┴──┐T +Error ✔ Error Error diff --git a/src/test/resources/branchTreeTests/reportAllErrors/lastPathFails_expected b/src/test/resources/branchTreeTests/reportAllErrors/lastPathFails_expected new file mode 100644 index 00000000..abf6886c --- /dev/null +++ b/src/test/resources/branchTreeTests/reportAllErrors/lastPathFails_expected @@ -0,0 +1,10 @@ + │ +┌─┴─┐ T +│ a ├── ✔ +└─┬─┘ + │F +┌─┴─┐ T +│ c ├── ✔ +└─┬─┘ + │F +Error diff --git a/src/test/resources/branchTreeTests/reportAllErrors/noBranches_expected b/src/test/resources/branchTreeTests/reportAllErrors/noBranches_expected new file mode 100644 index 00000000..49263a9e --- /dev/null +++ b/src/test/resources/branchTreeTests/reportAllErrors/noBranches_expected @@ -0,0 +1 @@ +Verification successful. \ No newline at end of file diff --git a/src/test/resources/branchTreeTests/reportAllErrors/onlyIf_expected b/src/test/resources/branchTreeTests/reportAllErrors/onlyIf_expected new file mode 100644 index 00000000..b43faf03 --- /dev/null +++ b/src/test/resources/branchTreeTests/reportAllErrors/onlyIf_expected @@ -0,0 +1,5 @@ + ┌─┴─┐ + │ d │ + └─┬─┘ + F┌──┴──┐T +Error Error diff --git a/src/test/resources/branchTreeTests/reportAllErrors/while_expected b/src/test/resources/branchTreeTests/reportAllErrors/while_expected new file mode 100644 index 00000000..3b4a031d --- /dev/null +++ b/src/test/resources/branchTreeTests/reportAllErrors/while_expected @@ -0,0 +1,6 @@ + │ +┌─┴─┐ T +│ a ├── ? +└─┬─┘ + │F +Error diff --git a/src/test/resources/branchTreeTests/reportTwoErrors/firstPathFails_expected b/src/test/resources/branchTreeTests/reportTwoErrors/firstPathFails_expected new file mode 100644 index 00000000..4e978087 --- /dev/null +++ b/src/test/resources/branchTreeTests/reportTwoErrors/firstPathFails_expected @@ -0,0 +1,9 @@ +┌─┴─┐ +│ a │ +└─┬─┘ +F┌┴─────┐T + ? ┌───┴───┐ + │ bcde │ + └───┬───┘ + F┌──┴──┐T + Error Error diff --git a/src/test/resources/branchTreeTests/reportTwoErrors/lastPathFails_expected b/src/test/resources/branchTreeTests/reportTwoErrors/lastPathFails_expected new file mode 100644 index 00000000..abf6886c --- /dev/null +++ b/src/test/resources/branchTreeTests/reportTwoErrors/lastPathFails_expected @@ -0,0 +1,10 @@ + │ +┌─┴─┐ T +│ a ├── ✔ +└─┬─┘ + │F +┌─┴─┐ T +│ c ├── ✔ +└─┬─┘ + │F +Error diff --git a/src/test/resources/branchTreeTests/while.vpr b/src/test/resources/branchTreeTests/while.vpr new file mode 100644 index 00000000..307ed321 --- /dev/null +++ b/src/test/resources/branchTreeTests/while.vpr @@ -0,0 +1,13 @@ +define P(z) z == true + +method foo(a: Bool, bcde: Bool, c: Bool) returns (z: Bool) +requires a ==> c +ensures P(z) { + while (a) { + if (bcde) { + z := !(bcde && a) + } else { + z := !(bcde && !a) + } + } +} \ No newline at end of file diff --git a/src/test/scala/BranchTreeTests.scala b/src/test/scala/BranchTreeTests.scala new file mode 100644 index 00000000..3e4a82f5 --- /dev/null +++ b/src/test/scala/BranchTreeTests.scala @@ -0,0 +1,85 @@ +// 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 distrcibuted with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. +// +// Copyright (c) 2011-2019 ETH Zurich. + +import org.scalatest.funsuite.AnyFunSuite +import viper.silver.ast.utility.DiskLoader + +import java.nio.file.Paths + +class BranchTreeTests extends AnyFunSuite { + def executeTestDefault(fileName: String) : Unit = executeTest(fileName, "default") + + test("FirstPathFailsPath") { + executeTestDefault("firstPathFails") + } + test("LastPathFailsPath") { + executeTestDefault("lastPathFails") + } + test("WhilePath") { + executeTestDefault("while") + } + test("OnlyIfPath") { + executeTestDefault("onlyIf") + } + test("AllPathsPath") { + executeTestDefault("allPathsCorrect") + } + test("NoBranchesPath") { + executeTestDefault("noBranches") + } + test("MultipleMethodsPath") { + executeTestDefault("multipleMethods") + } + + def executeTestReportAllErrors(fileName: String) : Unit = executeTest(fileName, "reportAllErrors", List("--numberOfErrorsToReport", "0")) + + test("FirstPathFailsTreeAll") { + executeTestReportAllErrors("firstPathFails") + } + test("LastPathFailsTreeAll") { + executeTestReportAllErrors("lastPathFails") + } + test("WhileTreeAll") { + executeTestReportAllErrors("while") + } + test("OnlyIfTreeAll") { + executeTestReportAllErrors("onlyIf") + } + test("AllPathsCorrectTreeAll") { + executeTestReportAllErrors("allPathsCorrect") + } + test("NoBranchesTreeAll") { + executeTestReportAllErrors("noBranches") + } + + def executeTestReportTwoErrors(fileName: String) : Unit = executeTest(fileName, "reportTwoErrors", List("--numberOfErrorsToReport", "2")) + + test("FirstPathFailsTreeTwo") { + executeTestReportTwoErrors("firstPathFails") + } + test("LastPathFailsTreeTwo") { + executeTestReportTwoErrors("lastPathFails") + } + + def getExpectedString(fileName: String, expectedFolder : String): String = { + val expectedFile = getClass.getClassLoader.getResource(s"branchTreeTests/$expectedFolder/"+fileName+"_expected") + DiskLoader.loadContent(Paths.get(expectedFile.toURI)).get + } + + def executeTest(fileName: String, expectedFolder : String, args: List[String] = List.empty) + : Unit = { + val expected = getExpectedString(fileName, expectedFolder) + + val frontend = tests.instantiateFrontend(args) + val program = tests.loadProgram("branchTreeTests/",fileName, frontend) + val actual = frontend.verifier.verify(program).toString.split("\n") + .filterNot(l => l.startsWith(" (")||l.startsWith(" [")||l.startsWith("Verification failed")) + .map(str => str+"\n").reduce((str,s)=>str+s) + assert(actual.contains(expected)) + } +} + + diff --git a/src/test/scala/tests.scala b/src/test/scala/tests.scala index 4cb16004..35197277 100644 --- a/src/test/scala/tests.scala +++ b/src/test/scala/tests.scala @@ -6,7 +6,7 @@ import java.nio.file.{Path, Paths} import viper.silver.ast.Program -import viper.silver.frontend.{SilFrontend, SilFrontendConfig, DefaultStates} +import viper.silver.frontend.{DefaultStates, SilFrontend, SilFrontendConfig} import viper.silver.verifier.{AbstractError, AbstractVerificationError, VerificationResult, Verifier, Failure => SilFailure} import viper.silicon.Silicon @@ -34,11 +34,11 @@ package object tests { override def verifier: Verifier = this._verifier.get } - def instantiateFrontend(): SilFrontend = { + def instantiateFrontend(args: List[String] = List.empty): SilFrontend = { val frontend = new DummyFrontend val backend = new Silicon(List("startedBy" -> s"Unit test ${this.getClass.getSimpleName}")) - backend.parseCommandLine(List("--ignoreFile", "dummy.sil")) + backend.parseCommandLine(List("--ignoreFile", "dummy.sil")++args) backend.start() frontend.init(backend)