From 8c16f3dd599e5f659bc89231dc7247df2bfe4470 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Sat, 18 Jan 2025 20:31:08 +0100 Subject: [PATCH 01/39] Display Failing Branches --- silver | 2 +- src/main/scala/rules/Brancher.scala | 190 ++++++++++++++++++---------- 2 files changed, 122 insertions(+), 70 deletions(-) diff --git a/silver b/silver index b9f72722..85c047d2 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit b9f7272234d6c2a2b84e140979d1b282c74ecba1 +Subproject commit 85c047d22a71d28e7b157a10664443ab3473dfd3 diff --git a/src/main/scala/rules/Brancher.scala b/src/main/scala/rules/Brancher.scala index fc2422b4..3c2885e9 100644 --- a/src/main/scala/rules/Brancher.scala +++ b/src/main/scala/rules/Brancher.scala @@ -15,10 +15,49 @@ import viper.silicon.state.State import viper.silicon.state.terms.{FunctionDecl, MacroDecl, Not, Term} import viper.silicon.verifier.Verifier import viper.silver.ast +import viper.silver.ast.Exp import viper.silver.reporter.BranchFailureMessage import viper.silver.verifier.Failure - -import scala.collection.immutable.HashSet +import viper.silver.verifier.errors.PostconditionViolatedBranch +import viper.silver.verifier.reasons.AssertionFalseAtBranch + +import java.io.Serializable +import scala.collection.immutable.{HashSet, Seq} +import scala.collection.mutable + + +case class BranchFailurePath(condition : Exp, taken : Boolean, sideResult : VerificationResult) +object branchFailurePaths extends mutable.HashMap[String, Vector[BranchFailurePath]] { + def prettyPrintPath(key : String) : String = { + var res = "" + val branchFailurePath = branchFailurePaths.get(key) + if (branchFailurePath.isDefined) { + val mappedBfp = branchFailurePath.get.collect(bf => { + val condStr = bf.condition.toString + val even = (n : Int) => (n & 1) == 0 + "│ "+ condStr + (if (even(condStr.length)) " " else "") + " ├" + }) + val maxLen = mappedBfp.map(_.length).max + val halfLen = maxLen / 2 + for ((condStr, bfp) <- mappedBfp zip branchFailurePath.get) { + val numChars = (maxLen - condStr.length) / 2 + val border = " "*numChars+"┌"+("─" * (condStr.length-2))+"┐"+" "*numChars + val borderTop = border + " " + (if (bfp.taken) "F" else "T") + "\n" + val halfBoxLen = (condStr.length-2) / 2 + val borderBottom = " "*numChars+"└"+("─" * halfBoxLen + "┬" + "─" * halfBoxLen)+"┘"+" "*numChars + "\n" + val sideResultSymbol = bfp.sideResult match { + case _: Unreachable => "?" + case _ => "✔" + } + val condStr_ = " "*numChars+condStr+"-"*numChars+s"──▶ "+ sideResultSymbol + "\n" + res += borderTop + condStr_ + borderBottom + res += " "*halfLen+"▼"+" "+(if (bfp.taken) "T" else "F")+"\n" + } + res += " "*(halfLen-2)+"Error"+"\n" + } + res + } +} trait BranchingRules extends SymbolicExecutionRules { def branch(s: State, @@ -28,7 +67,7 @@ trait BranchingRules extends SymbolicExecutionRules { fromShortCircuitingAnd: Boolean = false) (fTrue: (State, Verifier) => VerificationResult, fFalse: (State, Verifier) => VerificationResult) - : VerificationResult + : VerificationResult } object brancher extends BranchingRules { @@ -39,7 +78,7 @@ object brancher extends BranchingRules { fromShortCircuitingAnd: Boolean = false) (fThen: (State, Verifier) => VerificationResult, fElse: (State, Verifier) => VerificationResult) - : VerificationResult = { + : VerificationResult = { val negatedCondition = Not(condition) val negatedConditionExp = ast.Not(conditionExp._1)(pos = conditionExp._1.pos, info = conditionExp._1.info, ast.NoTrafos) @@ -51,29 +90,29 @@ object brancher extends BranchingRules { * (2) the branch condition contains a quantified variable */ val skipPathFeasibilityCheck = ( - fromShortCircuitingAnd - || ( s.quantifiedVariables.nonEmpty - && s.quantifiedVariables.map(_._1).exists(condition.freeVariables.contains)) - ) + fromShortCircuitingAnd + || ( s.quantifiedVariables.nonEmpty + && s.quantifiedVariables.map(_._1).exists(condition.freeVariables.contains)) + ) /* True if the then-branch is to be explored */ val executeThenBranch = ( - skipPathFeasibilityCheck - || !v.decider.check(negatedCondition, Verifier.config.checkTimeout())) + skipPathFeasibilityCheck + || !v.decider.check(negatedCondition, Verifier.config.checkTimeout())) /* False if the then-branch is to be explored */ val executeElseBranch = ( - !executeThenBranch /* Assumes that ast least one branch is feasible */ - || skipPathFeasibilityCheck - || !v.decider.check(condition, Verifier.config.checkTimeout())) + !executeThenBranch /* Assumes that ast least one branch is feasible */ + || skipPathFeasibilityCheck + || !v.decider.check(condition, Verifier.config.checkTimeout())) val parallelizeElseBranch = s.parallelizeBranches && executeThenBranch && executeElseBranch -// val additionalPaths = -// if (executeThenBranch && exploreFalseBranch) 1 -// else 0 + // val additionalPaths = + // if (executeThenBranch && exploreFalseBranch) 1 + // else 0 -// bookkeeper.branches += additionalPaths + // bookkeeper.branches += additionalPaths val cnt = v.counter(this).next() @@ -188,64 +227,77 @@ object brancher extends BranchingRules { CompletableFuture.completedFuture(Seq(Unreachable())) } - val res = { - val thenRes = if (executeThenBranch) { - v.symbExLog.markReachable(uidBranchPoint) - executionFlowController.locally(s, v)((s1, v1) => { - v1.decider.prover.comment(s"[then-branch: $cnt | $condition]") - v1.decider.setCurrentBranchCondition(condition, conditionExp) - - fThen(v1.stateConsolidator(s1).consolidateOptionally(s1, v1), v1) - }) - } else { - Unreachable() - } - if (thenRes.isFatal && !thenRes.isReported && s.parallelizeBranches && s.isLastRetry) { - thenRes.isReported = true - v.reporter.report(BranchFailureMessage("silicon", s.currentMember.get.asInstanceOf[ast.Member with Serializable], - condenseToViperResult(Seq(thenRes)).asInstanceOf[Failure])) - } - thenRes - }.combine({ - - /* [BRANCH-PARALLELISATION] */ - var rs: Seq[VerificationResult] = null - try { - if (parallelizeElseBranch) { - val pcsAfterThenBranch = v.decider.pcs.duplicate() - val noOfErrorsAfterThenBranch = v.errorsReportedSoFar.get() - - val pcsBefore = v.decider.pcs - - rs = elseBranchFuture.get() + // Then result + val thenRes = if (executeThenBranch) { + v.symbExLog.markReachable(uidBranchPoint) + executionFlowController.locally(s, v)((s1, v1) => { + v1.decider.prover.comment(s"[then-branch: $cnt | $condition]") + v1.decider.setCurrentBranchCondition(condition, conditionExp) + + fThen(v1.stateConsolidator(s1).consolidateOptionally(s1, v1), v1) + }) + } else { + Unreachable() + } + if (thenRes.isFatal && !thenRes.isReported && s.parallelizeBranches && s.isLastRetry) { + thenRes.isReported = true + v.reporter.report(BranchFailureMessage("silicon", s.currentMember.get.asInstanceOf[ast.Member with Serializable], + condenseToViperResult(Seq(thenRes)).asInstanceOf[Failure])) + } - if (v.decider.pcs != pcsBefore && v.uniqueId != elseBranchVerifier){ - // we have done other work during the join, need to reset - v.decider.prover.comment(s"Resetting path conditions after interruption") - v.decider.setPcs(pcsAfterThenBranch) - v.errorsReportedSoFar.set(noOfErrorsAfterThenBranch) - v.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract) - v.decider.resetProverOptions() - v.decider.setProverOptions(proverArgsOfCurrentDecider) - } - } else { - rs = elseBranchFuture.get() + // Else result + /* [BRANCH-PARALLELISATION] */ + var elseResults: Seq[VerificationResult] = null + try { + if (parallelizeElseBranch) { + val pcsAfterThenBranch = v.decider.pcs.duplicate() + val noOfErrorsAfterThenBranch = v.errorsReportedSoFar.get() + + val pcsBefore = v.decider.pcs + + elseResults = elseBranchFuture.get() + + if (v.decider.pcs != pcsBefore && v.uniqueId != elseBranchVerifier){ + // we have done other work during the join, need to reset + v.decider.prover.comment(s"Resetting path conditions after interruption") + v.decider.setPcs(pcsAfterThenBranch) + v.errorsReportedSoFar.set(noOfErrorsAfterThenBranch) + v.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract) + v.decider.resetProverOptions() + v.decider.setProverOptions(proverArgsOfCurrentDecider) } - } catch { - case ex: ExecutionException => - ex.getCause.printStackTrace() - throw ex + } else { + elseResults = elseBranchFuture.get() } + } catch { + case ex: ExecutionException => + ex.getCause.printStackTrace() + throw ex + } - assert(rs.length == 1, s"Expected a single verification result but found ${rs.length}") - if (rs.head.isFatal && !rs.head.isReported && s.parallelizeBranches && s.isLastRetry) { - rs.head.isReported = true - v.reporter.report(BranchFailureMessage("silicon", s.currentMember.get.asInstanceOf[ast.Member with Serializable], - condenseToViperResult(Seq(rs.head)).asInstanceOf[Failure])) + assert(elseResults.length == 1, s"Expected a single verification result but found ${elseResults.length}") + if (elseResults.head.isFatal && !elseResults.head.isReported && s.parallelizeBranches && s.isLastRetry) { + elseResults.head.isReported = true + v.reporter.report(BranchFailureMessage("silicon", s.currentMember.get.asInstanceOf[ast.Member with Serializable], + condenseToViperResult(Seq(elseResults.head)).asInstanceOf[Failure])) + } + val elseRes = elseResults.head + + val res = thenRes.combine(elseRes, alwaysWaitForOther = parallelizeElseBranch) + + if (s.currentMember.isDefined && res.isFatal) { + val bfp = branchFailurePaths.get(s.currentMember.get.name) + val sideRes = if (thenRes.isFatal) elseRes else thenRes + val newBfp = BranchFailurePath(conditionExp._1, thenRes.isFatal, sideRes) +: bfp.getOrElse(Vector[BranchFailurePath]()) + branchFailurePaths.put(s.currentMember.get.name, newBfp) + if ((thenRes.isFatal || elseRes.isFatal) && v.decider.pcs.branchConditionExps.length == 0) { + val firstCond = newBfp.head.condition + val failure = Failure(Seq(PostconditionViolatedBranch(firstCond, AssertionFalseAtBranch(firstCond, branchFailurePaths.prettyPrintPath(s.currentMember.get.name))))) + v.reporter.report(BranchFailureMessage(s"silicon", s.currentMember.get.asInstanceOf[ast.Member with Serializable], failure)) + branchFailurePaths.remove(s.currentMember.get.name) } - rs.head + } - }, alwaysWaitForOther = parallelizeElseBranch) v.symbExLog.endBranchPoint(uidBranchPoint) if (wasElseExecutedOnDifferentVerifier && s.underJoin) { From 1d7424d89528d7ba11480fe67d86b76d318c23a4 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Thu, 30 Jan 2025 16:24:21 +0100 Subject: [PATCH 02/39] Store trees & move class --- src/main/scala/decider/Decider.scala | 14 +- src/main/scala/decider/PathConditions.scala | 13 +- src/main/scala/rules/Brancher.scala | 160 ++++++------------ src/main/scala/rules/Consumer.scala | 9 +- .../scala/rules/SymbolicExecutionRules.scala | 8 +- src/main/scala/state/BranchFailureState.scala | 156 +++++++++++++++++ .../scala/verifier/DefaultMainVerifier.scala | 18 +- 7 files changed, 256 insertions(+), 122 deletions(-) create mode 100644 src/main/scala/state/BranchFailureState.scala 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/rules/Brancher.scala b/src/main/scala/rules/Brancher.scala index 3c2885e9..8ea4c9b6 100644 --- a/src/main/scala/rules/Brancher.scala +++ b/src/main/scala/rules/Brancher.scala @@ -15,49 +15,10 @@ import viper.silicon.state.State import viper.silicon.state.terms.{FunctionDecl, MacroDecl, Not, Term} import viper.silicon.verifier.Verifier import viper.silver.ast -import viper.silver.ast.Exp import viper.silver.reporter.BranchFailureMessage import viper.silver.verifier.Failure -import viper.silver.verifier.errors.PostconditionViolatedBranch -import viper.silver.verifier.reasons.AssertionFalseAtBranch - -import java.io.Serializable -import scala.collection.immutable.{HashSet, Seq} -import scala.collection.mutable - - -case class BranchFailurePath(condition : Exp, taken : Boolean, sideResult : VerificationResult) -object branchFailurePaths extends mutable.HashMap[String, Vector[BranchFailurePath]] { - def prettyPrintPath(key : String) : String = { - var res = "" - val branchFailurePath = branchFailurePaths.get(key) - if (branchFailurePath.isDefined) { - val mappedBfp = branchFailurePath.get.collect(bf => { - val condStr = bf.condition.toString - val even = (n : Int) => (n & 1) == 0 - "│ "+ condStr + (if (even(condStr.length)) " " else "") + " ├" - }) - val maxLen = mappedBfp.map(_.length).max - val halfLen = maxLen / 2 - for ((condStr, bfp) <- mappedBfp zip branchFailurePath.get) { - val numChars = (maxLen - condStr.length) / 2 - val border = " "*numChars+"┌"+("─" * (condStr.length-2))+"┐"+" "*numChars - val borderTop = border + " " + (if (bfp.taken) "F" else "T") + "\n" - val halfBoxLen = (condStr.length-2) / 2 - val borderBottom = " "*numChars+"└"+("─" * halfBoxLen + "┬" + "─" * halfBoxLen)+"┘"+" "*numChars + "\n" - val sideResultSymbol = bfp.sideResult match { - case _: Unreachable => "?" - case _ => "✔" - } - val condStr_ = " "*numChars+condStr+"-"*numChars+s"──▶ "+ sideResultSymbol + "\n" - res += borderTop + condStr_ + borderBottom - res += " "*halfLen+"▼"+" "+(if (bfp.taken) "T" else "F")+"\n" - } - res += " "*(halfLen-2)+"Error"+"\n" - } - res - } -} + +import scala.collection.immutable.HashSet trait BranchingRules extends SymbolicExecutionRules { def branch(s: State, @@ -227,77 +188,64 @@ object brancher extends BranchingRules { CompletableFuture.completedFuture(Seq(Unreachable())) } - // Then result - val thenRes = if (executeThenBranch) { - v.symbExLog.markReachable(uidBranchPoint) - executionFlowController.locally(s, v)((s1, v1) => { - v1.decider.prover.comment(s"[then-branch: $cnt | $condition]") - v1.decider.setCurrentBranchCondition(condition, conditionExp) - - fThen(v1.stateConsolidator(s1).consolidateOptionally(s1, v1), v1) - }) - } else { - Unreachable() - } - if (thenRes.isFatal && !thenRes.isReported && s.parallelizeBranches && s.isLastRetry) { - thenRes.isReported = true - v.reporter.report(BranchFailureMessage("silicon", s.currentMember.get.asInstanceOf[ast.Member with Serializable], - condenseToViperResult(Seq(thenRes)).asInstanceOf[Failure])) - } + val res = { + val thenRes = if (executeThenBranch) { + v.symbExLog.markReachable(uidBranchPoint) + executionFlowController.locally(s, v)((s1, v1) => { + v1.decider.prover.comment(s"[then-branch: $cnt | $condition]") + v1.decider.setCurrentBranchCondition(condition, conditionExp) - // Else result - /* [BRANCH-PARALLELISATION] */ - var elseResults: Seq[VerificationResult] = null - try { - if (parallelizeElseBranch) { - val pcsAfterThenBranch = v.decider.pcs.duplicate() - val noOfErrorsAfterThenBranch = v.errorsReportedSoFar.get() - - val pcsBefore = v.decider.pcs - - elseResults = elseBranchFuture.get() - - if (v.decider.pcs != pcsBefore && v.uniqueId != elseBranchVerifier){ - // we have done other work during the join, need to reset - v.decider.prover.comment(s"Resetting path conditions after interruption") - v.decider.setPcs(pcsAfterThenBranch) - v.errorsReportedSoFar.set(noOfErrorsAfterThenBranch) - v.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract) - v.decider.resetProverOptions() - v.decider.setProverOptions(proverArgsOfCurrentDecider) - } + fThen(v1.stateConsolidator(s1).consolidateOptionally(s1, v1), v1) + }) } else { - elseResults = elseBranchFuture.get() + Unreachable() } - } catch { - case ex: ExecutionException => - ex.getCause.printStackTrace() - throw ex - } + if (thenRes.isFatal && !thenRes.isReported && s.parallelizeBranches && s.isLastRetry) { + thenRes.isReported = true + v.reporter.report(BranchFailureMessage("silicon", s.currentMember.get.asInstanceOf[ast.Member with Serializable], + condenseToViperResult(Seq(thenRes)).asInstanceOf[Failure])) + } + thenRes + }.combine({ - assert(elseResults.length == 1, s"Expected a single verification result but found ${elseResults.length}") - if (elseResults.head.isFatal && !elseResults.head.isReported && s.parallelizeBranches && s.isLastRetry) { - elseResults.head.isReported = true - v.reporter.report(BranchFailureMessage("silicon", s.currentMember.get.asInstanceOf[ast.Member with Serializable], - condenseToViperResult(Seq(elseResults.head)).asInstanceOf[Failure])) - } - val elseRes = elseResults.head - - val res = thenRes.combine(elseRes, alwaysWaitForOther = parallelizeElseBranch) - - if (s.currentMember.isDefined && res.isFatal) { - val bfp = branchFailurePaths.get(s.currentMember.get.name) - val sideRes = if (thenRes.isFatal) elseRes else thenRes - val newBfp = BranchFailurePath(conditionExp._1, thenRes.isFatal, sideRes) +: bfp.getOrElse(Vector[BranchFailurePath]()) - branchFailurePaths.put(s.currentMember.get.name, newBfp) - if ((thenRes.isFatal || elseRes.isFatal) && v.decider.pcs.branchConditionExps.length == 0) { - val firstCond = newBfp.head.condition - val failure = Failure(Seq(PostconditionViolatedBranch(firstCond, AssertionFalseAtBranch(firstCond, branchFailurePaths.prettyPrintPath(s.currentMember.get.name))))) - v.reporter.report(BranchFailureMessage(s"silicon", s.currentMember.get.asInstanceOf[ast.Member with Serializable], failure)) - branchFailurePaths.remove(s.currentMember.get.name) + /* [BRANCH-PARALLELISATION] */ + var rs: Seq[VerificationResult] = null + try { + if (parallelizeElseBranch) { + val pcsAfterThenBranch = v.decider.pcs.duplicate() + val noOfErrorsAfterThenBranch = v.errorsReportedSoFar.get() + + val pcsBefore = v.decider.pcs + + rs = elseBranchFuture.get() + + if (v.decider.pcs != pcsBefore && v.uniqueId != elseBranchVerifier){ + // we have done other work during the join, need to reset + v.decider.prover.comment(s"Resetting path conditions after interruption") + v.decider.setPcs(pcsAfterThenBranch) + v.errorsReportedSoFar.set(noOfErrorsAfterThenBranch) + v.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract) + v.decider.resetProverOptions() + v.decider.setProverOptions(proverArgsOfCurrentDecider) + } + } else { + rs = elseBranchFuture.get() + } + } catch { + case ex: ExecutionException => + ex.getCause.printStackTrace() + throw ex } - } + assert(rs.length == 1, s"Expected a single verification result but found ${rs.length}") + if (rs.head.isFatal && !rs.head.isReported && s.parallelizeBranches && s.isLastRetry) { + rs.head.isReported = true + v.reporter.report(BranchFailureMessage("silicon", s.currentMember.get.asInstanceOf[ast.Member with Serializable], + condenseToViperResult(Seq(rs.head)).asInstanceOf[Failure])) + } + rs.head + + }, alwaysWaitForOther = parallelizeElseBranch) v.symbExLog.endBranchPoint(uidBranchPoint) if (wasElseExecutedOnDifferentVerifier && s.underJoin) { diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index fd3e34b9..9ce2e66c 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -620,9 +620,16 @@ 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) + if (s3.currentMember.isDefined){ + BranchFailureState.extendTree(s3.currentMember.get.name, v.decider.pcs.getBranchConditionsExp(),r) + } + r case false => val failure = createFailure(pve dueTo AssertionFalse(e), v2, s3, termToAssert, eNew) + if (s3.currentMember.isDefined){ + BranchFailureState.extendTree(s3.currentMember.get.name, v.decider.pcs.getBranchConditionsExp(),failure) + } if (s3.retryLevel == 0 && v2.reportFurtherErrors()){ v2.decider.assume(t, Option.when(withExp)(e), eNew) failure combine QS(s3, v2) diff --git a/src/main/scala/rules/SymbolicExecutionRules.scala b/src/main/scala/rules/SymbolicExecutionRules.scala index 6f18728d..eb3873ab 100644 --- a/src/main/scala/rules/SymbolicExecutionRules.scala +++ b/src/main/scala/rules/SymbolicExecutionRules.scala @@ -85,13 +85,7 @@ trait SymbolicExecutionRules { } 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) - }) + v.decider.pcs.getBranchConditionsExp() } else Seq() if (Verifier.config.enableDebugging()){ diff --git a/src/main/scala/state/BranchFailureState.scala b/src/main/scala/state/BranchFailureState.scala new file mode 100644 index 00000000..751ffb7c --- /dev/null +++ b/src/main/scala/state/BranchFailureState.scala @@ -0,0 +1,156 @@ +package viper.silicon.state + +import viper.silicon.interfaces.{FatalResult, VerificationResult} +import viper.silver.ast +import viper.silver.ast.Exp + +import scala.collection.mutable + +object BranchFailureState extends mutable.HashMap[String, Tree] { + private def generateTree(exps : Seq[Exp], result: VerificationResult) : Tree = { + if (exps.length == 0) { + Leaf(result) + } else { + val expsRev = exps.reverse + val headExp = expsRev.head + var tree = expsRev.head match { + case ast.Not(exp) => Branch(exp, Some(Leaf(result)), None) + case _ => Branch(headExp, None, Some(Leaf(result))) + } + for (elem <- expsRev.tail) { + var negated = false + elem match { + case ast.Not(exp) => { + negated = true + tree = Branch(exp, Some(tree), None) + } + case _ => { + tree = Branch(elem, None, Some(tree)) + } + } + } + tree + } + } + def extendTree(methodName: String, branchConditions : Seq[Exp], result: VerificationResult) = { + val entry = BranchFailureState.get(methodName) + var branchTree : Option[Tree] = None + if (!entry.isDefined) { + branchTree = Some(generateTree(branchConditions, result)) + BranchFailureState.put(methodName, branchTree.get) + } else if (branchConditions.length > 1) { + branchTree = Option(entry.get) + var currNode = branchTree + var currBranch = currNode.get.asInstanceOf[Branch] + var negated = branchConditions.head match { + case _: ast.Not => true + case _ => false + } + var tail = branchConditions.tail + var next = false + do { + val headExp = tail.head match { + case ast.Not(exp) => exp + case _ => tail.head + } + if (currBranch.left.isDefined && currBranch.left.get.isInstanceOf[Branch] + && headExp.toString.equals(currBranch.left.get.asInstanceOf[Branch].exp.toString) && negated) { + currNode = Option(currBranch.left.get) + next = true + } else if (currBranch.right.isDefined && currBranch.right.get.isInstanceOf[Branch] + && headExp.toString.equals(currBranch.right.get.asInstanceOf[Branch].exp.toString) && !negated) { + currNode = Option(currBranch.right.get) + next = true + } + if(next) { + currBranch = currNode.get.asInstanceOf[Branch] + negated = tail.head match { + case _: ast.Not => true + case _ => false + } + tail = tail.tail + } + } while (tail.length != 0 && next) + if (negated) { + val tailTree = generateTree(tail, result) + currBranch.left = Some(tailTree) + } else { + val tailTree = generateTree(tail, result) + currBranch.right = Some(tailTree) + } + BranchFailureState.put(methodName, branchTree.get) + } + } + private def buildTree(t: Option[Tree]) : (Vector[String], Int, Int) = { + t match { + case Some(Branch(exp, left, right)) => { + val expStr = exp.toString + val expStrLen = expStr.length + val even = (n: Int) => (n & 1) == 0 + var boxMiddle = "│ " + expStr + (if (even(expStr.length)) " " else "") + " │" + val boxLen = boxMiddle.length + val halfBoxLen = boxLen / 2 + + var (leftStrVec, _, prevLeftRightBoxLen) = buildTree(left) + var (rightStrVec, prevRightLeftBoxLen, _) = buildTree(right) + + 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 Some(Leaf(result)) => { + result match { + case _: FatalResult => (Vector("Error"), 2, 2) // ✘ + case _ => (Vector("✔"), 0, 0) + } + } + case _ => (Vector("?"), 0, 0) + } + } + def prettyPrint(methodName : String): String = { + val entry = BranchFailureState.get(methodName) + val tree = buildTree(entry) + val result = tree._1.reduce((str, s) => str + "\n" + s) + "\n" + result + } +} +trait Tree +private case class Leaf(result : VerificationResult) extends Tree +case class Branch(exp : Exp, var left: Option[Tree], var right: Option[Tree]) extends Tree \ No newline at end of file diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index b395ed21..a3dd7d88 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -31,11 +31,13 @@ import viper.silicon.supporters.functions.{DefaultFunctionVerificationUnitProvid import viper.silicon.supporters.qps._ import viper.silicon.utils.Counter import viper.silver.ast.utility.rewriter.Traverse -import viper.silver.ast.{BackendType, Member} +import viper.silver.ast.{BackendType, Exp, Member} import viper.silver.cfg.silver.SilverCfg import viper.silver.frontend.FrontendStateCache import viper.silver.reporter._ import viper.silver.verifier.VerifierWarning +import viper.silver.verifier.errors.PostconditionViolatedBranch +import viper.silver.verifier.reasons.AssertionFalseAtBranch /* TODO: Extract a suitable MainVerifier interface, probably including * - def verificationPoolManager: VerificationPoolManager) @@ -51,10 +53,10 @@ trait MainVerifier extends Verifier { class DefaultMainVerifier(config: Config, override val reporter: Reporter, override val rootSymbExLogger: SymbExLogger[_ <: MemberSymbExLogger]) - extends BaseVerifier(config, "00") - with MainVerifier - with DefaultFunctionVerificationUnitProvider - with DefaultPredicateVerificationUnitProvider { + extends BaseVerifier(config, "00") + with MainVerifier + with DefaultFunctionVerificationUnitProvider + with DefaultPredicateVerificationUnitProvider { Verifier.config = config @@ -266,6 +268,12 @@ class DefaultMainVerifier(config: Config, .flatMap(extractAllVerificationResults) val elapsed = System.currentTimeMillis() - startTime + val branchTree = BranchFailureState.get(method.name) + if (branchTree.isDefined){ + val firstCond = branchTree.get.asInstanceOf[Branch].exp + val failure = viper.silver.verifier.Failure(Seq(PostconditionViolatedBranch(firstCond, AssertionFalseAtBranch(firstCond, BranchFailureState.prettyPrint(method.name))))) + reporter report BranchFailureMessage(s"silicon", s.currentMember.get.asInstanceOf[ast.Member with Serializable], failure) + } reporter report VerificationResultMessage(s"silicon", method, elapsed, condenseToViperResult(results)) logger debug s"Silicon finished verification of method `${method.name}` in ${viper.silver.reporter.format.formatMillisReadably(elapsed)} seconds with the following result: ${condenseToViperResult(results).toString}" From 4f7a805eb547b187e2b8c813694ac8fb1c07dd7e Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Fri, 31 Jan 2025 16:39:52 +0100 Subject: [PATCH 03/39] Clean up --- silver | 2 +- src/main/scala/rules/Consumer.scala | 8 +- ...ureState.scala => BranchFailureTree.scala} | 105 +++++++++--------- src/main/scala/state/State.scala | 16 ++- .../scala/verifier/DefaultMainVerifier.scala | 6 +- 5 files changed, 71 insertions(+), 66 deletions(-) rename src/main/scala/state/{BranchFailureState.scala => BranchFailureTree.scala} (70%) diff --git a/silver b/silver index 85c047d2..4833685a 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 85c047d22a71d28e7b157a10664443ab3473dfd3 +Subproject commit 4833685a51d8f3c4e2793103db4121d9e71e0109 diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index 9ce2e66c..70728655 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -621,14 +621,14 @@ object consumer extends ConsumptionRules { case true => v2.decider.assume(t, Option.when(withExp)(e), eNew) val r = QS(s3, v2) - if (s3.currentMember.isDefined){ - BranchFailureState.extendTree(s3.currentMember.get.name, v.decider.pcs.getBranchConditionsExp(),r) + if (s3.branchFailureTreeMap.isDefined && s3.currentMember.isDefined){ + s3.branchFailureTreeMap.get.storeIntoTree(s3.currentMember.get.name, v.decider.pcs.getBranchConditionsExp(),r) } r case false => val failure = createFailure(pve dueTo AssertionFalse(e), v2, s3, termToAssert, eNew) - if (s3.currentMember.isDefined){ - BranchFailureState.extendTree(s3.currentMember.get.name, v.decider.pcs.getBranchConditionsExp(),failure) + if (s3.branchFailureTreeMap.isDefined && s3.currentMember.isDefined){ + s3.branchFailureTreeMap.get.storeIntoTree(s3.currentMember.get.name, v.decider.pcs.getBranchConditionsExp(),failure) } if (s3.retryLevel == 0 && v2.reportFurtherErrors()){ v2.decider.assume(t, Option.when(withExp)(e), eNew) diff --git a/src/main/scala/state/BranchFailureState.scala b/src/main/scala/state/BranchFailureTree.scala similarity index 70% rename from src/main/scala/state/BranchFailureState.scala rename to src/main/scala/state/BranchFailureTree.scala index 751ffb7c..75c2e472 100644 --- a/src/main/scala/state/BranchFailureState.scala +++ b/src/main/scala/state/BranchFailureTree.scala @@ -6,42 +6,22 @@ import viper.silver.ast.Exp import scala.collection.mutable -object BranchFailureState extends mutable.HashMap[String, Tree] { - private def generateTree(exps : Seq[Exp], result: VerificationResult) : Tree = { - if (exps.length == 0) { - Leaf(result) +class BranchFailureTreeMap extends mutable.HashMap[String, Tree] { + def storeIntoTree(method: String, branchConditions : Seq[Exp], result: VerificationResult): Unit = { + val branchTree = this.get(method) + if (branchTree.isDefined) { + branchTree.get.extend(branchConditions, result) } else { - val expsRev = exps.reverse - val headExp = expsRev.head - var tree = expsRev.head match { - case ast.Not(exp) => Branch(exp, Some(Leaf(result)), None) - case _ => Branch(headExp, None, Some(Leaf(result))) - } - for (elem <- expsRev.tail) { - var negated = false - elem match { - case ast.Not(exp) => { - negated = true - tree = Branch(exp, Some(tree), None) - } - case _ => { - tree = Branch(elem, None, Some(tree)) - } - } - } - tree + this.put(method, Tree.generate(branchConditions, result)) } } - def extendTree(methodName: String, branchConditions : Seq[Exp], result: VerificationResult) = { - val entry = BranchFailureState.get(methodName) - var branchTree : Option[Tree] = None - if (!entry.isDefined) { - branchTree = Some(generateTree(branchConditions, result)) - BranchFailureState.put(methodName, branchTree.get) - } else if (branchConditions.length > 1) { - branchTree = Option(entry.get) - var currNode = branchTree - var currBranch = currNode.get.asInstanceOf[Branch] +} + +abstract class Tree { + def extend(branchConditions : Seq[Exp], result: VerificationResult) = { + if (branchConditions.length > 1) { + var currNode = this + var currBranch = currNode.asInstanceOf[Branch] var negated = branchConditions.head match { case _: ast.Not => true case _ => false @@ -55,15 +35,15 @@ object BranchFailureState extends mutable.HashMap[String, Tree] { } if (currBranch.left.isDefined && currBranch.left.get.isInstanceOf[Branch] && headExp.toString.equals(currBranch.left.get.asInstanceOf[Branch].exp.toString) && negated) { - currNode = Option(currBranch.left.get) + currNode = currBranch.left.get next = true } else if (currBranch.right.isDefined && currBranch.right.get.isInstanceOf[Branch] && headExp.toString.equals(currBranch.right.get.asInstanceOf[Branch].exp.toString) && !negated) { - currNode = Option(currBranch.right.get) + currNode = currBranch.right.get next = true } - if(next) { - currBranch = currNode.get.asInstanceOf[Branch] + if (next) { + currBranch = currNode.asInstanceOf[Branch] negated = tail.head match { case _: ast.Not => true case _ => false @@ -72,18 +52,17 @@ object BranchFailureState extends mutable.HashMap[String, Tree] { } } while (tail.length != 0 && next) if (negated) { - val tailTree = generateTree(tail, result) + val tailTree = Tree.generate(tail, result) currBranch.left = Some(tailTree) } else { - val tailTree = generateTree(tail, result) + val tailTree = Tree.generate(tail, result) currBranch.right = Some(tailTree) } - BranchFailureState.put(methodName, branchTree.get) } } - private def buildTree(t: Option[Tree]) : (Vector[String], Int, Int) = { - t match { - case Some(Branch(exp, left, right)) => { + private def buildTree() : (Vector[String], Int, Int) = { + this match { + case Branch(exp, left, right) => val expStr = exp.toString val expStrLen = expStr.length val even = (n: Int) => (n & 1) == 0 @@ -91,8 +70,8 @@ object BranchFailureState extends mutable.HashMap[String, Tree] { val boxLen = boxMiddle.length val halfBoxLen = boxLen / 2 - var (leftStrVec, _, prevLeftRightBoxLen) = buildTree(left) - var (rightStrVec, prevRightLeftBoxLen, _) = buildTree(right) + var (leftStrVec, _, prevLeftRightBoxLen) = if(left.isDefined) left.get.buildTree() else (Vector("?"), 0, 0) + var (rightStrVec, prevRightLeftBoxLen, _) = if(right.isDefined) right.get.buildTree() else (Vector("?"), 0, 0) val halfExpStrLen = expStrLen / 2 val leftBoxLen = leftStrVec.head.length @@ -134,23 +113,43 @@ object BranchFailureState extends mutable.HashMap[String, Tree] { } } (boxTop +: boxMiddle +: boxBottom +: (leftStrVec zip rightStrVec).map(t => t._1 + t._2), leftFiller + halfBoxLen, rightFiller + halfBoxLen) - } - case Some(Leaf(result)) => { + case Leaf(result) => result match { case _: FatalResult => (Vector("Error"), 2, 2) // ✘ case _ => (Vector("✔"), 0, 0) } - } - case _ => (Vector("?"), 0, 0) } } - def prettyPrint(methodName : String): String = { - val entry = BranchFailureState.get(methodName) - val tree = buildTree(entry) + def prettyPrint() = { + val tree = this.buildTree() val result = tree._1.reduce((str, s) => str + "\n" + s) + "\n" result } } -trait Tree +object Tree { + def generate(expressions : Seq[Exp], result: VerificationResult) : Tree = { + if (expressions.length == 0) { + Leaf(result) + } else { + val reversedExpressions = expressions.reverse + val headExp = reversedExpressions.head + var tree = reversedExpressions.head match { + case ast.Not(exp) => Branch(exp, Some(Leaf(result)), None) + case _ => Branch(headExp, None, Some(Leaf(result))) + } + for (elem <- reversedExpressions.tail) { + var negated = false + elem match { + case ast.Not(exp) => + negated = true + tree = Branch(exp, Some(tree), None) + case _ => + tree = Branch(elem, None, Some(tree)) + } + } + tree + } + } +} private case class Leaf(result : VerificationResult) extends Tree case class Branch(exp : Exp, var left: Option[Tree], var right: Option[Tree]) extends Tree \ No newline at end of file diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index 6dc4c494..5acfaa05 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -80,7 +80,9 @@ final case class State(g: Store = Store(), /* ast.Field, ast.Predicate, or MagicWandIdentifier */ heapDependentTriggers: InsertionOrderedSet[Any] = InsertionOrderedSet.empty, moreCompleteExhale: Boolean = false, - moreJoins: JoinMode = JoinMode.Off) + moreJoins: JoinMode = JoinMode.Off, + + branchFailureTreeMap: Option[BranchFailureTreeMap] = None) extends Mergeable[State] { val isMethodVerification: Boolean = { @@ -179,7 +181,8 @@ object State { ssCache1, assertReadAccessOnly1, qpFields1, qpPredicates1, qpMagicWands1, permResources1, smCache1, pmCache1, smDomainNeeded1, predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers, - moreCompleteExhale, moreJoins) => + moreCompleteExhale, moreJoins, + branchFailureTreeMap) => /* Decompose state s2: most values must match those of s1 */ s2 match { @@ -204,7 +207,8 @@ object State { ssCache2, `assertReadAccessOnly1`, `qpFields1`, `qpPredicates1`, `qpMagicWands1`, `permResources1`, smCache2, pmCache2, `smDomainNeeded1`, `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`, - moreCompleteExhale2, `moreJoins`) => + moreCompleteExhale2, `moreJoins`, + `branchFailureTreeMap`) => val functionRecorder3 = functionRecorder1.merge(functionRecorder2) val triggerExp3 = triggerExp1 && triggerExp2 @@ -335,7 +339,8 @@ object State { ssCache1, assertReadAccessOnly1, qpFields1, qpPredicates1, qpMagicWands1, permResources1, smCache1, pmCache1, smDomainNeeded1, predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers, - moreCompleteExhale, moreJoins) => + moreCompleteExhale, moreJoins, + branchFailureState) => /* Decompose state s2: most values must match those of s1 */ s2 match { @@ -359,7 +364,8 @@ object State { ssCache2, `assertReadAccessOnly1`, `qpFields1`, `qpPredicates1`, `qpMagicWands1`, `permResources1`, smCache2, pmCache2, smDomainNeeded2, `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`, - moreCompleteExhale2, `moreJoins`) => + moreCompleteExhale2, `moreJoins`, + `branchFailureState`) => val functionRecorder3 = functionRecorder1.merge(functionRecorder2) val triggerExp3 = triggerExp1 && triggerExp2 diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index a3dd7d88..55a07a94 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -260,7 +260,7 @@ class DefaultMainVerifier(config: Config, program.methods.filterNot(excludeMethod).map(method => { val s = createInitialState(method, program, functionData, predicateData).copy(parallelizeBranches = - Verifier.config.parallelizeBranches()) /* [BRANCH-PARALLELISATION] */ + Verifier.config.parallelizeBranches(), branchFailureTreeMap = Option(new BranchFailureTreeMap())) /* [BRANCH-PARALLELISATION] */ _verificationPoolManager.queueVerificationTask(v => { val startTime = System.currentTimeMillis() @@ -268,10 +268,10 @@ class DefaultMainVerifier(config: Config, .flatMap(extractAllVerificationResults) val elapsed = System.currentTimeMillis() - startTime - val branchTree = BranchFailureState.get(method.name) + val branchTree = s.branchFailureTreeMap.get.get(method.name) if (branchTree.isDefined){ val firstCond = branchTree.get.asInstanceOf[Branch].exp - val failure = viper.silver.verifier.Failure(Seq(PostconditionViolatedBranch(firstCond, AssertionFalseAtBranch(firstCond, BranchFailureState.prettyPrint(method.name))))) + val failure = viper.silver.verifier.Failure(Seq(PostconditionViolatedBranch(firstCond, AssertionFalseAtBranch(firstCond, branchTree.get.prettyPrint())))) reporter report BranchFailureMessage(s"silicon", s.currentMember.get.asInstanceOf[ast.Member with Serializable], failure) } reporter report VerificationResultMessage(s"silicon", method, elapsed, condenseToViperResult(results)) From ce1c0354a301bc412fc165361f64c14c063b9187 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Sun, 2 Feb 2025 18:59:51 +0100 Subject: [PATCH 04/39] Refactoring + fixes --- src/main/scala/state/BranchFailureTree.scala | 27 +-- src/main/scala/state/State.scala | 178 +++++++++--------- .../scala/verifier/DefaultMainVerifier.scala | 74 ++++---- 3 files changed, 141 insertions(+), 138 deletions(-) diff --git a/src/main/scala/state/BranchFailureTree.scala b/src/main/scala/state/BranchFailureTree.scala index 75c2e472..e44facfe 100644 --- a/src/main/scala/state/BranchFailureTree.scala +++ b/src/main/scala/state/BranchFailureTree.scala @@ -17,9 +17,9 @@ class BranchFailureTreeMap extends mutable.HashMap[String, Tree] { } } -abstract class Tree { +class Tree { def extend(branchConditions : Seq[Exp], result: VerificationResult) = { - if (branchConditions.length > 1) { + if (branchConditions.length > 0) { var currNode = this var currBranch = currNode.asInstanceOf[Branch] var negated = branchConditions.head match { @@ -27,8 +27,9 @@ abstract class Tree { case _ => false } var tail = branchConditions.tail - var next = false - do { + var next = true + while (tail.length != 0 && next) { + next = false val headExp = tail.head match { case ast.Not(exp) => exp case _ => tail.head @@ -36,10 +37,12 @@ abstract class Tree { if (currBranch.left.isDefined && currBranch.left.get.isInstanceOf[Branch] && headExp.toString.equals(currBranch.left.get.asInstanceOf[Branch].exp.toString) && negated) { currNode = currBranch.left.get + currBranch.isLeftFatal = result.isFatal || currBranch.isLeftFatal next = true } else if (currBranch.right.isDefined && currBranch.right.get.isInstanceOf[Branch] && headExp.toString.equals(currBranch.right.get.asInstanceOf[Branch].exp.toString) && !negated) { currNode = currBranch.right.get + currBranch.isRightFatal = result.isFatal || currBranch.isRightFatal next = true } if (next) { @@ -50,19 +53,21 @@ abstract class Tree { } tail = tail.tail } - } while (tail.length != 0 && next) + } if (negated) { val tailTree = Tree.generate(tail, result) currBranch.left = Some(tailTree) + currBranch.isLeftFatal = result.isFatal || currBranch.isLeftFatal } else { val tailTree = Tree.generate(tail, result) currBranch.right = Some(tailTree) + currBranch.isRightFatal = result.isFatal || currBranch.isRightFatal } } } private def buildTree() : (Vector[String], Int, Int) = { this match { - case Branch(exp, left, right) => + case Branch(exp, left, right, _, _) => val expStr = exp.toString val expStrLen = expStr.length val even = (n: Int) => (n & 1) == 0 @@ -134,17 +139,17 @@ object Tree { val reversedExpressions = expressions.reverse val headExp = reversedExpressions.head var tree = reversedExpressions.head match { - case ast.Not(exp) => Branch(exp, Some(Leaf(result)), None) - case _ => Branch(headExp, None, Some(Leaf(result))) + case ast.Not(exp) => Branch(exp, Some(Leaf(result)), None, result.isFatal, false) + case _ => Branch(headExp, None, Some(Leaf(result)), false, result.isFatal) } for (elem <- reversedExpressions.tail) { var negated = false elem match { case ast.Not(exp) => negated = true - tree = Branch(exp, Some(tree), None) + tree = Branch(exp, Some(tree), None, result.isFatal, false) case _ => - tree = Branch(elem, None, Some(tree)) + tree = Branch(elem, None, Some(tree), false, result.isFatal) } } tree @@ -152,4 +157,4 @@ object Tree { } } private case class Leaf(result : VerificationResult) extends Tree -case class Branch(exp : Exp, var left: Option[Tree], var right: Option[Tree]) extends Tree \ No newline at end of file +case class Branch(exp : Exp, var left: Option[Tree], var right: Option[Tree], var isLeftFatal: Boolean, var isRightFatal: Boolean) extends Tree \ No newline at end of file diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index 5acfaa05..d9a438f7 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -17,7 +17,7 @@ import viper.silicon.interfaces.state.GeneralChunk import viper.silicon.state.State.OldHeaps import viper.silicon.state.terms.{Term, Var} import viper.silicon.interfaces.state.Chunk -import viper.silicon.state.terms.{And, Ite} +import viper.silicon.state.terms.{And, Ite, NoPerm} import viper.silicon.supporters.PredicateData import viper.silicon.supporters.functions.{FunctionData, FunctionRecorder, NoopFunctionRecorder} import viper.silicon.utils.ast.BigAnd @@ -64,7 +64,7 @@ final case class State(g: Store = Store(), exhaleExt: Boolean = false, ssCache: SsCache = Map.empty, - assertReadAccessOnly: Boolean = false, + hackIssue387DisablePermissionConsumption: Boolean = false, qpFields: InsertionOrderedSet[ast.Field] = InsertionOrderedSet.empty, qpPredicates: InsertionOrderedSet[ast.Predicate] = InsertionOrderedSet.empty, @@ -83,17 +83,13 @@ final case class State(g: Store = Store(), moreJoins: JoinMode = JoinMode.Off, branchFailureTreeMap: Option[BranchFailureTreeMap] = None) - extends Mergeable[State] { + extends Mergeable[State] { val isMethodVerification: Boolean = { // currentMember being None means we're verifying a CFG; this should behave like verifying a method. currentMember.isEmpty || currentMember.get.isInstanceOf[ast.Method] } - val mayAssumeUpperBounds: Boolean = { - currentMember.isEmpty || !currentMember.get.isInstanceOf[ast.Function] || Verifier.config.respectFunctionPrePermAmounts() - } - val isLastRetry: Boolean = retryLevel == 0 def incCycleCounter(m: ast.Predicate) = @@ -107,8 +103,8 @@ final case class State(g: Store = Store(), val (ms, others) = visited.partition(_ == m) copy(visited = ms.tail ::: others) } - else - this + else + this def cycles(m: ast.Member) = visited.count(_ == m) @@ -134,9 +130,9 @@ final case class State(g: Store = Store(), functionRecorder.data.fold(Seq.empty[(Var, Option[ast.AbstractLocalVar])])(d => d.arguments.zip(d.argumentExps)) def relevantQuantifiedVariables(filterPredicate: Var => Boolean): Seq[(Var, Option[ast.AbstractLocalVar])] = ( - functionRecorderQuantifiedVariables() - ++ quantifiedVariables.filter(x => filterPredicate(x._1)) - ) + functionRecorderQuantifiedVariables() + ++ quantifiedVariables.filter(x => filterPredicate(x._1)) + ) def relevantQuantifiedVariables(occurringIn: Seq[Term]): Seq[(Var, Option[ast.AbstractLocalVar])] = relevantQuantifiedVariables(x => occurringIn.exists(_.contains(x))) @@ -161,54 +157,54 @@ object State { s1 match { /* Decompose state s1 */ case State(g1, h1, program, member, - predicateData, - functionData, - oldHeaps1, - parallelizeBranches1, - recordVisited1, visited1, - methodCfg1, invariantContexts1, - constrainableARPs1, - quantifiedVariables1, - retrying1, - underJoin1, - functionRecorder1, - conservingSnapshotGeneration1, - recordPossibleTriggers1, possibleTriggers1, - triggerExp1, - partiallyConsumedHeap1, - permissionScalingFactor1, permissionScalingFactorExp1, isEvalInOld, - reserveHeaps1, reserveCfgs1, conservedPcs1, recordPcs1, exhaleExt1, - ssCache1, assertReadAccessOnly1, - qpFields1, qpPredicates1, qpMagicWands1, permResources1, smCache1, pmCache1, smDomainNeeded1, - predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers, - moreCompleteExhale, moreJoins, - branchFailureTreeMap) => + predicateData, + functionData, + oldHeaps1, + parallelizeBranches1, + recordVisited1, visited1, + methodCfg1, invariantContexts1, + constrainableARPs1, + quantifiedVariables1, + retrying1, + underJoin1, + functionRecorder1, + conservingSnapshotGeneration1, + recordPossibleTriggers1, possibleTriggers1, + triggerExp1, + partiallyConsumedHeap1, + permissionScalingFactor1, permissionScalingFactorExp1, isEvalInOld, + reserveHeaps1, reserveCfgs1, conservedPcs1, recordPcs1, exhaleExt1, + ssCache1, hackIssue387DisablePermissionConsumption1, + qpFields1, qpPredicates1, qpMagicWands1, permResources1, smCache1, pmCache1, smDomainNeeded1, + predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers, + moreCompleteExhale, moreJoins, + branchFailureTreeMap) => /* Decompose state s2: most values must match those of s1 */ s2 match { case State(`g1`, `h1`, - `program`, `member`, - `predicateData`, `functionData`, - `oldHeaps1`, - `parallelizeBranches1`, - `recordVisited1`, `visited1`, - `methodCfg1`, `invariantContexts1`, - constrainableARPs2, - quantifiedVariables2, - `retrying1`, - `underJoin1`, - functionRecorder2, - `conservingSnapshotGeneration1`, - `recordPossibleTriggers1`, possibleTriggers2, - triggerExp2, - `partiallyConsumedHeap1`, - `permissionScalingFactor1`, `permissionScalingFactorExp1`, `isEvalInOld`, - `reserveHeaps1`, `reserveCfgs1`, conservedPcs2, `recordPcs1`, `exhaleExt1`, - ssCache2, `assertReadAccessOnly1`, - `qpFields1`, `qpPredicates1`, `qpMagicWands1`, `permResources1`, smCache2, pmCache2, `smDomainNeeded1`, - `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`, - moreCompleteExhale2, `moreJoins`, - `branchFailureTreeMap`) => + `program`, `member`, + `predicateData`, `functionData`, + `oldHeaps1`, + `parallelizeBranches1`, + `recordVisited1`, `visited1`, + `methodCfg1`, `invariantContexts1`, + constrainableARPs2, + quantifiedVariables2, + `retrying1`, + `underJoin1`, + functionRecorder2, + `conservingSnapshotGeneration1`, + `recordPossibleTriggers1`, possibleTriggers2, + triggerExp2, + `partiallyConsumedHeap1`, + `permissionScalingFactor1`, `permissionScalingFactorExp1`, `isEvalInOld`, + `reserveHeaps1`, `reserveCfgs1`, conservedPcs2, `recordPcs1`, `exhaleExt1`, + ssCache2, `hackIssue387DisablePermissionConsumption1`, + `qpFields1`, `qpPredicates1`, `qpMagicWands1`, `permResources1`, smCache2, pmCache2, `smDomainNeeded1`, + `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`, + moreCompleteExhale2, `moreJoins`, + `branchFailureTreeMap`) => val functionRecorder3 = functionRecorder1.merge(functionRecorder2) val triggerExp3 = triggerExp1 && triggerExp2 @@ -228,15 +224,15 @@ object State { .map({ case (pcs1, pcs2) => (pcs1 ++ pcs2).distinct }) s1.copy(functionRecorder = functionRecorder3, - possibleTriggers = possibleTriggers3, - triggerExp = triggerExp3, - constrainableARPs = constrainableARPs3, - quantifiedVariables = quantifiedVariables3, - ssCache = ssCache3, - smCache = smCache3, - pmCache = pmCache3, - moreCompleteExhale = moreCompleteExhale3, - conservedPcs = conservedPcs3) + possibleTriggers = possibleTriggers3, + triggerExp = triggerExp3, + constrainableARPs = constrainableARPs3, + quantifiedVariables = quantifiedVariables3, + ssCache = ssCache3, + smCache = smCache3, + pmCache = pmCache3, + moreCompleteExhale = moreCompleteExhale3, + conservedPcs = conservedPcs3) case _ => val err = new StringBuilder() @@ -248,7 +244,7 @@ object State { } } sys.error(s"State merging failed: unexpected mismatch between symbolic states: $err") - } + } } } @@ -274,7 +270,7 @@ object State { private def mergeMaps[K, V, D](map1: Map[K, V], data1: D, map2: Map[K, V], data2: D) (fOnce: (V, D) => Option[V]) (fTwice: (V, D, V, D) => Option[V]) - : Map[K, V] = { + : Map[K, V] = { map1.flatMap({ case (k, v1) => (map2.get(k) match { @@ -336,7 +332,7 @@ object State { partiallyConsumedHeap1, permissionScalingFactor1, permissionScalingFactorExp1, isEvalInOld, reserveHeaps1, reserveCfgs1, conservedPcs1, recordPcs1, exhaleExt1, - ssCache1, assertReadAccessOnly1, + ssCache1, hackIssue387DisablePermissionConsumption1, qpFields1, qpPredicates1, qpMagicWands1, permResources1, smCache1, pmCache1, smDomainNeeded1, predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers, moreCompleteExhale, moreJoins, @@ -361,11 +357,11 @@ object State { partiallyConsumedHeap2, `permissionScalingFactor1`, `permissionScalingFactorExp1`, `isEvalInOld`, reserveHeaps2, `reserveCfgs1`, conservedPcs2, `recordPcs1`, `exhaleExt1`, - ssCache2, `assertReadAccessOnly1`, + ssCache2, `hackIssue387DisablePermissionConsumption1`, `qpFields1`, `qpPredicates1`, `qpMagicWands1`, `permResources1`, smCache2, pmCache2, smDomainNeeded2, `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`, moreCompleteExhale2, `moreJoins`, - `branchFailureState`) => + `branchFailureState`) => val functionRecorder3 = functionRecorder1.merge(functionRecorder2) val triggerExp3 = triggerExp1 && triggerExp2 @@ -440,27 +436,27 @@ object State { val pmCache3 = pmCache1 ++ pmCache2 val s3 = s1.copy(functionRecorder = functionRecorder3, - possibleTriggers = possibleTriggers3, - triggerExp = triggerExp3, - constrainableARPs = constrainableARPs3, - ssCache = ssCache3, - smCache = smCache3, - pmCache = pmCache3, - g = g3, - h = h3, - oldHeaps = oldHeaps3, - partiallyConsumedHeap = partiallyConsumedHeap3, - smDomainNeeded = smDomainNeeded3, - invariantContexts = invariantContexts3, - reserveHeaps = reserveHeaps3, - conservedPcs = conservedPcs3) + possibleTriggers = possibleTriggers3, + triggerExp = triggerExp3, + constrainableARPs = constrainableARPs3, + ssCache = ssCache3, + smCache = smCache3, + pmCache = pmCache3, + g = g3, + h = h3, + oldHeaps = oldHeaps3, + partiallyConsumedHeap = partiallyConsumedHeap3, + smDomainNeeded = smDomainNeeded3, + invariantContexts = invariantContexts3, + reserveHeaps = reserveHeaps3, + conservedPcs = conservedPcs3) s3 - // Optionally, we could also do a state consolidation after each - // state merging, but this has shown to decrease performance a bit. - //val s4 = verifier.stateConsolidator.consolidate(s3, verifier) - //s4 + // Optionally, we could also do a state consolidation after each + // state merging, but this has shown to decrease performance a bit. + //val s4 = verifier.stateConsolidator.consolidate(s3, verifier) + //s4 case _ => { println("Error at new merge function:") @@ -472,9 +468,9 @@ object State { def preserveAfterLocalEvaluation(pre: State, post: State): State = { pre.copy(functionRecorder = post.functionRecorder, - possibleTriggers = post.possibleTriggers, - smCache = post.smCache, - constrainableARPs = post.constrainableARPs) + possibleTriggers = post.possibleTriggers, + smCache = post.smCache, + constrainableARPs = post.constrainableARPs) } def conflictFreeUnionOrAbort[K, V](m1: Map[K, V], m2: Map[K, V]): Map[K,V] = diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index 55a07a94..a63a74f4 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -31,7 +31,7 @@ import viper.silicon.supporters.functions.{DefaultFunctionVerificationUnitProvid import viper.silicon.supporters.qps._ import viper.silicon.utils.Counter import viper.silver.ast.utility.rewriter.Traverse -import viper.silver.ast.{BackendType, Exp, Member} +import viper.silver.ast.{BackendType, Member} import viper.silver.cfg.silver.SilverCfg import viper.silver.frontend.FrontendStateCache import viper.silver.reporter._ @@ -169,11 +169,11 @@ class DefaultMainVerifier(config: Config, def verify(originalProgram: ast.Program, cfgs: Seq[SilverCfg], inputFile: Option[String]): List[VerificationResult] = { /** Trigger computation is currently not thread-safe; hence, all triggers are computed - * up-front, before the program is verified in parallel. - * This is done bottom-up to ensure that nested quantifiers are transformed as well - * (top-down should also work, but the default of 'innermost' won't). - * See also [[viper.silicon.utils.ast.autoTrigger]]. - */ + * up-front, before the program is verified in parallel. + * This is done bottom-up to ensure that nested quantifiers are transformed as well + * (top-down should also work, but the default of 'innermost' won't). + * See also [[viper.silicon.utils.ast.autoTrigger]]. + */ var program: ast.Program = originalProgram.transform({ case forall: ast.Forall if forall.isPure => @@ -264,15 +264,17 @@ class DefaultMainVerifier(config: Config, _verificationPoolManager.queueVerificationTask(v => { val startTime = System.currentTimeMillis() - val results = v.methodSupporter.verify(s, method) + var results = v.methodSupporter.verify(s, method) .flatMap(extractAllVerificationResults) val elapsed = System.currentTimeMillis() - startTime val branchTree = s.branchFailureTreeMap.get.get(method.name) - if (branchTree.isDefined){ - val firstCond = branchTree.get.asInstanceOf[Branch].exp - val failure = viper.silver.verifier.Failure(Seq(PostconditionViolatedBranch(firstCond, AssertionFalseAtBranch(firstCond, branchTree.get.prettyPrint())))) - reporter report BranchFailureMessage(s"silicon", s.currentMember.get.asInstanceOf[ast.Member with Serializable], failure) + if (branchTree.isDefined) { + val branch = branchTree.get.asInstanceOf[Branch] + if (branch.isLeftFatal || branch.isRightFatal) { + val firstCond = branchTree.get.asInstanceOf[Branch].exp + results +:= Failure(PostconditionViolatedBranch(firstCond, AssertionFalseAtBranch(firstCond, branchTree.get.prettyPrint()), branch.isLeftFatal, branch.isRightFatal)) + } } reporter report VerificationResultMessage(s"silicon", method, elapsed, condenseToViperResult(results)) logger debug s"Silicon finished verification of method `${method.name}` in ${viper.silver.reporter.format.formatMillisReadably(elapsed)} seconds with the following result: ${condenseToViperResult(results).toString}" @@ -306,8 +308,8 @@ class DefaultMainVerifier(config: Config, reporter report VerificationTerminationMessage() val verificationResults = ( functionVerificationResults - ++ predicateVerificationResults - ++ methodVerificationResults) + ++ predicateVerificationResults + ++ methodVerificationResults) if (Verifier.config.enableDebugging()){ val debugger = new SiliconDebugger(verificationResults, identifierFactory, reporter, FrontendStateCache.resolver, FrontendStateCache.pprogram, FrontendStateCache.translator, this) @@ -317,7 +319,7 @@ class DefaultMainVerifier(config: Config, verificationResults } - private def createInitialState(member: ast.Member, + private def createInitialState(member: ast.Member, program: ast.Program, functionData: Map[ast.Function, FunctionData], predicateData: Map[ast.Predicate, PredicateData]): State = { @@ -401,18 +403,18 @@ class DefaultMainVerifier(config: Config, } else InsertionOrderedSet.empty State(program = program, - functionData = functionData, - predicateData = predicateData, - qpFields = quantifiedFields, - qpPredicates = quantifiedPredicates, - qpMagicWands = quantifiedMagicWands, - permLocations = permResources, - predicateSnapMap = predSnapGenerator.snapMap, - predicateFormalVarMap = predSnapGenerator.formalVarMap, - currentMember = Some(member), - heapDependentTriggers = resourceTriggers, - moreCompleteExhale = mce, - moreJoins = moreJoins) + functionData = functionData, + predicateData = predicateData, + qpFields = quantifiedFields, + qpPredicates = quantifiedPredicates, + qpMagicWands = quantifiedMagicWands, + permLocations = permResources, + predicateSnapMap = predSnapGenerator.snapMap, + predicateFormalVarMap = predSnapGenerator.formalVarMap, + currentMember = Some(member), + heapDependentTriggers = resourceTriggers, + moreCompleteExhale = mce, + moreJoins = moreJoins) } private def createInitialState(@unused cfg: SilverCfg, @@ -438,8 +440,8 @@ class DefaultMainVerifier(config: Config, } private def excludeMethod(method: ast.Method) = ( - !method.name.matches(config.includeMethods()) - || method.name.matches(config.excludeMethods())) + !method.name.matches(config.includeMethods()) + || method.name.matches(config.excludeMethods())) /* Prover preamble: Static preamble */ @@ -609,13 +611,13 @@ class DefaultMainVerifier(config: Config, preambleReader.emitParametricPreamble("/sortwrappers.smt2", Map("$T$" -> s"$$T$i$$", - "$S$" -> sanitizedSortString, - s"$$T$i$$" -> sortString), + "$S$" -> sanitizedSortString, + s"$$T$i$$" -> sortString), sink) } else { preambleReader.emitParametricPreamble("/sortwrappers.smt2", Map("$S$" -> sanitizedSortString, - "$T$" -> sortString), + "$T$" -> sortString), sink) } @@ -632,10 +634,10 @@ class DefaultMainVerifier(config: Config, } /** - * In case Silicon encounters an expected error (i.e. `ErrorMessage.isExpected`), Silicon continues (until at most - * config.numberOfErrorsToReport() have been encountered (per member)). - * This function combines the verification result with verification results stored in its `previous` field. - */ + * In case Silicon encounters an expected error (i.e. `ErrorMessage.isExpected`), Silicon continues (until at most + * config.numberOfErrorsToReport() have been encountered (per member)). + * This function combines the verification result with verification results stored in its `previous` field. + */ private def extractAllVerificationResults(res: VerificationResult): Seq[VerificationResult] = res :: res.previous.toList -} +} \ No newline at end of file From a44182994f21199b5220fe787aefea3187057607 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Tue, 4 Feb 2025 18:21:19 +0100 Subject: [PATCH 05/39] Refactoring --- src/main/scala/rules/Consumer.scala | 16 ++-- src/main/scala/state/BranchFailureTree.scala | 2 +- src/main/scala/state/State.scala | 96 +++++++++---------- .../scala/verifier/DefaultMainVerifier.scala | 4 +- 4 files changed, 61 insertions(+), 57 deletions(-) diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index 70728655..9f024ee4 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -589,6 +589,14 @@ object consumer extends ConsumptionRules { ) } + private def storeIntoBranchTree(v: Verifier, s: State, r: VerificationResult) = { + if (s.branchTreeMap.isDefined && s.currentMember.isDefined){ + val branchConditions = v.decider.pcs.getBranchConditionsExp() + if (branchConditions.length > 0) { + s.branchTreeMap.get.storeIntoTree(s.currentMember.get.name, branchConditions,r) + } + } + } private def evalAndAssert(s: State, e: ast.Exp, returnSnap: Boolean, pve: PartialVerificationError, v: Verifier) (Q: (State, Option[Term], Verifier) => VerificationResult) @@ -621,15 +629,11 @@ object consumer extends ConsumptionRules { case true => v2.decider.assume(t, Option.when(withExp)(e), eNew) val r = QS(s3, v2) - if (s3.branchFailureTreeMap.isDefined && s3.currentMember.isDefined){ - s3.branchFailureTreeMap.get.storeIntoTree(s3.currentMember.get.name, v.decider.pcs.getBranchConditionsExp(),r) - } + storeIntoBranchTree(v,s,r) r case false => val failure = createFailure(pve dueTo AssertionFalse(e), v2, s3, termToAssert, eNew) - if (s3.branchFailureTreeMap.isDefined && s3.currentMember.isDefined){ - s3.branchFailureTreeMap.get.storeIntoTree(s3.currentMember.get.name, v.decider.pcs.getBranchConditionsExp(),failure) - } + storeIntoBranchTree(v,s,failure) if (s3.retryLevel == 0 && v2.reportFurtherErrors()){ v2.decider.assume(t, Option.when(withExp)(e), eNew) failure combine QS(s3, v2) diff --git a/src/main/scala/state/BranchFailureTree.scala b/src/main/scala/state/BranchFailureTree.scala index e44facfe..d31f3f7e 100644 --- a/src/main/scala/state/BranchFailureTree.scala +++ b/src/main/scala/state/BranchFailureTree.scala @@ -6,7 +6,7 @@ import viper.silver.ast.Exp import scala.collection.mutable -class BranchFailureTreeMap extends mutable.HashMap[String, Tree] { +class BranchTreeMap extends mutable.HashMap[String, Tree] { def storeIntoTree(method: String, branchConditions : Seq[Exp], result: VerificationResult): Unit = { val branchTree = this.get(method) if (branchTree.isDefined) { diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index d9a438f7..d51b766f 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -82,8 +82,8 @@ final case class State(g: Store = Store(), moreCompleteExhale: Boolean = false, moreJoins: JoinMode = JoinMode.Off, - branchFailureTreeMap: Option[BranchFailureTreeMap] = None) - extends Mergeable[State] { + branchTreeMap: Option[BranchTreeMap] = None) + extends Mergeable[State] { val isMethodVerification: Boolean = { // currentMember being None means we're verifying a CFG; this should behave like verifying a method. @@ -157,54 +157,54 @@ object State { s1 match { /* Decompose state s1 */ case State(g1, h1, program, member, - predicateData, - functionData, - oldHeaps1, - parallelizeBranches1, - recordVisited1, visited1, - methodCfg1, invariantContexts1, - constrainableARPs1, - quantifiedVariables1, - retrying1, - underJoin1, - functionRecorder1, - conservingSnapshotGeneration1, - recordPossibleTriggers1, possibleTriggers1, - triggerExp1, - partiallyConsumedHeap1, - permissionScalingFactor1, permissionScalingFactorExp1, isEvalInOld, - reserveHeaps1, reserveCfgs1, conservedPcs1, recordPcs1, exhaleExt1, - ssCache1, hackIssue387DisablePermissionConsumption1, - qpFields1, qpPredicates1, qpMagicWands1, permResources1, smCache1, pmCache1, smDomainNeeded1, - predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers, - moreCompleteExhale, moreJoins, - branchFailureTreeMap) => + predicateData, + functionData, + oldHeaps1, + parallelizeBranches1, + recordVisited1, visited1, + methodCfg1, invariantContexts1, + constrainableARPs1, + quantifiedVariables1, + retrying1, + underJoin1, + functionRecorder1, + conservingSnapshotGeneration1, + recordPossibleTriggers1, possibleTriggers1, + triggerExp1, + partiallyConsumedHeap1, + permissionScalingFactor1, permissionScalingFactorExp1, isEvalInOld, + reserveHeaps1, reserveCfgs1, conservedPcs1, recordPcs1, exhaleExt1, + ssCache1, hackIssue387DisablePermissionConsumption1, + qpFields1, qpPredicates1, qpMagicWands1, permResources1, smCache1, pmCache1, smDomainNeeded1, + predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers, + moreCompleteExhale, moreJoins, + branchTreeMap) => /* Decompose state s2: most values must match those of s1 */ s2 match { case State(`g1`, `h1`, - `program`, `member`, - `predicateData`, `functionData`, - `oldHeaps1`, - `parallelizeBranches1`, - `recordVisited1`, `visited1`, - `methodCfg1`, `invariantContexts1`, - constrainableARPs2, - quantifiedVariables2, - `retrying1`, - `underJoin1`, - functionRecorder2, - `conservingSnapshotGeneration1`, - `recordPossibleTriggers1`, possibleTriggers2, - triggerExp2, - `partiallyConsumedHeap1`, - `permissionScalingFactor1`, `permissionScalingFactorExp1`, `isEvalInOld`, - `reserveHeaps1`, `reserveCfgs1`, conservedPcs2, `recordPcs1`, `exhaleExt1`, - ssCache2, `hackIssue387DisablePermissionConsumption1`, - `qpFields1`, `qpPredicates1`, `qpMagicWands1`, `permResources1`, smCache2, pmCache2, `smDomainNeeded1`, - `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`, - moreCompleteExhale2, `moreJoins`, - `branchFailureTreeMap`) => + `program`, `member`, + `predicateData`, `functionData`, + `oldHeaps1`, + `parallelizeBranches1`, + `recordVisited1`, `visited1`, + `methodCfg1`, `invariantContexts1`, + constrainableARPs2, + quantifiedVariables2, + `retrying1`, + `underJoin1`, + functionRecorder2, + `conservingSnapshotGeneration1`, + `recordPossibleTriggers1`, possibleTriggers2, + triggerExp2, + `partiallyConsumedHeap1`, + `permissionScalingFactor1`, `permissionScalingFactorExp1`, `isEvalInOld`, + `reserveHeaps1`, `reserveCfgs1`, conservedPcs2, `recordPcs1`, `exhaleExt1`, + ssCache2, `hackIssue387DisablePermissionConsumption1`, + `qpFields1`, `qpPredicates1`, `qpMagicWands1`, `permResources1`, smCache2, pmCache2, `smDomainNeeded1`, + `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`, + moreCompleteExhale2, `moreJoins`, + `branchTreeMap`) => val functionRecorder3 = functionRecorder1.merge(functionRecorder2) val triggerExp3 = triggerExp1 && triggerExp2 @@ -336,7 +336,7 @@ object State { qpFields1, qpPredicates1, qpMagicWands1, permResources1, smCache1, pmCache1, smDomainNeeded1, predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers, moreCompleteExhale, moreJoins, - branchFailureState) => + branchTreeMap) => /* Decompose state s2: most values must match those of s1 */ s2 match { @@ -361,7 +361,7 @@ object State { `qpFields1`, `qpPredicates1`, `qpMagicWands1`, `permResources1`, smCache2, pmCache2, smDomainNeeded2, `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`, moreCompleteExhale2, `moreJoins`, - `branchFailureState`) => + `branchTreeMap`) => val functionRecorder3 = functionRecorder1.merge(functionRecorder2) val triggerExp3 = triggerExp1 && triggerExp2 diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index a63a74f4..38f96d86 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -260,7 +260,7 @@ class DefaultMainVerifier(config: Config, program.methods.filterNot(excludeMethod).map(method => { val s = createInitialState(method, program, functionData, predicateData).copy(parallelizeBranches = - Verifier.config.parallelizeBranches(), branchFailureTreeMap = Option(new BranchFailureTreeMap())) /* [BRANCH-PARALLELISATION] */ + Verifier.config.parallelizeBranches(), branchTreeMap = Option(new BranchTreeMap())) /* [BRANCH-PARALLELISATION] */ _verificationPoolManager.queueVerificationTask(v => { val startTime = System.currentTimeMillis() @@ -268,7 +268,7 @@ class DefaultMainVerifier(config: Config, .flatMap(extractAllVerificationResults) val elapsed = System.currentTimeMillis() - startTime - val branchTree = s.branchFailureTreeMap.get.get(method.name) + val branchTree = s.branchTreeMap.get.get(method.name) if (branchTree.isDefined) { val branch = branchTree.get.asInstanceOf[Branch] if (branch.isLeftFatal || branch.isRightFatal) { From 472434b77c1f3045746f45c1ce6cdbae66df1778 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Wed, 5 Feb 2025 15:33:30 +0100 Subject: [PATCH 06/39] Refactoring --- .../scala/state/{BranchFailureTree.scala => BranchTree.scala} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename src/main/scala/state/{BranchFailureTree.scala => BranchTree.scala} (100%) diff --git a/src/main/scala/state/BranchFailureTree.scala b/src/main/scala/state/BranchTree.scala similarity index 100% rename from src/main/scala/state/BranchFailureTree.scala rename to src/main/scala/state/BranchTree.scala From 7b25a2ea118454e10b73d58d97c2c16de4959a3e Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Wed, 5 Feb 2025 15:34:33 +0100 Subject: [PATCH 07/39] Add tests --- .../branchTreeTests/allPathsCorrect.vpr | 10 ++++ .../branchTreeTests/allPathsCorrect_expected | 1 + .../branchTreeTests/firstPathFails.vpr | 19 +++++++ .../branchTreeTests/firstPathFails_expected | 10 ++++ .../branchTreeTests/lastPathFails.vpr | 19 +++++++ .../branchTreeTests/lastPathFails_expected | 10 ++++ .../resources/branchTreeTests/noBranches.vpr | 6 +++ .../branchTreeTests/noBranches_expected | 1 + src/test/resources/branchTreeTests/onlyIf.vpr | 14 ++++++ .../resources/branchTreeTests/onlyIf_expected | 6 +++ src/test/resources/branchTreeTests/while.vpr | 13 +++++ .../resources/branchTreeTests/while_expected | 6 +++ src/test/scala/BranchTreeTests.scala | 49 +++++++++++++++++++ 13 files changed, 164 insertions(+) create mode 100644 src/test/resources/branchTreeTests/allPathsCorrect.vpr create mode 100644 src/test/resources/branchTreeTests/allPathsCorrect_expected create mode 100644 src/test/resources/branchTreeTests/firstPathFails.vpr create mode 100644 src/test/resources/branchTreeTests/firstPathFails_expected create mode 100644 src/test/resources/branchTreeTests/lastPathFails.vpr create mode 100644 src/test/resources/branchTreeTests/lastPathFails_expected create mode 100644 src/test/resources/branchTreeTests/noBranches.vpr create mode 100644 src/test/resources/branchTreeTests/noBranches_expected create mode 100644 src/test/resources/branchTreeTests/onlyIf.vpr create mode 100644 src/test/resources/branchTreeTests/onlyIf_expected create mode 100644 src/test/resources/branchTreeTests/while.vpr create mode 100644 src/test/resources/branchTreeTests/while_expected create mode 100644 src/test/scala/BranchTreeTests.scala 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/allPathsCorrect_expected b/src/test/resources/branchTreeTests/allPathsCorrect_expected new file mode 100644 index 00000000..49263a9e --- /dev/null +++ b/src/test/resources/branchTreeTests/allPathsCorrect_expected @@ -0,0 +1 @@ +Verification successful. \ No newline at end of file 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/firstPathFails_expected b/src/test/resources/branchTreeTests/firstPathFails_expected new file mode 100644 index 00000000..3261bfed --- /dev/null +++ b/src/test/resources/branchTreeTests/firstPathFails_expected @@ -0,0 +1,10 @@ +Branch fails. +┌─┴─┐ +│ a │ +└─┬─┘ +F┌┴────┐T + ? ┌───┴───┐ + │ bcde │ + └───┬───┘ + F┌┴──┐T + ? Error \ 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/lastPathFails_expected b/src/test/resources/branchTreeTests/lastPathFails_expected new file mode 100644 index 00000000..2a2b9156 --- /dev/null +++ b/src/test/resources/branchTreeTests/lastPathFails_expected @@ -0,0 +1,10 @@ + Branch fails. + ┌─┴─┐ + │ a │ + └─┬─┘ + F┌──┴────┐T + ┌─┴─┐ ┌───┴───┐ + │ c │ │ bcde │ + └─┬─┘ └───┬───┘ + F┌──┴┐T F┌┴┐T +Error ✔ ✔ ✔ \ 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/noBranches_expected b/src/test/resources/branchTreeTests/noBranches_expected new file mode 100644 index 00000000..49263a9e --- /dev/null +++ b/src/test/resources/branchTreeTests/noBranches_expected @@ -0,0 +1 @@ +Verification successful. \ 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/onlyIf_expected b/src/test/resources/branchTreeTests/onlyIf_expected new file mode 100644 index 00000000..19580812 --- /dev/null +++ b/src/test/resources/branchTreeTests/onlyIf_expected @@ -0,0 +1,6 @@ +Branch fails. +┌─┴─┐ +│ d │ +└─┬─┘ +F┌┴──┐T +? Error \ No newline at end of file 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/resources/branchTreeTests/while_expected b/src/test/resources/branchTreeTests/while_expected new file mode 100644 index 00000000..f6ae05ac --- /dev/null +++ b/src/test/resources/branchTreeTests/while_expected @@ -0,0 +1,6 @@ +Branch fails. + ┌─┴─┐ + │ a │ + └─┬─┘ +F┌──┴┐T +Error ? \ 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..5af7a587 --- /dev/null +++ b/src/test/scala/BranchTreeTests.scala @@ -0,0 +1,49 @@ +// 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.{Files, Paths} + +class BranchTreeTests extends AnyFunSuite { + val frontend = tests.instantiateFrontend() + + test("FirstPathFails") { + executeTest("firstPathFails") + } + + test("LastPathFails") { + executeTest("lastPathFails") + } + + test("While") { + executeTest("while") + } + + test("OnlyIf") { + executeTest("onlyIf") + } + + test("AllPathsCorrect") { + executeTest("allPathsCorrect") + } + + test("NoBranches") { + executeTest("noBranches") + } + + def executeTest(fileName: String) + : Unit = { + val expectedFile = getClass.getClassLoader.getResource(s"branchTreeTests/"+fileName+"_expected") + val expected = DiskLoader.loadContent(Paths.get(expectedFile.toURI)).get + val program = tests.loadProgram("branchTreeTests/",fileName, frontend) + val actual = frontend.verifier.verify(program) + assert(actual.toString.contains(expected)) + } +} + + From eb50f57e6be114daa1bc0470d8ebf96cbdd4e191 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Wed, 5 Feb 2025 17:41:38 +0100 Subject: [PATCH 08/39] Fix tests --- .../branchTreeTests/firstPathFails_expected | 24 +++++++++++-------- .../resources/branchTreeTests/onlyIf_expected | 16 ++++++++----- .../resources/branchTreeTests/while_expected | 8 +++---- src/test/scala/BranchTreeTests.scala | 4 ++-- 4 files changed, 30 insertions(+), 22 deletions(-) diff --git a/src/test/resources/branchTreeTests/firstPathFails_expected b/src/test/resources/branchTreeTests/firstPathFails_expected index 3261bfed..0249f7e6 100644 --- a/src/test/resources/branchTreeTests/firstPathFails_expected +++ b/src/test/resources/branchTreeTests/firstPathFails_expected @@ -1,10 +1,14 @@ -Branch fails. -┌─┴─┐ -│ a │ -└─┬─┘ -F┌┴────┐T - ? ┌───┴───┐ - │ bcde │ - └───┬───┘ - F┌┴──┐T - ? Error \ No newline at end of file +Verification failed with 2 errors: + [postcondition.violated:assertion.false] Postcondition of foo might not hold. Assertion z == true might not hold. (firstPathFails.vpr@5.9--5.13) + + [postcondition.violated.branch:assertion.false.branch] Branch fails. +┌─┴─┐ +│ a │ +└─┬─┘ +F┌┴────┐T + ? ┌───┴───┐ + │ bcde │ + └───┬───┘ + F┌┴──┐T + ? Error + (firstPathFails.vpr@6.9--6.10) \ No newline at end of file diff --git a/src/test/resources/branchTreeTests/onlyIf_expected b/src/test/resources/branchTreeTests/onlyIf_expected index 19580812..d661aa8e 100644 --- a/src/test/resources/branchTreeTests/onlyIf_expected +++ b/src/test/resources/branchTreeTests/onlyIf_expected @@ -1,6 +1,10 @@ -Branch fails. -┌─┴─┐ -│ d │ -└─┬─┘ -F┌┴──┐T -? Error \ No newline at end of file +Verification failed with 2 errors: + [postcondition.violated:assertion.false] Postcondition of foo might not hold. Assertion z == true might not hold. (onlyIf.vpr@4.9--4.13) + + [postcondition.violated.branch:assertion.false.branch] Branch fails. +┌─┴─┐ +│ d │ +└─┬─┘ +F┌┴──┐T + ? Error + (onlyIf.vpr@7.9--7.10) \ No newline at end of file diff --git a/src/test/resources/branchTreeTests/while_expected b/src/test/resources/branchTreeTests/while_expected index f6ae05ac..1b52d4cc 100644 --- a/src/test/resources/branchTreeTests/while_expected +++ b/src/test/resources/branchTreeTests/while_expected @@ -1,6 +1,6 @@ Branch fails. - ┌─┴─┐ - │ a │ - └─┬─┘ -F┌──┴┐T + ┌─┴─┐ + │ a │ + └─┬─┘ + F┌──┴┐T Error ? \ No newline at end of file diff --git a/src/test/scala/BranchTreeTests.scala b/src/test/scala/BranchTreeTests.scala index 5af7a587..85cc53e2 100644 --- a/src/test/scala/BranchTreeTests.scala +++ b/src/test/scala/BranchTreeTests.scala @@ -7,7 +7,7 @@ import org.scalatest.funsuite.AnyFunSuite import viper.silver.ast.utility.DiskLoader -import java.nio.file.{Files, Paths} +import java.nio.file.{Paths} class BranchTreeTests extends AnyFunSuite { val frontend = tests.instantiateFrontend() @@ -37,7 +37,7 @@ class BranchTreeTests extends AnyFunSuite { } def executeTest(fileName: String) - : Unit = { + : Unit = { val expectedFile = getClass.getClassLoader.getResource(s"branchTreeTests/"+fileName+"_expected") val expected = DiskLoader.loadContent(Paths.get(expectedFile.toURI)).get val program = tests.loadProgram("branchTreeTests/",fileName, frontend) From ff1068744c5d21b8740c1c66760cb3b9b4357b5a Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Mon, 17 Feb 2025 16:28:10 +0100 Subject: [PATCH 09/39] Branch Tree: Print single path --- src/main/scala/state/BranchTree.scala | 140 +++++++++++++----- .../scala/verifier/DefaultMainVerifier.scala | 29 ++-- 2 files changed, 124 insertions(+), 45 deletions(-) diff --git a/src/main/scala/state/BranchTree.scala b/src/main/scala/state/BranchTree.scala index d31f3f7e..90e4fa4f 100644 --- a/src/main/scala/state/BranchTree.scala +++ b/src/main/scala/state/BranchTree.scala @@ -1,6 +1,6 @@ package viper.silicon.state -import viper.silicon.interfaces.{FatalResult, VerificationResult} +import viper.silicon.interfaces.{VerificationResult} import viper.silver.ast import viper.silver.ast.Exp @@ -18,6 +18,8 @@ class BranchTreeMap extends mutable.HashMap[String, Tree] { } class Tree { + private def combine(isCurrBranchResultFatal: Option[Boolean], result: VerificationResult) : Option[Boolean] = + if (result.isFatal) Some(true) else isCurrBranchResultFatal def extend(branchConditions : Seq[Exp], result: VerificationResult) = { if (branchConditions.length > 0) { var currNode = this @@ -34,15 +36,15 @@ class Tree { case ast.Not(exp) => exp case _ => tail.head } - if (currBranch.left.isDefined && currBranch.left.get.isInstanceOf[Branch] - && headExp.toString.equals(currBranch.left.get.asInstanceOf[Branch].exp.toString) && negated) { - currNode = currBranch.left.get - currBranch.isLeftFatal = result.isFatal || currBranch.isLeftFatal + if (currBranch.left.isInstanceOf[Branch] + && headExp.toString.equals(currBranch.left.asInstanceOf[Branch].exp.toString) && negated) { + currNode = currBranch.left + currBranch.leftResultFatal = combine(currBranch.leftResultFatal,result) next = true - } else if (currBranch.right.isDefined && currBranch.right.get.isInstanceOf[Branch] - && headExp.toString.equals(currBranch.right.get.asInstanceOf[Branch].exp.toString) && !negated) { - currNode = currBranch.right.get - currBranch.isRightFatal = result.isFatal || currBranch.isRightFatal + } else if (currBranch.right.isInstanceOf[Branch] + && headExp.toString.equals(currBranch.right.asInstanceOf[Branch].exp.toString) && !negated) { + currNode = currBranch.right + currBranch.rightResultFatal = combine(currBranch.rightResultFatal,result) next = true } if (next) { @@ -55,28 +57,39 @@ class Tree { } } if (negated) { - val tailTree = Tree.generate(tail, result) - currBranch.left = Some(tailTree) - currBranch.isLeftFatal = result.isFatal || currBranch.isLeftFatal + currBranch.left = Tree.generate(tail, result) + currBranch.leftResultFatal = combine(currBranch.leftResultFatal,result) } else { - val tailTree = Tree.generate(tail, result) - currBranch.right = Some(tailTree) - currBranch.isRightFatal = result.isFatal || currBranch.isRightFatal + currBranch.right = Tree.generate(tail, result) + currBranch.rightResultFatal = combine(currBranch.rightResultFatal,result) } } } + private def recurse(tree: Tree, isFatal: Boolean) : (Vector[String], Int, Int) = { + tree match { + case Leaf => + if (isFatal) { + (Vector("Error"), 2, 2) // ✘ + } else { + (Vector("✔"), 0, 0) + } + case _ : Branch => tree.buildTree() + case _=> (Vector("?"), 0, 0) + } + } + private def even(n: Int) = (n & 1) == 0 private def buildTree() : (Vector[String], Int, Int) = { this match { - case Branch(exp, left, right, _, _) => + case b@Branch(exp, left, right, _, _) => val expStr = exp.toString val expStrLen = expStr.length - val even = (n: Int) => (n & 1) == 0 + var boxMiddle = "│ " + expStr + (if (even(expStr.length)) " " else "") + " │" val boxLen = boxMiddle.length val halfBoxLen = boxLen / 2 - var (leftStrVec, _, prevLeftRightBoxLen) = if(left.isDefined) left.get.buildTree() else (Vector("?"), 0, 0) - var (rightStrVec, prevRightLeftBoxLen, _) = if(right.isDefined) right.get.buildTree() else (Vector("?"), 0, 0) + var (leftStrVec, _, prevLeftRightBoxLen) = recurse(left, b.isLeftFatal) + var (rightStrVec, prevRightLeftBoxLen, _) = recurse(right, b.isRightFatal) val halfExpStrLen = expStrLen / 2 val leftBoxLen = leftStrVec.head.length @@ -118,43 +131,100 @@ class Tree { } } (boxTop +: boxMiddle +: boxBottom +: (leftStrVec zip rightStrVec).map(t => t._1 + t._2), leftFiller + halfBoxLen, rightFiller + halfBoxLen) - case Leaf(result) => - result match { - case _: FatalResult => (Vector("Error"), 2, 2) // ✘ - case _ => (Vector("✔"), 0, 0) - } + 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 printSinglePath() : String = { + var currTree : Tree = 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, _, _) => + val expStr = e.toString + val halfExpStrLen = expStr.length / 2 + val pathTaken = if (b.isLeftFatal) "F" else "T" + val pathNotTaken = if (b.isLeftFatal) "T" else "F" + + 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) + + val sideResultFatal = if(b.isLeftFatal) b.rightResultFatal else b.leftResultFatal + sideResultFatal match { + case Some(false) => side ++= Vector("\n"," Error\n","\n","\n") + case Some(_) => side ++= Vector("\n"," ✔\n","\n","\n") + case _ => side ++= Vector("\n"," ?\n","\n","\n") + } + + path ++= box + currTree = if (b.isLeftFatal) l else r + 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 prettyPrint() = { - val tree = this.buildTree() - val result = tree._1.reduce((str, s) => str + "\n" + s) + "\n" - result + def prettyPrint(reportFurtherErrors: Boolean = false) : String = { + if (reportFurtherErrors) { + this.buildTree()._1.reduce((str, s) => str + "\n" + s) + "\n" + } else { + this.printSinglePath() + } } } object Tree { def generate(expressions : Seq[Exp], result: VerificationResult) : Tree = { if (expressions.length == 0) { - Leaf(result) + Leaf } else { val reversedExpressions = expressions.reverse val headExp = reversedExpressions.head var tree = reversedExpressions.head match { - case ast.Not(exp) => Branch(exp, Some(Leaf(result)), None, result.isFatal, false) - case _ => Branch(headExp, None, Some(Leaf(result)), false, result.isFatal) + case ast.Not(exp) => Branch(exp, Leaf, Leaf, Some(result.isFatal), None) + case _ => Branch(headExp, Leaf, Leaf, None, Some(result.isFatal)) } for (elem <- reversedExpressions.tail) { var negated = false elem match { case ast.Not(exp) => negated = true - tree = Branch(exp, Some(tree), None, result.isFatal, false) + tree = Branch(exp, tree, Leaf, Some(result.isFatal), None) case _ => - tree = Branch(elem, None, Some(tree), false, result.isFatal) + tree = Branch(elem, Leaf, tree, None, Some(result.isFatal)) } } tree } } } -private case class Leaf(result : VerificationResult) extends Tree -case class Branch(exp : Exp, var left: Option[Tree], var right: Option[Tree], var isLeftFatal: Boolean, var isRightFatal: Boolean) extends Tree \ No newline at end of file +private object Leaf extends Tree +case class Branch(var exp : Exp, + var left: Tree, + var right: Tree, + var leftResultFatal: Option[Boolean], + var rightResultFatal: Option[Boolean]) extends Tree { + def isLeftFatal = leftResultFatal.isDefined && leftResultFatal.get + def isRightFatal = rightResultFatal.isDefined && rightResultFatal.get +} \ No newline at end of file diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index 38f96d86..e4696294 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -53,10 +53,10 @@ trait MainVerifier extends Verifier { class DefaultMainVerifier(config: Config, override val reporter: Reporter, override val rootSymbExLogger: SymbExLogger[_ <: MemberSymbExLogger]) - extends BaseVerifier(config, "00") - with MainVerifier - with DefaultFunctionVerificationUnitProvider - with DefaultPredicateVerificationUnitProvider { + extends BaseVerifier(config, "00") + with MainVerifier + with DefaultFunctionVerificationUnitProvider + with DefaultPredicateVerificationUnitProvider { Verifier.config = config @@ -169,11 +169,11 @@ class DefaultMainVerifier(config: Config, def verify(originalProgram: ast.Program, cfgs: Seq[SilverCfg], inputFile: Option[String]): List[VerificationResult] = { /** Trigger computation is currently not thread-safe; hence, all triggers are computed - * up-front, before the program is verified in parallel. - * This is done bottom-up to ensure that nested quantifiers are transformed as well - * (top-down should also work, but the default of 'innermost' won't). - * See also [[viper.silicon.utils.ast.autoTrigger]]. - */ + * up-front, before the program is verified in parallel. + * This is done bottom-up to ensure that nested quantifiers are transformed as well + * (top-down should also work, but the default of 'innermost' won't). + * See also [[viper.silicon.utils.ast.autoTrigger]]. + */ var program: ast.Program = originalProgram.transform({ case forall: ast.Forall if forall.isPure => @@ -273,7 +273,16 @@ class DefaultMainVerifier(config: Config, val branch = branchTree.get.asInstanceOf[Branch] if (branch.isLeftFatal || branch.isRightFatal) { val firstCond = branchTree.get.asInstanceOf[Branch].exp - results +:= Failure(PostconditionViolatedBranch(firstCond, AssertionFalseAtBranch(firstCond, branchTree.get.prettyPrint()), branch.isLeftFatal, branch.isRightFatal)) + results +:= Failure( + PostconditionViolatedBranch( + firstCond, + AssertionFalseAtBranch( + firstCond, + branchTree.get.prettyPrint(v.reportFurtherErrors()) + ), + branch.isLeftFatal, + branch.isRightFatal) + ) } } reporter report VerificationResultMessage(s"silicon", method, elapsed, condenseToViperResult(results)) From 213df1dc137fc4fb9c5aa31128346a70c80a702a Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Mon, 17 Feb 2025 18:39:12 +0100 Subject: [PATCH 10/39] Fix tests --- .../{ => default}/allPathsCorrect_expected | 0 .../default/firstPathFails_expected | 10 +++ .../{ => default}/lastPathFails_expected | 4 +- .../{ => default}/noBranches_expected | 0 .../branchTreeTests/default/onlyIf_expected | 7 +++ .../{ => default}/while_expected | 4 +- .../branchTreeTests/firstPathFails_expected | 14 ----- .../resources/branchTreeTests/onlyIf_expected | 10 --- .../reportAllErrors/allPathsCorrect_expected | 1 + .../reportAllErrors/firstPathFails_expected | 10 +++ .../reportAllErrors/lastPathFails_expected | 10 +++ .../reportAllErrors/noBranches_expected | 1 + .../reportAllErrors/onlyIf_expected | 6 ++ .../reportAllErrors/while_expected | 6 ++ src/test/scala/BranchTreeTests.scala | 63 ++++++++++++------- src/test/scala/tests.scala | 6 +- 16 files changed, 100 insertions(+), 52 deletions(-) rename src/test/resources/branchTreeTests/{ => default}/allPathsCorrect_expected (100%) create mode 100644 src/test/resources/branchTreeTests/default/firstPathFails_expected rename src/test/resources/branchTreeTests/{ => default}/lastPathFails_expected (87%) rename src/test/resources/branchTreeTests/{ => default}/noBranches_expected (100%) create mode 100644 src/test/resources/branchTreeTests/default/onlyIf_expected rename src/test/resources/branchTreeTests/{ => default}/while_expected (76%) delete mode 100644 src/test/resources/branchTreeTests/firstPathFails_expected delete mode 100644 src/test/resources/branchTreeTests/onlyIf_expected create mode 100644 src/test/resources/branchTreeTests/reportAllErrors/allPathsCorrect_expected create mode 100644 src/test/resources/branchTreeTests/reportAllErrors/firstPathFails_expected create mode 100644 src/test/resources/branchTreeTests/reportAllErrors/lastPathFails_expected create mode 100644 src/test/resources/branchTreeTests/reportAllErrors/noBranches_expected create mode 100644 src/test/resources/branchTreeTests/reportAllErrors/onlyIf_expected create mode 100644 src/test/resources/branchTreeTests/reportAllErrors/while_expected diff --git a/src/test/resources/branchTreeTests/allPathsCorrect_expected b/src/test/resources/branchTreeTests/default/allPathsCorrect_expected similarity index 100% rename from src/test/resources/branchTreeTests/allPathsCorrect_expected rename to src/test/resources/branchTreeTests/default/allPathsCorrect_expected diff --git a/src/test/resources/branchTreeTests/default/firstPathFails_expected b/src/test/resources/branchTreeTests/default/firstPathFails_expected new file mode 100644 index 00000000..627f21c2 --- /dev/null +++ b/src/test/resources/branchTreeTests/default/firstPathFails_expected @@ -0,0 +1,10 @@ + + ┌─┴─┐ + │ a │ + └─┬─┘ + F┌──┴─────┐T + ┌─┴─┐ ┌───┴───┐ + │ c │ │ bcde │ + └─┬─┘ └───┬───┘ + F┌──┴┐T F┌──┴──┐T +Error ✔ Error Error \ No newline at end of file diff --git a/src/test/resources/branchTreeTests/lastPathFails_expected b/src/test/resources/branchTreeTests/default/lastPathFails_expected similarity index 87% rename from src/test/resources/branchTreeTests/lastPathFails_expected rename to src/test/resources/branchTreeTests/default/lastPathFails_expected index 2a2b9156..5766e420 100644 --- a/src/test/resources/branchTreeTests/lastPathFails_expected +++ b/src/test/resources/branchTreeTests/default/lastPathFails_expected @@ -1,4 +1,4 @@ - Branch fails. + ┌─┴─┐ │ a │ └─┬─┘ @@ -7,4 +7,4 @@ │ c │ │ bcde │ └─┬─┘ └───┬───┘ F┌──┴┐T F┌┴┐T -Error ✔ ✔ ✔ \ No newline at end of file +Error ✔ ✔ ✔ \ No newline at end of file diff --git a/src/test/resources/branchTreeTests/noBranches_expected b/src/test/resources/branchTreeTests/default/noBranches_expected similarity index 100% rename from src/test/resources/branchTreeTests/noBranches_expected rename to src/test/resources/branchTreeTests/default/noBranches_expected diff --git a/src/test/resources/branchTreeTests/default/onlyIf_expected b/src/test/resources/branchTreeTests/default/onlyIf_expected new file mode 100644 index 00000000..a5ce8f8b --- /dev/null +++ b/src/test/resources/branchTreeTests/default/onlyIf_expected @@ -0,0 +1,7 @@ + + ┌─┴─┐ + │ d │ + └─┬─┘ + F┌──┴──┐T +Error Error + (onlyIf.vpr@7.9--7.10) diff --git a/src/test/resources/branchTreeTests/while_expected b/src/test/resources/branchTreeTests/default/while_expected similarity index 76% rename from src/test/resources/branchTreeTests/while_expected rename to src/test/resources/branchTreeTests/default/while_expected index 1b52d4cc..016f9c56 100644 --- a/src/test/resources/branchTreeTests/while_expected +++ b/src/test/resources/branchTreeTests/default/while_expected @@ -1,6 +1,6 @@ -Branch fails. + ┌─┴─┐ │ a │ └─┬─┘ F┌──┴┐T -Error ? \ No newline at end of file +Error ✔ \ No newline at end of file diff --git a/src/test/resources/branchTreeTests/firstPathFails_expected b/src/test/resources/branchTreeTests/firstPathFails_expected deleted file mode 100644 index 0249f7e6..00000000 --- a/src/test/resources/branchTreeTests/firstPathFails_expected +++ /dev/null @@ -1,14 +0,0 @@ -Verification failed with 2 errors: - [postcondition.violated:assertion.false] Postcondition of foo might not hold. Assertion z == true might not hold. (firstPathFails.vpr@5.9--5.13) - - [postcondition.violated.branch:assertion.false.branch] Branch fails. -┌─┴─┐ -│ a │ -└─┬─┘ -F┌┴────┐T - ? ┌───┴───┐ - │ bcde │ - └───┬───┘ - F┌┴──┐T - ? Error - (firstPathFails.vpr@6.9--6.10) \ No newline at end of file diff --git a/src/test/resources/branchTreeTests/onlyIf_expected b/src/test/resources/branchTreeTests/onlyIf_expected deleted file mode 100644 index d661aa8e..00000000 --- a/src/test/resources/branchTreeTests/onlyIf_expected +++ /dev/null @@ -1,10 +0,0 @@ -Verification failed with 2 errors: - [postcondition.violated:assertion.false] Postcondition of foo might not hold. Assertion z == true might not hold. (onlyIf.vpr@4.9--4.13) - - [postcondition.violated.branch:assertion.false.branch] Branch fails. -┌─┴─┐ -│ d │ -└─┬─┘ -F┌┴──┐T - ? Error - (onlyIf.vpr@7.9--7.10) \ 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..a590cb67 --- /dev/null +++ b/src/test/resources/branchTreeTests/reportAllErrors/firstPathFails_expected @@ -0,0 +1,10 @@ + + ┌─┴─┐ + │ 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..5766e420 --- /dev/null +++ b/src/test/resources/branchTreeTests/reportAllErrors/lastPathFails_expected @@ -0,0 +1,10 @@ + + ┌─┴─┐ + │ a │ + └─┬─┘ + F┌──┴────┐T + ┌─┴─┐ ┌───┴───┐ + │ c │ │ bcde │ + └─┬─┘ └───┬───┘ + F┌──┴┐T F┌┴┐T +Error ✔ ✔ ✔ \ No newline at end of file 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..da3d2a15 --- /dev/null +++ b/src/test/resources/branchTreeTests/reportAllErrors/onlyIf_expected @@ -0,0 +1,6 @@ + + ┌─┴─┐ + │ 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..f25e2367 --- /dev/null +++ b/src/test/resources/branchTreeTests/reportAllErrors/while_expected @@ -0,0 +1,6 @@ + + ┌─┴─┐ + │ a │ + └─┬─┘ + F┌──┴┐T +Error ✔ diff --git a/src/test/scala/BranchTreeTests.scala b/src/test/scala/BranchTreeTests.scala index 85cc53e2..9ae67a5a 100644 --- a/src/test/scala/BranchTreeTests.scala +++ b/src/test/scala/BranchTreeTests.scala @@ -6,39 +6,60 @@ import org.scalatest.funsuite.AnyFunSuite import viper.silver.ast.utility.DiskLoader +import viper.silver.frontend.SilFrontend -import java.nio.file.{Paths} +import java.nio.file.Paths class BranchTreeTests extends AnyFunSuite { - val frontend = tests.instantiateFrontend() + val defaultFrontend = tests.instantiateFrontend() + val frontendAllErrors = tests.instantiateFrontend(List("--numberOfErrorsToReport", "0")) - test("FirstPathFails") { - executeTest("firstPathFails") + test("FirstPathFailsPath") { + executeTestDefault("firstPathFails") } - - test("LastPathFails") { - executeTest("lastPathFails") + test("LastPathFailsPath") { + executeTestDefault("lastPathFails") } - - test("While") { - executeTest("while") + test("WhilePath") { + executeTestDefault("while") } - - test("OnlyIf") { - executeTest("onlyIf") + test("OnlyIfPath") { + executeTestDefault("onlyIf") } - - test("AllPathsCorrect") { - executeTest("allPathsCorrect") + test("AllPathsPath") { + executeTestDefault("allPathsCorrect") } + test("NoBranchesPath") { + executeTestDefault("noBranches") + } + + def executeTestDefault(fileName: String) : Unit = executeTest(fileName, defaultFrontend, "default") + - test("NoBranches") { - executeTest("noBranches") + test("FirstPathFailsTree") { + executeTestDefault("firstPathFails") } + test("LastPathFailsTree") { + executeTestDefault("lastPathFails") + } + test("WhileTree") { + executeTestDefault("while") + } + test("OnlyIfTree") { + executeTestDefault("onlyIf") + } + test("AllPathsCorrectTree") { + executeTestDefault("allPathsCorrect") + } + test("NoBranchesTree") { + executeTestDefault("noBranches") + } + + def executeTestReportAllErrors(fileName: String) : Unit = executeTest(fileName, frontendAllErrors, "reportAllErrors") - def executeTest(fileName: String) - : Unit = { - val expectedFile = getClass.getClassLoader.getResource(s"branchTreeTests/"+fileName+"_expected") + def executeTest(fileName: String, frontend : SilFrontend, expectedFolder : String) + : Unit = { + val expectedFile = getClass.getClassLoader.getResource(s"branchTreeTests/$expectedFolder/"+fileName+"_expected") val expected = DiskLoader.loadContent(Paths.get(expectedFile.toURI)).get val program = tests.loadProgram("branchTreeTests/",fileName, frontend) val actual = frontend.verifier.verify(program) 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) From d8856bcf73633ed482e39726991ee4e31be7811f Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Mon, 17 Feb 2025 19:29:35 +0100 Subject: [PATCH 11/39] Really fix tests --- .../default/firstPathFails_expected | 19 +++++++------- .../default/lastPathFails_expected | 19 +++++++------- .../branchTreeTests/default/onlyIf_expected | 12 ++++----- .../branchTreeTests/default/while_expected | 11 ++++---- src/test/scala/BranchTreeTests.scala | 26 ++++++++----------- 5 files changed, 43 insertions(+), 44 deletions(-) diff --git a/src/test/resources/branchTreeTests/default/firstPathFails_expected b/src/test/resources/branchTreeTests/default/firstPathFails_expected index 627f21c2..2607b87a 100644 --- a/src/test/resources/branchTreeTests/default/firstPathFails_expected +++ b/src/test/resources/branchTreeTests/default/firstPathFails_expected @@ -1,10 +1,11 @@ - ┌─┴─┐ - │ a │ - └─┬─┘ - F┌──┴─────┐T - ┌─┴─┐ ┌───┴───┐ - │ c │ │ bcde │ - └─┬─┘ └───┬───┘ - F┌──┴┐T F┌──┴──┐T -Error ✔ Error Error \ No newline at end of file + │ + ┌─┴─┐ F + │ a ├──── ? + └─┬─┘ + │T +┌───┴───┐ F +│ bcde ├── ? +└───┬───┘ + │T + Error \ No newline at end of file diff --git a/src/test/resources/branchTreeTests/default/lastPathFails_expected b/src/test/resources/branchTreeTests/default/lastPathFails_expected index 5766e420..4359f99a 100644 --- a/src/test/resources/branchTreeTests/default/lastPathFails_expected +++ b/src/test/resources/branchTreeTests/default/lastPathFails_expected @@ -1,10 +1,11 @@ - ┌─┴─┐ - │ a │ - └─┬─┘ - F┌──┴────┐T - ┌─┴─┐ ┌───┴───┐ - │ c │ │ bcde │ - └─┬─┘ └───┬───┘ - F┌──┴┐T F┌┴┐T -Error ✔ ✔ ✔ \ No newline at end of file + │ +┌─┴─┐ T +│ a ├── Error +└─┬─┘ + │F +┌─┴─┐ T +│ c ├── Error +└─┬─┘ + │F +Error \ No newline at end of file diff --git a/src/test/resources/branchTreeTests/default/onlyIf_expected b/src/test/resources/branchTreeTests/default/onlyIf_expected index a5ce8f8b..f7567aa6 100644 --- a/src/test/resources/branchTreeTests/default/onlyIf_expected +++ b/src/test/resources/branchTreeTests/default/onlyIf_expected @@ -1,7 +1,7 @@ - ┌─┴─┐ - │ d │ - └─┬─┘ - F┌──┴──┐T -Error Error - (onlyIf.vpr@7.9--7.10) + │ +┌─┴─┐ F +│ d ├── ? +└─┬─┘ + │T +Error \ No newline at end of file diff --git a/src/test/resources/branchTreeTests/default/while_expected b/src/test/resources/branchTreeTests/default/while_expected index 016f9c56..541f4c49 100644 --- a/src/test/resources/branchTreeTests/default/while_expected +++ b/src/test/resources/branchTreeTests/default/while_expected @@ -1,6 +1,7 @@ - ┌─┴─┐ - │ a │ - └─┬─┘ - F┌──┴┐T -Error ✔ \ No newline at end of file + │ +┌─┴─┐ T +│ a ├── ? +└─┬─┘ + │F +Error \ No newline at end of file diff --git a/src/test/scala/BranchTreeTests.scala b/src/test/scala/BranchTreeTests.scala index 9ae67a5a..66b5a800 100644 --- a/src/test/scala/BranchTreeTests.scala +++ b/src/test/scala/BranchTreeTests.scala @@ -6,13 +6,11 @@ import org.scalatest.funsuite.AnyFunSuite import viper.silver.ast.utility.DiskLoader -import viper.silver.frontend.SilFrontend -import java.nio.file.Paths +import java.nio.file.{Paths} class BranchTreeTests extends AnyFunSuite { - val defaultFrontend = tests.instantiateFrontend() - val frontendAllErrors = tests.instantiateFrontend(List("--numberOfErrorsToReport", "0")) + def executeTestDefault(fileName: String) : Unit = executeTest(fileName, "default") test("FirstPathFailsPath") { executeTestDefault("firstPathFails") @@ -33,34 +31,32 @@ class BranchTreeTests extends AnyFunSuite { executeTestDefault("noBranches") } - def executeTestDefault(fileName: String) : Unit = executeTest(fileName, defaultFrontend, "default") - + def executeTestReportAllErrors(fileName: String) : Unit = executeTest(fileName, "reportAllErrors", List("--numberOfErrorsToReport", "0")) test("FirstPathFailsTree") { - executeTestDefault("firstPathFails") + executeTestReportAllErrors("firstPathFails") } test("LastPathFailsTree") { - executeTestDefault("lastPathFails") + executeTestReportAllErrors("lastPathFails") } test("WhileTree") { - executeTestDefault("while") + executeTestReportAllErrors("while") } test("OnlyIfTree") { - executeTestDefault("onlyIf") + executeTestReportAllErrors("onlyIf") } test("AllPathsCorrectTree") { - executeTestDefault("allPathsCorrect") + executeTestReportAllErrors("allPathsCorrect") } test("NoBranchesTree") { - executeTestDefault("noBranches") + executeTestReportAllErrors("noBranches") } - def executeTestReportAllErrors(fileName: String) : Unit = executeTest(fileName, frontendAllErrors, "reportAllErrors") - - def executeTest(fileName: String, frontend : SilFrontend, expectedFolder : String) + def executeTest(fileName: String, expectedFolder : String, args: List[String] = List.empty) : Unit = { val expectedFile = getClass.getClassLoader.getResource(s"branchTreeTests/$expectedFolder/"+fileName+"_expected") val expected = DiskLoader.loadContent(Paths.get(expectedFile.toURI)).get + val frontend = tests.instantiateFrontend(args) val program = tests.loadProgram("branchTreeTests/",fileName, frontend) val actual = frontend.verifier.verify(program) assert(actual.toString.contains(expected)) From 1251bb1a3ab3313b63382abb5270c68b52fbd27b Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Wed, 19 Feb 2025 12:32:11 +0100 Subject: [PATCH 12/39] Fix tests --- src/main/scala/rules/Consumer.scala | 6 +- src/main/scala/state/BranchTree.scala | 123 +++++++++--------- .../scala/verifier/DefaultMainVerifier.scala | 6 +- .../default/lastPathFails_expected | 4 +- .../default/multipleMethods_expected | 22 ++++ .../branchTreeTests/multipleMethods.vpr | 37 ++++++ .../reportAllErrors/while_expected | 11 +- .../reportTwoErrors/firstPathFails_expected | 10 ++ .../reportTwoErrors/lastPathFails_expected | 10 ++ src/test/scala/BranchTreeTests.scala | 32 +++-- 10 files changed, 181 insertions(+), 80 deletions(-) create mode 100644 src/test/resources/branchTreeTests/default/multipleMethods_expected create mode 100644 src/test/resources/branchTreeTests/multipleMethods.vpr create mode 100644 src/test/resources/branchTreeTests/reportTwoErrors/firstPathFails_expected create mode 100644 src/test/resources/branchTreeTests/reportTwoErrors/lastPathFails_expected diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index 9f024ee4..c9ccfc97 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -234,7 +234,7 @@ object consumer extends ConsumptionRules { v3.symbExLog.closeScope(uidCondExp) Q(s3, h1, t1, v3) }), - (s2, v2) => consumeR(s2, h, a2, returnSnap, pve, v2)((s3, h1, t1, v3) => { + (s2, v2) => consumeR(s2, h, a2, pve, v2)((s3, h1, t1, v3) => { v3.symbExLog.closeScope(uidCondExp) Q(s3, h1, t1, v3) }))) @@ -541,7 +541,7 @@ object consumer extends ConsumptionRules { private def consumeConditionalTlcMoreJoins(s: State, h: Heap, e0: ast.Exp, a1: ast.Exp, a2: Option[ast.Exp], scopeUid: Int, returnSnap: Boolean, pve: PartialVerificationError, v: Verifier) - (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) + (Q: (State, Heap, Term, Verifier) => VerificationResult) : VerificationResult = { eval(s, e0, pve, v)((s1, t0, e0New, v1) => joiner.join[(Heap, Option[Term]), (Heap, Option[Term])](s1, v1, resetState = false)((s1, v1, QB) => { @@ -593,7 +593,7 @@ object consumer extends ConsumptionRules { if (s.branchTreeMap.isDefined && s.currentMember.isDefined){ val branchConditions = v.decider.pcs.getBranchConditionsExp() if (branchConditions.length > 0) { - s.branchTreeMap.get.storeIntoTree(s.currentMember.get.name, branchConditions,r) + s.branchTreeMap.get.storeIntoTree(s.currentMember.get.name, branchConditions, r.isFatal) } } } diff --git a/src/main/scala/state/BranchTree.scala b/src/main/scala/state/BranchTree.scala index 90e4fa4f..86f1c719 100644 --- a/src/main/scala/state/BranchTree.scala +++ b/src/main/scala/state/BranchTree.scala @@ -1,26 +1,30 @@ package viper.silicon.state -import viper.silicon.interfaces.{VerificationResult} +import viper.silicon.verifier.Verifier import viper.silver.ast import viper.silver.ast.Exp import scala.collection.mutable -class BranchTreeMap extends mutable.HashMap[String, Tree] { - def storeIntoTree(method: String, branchConditions : Seq[Exp], result: VerificationResult): Unit = { - val branchTree = this.get(method) +class BranchTreeMap { + private val map : mutable.Map[String, Tree] = new mutable.HashMap[String,Tree]() + def Map(): mutable.Map[String, Tree] = map + + def storeIntoTree(method: String, branchConditions : Seq[Exp], isResultFatal: Boolean): Unit = { + val branchTree = map.get(method) if (branchTree.isDefined) { - branchTree.get.extend(branchConditions, result) + branchTree.get.extend(branchConditions, isResultFatal) } else { - this.put(method, Tree.generate(branchConditions, result)) + map.put(method, Tree.generate(branchConditions, isResultFatal)) } } } class Tree { - private def combine(isCurrBranchResultFatal: Option[Boolean], result: VerificationResult) : Option[Boolean] = - if (result.isFatal) Some(true) else isCurrBranchResultFatal - def extend(branchConditions : Seq[Exp], result: VerificationResult) = { + private def incrementIfFatal(currBranchResultFatal: Int, isResultFatal: Boolean) : Int = + if (isResultFatal) Math.max(currBranchResultFatal,0)+1 else currBranchResultFatal + + def extend(branchConditions : Seq[Exp], isResultFatal: Boolean) = { if (branchConditions.length > 0) { var currNode = this var currBranch = currNode.asInstanceOf[Branch] @@ -39,12 +43,12 @@ class Tree { if (currBranch.left.isInstanceOf[Branch] && headExp.toString.equals(currBranch.left.asInstanceOf[Branch].exp.toString) && negated) { currNode = currBranch.left - currBranch.leftResultFatal = combine(currBranch.leftResultFatal,result) + currBranch.leftResFatalCount = incrementIfFatal(currBranch.leftResFatalCount,isResultFatal) next = true } else if (currBranch.right.isInstanceOf[Branch] && headExp.toString.equals(currBranch.right.asInstanceOf[Branch].exp.toString) && !negated) { currNode = currBranch.right - currBranch.rightResultFatal = combine(currBranch.rightResultFatal,result) + currBranch.rightResFatalCount = incrementIfFatal(currBranch.rightResFatalCount,isResultFatal) next = true } if (next) { @@ -56,31 +60,31 @@ class Tree { tail = tail.tail } } + val errorCount = if (isResultFatal) 1 else -1 // -1 for successful result if (negated) { - currBranch.left = Tree.generate(tail, result) - currBranch.leftResultFatal = combine(currBranch.leftResultFatal,result) + currBranch.left = Tree.generate(tail, errorCount) + currBranch.leftResFatalCount = errorCount } else { - currBranch.right = Tree.generate(tail, result) - currBranch.rightResultFatal = combine(currBranch.rightResultFatal,result) + currBranch.right = Tree.generate(tail, errorCount) + currBranch.rightResFatalCount = errorCount } } } - private def recurse(tree: Tree, isFatal: Boolean) : (Vector[String], Int, Int) = { + + private def recurse(tree: Tree, fatalCount: Int) : (Vector[String], Int, Int) = { tree match { - case Leaf => - if (isFatal) { - (Vector("Error"), 2, 2) // ✘ - } else { - (Vector("✔"), 0, 0) - } + case Leaf if fatalCount == -1 => (Vector("✔"), 0, 0) + case Leaf if fatalCount > 0 => (Vector("Error"), 2, 2) // ✘ case _ : Branch => tree.buildTree() - case _=> (Vector("?"), 0, 0) + case _ => (Vector("?"), 0, 0) } } + private def even(n: Int) = (n & 1) == 0 + private def buildTree() : (Vector[String], Int, Int) = { this match { - case b@Branch(exp, left, right, _, _) => + case Branch(exp, left, right, leftErrCount, rightErrCount) => val expStr = exp.toString val expStrLen = expStr.length @@ -88,8 +92,8 @@ class Tree { val boxLen = boxMiddle.length val halfBoxLen = boxLen / 2 - var (leftStrVec, _, prevLeftRightBoxLen) = recurse(left, b.isLeftFatal) - var (rightStrVec, prevRightLeftBoxLen, _) = recurse(right, b.isRightFatal) + var (leftStrVec, _, prevLeftRightBoxLen) = recurse(left, leftErrCount) + var (rightStrVec, prevRightLeftBoxLen, _) = recurse(right, rightErrCount) val halfExpStrLen = expStrLen / 2 val leftBoxLen = leftStrVec.head.length @@ -145,6 +149,7 @@ class Tree { ) }).toVector } + private def printSinglePath() : String = { var currTree : Tree = this var maxBoxLen = 5 // for 'Error' @@ -152,7 +157,7 @@ class Tree { var side = Vector[String]() while (currTree != Leaf) { currTree match { - case b@Branch(e, l, r, _, _) => + case b@Branch(e, l, r, lc, rc) => val expStr = e.toString val halfExpStrLen = expStr.length / 2 val pathTaken = if (b.isLeftFatal) "F" else "T" @@ -169,11 +174,10 @@ class Tree { if (maxBoxLen > boxLen) box = fill(box, filler) else path = fill(path, filler) maxBoxLen = Math.max(maxBoxLen, boxLen) - val sideResultFatal = if(b.isLeftFatal) b.rightResultFatal else b.leftResultFatal - sideResultFatal match { - case Some(false) => side ++= Vector("\n"," Error\n","\n","\n") - case Some(_) => side ++= Vector("\n"," ✔\n","\n","\n") - case _ => side ++= Vector("\n"," ?\n","\n","\n") + (if(b.isLeftFatal) rc else lc) 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 @@ -186,45 +190,48 @@ class Tree { ((" "*filler + "│" + " "*filler + "\n") +: combined :+ (" "*(filler-2)+"Error\n")) .reduce((str, s) => str + s) } - def prettyPrint(reportFurtherErrors: Boolean = false) : String = { - if (reportFurtherErrors) { - this.buildTree()._1.reduce((str, s) => str + "\n" + s) + "\n" - } else { + + def getErrorCount(): Int = { + this match { + case Branch(_,_,_,lf,rf) => lf + rf + case _ => 0 + } + } + + def prettyPrint() : String = { + if (Verifier.config.numberOfErrorsToReport() == 1 || this.getErrorCount() == 1) { this.printSinglePath() + } else { + this.buildTree()._1.reduce((str, s) => str + "\n" + s) + "\n" } } } + object Tree { - def generate(expressions : Seq[Exp], result: VerificationResult) : Tree = { - if (expressions.length == 0) { - Leaf - } else { - val reversedExpressions = expressions.reverse - val headExp = reversedExpressions.head - var tree = reversedExpressions.head match { - case ast.Not(exp) => Branch(exp, Leaf, Leaf, Some(result.isFatal), None) - case _ => Branch(headExp, Leaf, Leaf, None, Some(result.isFatal)) - } - for (elem <- reversedExpressions.tail) { - var negated = false - elem match { + private def generate(expressions : Seq[Exp], errorCount: Int) : Tree = { + expressions.length match { + case 0 => Leaf + case _ => + val subtree = generate(expressions.tail, errorCount) + expressions.head match { case ast.Not(exp) => - negated = true - tree = Branch(exp, tree, Leaf, Some(result.isFatal), None) + Branch(exp, subtree, Leaf, errorCount, 0) case _ => - tree = Branch(elem, Leaf, tree, None, Some(result.isFatal)) + Branch(expressions.head, Leaf, subtree, 0, errorCount) } - } - tree } } + + def generate(expressions : Seq[Exp], isFatal: Boolean) : Tree = + generate(expressions, if (isFatal) 1 else -1) // -1 or distinguishing successful from no result at leaves } + private object Leaf extends Tree case class Branch(var exp : Exp, var left: Tree, var right: Tree, - var leftResultFatal: Option[Boolean], - var rightResultFatal: Option[Boolean]) extends Tree { - def isLeftFatal = leftResultFatal.isDefined && leftResultFatal.get - def isRightFatal = rightResultFatal.isDefined && rightResultFatal.get + var leftResFatalCount: Int, + var rightResFatalCount: Int) extends Tree { + def isLeftFatal = leftResFatalCount > 0 + def isRightFatal = rightResFatalCount > 0 } \ No newline at end of file diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index e4696294..98ca1740 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -260,7 +260,7 @@ class DefaultMainVerifier(config: Config, program.methods.filterNot(excludeMethod).map(method => { val s = createInitialState(method, program, functionData, predicateData).copy(parallelizeBranches = - Verifier.config.parallelizeBranches(), branchTreeMap = Option(new BranchTreeMap())) /* [BRANCH-PARALLELISATION] */ + Verifier.config.parallelizeBranches(), branchTreeMap = Some(new BranchTreeMap())) /* [BRANCH-PARALLELISATION] */ _verificationPoolManager.queueVerificationTask(v => { val startTime = System.currentTimeMillis() @@ -268,7 +268,7 @@ class DefaultMainVerifier(config: Config, .flatMap(extractAllVerificationResults) val elapsed = System.currentTimeMillis() - startTime - val branchTree = s.branchTreeMap.get.get(method.name) + val branchTree = s.branchTreeMap.get.Map().get(method.name) if (branchTree.isDefined) { val branch = branchTree.get.asInstanceOf[Branch] if (branch.isLeftFatal || branch.isRightFatal) { @@ -278,7 +278,7 @@ class DefaultMainVerifier(config: Config, firstCond, AssertionFalseAtBranch( firstCond, - branchTree.get.prettyPrint(v.reportFurtherErrors()) + branchTree.get.prettyPrint() ), branch.isLeftFatal, branch.isRightFatal) diff --git a/src/test/resources/branchTreeTests/default/lastPathFails_expected b/src/test/resources/branchTreeTests/default/lastPathFails_expected index 4359f99a..1911a26b 100644 --- a/src/test/resources/branchTreeTests/default/lastPathFails_expected +++ b/src/test/resources/branchTreeTests/default/lastPathFails_expected @@ -1,11 +1,11 @@ │ ┌─┴─┐ T -│ a ├── Error +│ a ├── ✔ └─┬─┘ │F ┌─┴─┐ T -│ c ├── Error +│ c ├── ✔ └─┬─┘ │F Error \ No newline at end of file diff --git a/src/test/resources/branchTreeTests/default/multipleMethods_expected b/src/test/resources/branchTreeTests/default/multipleMethods_expected new file mode 100644 index 00000000..d02e358a --- /dev/null +++ b/src/test/resources/branchTreeTests/default/multipleMethods_expected @@ -0,0 +1,22 @@ + + │ + ┌─┴─┐ F + │ a ├──── ? + └─┬─┘ + │T +┌───┴───┐ F +│ bcde ├── ? +└───┬───┘ + │T + Error + + │ +┌─┴─┐ T +│ a ├── ✔ +└─┬─┘ + │F +┌─┴─┐ T +│ c ├── ✔ +└─┬─┘ + │F +Error 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/reportAllErrors/while_expected b/src/test/resources/branchTreeTests/reportAllErrors/while_expected index f25e2367..541f4c49 100644 --- a/src/test/resources/branchTreeTests/reportAllErrors/while_expected +++ b/src/test/resources/branchTreeTests/reportAllErrors/while_expected @@ -1,6 +1,7 @@ - ┌─┴─┐ - │ a │ - └─┬─┘ - F┌──┴┐T -Error ✔ + │ +┌─┴─┐ T +│ a ├── ? +└─┬─┘ + │F +Error \ No newline at end of file diff --git a/src/test/resources/branchTreeTests/reportTwoErrors/firstPathFails_expected b/src/test/resources/branchTreeTests/reportTwoErrors/firstPathFails_expected new file mode 100644 index 00000000..8852b966 --- /dev/null +++ b/src/test/resources/branchTreeTests/reportTwoErrors/firstPathFails_expected @@ -0,0 +1,10 @@ + +┌─┴─┐ +│ 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..5766e420 --- /dev/null +++ b/src/test/resources/branchTreeTests/reportTwoErrors/lastPathFails_expected @@ -0,0 +1,10 @@ + + ┌─┴─┐ + │ a │ + └─┬─┘ + F┌──┴────┐T + ┌─┴─┐ ┌───┴───┐ + │ c │ │ bcde │ + └─┬─┘ └───┬───┘ + F┌──┴┐T F┌┴┐T +Error ✔ ✔ ✔ \ No newline at end of file diff --git a/src/test/scala/BranchTreeTests.scala b/src/test/scala/BranchTreeTests.scala index 66b5a800..16dc1f2b 100644 --- a/src/test/scala/BranchTreeTests.scala +++ b/src/test/scala/BranchTreeTests.scala @@ -7,7 +7,7 @@ import org.scalatest.funsuite.AnyFunSuite import viper.silver.ast.utility.DiskLoader -import java.nio.file.{Paths} +import java.nio.file.Paths class BranchTreeTests extends AnyFunSuite { def executeTestDefault(fileName: String) : Unit = executeTest(fileName, "default") @@ -30,36 +30,50 @@ class BranchTreeTests extends AnyFunSuite { test("NoBranchesPath") { executeTestDefault("noBranches") } + test("MultipleMethodsPath") { + executeTestDefault("multipleMethods") + } def executeTestReportAllErrors(fileName: String) : Unit = executeTest(fileName, "reportAllErrors", List("--numberOfErrorsToReport", "0")) - test("FirstPathFailsTree") { + test("FirstPathFailsTreeAll") { executeTestReportAllErrors("firstPathFails") } - test("LastPathFailsTree") { + test("LastPathFailsTreeAll") { executeTestReportAllErrors("lastPathFails") } - test("WhileTree") { + test("WhileTreeAll") { executeTestReportAllErrors("while") } - test("OnlyIfTree") { + test("OnlyIfTreeAll") { executeTestReportAllErrors("onlyIf") } - test("AllPathsCorrectTree") { + test("AllPathsCorrectTreeAll") { executeTestReportAllErrors("allPathsCorrect") } - test("NoBranchesTree") { + test("NoBranchesTreeAll") { executeTestReportAllErrors("noBranches") } + def executeTestReportTwoErrors(fileName: String) : Unit = executeTest(fileName, "reportTwoErrors", List("--numberOfErrorsToReport", "2")) + + test("FirstPathFailsTree") { + executeTestReportTwoErrors("firstPathFails") + } + test("LastPathFailsTree") { + executeTestReportTwoErrors("lastPathFails") + } + def executeTest(fileName: String, expectedFolder : String, args: List[String] = List.empty) : Unit = { val expectedFile = getClass.getClassLoader.getResource(s"branchTreeTests/$expectedFolder/"+fileName+"_expected") val expected = DiskLoader.loadContent(Paths.get(expectedFile.toURI)).get val frontend = tests.instantiateFrontend(args) val program = tests.loadProgram("branchTreeTests/",fileName, frontend) - val actual = frontend.verifier.verify(program) - assert(actual.toString.contains(expected)) + 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)) } } From d093d43d66fee85495e298a6409411b2324cf592 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Wed, 26 Feb 2025 17:02:22 +0100 Subject: [PATCH 13/39] Revert changes to brancher --- src/main/scala/rules/Brancher.scala | 48 ++++++++++++++--------------- 1 file changed, 24 insertions(+), 24 deletions(-) diff --git a/src/main/scala/rules/Brancher.scala b/src/main/scala/rules/Brancher.scala index 8ea4c9b6..fc2422b4 100644 --- a/src/main/scala/rules/Brancher.scala +++ b/src/main/scala/rules/Brancher.scala @@ -28,7 +28,7 @@ trait BranchingRules extends SymbolicExecutionRules { fromShortCircuitingAnd: Boolean = false) (fTrue: (State, Verifier) => VerificationResult, fFalse: (State, Verifier) => VerificationResult) - : VerificationResult + : VerificationResult } object brancher extends BranchingRules { @@ -39,7 +39,7 @@ object brancher extends BranchingRules { fromShortCircuitingAnd: Boolean = false) (fThen: (State, Verifier) => VerificationResult, fElse: (State, Verifier) => VerificationResult) - : VerificationResult = { + : VerificationResult = { val negatedCondition = Not(condition) val negatedConditionExp = ast.Not(conditionExp._1)(pos = conditionExp._1.pos, info = conditionExp._1.info, ast.NoTrafos) @@ -51,29 +51,29 @@ object brancher extends BranchingRules { * (2) the branch condition contains a quantified variable */ val skipPathFeasibilityCheck = ( - fromShortCircuitingAnd - || ( s.quantifiedVariables.nonEmpty - && s.quantifiedVariables.map(_._1).exists(condition.freeVariables.contains)) - ) + fromShortCircuitingAnd + || ( s.quantifiedVariables.nonEmpty + && s.quantifiedVariables.map(_._1).exists(condition.freeVariables.contains)) + ) /* True if the then-branch is to be explored */ val executeThenBranch = ( - skipPathFeasibilityCheck - || !v.decider.check(negatedCondition, Verifier.config.checkTimeout())) + skipPathFeasibilityCheck + || !v.decider.check(negatedCondition, Verifier.config.checkTimeout())) /* False if the then-branch is to be explored */ val executeElseBranch = ( - !executeThenBranch /* Assumes that ast least one branch is feasible */ - || skipPathFeasibilityCheck - || !v.decider.check(condition, Verifier.config.checkTimeout())) + !executeThenBranch /* Assumes that ast least one branch is feasible */ + || skipPathFeasibilityCheck + || !v.decider.check(condition, Verifier.config.checkTimeout())) val parallelizeElseBranch = s.parallelizeBranches && executeThenBranch && executeElseBranch - // val additionalPaths = - // if (executeThenBranch && exploreFalseBranch) 1 - // else 0 +// val additionalPaths = +// if (executeThenBranch && exploreFalseBranch) 1 +// else 0 - // bookkeeper.branches += additionalPaths +// bookkeeper.branches += additionalPaths val cnt = v.counter(this).next() @@ -190,16 +190,16 @@ object brancher extends BranchingRules { val res = { val thenRes = if (executeThenBranch) { - v.symbExLog.markReachable(uidBranchPoint) - executionFlowController.locally(s, v)((s1, v1) => { - v1.decider.prover.comment(s"[then-branch: $cnt | $condition]") - v1.decider.setCurrentBranchCondition(condition, conditionExp) + v.symbExLog.markReachable(uidBranchPoint) + executionFlowController.locally(s, v)((s1, v1) => { + v1.decider.prover.comment(s"[then-branch: $cnt | $condition]") + v1.decider.setCurrentBranchCondition(condition, conditionExp) - fThen(v1.stateConsolidator(s1).consolidateOptionally(s1, v1), v1) - }) - } else { - Unreachable() - } + fThen(v1.stateConsolidator(s1).consolidateOptionally(s1, v1), v1) + }) + } else { + Unreachable() + } if (thenRes.isFatal && !thenRes.isReported && s.parallelizeBranches && s.isLastRetry) { thenRes.isReported = true v.reporter.report(BranchFailureMessage("silicon", s.currentMember.get.asInstanceOf[ast.Member with Serializable], From b82921fcd57e4ceef0dc55d19d66b164a8136e45 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Wed, 26 Feb 2025 17:05:45 +0100 Subject: [PATCH 14/39] Revert unwanted changes to consumer --- src/main/scala/rules/Consumer.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index c9ccfc97..200b7113 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -234,7 +234,7 @@ object consumer extends ConsumptionRules { v3.symbExLog.closeScope(uidCondExp) Q(s3, h1, t1, v3) }), - (s2, v2) => consumeR(s2, h, a2, pve, v2)((s3, h1, t1, v3) => { + (s2, v2) => consumeR(s2, h, a2, returnSnap, pve, v2)((s3, h1, t1, v3) => { v3.symbExLog.closeScope(uidCondExp) Q(s3, h1, t1, v3) }))) @@ -541,7 +541,7 @@ object consumer extends ConsumptionRules { private def consumeConditionalTlcMoreJoins(s: State, h: Heap, e0: ast.Exp, a1: ast.Exp, a2: Option[ast.Exp], scopeUid: Int, returnSnap: Boolean, pve: PartialVerificationError, v: Verifier) - (Q: (State, Heap, Term, Verifier) => VerificationResult) + (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) : VerificationResult = { eval(s, e0, pve, v)((s1, t0, e0New, v1) => joiner.join[(Heap, Option[Term]), (Heap, Option[Term])](s1, v1, resetState = false)((s1, v1, QB) => { From e1c04944256ebd8712d5db59f93c2e36efc19c68 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Wed, 26 Feb 2025 17:16:22 +0100 Subject: [PATCH 15/39] Revert unwanted changes to state --- src/main/scala/state/State.scala | 85 +++++++++++++++++--------------- 1 file changed, 45 insertions(+), 40 deletions(-) diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index d51b766f..42c8b5bc 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -64,7 +64,7 @@ final case class State(g: Store = Store(), exhaleExt: Boolean = false, ssCache: SsCache = Map.empty, - hackIssue387DisablePermissionConsumption: Boolean = false, + assertReadAccessOnly: Boolean = false, qpFields: InsertionOrderedSet[ast.Field] = InsertionOrderedSet.empty, qpPredicates: InsertionOrderedSet[ast.Predicate] = InsertionOrderedSet.empty, @@ -90,6 +90,11 @@ final case class State(g: Store = Store(), currentMember.isEmpty || currentMember.get.isInstanceOf[ast.Method] } + val mayAssumeUpperBounds: Boolean = { + currentMember.isEmpty || !currentMember.get.isInstanceOf[ast.Function] || +Verifier.config.respectFunctionPrePermAmounts() + } + val isLastRetry: Boolean = retryLevel == 0 def incCycleCounter(m: ast.Predicate) = @@ -103,8 +108,8 @@ final case class State(g: Store = Store(), val (ms, others) = visited.partition(_ == m) copy(visited = ms.tail ::: others) } - else - this + else + this def cycles(m: ast.Member) = visited.count(_ == m) @@ -131,8 +136,8 @@ final case class State(g: Store = Store(), def relevantQuantifiedVariables(filterPredicate: Var => Boolean): Seq[(Var, Option[ast.AbstractLocalVar])] = ( functionRecorderQuantifiedVariables() - ++ quantifiedVariables.filter(x => filterPredicate(x._1)) - ) + ++ quantifiedVariables.filter(x => filterPredicate(x._1)) + ) def relevantQuantifiedVariables(occurringIn: Seq[Term]): Seq[(Var, Option[ast.AbstractLocalVar])] = relevantQuantifiedVariables(x => occurringIn.exists(_.contains(x))) @@ -174,7 +179,7 @@ object State { partiallyConsumedHeap1, permissionScalingFactor1, permissionScalingFactorExp1, isEvalInOld, reserveHeaps1, reserveCfgs1, conservedPcs1, recordPcs1, exhaleExt1, - ssCache1, hackIssue387DisablePermissionConsumption1, + ssCache1, assertReadAccessOnly1, qpFields1, qpPredicates1, qpMagicWands1, permResources1, smCache1, pmCache1, smDomainNeeded1, predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers, moreCompleteExhale, moreJoins, @@ -200,7 +205,7 @@ object State { `partiallyConsumedHeap1`, `permissionScalingFactor1`, `permissionScalingFactorExp1`, `isEvalInOld`, `reserveHeaps1`, `reserveCfgs1`, conservedPcs2, `recordPcs1`, `exhaleExt1`, - ssCache2, `hackIssue387DisablePermissionConsumption1`, + ssCache2, `assertReadAccessOnly1`, `qpFields1`, `qpPredicates1`, `qpMagicWands1`, `permResources1`, smCache2, pmCache2, `smDomainNeeded1`, `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`, moreCompleteExhale2, `moreJoins`, @@ -224,15 +229,15 @@ object State { .map({ case (pcs1, pcs2) => (pcs1 ++ pcs2).distinct }) s1.copy(functionRecorder = functionRecorder3, - possibleTriggers = possibleTriggers3, - triggerExp = triggerExp3, - constrainableARPs = constrainableARPs3, - quantifiedVariables = quantifiedVariables3, - ssCache = ssCache3, - smCache = smCache3, - pmCache = pmCache3, - moreCompleteExhale = moreCompleteExhale3, - conservedPcs = conservedPcs3) + possibleTriggers = possibleTriggers3, + triggerExp = triggerExp3, + constrainableARPs = constrainableARPs3, + quantifiedVariables = quantifiedVariables3, + ssCache = ssCache3, + smCache = smCache3, + pmCache = pmCache3, + moreCompleteExhale = moreCompleteExhale3, + conservedPcs = conservedPcs3) case _ => val err = new StringBuilder() @@ -270,7 +275,7 @@ object State { private def mergeMaps[K, V, D](map1: Map[K, V], data1: D, map2: Map[K, V], data2: D) (fOnce: (V, D) => Option[V]) (fTwice: (V, D, V, D) => Option[V]) - : Map[K, V] = { + : Map[K, V] = { map1.flatMap({ case (k, v1) => (map2.get(k) match { @@ -332,7 +337,7 @@ object State { partiallyConsumedHeap1, permissionScalingFactor1, permissionScalingFactorExp1, isEvalInOld, reserveHeaps1, reserveCfgs1, conservedPcs1, recordPcs1, exhaleExt1, - ssCache1, hackIssue387DisablePermissionConsumption1, + ssCache1, assertReadAccessOnly1, qpFields1, qpPredicates1, qpMagicWands1, permResources1, smCache1, pmCache1, smDomainNeeded1, predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers, moreCompleteExhale, moreJoins, @@ -357,7 +362,7 @@ object State { partiallyConsumedHeap2, `permissionScalingFactor1`, `permissionScalingFactorExp1`, `isEvalInOld`, reserveHeaps2, `reserveCfgs1`, conservedPcs2, `recordPcs1`, `exhaleExt1`, - ssCache2, `hackIssue387DisablePermissionConsumption1`, + ssCache2, `assertReadAccessOnly1`, `qpFields1`, `qpPredicates1`, `qpMagicWands1`, `permResources1`, smCache2, pmCache2, smDomainNeeded2, `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`, moreCompleteExhale2, `moreJoins`, @@ -436,27 +441,27 @@ object State { val pmCache3 = pmCache1 ++ pmCache2 val s3 = s1.copy(functionRecorder = functionRecorder3, - possibleTriggers = possibleTriggers3, - triggerExp = triggerExp3, - constrainableARPs = constrainableARPs3, - ssCache = ssCache3, - smCache = smCache3, - pmCache = pmCache3, - g = g3, - h = h3, - oldHeaps = oldHeaps3, - partiallyConsumedHeap = partiallyConsumedHeap3, - smDomainNeeded = smDomainNeeded3, - invariantContexts = invariantContexts3, - reserveHeaps = reserveHeaps3, - conservedPcs = conservedPcs3) + possibleTriggers = possibleTriggers3, + triggerExp = triggerExp3, + constrainableARPs = constrainableARPs3, + ssCache = ssCache3, + smCache = smCache3, + pmCache = pmCache3, + g = g3, + h = h3, + oldHeaps = oldHeaps3, + partiallyConsumedHeap = partiallyConsumedHeap3, + smDomainNeeded = smDomainNeeded3, + invariantContexts = invariantContexts3, + reserveHeaps = reserveHeaps3, + conservedPcs = conservedPcs3) s3 - // Optionally, we could also do a state consolidation after each - // state merging, but this has shown to decrease performance a bit. - //val s4 = verifier.stateConsolidator.consolidate(s3, verifier) - //s4 + // Optionally, we could also do a state consolidation after each + // state merging, but this has shown to decrease performance a bit. + //val s4 = verifier.stateConsolidator.consolidate(s3, verifier) + //s4 case _ => { println("Error at new merge function:") @@ -468,9 +473,9 @@ object State { def preserveAfterLocalEvaluation(pre: State, post: State): State = { pre.copy(functionRecorder = post.functionRecorder, - possibleTriggers = post.possibleTriggers, - smCache = post.smCache, - constrainableARPs = post.constrainableARPs) + possibleTriggers = post.possibleTriggers, + smCache = post.smCache, + constrainableARPs = post.constrainableARPs) } def conflictFreeUnionOrAbort[K, V](m1: Map[K, V], m2: Map[K, V]): Map[K,V] = From 2c05828120c114645ad01f6eadcbc37389da3f9f Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Wed, 26 Feb 2025 17:18:55 +0100 Subject: [PATCH 16/39] Revert unwanted changes to state --- src/main/scala/state/State.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index 42c8b5bc..04c850e6 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -135,7 +135,7 @@ Verifier.config.respectFunctionPrePermAmounts() functionRecorder.data.fold(Seq.empty[(Var, Option[ast.AbstractLocalVar])])(d => d.arguments.zip(d.argumentExps)) def relevantQuantifiedVariables(filterPredicate: Var => Boolean): Seq[(Var, Option[ast.AbstractLocalVar])] = ( - functionRecorderQuantifiedVariables() + functionRecorderQuantifiedVariables() ++ quantifiedVariables.filter(x => filterPredicate(x._1)) ) @@ -248,7 +248,7 @@ object State { err ++= s"\n- Field index ${s1.productElementName(ix)} not equal." } } - sys.error(s"State merging failed: unexpected mismatch between symbolic states: $err") + sys.error(s"State merging failed: unexpected mismatch between symbolic states: $err") } } } From 23682f98dc88d143f9c207ba316d1367e558ad8a Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Wed, 26 Feb 2025 17:20:29 +0100 Subject: [PATCH 17/39] Revert unwanted changes to state --- src/main/scala/state/State.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index 04c850e6..95f0762e 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -249,7 +249,7 @@ object State { } } sys.error(s"State merging failed: unexpected mismatch between symbolic states: $err") - } + } } } From 7a468dee7a9fd24a5012b56fbd194cbbb52a9191 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Wed, 26 Feb 2025 17:24:47 +0100 Subject: [PATCH 18/39] Revert unwanted changes to DefaultMainVerifier --- .../scala/verifier/DefaultMainVerifier.scala | 48 +++++++++---------- 1 file changed, 24 insertions(+), 24 deletions(-) diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index 98ca1740..7eaca9c6 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -317,8 +317,8 @@ class DefaultMainVerifier(config: Config, reporter report VerificationTerminationMessage() val verificationResults = ( functionVerificationResults - ++ predicateVerificationResults - ++ methodVerificationResults) + ++ predicateVerificationResults + ++ methodVerificationResults) if (Verifier.config.enableDebugging()){ val debugger = new SiliconDebugger(verificationResults, identifierFactory, reporter, FrontendStateCache.resolver, FrontendStateCache.pprogram, FrontendStateCache.translator, this) @@ -328,7 +328,7 @@ class DefaultMainVerifier(config: Config, verificationResults } - private def createInitialState(member: ast.Member, + private def createInitialState(member: ast.Member, program: ast.Program, functionData: Map[ast.Function, FunctionData], predicateData: Map[ast.Predicate, PredicateData]): State = { @@ -412,18 +412,18 @@ class DefaultMainVerifier(config: Config, } else InsertionOrderedSet.empty State(program = program, - functionData = functionData, - predicateData = predicateData, - qpFields = quantifiedFields, - qpPredicates = quantifiedPredicates, - qpMagicWands = quantifiedMagicWands, - permLocations = permResources, - predicateSnapMap = predSnapGenerator.snapMap, - predicateFormalVarMap = predSnapGenerator.formalVarMap, - currentMember = Some(member), - heapDependentTriggers = resourceTriggers, - moreCompleteExhale = mce, - moreJoins = moreJoins) + functionData = functionData, + predicateData = predicateData, + qpFields = quantifiedFields, + qpPredicates = quantifiedPredicates, + qpMagicWands = quantifiedMagicWands, + permLocations = permResources, + predicateSnapMap = predSnapGenerator.snapMap, + predicateFormalVarMap = predSnapGenerator.formalVarMap, + currentMember = Some(member), + heapDependentTriggers = resourceTriggers, + moreCompleteExhale = mce, + moreJoins = moreJoins) } private def createInitialState(@unused cfg: SilverCfg, @@ -449,8 +449,8 @@ class DefaultMainVerifier(config: Config, } private def excludeMethod(method: ast.Method) = ( - !method.name.matches(config.includeMethods()) - || method.name.matches(config.excludeMethods())) + !method.name.matches(config.includeMethods()) + || method.name.matches(config.excludeMethods())) /* Prover preamble: Static preamble */ @@ -620,13 +620,13 @@ class DefaultMainVerifier(config: Config, preambleReader.emitParametricPreamble("/sortwrappers.smt2", Map("$T$" -> s"$$T$i$$", - "$S$" -> sanitizedSortString, - s"$$T$i$$" -> sortString), + "$S$" -> sanitizedSortString, + s"$$T$i$$" -> sortString), sink) } else { preambleReader.emitParametricPreamble("/sortwrappers.smt2", Map("$S$" -> sanitizedSortString, - "$T$" -> sortString), + "$T$" -> sortString), sink) } @@ -643,10 +643,10 @@ class DefaultMainVerifier(config: Config, } /** - * In case Silicon encounters an expected error (i.e. `ErrorMessage.isExpected`), Silicon continues (until at most - * config.numberOfErrorsToReport() have been encountered (per member)). - * This function combines the verification result with verification results stored in its `previous` field. - */ + * In case Silicon encounters an expected error (i.e. `ErrorMessage.isExpected`), Silicon continues (until at most + * config.numberOfErrorsToReport() have been encountered (per member)). + * This function combines the verification result with verification results stored in its `previous` field. + */ private def extractAllVerificationResults(res: VerificationResult): Seq[VerificationResult] = res :: res.previous.toList } \ No newline at end of file From 28a6cc0db5a946d93dc687de669b155a62021e0d Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Wed, 26 Feb 2025 17:26:05 +0100 Subject: [PATCH 19/39] Revert unwanted changes to State --- src/main/scala/state/State.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index 95f0762e..c46dcb46 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -248,7 +248,7 @@ object State { err ++= s"\n- Field index ${s1.productElementName(ix)} not equal." } } - sys.error(s"State merging failed: unexpected mismatch between symbolic states: $err") + sys.error(s"State merging failed: unexpected mismatch between symbolic states: $err") } } } From 7d3b6f1d1f11c6982f1aa7b33e0288680add9820 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Fri, 28 Feb 2025 22:36:59 +0100 Subject: [PATCH 20/39] Collect all failures --- src/main/scala/rules/Consumer.scala | 12 +----------- src/main/scala/rules/SymbolicExecutionRules.scala | 3 ++- src/main/scala/state/State.scala | 9 +++++++++ 3 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index 200b7113..ceca9c63 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -589,15 +589,6 @@ object consumer extends ConsumptionRules { ) } - private def storeIntoBranchTree(v: Verifier, s: State, r: VerificationResult) = { - if (s.branchTreeMap.isDefined && s.currentMember.isDefined){ - val branchConditions = v.decider.pcs.getBranchConditionsExp() - if (branchConditions.length > 0) { - s.branchTreeMap.get.storeIntoTree(s.currentMember.get.name, branchConditions, r.isFatal) - } - } - } - private def evalAndAssert(s: State, e: ast.Exp, returnSnap: Boolean, pve: PartialVerificationError, v: Verifier) (Q: (State, Option[Term], Verifier) => VerificationResult) : VerificationResult = { @@ -629,11 +620,10 @@ object consumer extends ConsumptionRules { case true => v2.decider.assume(t, Option.when(withExp)(e), eNew) val r = QS(s3, v2) - storeIntoBranchTree(v,s,r) + s.storeIntoTree(v.decider.pcs.getBranchConditionsExp(),false) r case false => val failure = createFailure(pve dueTo AssertionFalse(e), v2, s3, termToAssert, eNew) - storeIntoBranchTree(v,s,failure) if (s3.retryLevel == 0 && v2.reportFurtherErrors()){ v2.decider.assume(t, Option.when(withExp)(e), eNew) failure combine QS(s3, v2) diff --git a/src/main/scala/rules/SymbolicExecutionRules.scala b/src/main/scala/rules/SymbolicExecutionRules.scala index eb3873ab..ec6877ad 100644 --- a/src/main/scala/rules/SymbolicExecutionRules.scala +++ b/src/main/scala/rules/SymbolicExecutionRules.scala @@ -8,7 +8,7 @@ package viper.silicon.rules import viper.silicon.debugger.DebugExp import viper.silicon.interfaces.{Failure, SiliconDebuggingFailureContext, SiliconFailureContext, SiliconMappedCounterexample, SiliconNativeCounterexample, SiliconVariableCounterexample} -import viper.silicon.state.State +import viper.silicon.state.{State} import viper.silicon.state.terms.{False, Term} import viper.silicon.verifier.Verifier import viper.silver.ast @@ -87,6 +87,7 @@ trait SymbolicExecutionRules { val branchconditions = if (Verifier.config.enableBranchconditionReporting()) { v.decider.pcs.getBranchConditionsExp() } else Seq() + s.storeIntoTree(branchconditions, true) if (Verifier.config.enableDebugging()){ val assumptions = v.decider.pcs.assumptionExps diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index c46dcb46..fb21f39c 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -23,6 +23,7 @@ import viper.silicon.supporters.functions.{FunctionData, FunctionRecorder, NoopF import viper.silicon.utils.ast.BigAnd import viper.silicon.verifier.Verifier import viper.silicon.{Map, Stack} +import viper.silver.ast.Exp import viper.silver.utility.Sanitizer final case class State(g: Store = Store(), @@ -151,6 +152,14 @@ Verifier.config.respectFunctionPrePermAmounts() lazy val relevantQuantifiedVariables: Seq[(Var, Option[ast.AbstractLocalVar])] = relevantQuantifiedVariables(_ => true) + def storeIntoTree(branchConditions: Seq[Exp], isResultFatal: Boolean) = { + if (this.branchTreeMap.isDefined && this.currentMember.isDefined){ + if (branchConditions.length > 0) { + this.branchTreeMap.get.storeIntoTree(this.currentMember.get.name, branchConditions, isResultFatal) + } + } + } + override val toString = s"${this.getClass.getSimpleName}(...)" } From f41d8588d94dcdbb8f16dc2e14b31d18ef758825 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Sun, 2 Mar 2025 17:02:35 +0100 Subject: [PATCH 21/39] Change size check --- src/main/scala/state/State.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index fb21f39c..4ed61665 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -154,7 +154,7 @@ Verifier.config.respectFunctionPrePermAmounts() def storeIntoTree(branchConditions: Seq[Exp], isResultFatal: Boolean) = { if (this.branchTreeMap.isDefined && this.currentMember.isDefined){ - if (branchConditions.length > 0) { + if (branchConditions.nonEmpty) { this.branchTreeMap.get.storeIntoTree(this.currentMember.get.name, branchConditions, isResultFatal) } } From 326c5e5c422bcc98f2f33a060efcfc8034050ec8 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Sun, 2 Mar 2025 21:15:07 +0100 Subject: [PATCH 22/39] Remove braces --- src/main/scala/state/BranchTree.scala | 2 +- src/main/scala/verifier/DefaultMainVerifier.scala | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/scala/state/BranchTree.scala b/src/main/scala/state/BranchTree.scala index 86f1c719..c4522f57 100644 --- a/src/main/scala/state/BranchTree.scala +++ b/src/main/scala/state/BranchTree.scala @@ -8,7 +8,7 @@ import scala.collection.mutable class BranchTreeMap { private val map : mutable.Map[String, Tree] = new mutable.HashMap[String,Tree]() - def Map(): mutable.Map[String, Tree] = map + def Map: mutable.Map[String, Tree] = map def storeIntoTree(method: String, branchConditions : Seq[Exp], isResultFatal: Boolean): Unit = { val branchTree = map.get(method) diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index 7eaca9c6..3312894c 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -268,7 +268,7 @@ class DefaultMainVerifier(config: Config, .flatMap(extractAllVerificationResults) val elapsed = System.currentTimeMillis() - startTime - val branchTree = s.branchTreeMap.get.Map().get(method.name) + val branchTree = s.branchTreeMap.get.Map.get(method.name) if (branchTree.isDefined) { val branch = branchTree.get.asInstanceOf[Branch] if (branch.isLeftFatal || branch.isRightFatal) { From bfe81d39f8820dcdd5d47be99e479814370829e5 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Sun, 2 Mar 2025 21:24:49 +0100 Subject: [PATCH 23/39] Fix --- src/main/scala/state/BranchTree.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/state/BranchTree.scala b/src/main/scala/state/BranchTree.scala index c4522f57..e5ef06fe 100644 --- a/src/main/scala/state/BranchTree.scala +++ b/src/main/scala/state/BranchTree.scala @@ -193,7 +193,7 @@ class Tree { def getErrorCount(): Int = { this match { - case Branch(_,_,_,lf,rf) => lf + rf + case Branch(_,_,_,lf,rf) => Math.max(lf,0) + Math.max(rf,0) case _ => 0 } } From c461458de6e3dd91600c47144a2f69caeafd7358 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Sun, 2 Mar 2025 23:15:17 +0100 Subject: [PATCH 24/39] Renaming --- src/main/scala/verifier/DefaultMainVerifier.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index 3312894c..724e6102 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -37,7 +37,7 @@ import viper.silver.frontend.FrontendStateCache import viper.silver.reporter._ import viper.silver.verifier.VerifierWarning import viper.silver.verifier.errors.PostconditionViolatedBranch -import viper.silver.verifier.reasons.AssertionFalseAtBranch +import viper.silver.verifier.reasons.BranchFailure /* TODO: Extract a suitable MainVerifier interface, probably including * - def verificationPoolManager: VerificationPoolManager) @@ -276,7 +276,7 @@ class DefaultMainVerifier(config: Config, results +:= Failure( PostconditionViolatedBranch( firstCond, - AssertionFalseAtBranch( + BranchFailure( firstCond, branchTree.get.prettyPrint() ), From 63898f1a10b3bf46ee72a84140efc1184245339e Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Mon, 3 Mar 2025 22:44:31 +0100 Subject: [PATCH 25/39] Clean up --- .../scala/rules/SymbolicExecutionRules.scala | 10 +++--- src/main/scala/state/BranchTree.scala | 12 +++---- src/main/scala/state/State.scala | 14 +++----- .../scala/supporters/MethodSupporter.scala | 21 ++++++++++-- .../default/multipleMethods_expected | 3 +- src/test/scala/BranchTreeTests.scala | 32 +++++++++++++++---- src/test/scala/tests.scala | 3 +- 7 files changed, 63 insertions(+), 32 deletions(-) diff --git a/src/main/scala/rules/SymbolicExecutionRules.scala b/src/main/scala/rules/SymbolicExecutionRules.scala index ec6877ad..ba76c203 100644 --- a/src/main/scala/rules/SymbolicExecutionRules.scala +++ b/src/main/scala/rules/SymbolicExecutionRules.scala @@ -84,10 +84,8 @@ trait SymbolicExecutionRules { None } - val branchconditions = if (Verifier.config.enableBranchconditionReporting()) { - v.decider.pcs.getBranchConditionsExp() - } else Seq() - s.storeIntoTree(branchconditions, true) + val branchConditions = v.decider.pcs.getBranchConditionsExp() + s.storeIntoTree(branchConditions, true) if (Verifier.config.enableDebugging()){ val assumptions = v.decider.pcs.assumptionExps @@ -95,10 +93,10 @@ 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()) - } } diff --git a/src/main/scala/state/BranchTree.scala b/src/main/scala/state/BranchTree.scala index e5ef06fe..37b4fd40 100644 --- a/src/main/scala/state/BranchTree.scala +++ b/src/main/scala/state/BranchTree.scala @@ -8,7 +8,7 @@ import scala.collection.mutable class BranchTreeMap { private val map : mutable.Map[String, Tree] = new mutable.HashMap[String,Tree]() - def Map: mutable.Map[String, Tree] = map + def Map : mutable.Map[String, Tree] = map def storeIntoTree(method: String, branchConditions : Seq[Exp], isResultFatal: Boolean): Unit = { val branchTree = map.get(method) @@ -73,10 +73,10 @@ class Tree { private def recurse(tree: Tree, fatalCount: Int) : (Vector[String], Int, Int) = { tree match { - case Leaf if fatalCount == -1 => (Vector("✔"), 0, 0) - case Leaf if fatalCount > 0 => (Vector("Error"), 2, 2) // ✘ - case _ : Branch => tree.buildTree() - case _ => (Vector("?"), 0, 0) + case Leaf if fatalCount == -1 => (Vector("✔"), 0, 0) + case Leaf if fatalCount > 0 => (Vector("Error"), 2, 2) // ✘ + case _ : Branch => tree.buildTree() + case _ => (Vector("?"), 0, 0) } } @@ -147,7 +147,7 @@ class Tree { " "*filler + elems(2) + " "*filler, " "*filler + elems(3) + " "*filler ) - }).toVector + }).toVector } private def printSinglePath() : String = { diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index 4ed61665..e05406dc 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -17,7 +17,7 @@ import viper.silicon.interfaces.state.GeneralChunk import viper.silicon.state.State.OldHeaps import viper.silicon.state.terms.{Term, Var} import viper.silicon.interfaces.state.Chunk -import viper.silicon.state.terms.{And, Ite, NoPerm} +import viper.silicon.state.terms.{And, Ite} import viper.silicon.supporters.PredicateData import viper.silicon.supporters.functions.{FunctionData, FunctionRecorder, NoopFunctionRecorder} import viper.silicon.utils.ast.BigAnd @@ -191,8 +191,7 @@ object State { ssCache1, assertReadAccessOnly1, qpFields1, qpPredicates1, qpMagicWands1, permResources1, smCache1, pmCache1, smDomainNeeded1, predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers, - moreCompleteExhale, moreJoins, - branchTreeMap) => + moreCompleteExhale, moreJoins, branchTreeMap) => /* Decompose state s2: most values must match those of s1 */ s2 match { @@ -217,8 +216,7 @@ object State { ssCache2, `assertReadAccessOnly1`, `qpFields1`, `qpPredicates1`, `qpMagicWands1`, `permResources1`, smCache2, pmCache2, `smDomainNeeded1`, `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`, - moreCompleteExhale2, `moreJoins`, - `branchTreeMap`) => + moreCompleteExhale2, `moreJoins`, `branchTreeMap`) => val functionRecorder3 = functionRecorder1.merge(functionRecorder2) val triggerExp3 = triggerExp1 && triggerExp2 @@ -349,8 +347,7 @@ object State { ssCache1, assertReadAccessOnly1, qpFields1, qpPredicates1, qpMagicWands1, permResources1, smCache1, pmCache1, smDomainNeeded1, predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers, - moreCompleteExhale, moreJoins, - branchTreeMap) => + moreCompleteExhale, moreJoins, branchTreeMap) => /* Decompose state s2: most values must match those of s1 */ s2 match { @@ -374,8 +371,7 @@ object State { ssCache2, `assertReadAccessOnly1`, `qpFields1`, `qpPredicates1`, `qpMagicWands1`, `permResources1`, smCache2, pmCache2, smDomainNeeded2, `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`, - moreCompleteExhale2, `moreJoins`, - `branchTreeMap`) => + moreCompleteExhale2, `moreJoins`, `branchTreeMap`) => val functionRecorder3 = functionRecorder1.merge(functionRecorder2) val triggerExp3 = triggerExp1 && triggerExp2 diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index 9b483ff4..8588fdc0 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/src/main/scala/supporters/MethodSupporter.scala @@ -14,11 +14,11 @@ import viper.silicon.interfaces._ import viper.silicon.decider.Decider import viper.silicon.logger.records.data.WellformednessCheckRecord import viper.silicon.rules.{consumer, executionFlowController, executor, producer} -import viper.silicon.state.{Heap, State, Store} +import viper.silicon.state.{Branch, BranchTreeMap, Heap, State, Store} import viper.silicon.state.State.OldHeaps import viper.silicon.verifier.{Verifier, VerifierComponent} import viper.silicon.utils.freshSnap -import viper.silver.reporter.AnnotationWarning +import viper.silver.reporter.{AnnotationWarning, BeamInfo, BranchTreeReport} import viper.silicon.{Map, toMap} /* TODO: Consider changing the DefaultMethodVerificationUnitProvider into a SymbolicExecutionRule */ @@ -84,7 +84,8 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif val s = sInit.copy(g = g, h = Heap(), oldHeaps = OldHeaps(), - methodCfg = body) + methodCfg = body, + branchTreeMap = Some(new BranchTreeMap())) if (Verifier.config.printMethodCFGs()) { viper.silicon.common.io.toFile( @@ -117,6 +118,20 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif v.decider.resetProverOptions() symbExLog.closeMemberScope() + + s.branchTreeMap.get.Map.get(method.name).foreach( + branchTree => { + val branch = branchTree.asInstanceOf[Branch] + if (branch.getErrorCount() > 0) { + v.reporter.report( + BranchTreeReport(s.currentMember.get.asInstanceOf[ast.Method], + s"Branch fails.\n${branchTree.prettyPrint()}", + Seq(BeamInfo(branch.exp, branch.isLeftFatal, branch.isRightFatal)) + )) + } + } + ) + Seq(result) } diff --git a/src/test/resources/branchTreeTests/default/multipleMethods_expected b/src/test/resources/branchTreeTests/default/multipleMethods_expected index d02e358a..6b25ad25 100644 --- a/src/test/resources/branchTreeTests/default/multipleMethods_expected +++ b/src/test/resources/branchTreeTests/default/multipleMethods_expected @@ -1,4 +1,4 @@ - +Branch fails. │ ┌─┴─┐ F │ a ├──── ? @@ -10,6 +10,7 @@ │T Error +Branch fails. │ ┌─┴─┐ T │ a ├── ✔ diff --git a/src/test/scala/BranchTreeTests.scala b/src/test/scala/BranchTreeTests.scala index 16dc1f2b..f06441e2 100644 --- a/src/test/scala/BranchTreeTests.scala +++ b/src/test/scala/BranchTreeTests.scala @@ -6,9 +6,23 @@ import org.scalatest.funsuite.AnyFunSuite import viper.silver.ast.utility.DiskLoader +import viper.silver.reporter.{BranchTreeReport, Message, Reporter} import java.nio.file.Paths +class DummyReporter extends Reporter { + val name: String = "DummyReporter" + var breports: Set[String] = Set() + def getBranchTreeMessage = if (breports.nonEmpty) breports.mkString("\n") + else "Verification successful." + def report(msg: Message): Unit = { + msg match { + case m : BranchTreeReport => this.breports += m.tree + case _ => + } + } +} + class BranchTreeTests extends AnyFunSuite { def executeTestDefault(fileName: String) : Unit = executeTest(fileName, "default") @@ -64,15 +78,21 @@ class BranchTreeTests extends AnyFunSuite { 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 expectedFile = getClass.getClassLoader.getResource(s"branchTreeTests/$expectedFolder/"+fileName+"_expected") - val expected = DiskLoader.loadContent(Paths.get(expectedFile.toURI)).get - val frontend = tests.instantiateFrontend(args) + val expected = getExpectedString(fileName, expectedFolder) + + val dummyReporter = new DummyReporter() + val frontend = tests.instantiateFrontend(args, Some(dummyReporter)) 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) + frontend.verifier.verify(program) + + val actual = dummyReporter.getBranchTreeMessage assert(actual.contains(expected)) } } diff --git a/src/test/scala/tests.scala b/src/test/scala/tests.scala index 35197277..3b432a34 100644 --- a/src/test/scala/tests.scala +++ b/src/test/scala/tests.scala @@ -9,6 +9,7 @@ import viper.silver.ast.Program import viper.silver.frontend.{DefaultStates, SilFrontend, SilFrontendConfig} import viper.silver.verifier.{AbstractError, AbstractVerificationError, VerificationResult, Verifier, Failure => SilFailure} import viper.silicon.Silicon +import viper.silver.reporter.Reporter package object tests { class DummyFrontend extends SilFrontend { @@ -34,7 +35,7 @@ package object tests { override def verifier: Verifier = this._verifier.get } - def instantiateFrontend(args: List[String] = List.empty): SilFrontend = { + def instantiateFrontend(args: List[String] = List.empty, reporter : Option[Reporter] = None): SilFrontend = { val frontend = new DummyFrontend val backend = new Silicon(List("startedBy" -> s"Unit test ${this.getClass.getSimpleName}")) From 01f7bf17971d551d90ae531919943c16f8c35882 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Tue, 4 Mar 2025 13:07:28 +0100 Subject: [PATCH 26/39] Dot representation + report whole tree --- src/main/scala/state/BranchTree.scala | 72 ++++++++++++++++++- .../scala/supporters/MethodSupporter.scala | 2 +- .../default/firstPathFails_expected | 3 +- .../default/lastPathFails_expected | 3 +- .../default/multipleMethods_expected | 2 - .../branchTreeTests/default/onlyIf_expected | 3 +- .../branchTreeTests/default/while_expected | 3 +- .../reportAllErrors/firstPathFails_expected | 1 - .../reportAllErrors/lastPathFails_expected | 3 +- .../reportAllErrors/onlyIf_expected | 1 - .../reportAllErrors/while_expected | 3 +- .../reportTwoErrors/firstPathFails_expected | 1 - .../reportTwoErrors/lastPathFails_expected | 3 +- src/test/scala/BranchTreeTests.scala | 2 +- 14 files changed, 80 insertions(+), 22 deletions(-) diff --git a/src/main/scala/state/BranchTree.scala b/src/main/scala/state/BranchTree.scala index 37b4fd40..ba26c013 100644 --- a/src/main/scala/state/BranchTree.scala +++ b/src/main/scala/state/BranchTree.scala @@ -1,8 +1,10 @@ package viper.silicon.state +import viper.silicon.common.io.PrintWriter import viper.silicon.verifier.Verifier import viper.silver.ast import viper.silver.ast.Exp +import viper.silver.reporter.BranchTree import scala.collection.mutable @@ -20,7 +22,7 @@ class BranchTreeMap { } } -class Tree { +class Tree extends BranchTree { private def incrementIfFatal(currBranchResultFatal: Int, isResultFatal: Boolean) : Int = if (isResultFatal) Math.max(currBranchResultFatal,0)+1 else currBranchResultFatal @@ -205,9 +207,77 @@ class Tree { this.buildTree()._1.reduce((str, s) => str + "\n" + s) + "\n" } } + + /*digraph { + a -> b[label="0.2"]; + a -> c[label="0.4",weight="0.4"]; + c -> b[label="0.6",weight="0.6"]; + c -> e[label="0.6",weight="0.6"]; + e -> e[label="0.1",weight="0.1"]; + e -> b[label="0.7",weight="0.7"]; + }*/ + protected 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\"" + } + } + + protected 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 visitedCountLeft = left match { + case b1 : Branch => + val newVisitedCount = visitedCount + 1 + val leftBranchIdn = s"B$newVisitedCount" + val visitedCountLeft_ = b1.writeDotFileRec(writer, newVisitedCount) + writer.write(s" $parentIdn -> $leftBranchIdn[label=\"F\"];\n") + visitedCountLeft_ + case Leaf => + val newVisitedCount = visitedCount + 1 + val leftLeafIdn = s"B$newVisitedCount" + writer.write(s" $leftLeafIdn[${leafToDotNodeContent(leftResFatalCount)}];\n") + writer.write(s" $parentIdn -> $leftLeafIdn [label=\"F\"];\n") + newVisitedCount + } + val visitedCountRight = right match { + case b2 : Branch => + val newVisitedCount = visitedCountLeft + 1 + val rightBranchIdn = s"B$newVisitedCount" + val visitedCountRight_ = b2.writeDotFileRec(writer, newVisitedCount) + writer.write(s" $parentIdn -> $rightBranchIdn[label=\"T\"];\n") + visitedCountRight_ + case Leaf => + val newVisitedCount = visitedCountLeft + 1 + val rightLeafIdn = s"B$newVisitedCount" + writer.write(s" $rightLeafIdn[${leafToDotNodeContent(rightResFatalCount)}];\n") + writer.write(s" $parentIdn -> $rightLeafIdn [label=\"T\"];\n") + newVisitedCount + } + visitedCountRight + case _ => 0 + } + } + def toDotFile(): Unit = { + println("TEST TEST TEST TEST TEST") + println(Tree.DotFilePath) + val writer = PrintWriter(new java.io.File(Tree.DotFilePath),true) + writer.write("digraph {\n") + this.writeDotFileRec(writer) + writer.write("}\n") + writer.close() + /*viper.silicon.common.io.toFile( + dotString, + new java.io.File(Tree.DotFilePath))*/ + } } object Tree { + val DotFilePath = s"${Verifier.config.tempDirectory()}/BranchTree.dot" + private def generate(expressions : Seq[Exp], errorCount: Int) : Tree = { expressions.length match { case 0 => Leaf diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index 8588fdc0..a6ba24eb 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/src/main/scala/supporters/MethodSupporter.scala @@ -125,7 +125,7 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif if (branch.getErrorCount() > 0) { v.reporter.report( BranchTreeReport(s.currentMember.get.asInstanceOf[ast.Method], - s"Branch fails.\n${branchTree.prettyPrint()}", + branchTree, Seq(BeamInfo(branch.exp, branch.isLeftFatal, branch.isRightFatal)) )) } diff --git a/src/test/resources/branchTreeTests/default/firstPathFails_expected b/src/test/resources/branchTreeTests/default/firstPathFails_expected index 2607b87a..118145ee 100644 --- a/src/test/resources/branchTreeTests/default/firstPathFails_expected +++ b/src/test/resources/branchTreeTests/default/firstPathFails_expected @@ -1,4 +1,3 @@ - │ ┌─┴─┐ F │ a ├──── ? @@ -8,4 +7,4 @@ │ bcde ├── ? └───┬───┘ │T - Error \ No newline at end of file + Error diff --git a/src/test/resources/branchTreeTests/default/lastPathFails_expected b/src/test/resources/branchTreeTests/default/lastPathFails_expected index 1911a26b..abf6886c 100644 --- a/src/test/resources/branchTreeTests/default/lastPathFails_expected +++ b/src/test/resources/branchTreeTests/default/lastPathFails_expected @@ -1,4 +1,3 @@ - │ ┌─┴─┐ T │ a ├── ✔ @@ -8,4 +7,4 @@ │ c ├── ✔ └─┬─┘ │F -Error \ No newline at end of file +Error diff --git a/src/test/resources/branchTreeTests/default/multipleMethods_expected b/src/test/resources/branchTreeTests/default/multipleMethods_expected index 6b25ad25..360dffef 100644 --- a/src/test/resources/branchTreeTests/default/multipleMethods_expected +++ b/src/test/resources/branchTreeTests/default/multipleMethods_expected @@ -1,4 +1,3 @@ -Branch fails. │ ┌─┴─┐ F │ a ├──── ? @@ -10,7 +9,6 @@ Branch fails. │T Error -Branch fails. │ ┌─┴─┐ T │ a ├── ✔ diff --git a/src/test/resources/branchTreeTests/default/onlyIf_expected b/src/test/resources/branchTreeTests/default/onlyIf_expected index f7567aa6..2035a798 100644 --- a/src/test/resources/branchTreeTests/default/onlyIf_expected +++ b/src/test/resources/branchTreeTests/default/onlyIf_expected @@ -1,7 +1,6 @@ - │ ┌─┴─┐ F │ d ├── ? └─┬─┘ │T -Error \ No newline at end of file +Error diff --git a/src/test/resources/branchTreeTests/default/while_expected b/src/test/resources/branchTreeTests/default/while_expected index 541f4c49..3b4a031d 100644 --- a/src/test/resources/branchTreeTests/default/while_expected +++ b/src/test/resources/branchTreeTests/default/while_expected @@ -1,7 +1,6 @@ - │ ┌─┴─┐ T │ a ├── ? └─┬─┘ │F -Error \ No newline at end of file +Error diff --git a/src/test/resources/branchTreeTests/reportAllErrors/firstPathFails_expected b/src/test/resources/branchTreeTests/reportAllErrors/firstPathFails_expected index a590cb67..ef79e48e 100644 --- a/src/test/resources/branchTreeTests/reportAllErrors/firstPathFails_expected +++ b/src/test/resources/branchTreeTests/reportAllErrors/firstPathFails_expected @@ -1,4 +1,3 @@ - ┌─┴─┐ │ a │ └─┬─┘ diff --git a/src/test/resources/branchTreeTests/reportAllErrors/lastPathFails_expected b/src/test/resources/branchTreeTests/reportAllErrors/lastPathFails_expected index 5766e420..d12eb8ef 100644 --- a/src/test/resources/branchTreeTests/reportAllErrors/lastPathFails_expected +++ b/src/test/resources/branchTreeTests/reportAllErrors/lastPathFails_expected @@ -1,4 +1,3 @@ - ┌─┴─┐ │ a │ └─┬─┘ @@ -7,4 +6,4 @@ │ c │ │ bcde │ └─┬─┘ └───┬───┘ F┌──┴┐T F┌┴┐T -Error ✔ ✔ ✔ \ No newline at end of file +Error ✔ ✔ ✔ diff --git a/src/test/resources/branchTreeTests/reportAllErrors/onlyIf_expected b/src/test/resources/branchTreeTests/reportAllErrors/onlyIf_expected index da3d2a15..b43faf03 100644 --- a/src/test/resources/branchTreeTests/reportAllErrors/onlyIf_expected +++ b/src/test/resources/branchTreeTests/reportAllErrors/onlyIf_expected @@ -1,4 +1,3 @@ - ┌─┴─┐ │ d │ └─┬─┘ diff --git a/src/test/resources/branchTreeTests/reportAllErrors/while_expected b/src/test/resources/branchTreeTests/reportAllErrors/while_expected index 541f4c49..3b4a031d 100644 --- a/src/test/resources/branchTreeTests/reportAllErrors/while_expected +++ b/src/test/resources/branchTreeTests/reportAllErrors/while_expected @@ -1,7 +1,6 @@ - │ ┌─┴─┐ T │ a ├── ? └─┬─┘ │F -Error \ No newline at end of file +Error diff --git a/src/test/resources/branchTreeTests/reportTwoErrors/firstPathFails_expected b/src/test/resources/branchTreeTests/reportTwoErrors/firstPathFails_expected index 8852b966..4e978087 100644 --- a/src/test/resources/branchTreeTests/reportTwoErrors/firstPathFails_expected +++ b/src/test/resources/branchTreeTests/reportTwoErrors/firstPathFails_expected @@ -1,4 +1,3 @@ - ┌─┴─┐ │ a │ └─┬─┘ diff --git a/src/test/resources/branchTreeTests/reportTwoErrors/lastPathFails_expected b/src/test/resources/branchTreeTests/reportTwoErrors/lastPathFails_expected index 5766e420..d12eb8ef 100644 --- a/src/test/resources/branchTreeTests/reportTwoErrors/lastPathFails_expected +++ b/src/test/resources/branchTreeTests/reportTwoErrors/lastPathFails_expected @@ -1,4 +1,3 @@ - ┌─┴─┐ │ a │ └─┬─┘ @@ -7,4 +6,4 @@ │ c │ │ bcde │ └─┬─┘ └───┬───┘ F┌──┴┐T F┌┴┐T -Error ✔ ✔ ✔ \ No newline at end of file +Error ✔ ✔ ✔ diff --git a/src/test/scala/BranchTreeTests.scala b/src/test/scala/BranchTreeTests.scala index f06441e2..93ed9738 100644 --- a/src/test/scala/BranchTreeTests.scala +++ b/src/test/scala/BranchTreeTests.scala @@ -17,7 +17,7 @@ class DummyReporter extends Reporter { else "Verification successful." def report(msg: Message): Unit = { msg match { - case m : BranchTreeReport => this.breports += m.tree + case m : BranchTreeReport => this.breports += m.tree.prettyPrint() case _ => } } From 93189b9b63501a4e99844616aef17cfb14f2f61d Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Tue, 4 Mar 2025 21:31:12 +0100 Subject: [PATCH 27/39] Concurrent Map inside branchTreeMap --- src/main/scala/state/BranchTree.scala | 13 ++++++------- src/main/scala/supporters/MethodSupporter.scala | 2 +- 2 files changed, 7 insertions(+), 8 deletions(-) diff --git a/src/main/scala/state/BranchTree.scala b/src/main/scala/state/BranchTree.scala index ba26c013..0581f512 100644 --- a/src/main/scala/state/BranchTree.scala +++ b/src/main/scala/state/BranchTree.scala @@ -5,17 +5,16 @@ import viper.silicon.verifier.Verifier import viper.silver.ast import viper.silver.ast.Exp import viper.silver.reporter.BranchTree - -import scala.collection.mutable +import java.util.concurrent.{ConcurrentHashMap, ConcurrentMap} class BranchTreeMap { - private val map : mutable.Map[String, Tree] = new mutable.HashMap[String,Tree]() - def Map : mutable.Map[String, Tree] = map + private val map : ConcurrentMap[String, Tree] = new ConcurrentHashMap[String,Tree]() + def get(method: String) : Tree = map.get(method) def storeIntoTree(method: String, branchConditions : Seq[Exp], isResultFatal: Boolean): Unit = { - val branchTree = map.get(method) - if (branchTree.isDefined) { - branchTree.get.extend(branchConditions, isResultFatal) + if (map.containsKey(method)) { + val branchTree = map.get(method) + branchTree.extend(branchConditions, isResultFatal) } else { map.put(method, Tree.generate(branchConditions, isResultFatal)) } diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index a6ba24eb..eb50a36d 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/src/main/scala/supporters/MethodSupporter.scala @@ -119,7 +119,7 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif symbExLog.closeMemberScope() - s.branchTreeMap.get.Map.get(method.name).foreach( + Option(branchTreeMap.get(method.name)).foreach( branchTree => { val branch = branchTree.asInstanceOf[Branch] if (branch.getErrorCount() > 0) { From 4eb19d97bce9ddd26564be23bac1ced1fea7c8af Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Tue, 4 Mar 2025 23:56:54 +0100 Subject: [PATCH 28/39] Make dot file path absolute --- src/main/scala/state/BranchTree.scala | 37 ++++++++------------------- 1 file changed, 11 insertions(+), 26 deletions(-) diff --git a/src/main/scala/state/BranchTree.scala b/src/main/scala/state/BranchTree.scala index 0581f512..9fd6dfc5 100644 --- a/src/main/scala/state/BranchTree.scala +++ b/src/main/scala/state/BranchTree.scala @@ -207,14 +207,6 @@ class Tree extends BranchTree { } } - /*digraph { - a -> b[label="0.2"]; - a -> c[label="0.4",weight="0.4"]; - c -> b[label="0.6",weight="0.6"]; - c -> e[label="0.6",weight="0.6"]; - e -> e[label="0.1",weight="0.1"]; - e -> b[label="0.7",weight="0.7"]; - }*/ protected def leafToDotNodeContent(fatalCount : Int): String = { fatalCount match { case -1 => "label=\"✔\",shape=\"octagon\",style=\"filled\", fillcolor=\"palegreen\"" @@ -228,54 +220,47 @@ class Tree extends BranchTree { 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 b1 : Branch => - val newVisitedCount = visitedCount + 1 - val leftBranchIdn = s"B$newVisitedCount" - val visitedCountLeft_ = b1.writeDotFileRec(writer, newVisitedCount) + val leftBranchIdn = s"B$newVisitedCountLeft" + val visitedCountLeft_ = b1.writeDotFileRec(writer, newVisitedCountLeft) writer.write(s" $parentIdn -> $leftBranchIdn[label=\"F\"];\n") visitedCountLeft_ case Leaf => - val newVisitedCount = visitedCount + 1 - val leftLeafIdn = s"B$newVisitedCount" + val leftLeafIdn = s"B$newVisitedCountLeft" writer.write(s" $leftLeafIdn[${leafToDotNodeContent(leftResFatalCount)}];\n") writer.write(s" $parentIdn -> $leftLeafIdn [label=\"F\"];\n") - newVisitedCount + newVisitedCountLeft } + val newVisitedCountRight = visitedCountLeft + 1 val visitedCountRight = right match { case b2 : Branch => - val newVisitedCount = visitedCountLeft + 1 - val rightBranchIdn = s"B$newVisitedCount" - val visitedCountRight_ = b2.writeDotFileRec(writer, newVisitedCount) + val rightBranchIdn = s"B$newVisitedCountRight" + val visitedCountRight_ = b2.writeDotFileRec(writer, newVisitedCountRight) writer.write(s" $parentIdn -> $rightBranchIdn[label=\"T\"];\n") visitedCountRight_ case Leaf => - val newVisitedCount = visitedCountLeft + 1 - val rightLeafIdn = s"B$newVisitedCount" + val rightLeafIdn = s"B$newVisitedCountRight" writer.write(s" $rightLeafIdn[${leafToDotNodeContent(rightResFatalCount)}];\n") writer.write(s" $parentIdn -> $rightLeafIdn [label=\"T\"];\n") - newVisitedCount + newVisitedCountRight } visitedCountRight case _ => 0 } } def toDotFile(): Unit = { - println("TEST TEST TEST TEST TEST") - println(Tree.DotFilePath) val writer = PrintWriter(new java.io.File(Tree.DotFilePath),true) writer.write("digraph {\n") this.writeDotFileRec(writer) writer.write("}\n") writer.close() - /*viper.silicon.common.io.toFile( - dotString, - new java.io.File(Tree.DotFilePath))*/ } } object Tree { - val DotFilePath = s"${Verifier.config.tempDirectory()}/BranchTree.dot" + val DotFilePath = s"${System.getProperty("user.dir")}/${Verifier.config.tempDirectory()}/BranchTree.dot" private def generate(expressions : Seq[Exp], errorCount: Int) : Tree = { expressions.length match { From 089fc05bb5138ccb711ff25afac7ef0edfa606ce Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Fri, 7 Mar 2025 19:30:22 +0100 Subject: [PATCH 29/39] Add missing change --- src/test/scala/tests.scala | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/test/scala/tests.scala b/src/test/scala/tests.scala index 3b432a34..c6492882 100644 --- a/src/test/scala/tests.scala +++ b/src/test/scala/tests.scala @@ -38,7 +38,10 @@ package object tests { def instantiateFrontend(args: List[String] = List.empty, reporter : Option[Reporter] = None): SilFrontend = { val frontend = new DummyFrontend - val backend = new Silicon(List("startedBy" -> s"Unit test ${this.getClass.getSimpleName}")) + val backend = reporter match { + case Some(r) => new Silicon(r,List("startedBy" -> s"Unit test ${this.getClass.getSimpleName}")) + case _ => new Silicon(List("startedBy" -> s"Unit test ${this.getClass.getSimpleName}")) + } backend.parseCommandLine(List("--ignoreFile", "dummy.sil")++args) backend.start() From 29d114d1197c27f30cbf9c34f7b3a251acc7a8be Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Fri, 7 Mar 2025 19:41:41 +0100 Subject: [PATCH 30/39] Add missing change --- src/main/scala/supporters/MethodSupporter.scala | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index eb50a36d..4d35b891 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/src/main/scala/supporters/MethodSupporter.scala @@ -81,11 +81,12 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif ++ outs.map(x => (x, decider.fresh(x))) ++ method.scopedDecls.collect { case l: ast.LocalVarDecl => l }.map(_.localVar).map(x => (x, decider.fresh(x)))) + val branchTreeMap = new BranchTreeMap() val s = sInit.copy(g = g, h = Heap(), oldHeaps = OldHeaps(), methodCfg = body, - branchTreeMap = Some(new BranchTreeMap())) + branchTreeMap = Some(branchTreeMap)) if (Verifier.config.printMethodCFGs()) { viper.silicon.common.io.toFile( From 370c675824bdc0ecd5d69f949447f82d62ef4b8b Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Fri, 7 Mar 2025 22:50:49 +0100 Subject: [PATCH 31/39] Change back from reporting to errors --- src/main/scala/state/BranchTree.scala | 2 +- .../scala/supporters/MethodSupporter.scala | 32 ++++++++++--------- src/test/scala/BranchTreeTests.scala | 23 +++---------- src/test/scala/tests.scala | 7 ++-- 4 files changed, 24 insertions(+), 40 deletions(-) diff --git a/src/main/scala/state/BranchTree.scala b/src/main/scala/state/BranchTree.scala index 9fd6dfc5..ab34b773 100644 --- a/src/main/scala/state/BranchTree.scala +++ b/src/main/scala/state/BranchTree.scala @@ -4,7 +4,7 @@ import viper.silicon.common.io.PrintWriter import viper.silicon.verifier.Verifier import viper.silver.ast import viper.silver.ast.Exp -import viper.silver.reporter.BranchTree +import viper.silver.verifier.errors.BranchTree import java.util.concurrent.{ConcurrentHashMap, ConcurrentMap} class BranchTreeMap { diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index 4d35b891..0457496f 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/src/main/scala/supporters/MethodSupporter.scala @@ -10,7 +10,7 @@ import com.typesafe.scalalogging.Logger import viper.silver.ast import viper.silver.components.StatefulComponent import viper.silver.verifier.errors._ -import viper.silicon.interfaces._ +import viper.silicon.interfaces.{Failure, _} import viper.silicon.decider.Decider import viper.silicon.logger.records.data.WellformednessCheckRecord import viper.silicon.rules.{consumer, executionFlowController, executor, producer} @@ -18,8 +18,9 @@ import viper.silicon.state.{Branch, BranchTreeMap, Heap, State, Store} import viper.silicon.state.State.OldHeaps import viper.silicon.verifier.{Verifier, VerifierComponent} import viper.silicon.utils.freshSnap -import viper.silver.reporter.{AnnotationWarning, BeamInfo, BranchTreeReport} +import viper.silver.reporter.AnnotationWarning import viper.silicon.{Map, toMap} +import viper.silver.verifier.reasons.BranchFails /* TODO: Consider changing the DefaultMethodVerificationUnitProvider into a SymbolicExecutionRule */ @@ -120,20 +121,21 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif symbExLog.closeMemberScope() - Option(branchTreeMap.get(method.name)).foreach( - branchTree => { - val branch = branchTree.asInstanceOf[Branch] - if (branch.getErrorCount() > 0) { - v.reporter.report( - BranchTreeReport(s.currentMember.get.asInstanceOf[ast.Method], + Option(branchTreeMap.get(method.name)).collect({ + case branchTree : Branch if branchTree.getErrorCount() > 0 => + val method = s.currentMember.get.asInstanceOf[ast.Method] + Seq(result, Failure( + BranchFailed( + method, + BranchFails( + method, branchTree, - Seq(BeamInfo(branch.exp, branch.isLeftFatal, branch.isRightFatal)) - )) - } - } - ) - - Seq(result) + Seq(BeamInfo(branchTree.exp, branchTree.isLeftFatal, branchTree.isRightFatal)) + ) + ) + )) + case _=> Seq(result) + }).getOrElse(Seq(result)) } /* Lifetime */ diff --git a/src/test/scala/BranchTreeTests.scala b/src/test/scala/BranchTreeTests.scala index 93ed9738..b7d53720 100644 --- a/src/test/scala/BranchTreeTests.scala +++ b/src/test/scala/BranchTreeTests.scala @@ -6,23 +6,9 @@ import org.scalatest.funsuite.AnyFunSuite import viper.silver.ast.utility.DiskLoader -import viper.silver.reporter.{BranchTreeReport, Message, Reporter} import java.nio.file.Paths -class DummyReporter extends Reporter { - val name: String = "DummyReporter" - var breports: Set[String] = Set() - def getBranchTreeMessage = if (breports.nonEmpty) breports.mkString("\n") - else "Verification successful." - def report(msg: Message): Unit = { - msg match { - case m : BranchTreeReport => this.breports += m.tree.prettyPrint() - case _ => - } - } -} - class BranchTreeTests extends AnyFunSuite { def executeTestDefault(fileName: String) : Unit = executeTest(fileName, "default") @@ -87,12 +73,11 @@ class BranchTreeTests extends AnyFunSuite { : Unit = { val expected = getExpectedString(fileName, expectedFolder) - val dummyReporter = new DummyReporter() - val frontend = tests.instantiateFrontend(args, Some(dummyReporter)) + val frontend = tests.instantiateFrontend(args) val program = tests.loadProgram("branchTreeTests/",fileName, frontend) - frontend.verifier.verify(program) - - val actual = dummyReporter.getBranchTreeMessage + 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 c6492882..a41a4363 100644 --- a/src/test/scala/tests.scala +++ b/src/test/scala/tests.scala @@ -35,13 +35,10 @@ package object tests { override def verifier: Verifier = this._verifier.get } - def instantiateFrontend(args: List[String] = List.empty, reporter : Option[Reporter] = None): SilFrontend = { + def instantiateFrontend(args: List[String] = List.empty): SilFrontend = { val frontend = new DummyFrontend - val backend = reporter match { - case Some(r) => new Silicon(r,List("startedBy" -> s"Unit test ${this.getClass.getSimpleName}")) - case _ => new Silicon(List("startedBy" -> s"Unit test ${this.getClass.getSimpleName}")) - } + val backend = new Silicon(List("startedBy" -> s"Unit test ${this.getClass.getSimpleName}")) backend.parseCommandLine(List("--ignoreFile", "dummy.sil")++args) backend.start() From bf1a48d527ee393cd72938770f7fed4cb8229ef7 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Sun, 9 Mar 2025 11:36:12 +0100 Subject: [PATCH 32/39] Refactoring --- src/main/scala/state/BranchTree.scala | 78 +++++++++++++++------------ 1 file changed, 43 insertions(+), 35 deletions(-) diff --git a/src/main/scala/state/BranchTree.scala b/src/main/scala/state/BranchTree.scala index ab34b773..6173c2b6 100644 --- a/src/main/scala/state/BranchTree.scala +++ b/src/main/scala/state/BranchTree.scala @@ -5,6 +5,7 @@ import viper.silicon.verifier.Verifier import viper.silver.ast import viper.silver.ast.Exp import viper.silver.verifier.errors.BranchTree + import java.util.concurrent.{ConcurrentHashMap, ConcurrentMap} class BranchTreeMap { @@ -22,6 +23,7 @@ class BranchTreeMap { } class Tree extends BranchTree { + private def incrementIfFatal(currBranchResultFatal: Int, isResultFatal: Boolean) : Int = if (isResultFatal) Math.max(currBranchResultFatal,0)+1 else currBranchResultFatal @@ -41,16 +43,16 @@ class Tree extends BranchTree { case ast.Not(exp) => exp case _ => tail.head } - if (currBranch.left.isInstanceOf[Branch] - && headExp.toString.equals(currBranch.left.asInstanceOf[Branch].exp.toString) && negated) { - currNode = currBranch.left - currBranch.leftResFatalCount = incrementIfFatal(currBranch.leftResFatalCount,isResultFatal) - next = true - } else if (currBranch.right.isInstanceOf[Branch] - && headExp.toString.equals(currBranch.right.asInstanceOf[Branch].exp.toString) && !negated) { - currNode = currBranch.right - currBranch.rightResFatalCount = incrementIfFatal(currBranch.rightResFatalCount,isResultFatal) - next = true + (currBranch.left, currBranch.right) match { + case (Branch(exp,_,_,_,_),_) if headExp.toString == exp.toString && negated => + currNode = currBranch.left + currBranch.leftResFatalCount = incrementIfFatal(currBranch.leftResFatalCount,isResultFatal) + next = true + case (_,Branch(exp,_,_,_,_)) if headExp.toString == exp.toString && !negated => + currNode = currBranch.right + currBranch.rightResFatalCount = incrementIfFatal(currBranch.rightResFatalCount,isResultFatal) + next = true + case _ => } if (next) { currBranch = currNode.asInstanceOf[Branch] @@ -62,28 +64,30 @@ class Tree extends BranchTree { } } val errorCount = if (isResultFatal) 1 else -1 // -1 for successful result - if (negated) { - currBranch.left = Tree.generate(tail, errorCount) - currBranch.leftResFatalCount = errorCount - } else { - currBranch.right = Tree.generate(tail, errorCount) - currBranch.rightResFatalCount = errorCount + negated match { + case true => + currBranch.left = Tree.generate(tail, errorCount) + currBranch.leftResFatalCount = errorCount + case _ => + currBranch.right = Tree.generate(tail, errorCount) + currBranch.rightResFatalCount = errorCount } } } - private def recurse(tree: Tree, fatalCount: Int) : (Vector[String], Int, Int) = { - tree match { + + 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 => tree.buildTree() + case _ : Branch => this.buildTreeStr() case _ => (Vector("?"), 0, 0) } } - private def even(n: Int) = (n & 1) == 0 - - private def buildTree() : (Vector[String], Int, Int) = { + private def buildTreeStr() : (Vector[String], Int, Int) = { this match { case Branch(exp, left, right, leftErrCount, rightErrCount) => val expStr = exp.toString @@ -93,8 +97,8 @@ class Tree extends BranchTree { val boxLen = boxMiddle.length val halfBoxLen = boxLen / 2 - var (leftStrVec, _, prevLeftRightBoxLen) = recurse(left, leftErrCount) - var (rightStrVec, prevRightLeftBoxLen, _) = recurse(right, rightErrCount) + var (leftStrVec, _, prevLeftRightBoxLen) = left.buildTreeStrRec(leftErrCount) + var (rightStrVec, prevRightLeftBoxLen, _) = right.buildTreeStrRec(rightErrCount) val halfExpStrLen = expStrLen / 2 val leftBoxLen = leftStrVec.head.length @@ -139,6 +143,8 @@ class Tree extends BranchTree { case _ => (Vector.empty, -1, -1) // Should not happen } } + + private def fill(vec : Vector[String], filler :Int): Vector[String] = { vec.grouped(4) .flatMap(elems => { @@ -151,7 +157,7 @@ class Tree extends BranchTree { }).toVector } - private def printSinglePath() : String = { + private def buildPathStr() : String = { var currTree : Tree = this var maxBoxLen = 5 // for 'Error' var path = Vector[String]() @@ -201,13 +207,14 @@ class Tree extends BranchTree { def prettyPrint() : String = { if (Verifier.config.numberOfErrorsToReport() == 1 || this.getErrorCount() == 1) { - this.printSinglePath() + this.buildPathStr() } else { - this.buildTree()._1.reduce((str, s) => str + "\n" + s) + "\n" + this.buildTreeStr()._1.reduce((str, s) => str + "\n" + s) + "\n" } } - protected def leafToDotNodeContent(fatalCount : Int): String = { + + 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\"" @@ -215,16 +222,16 @@ class Tree extends BranchTree { } } - protected def writeDotFileRec(writer: java.io.PrintWriter, visitedCount : Int = 0) : Int = { + 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 b1 : Branch => + case _ : Branch => val leftBranchIdn = s"B$newVisitedCountLeft" - val visitedCountLeft_ = b1.writeDotFileRec(writer, newVisitedCountLeft) + val visitedCountLeft_ = left.writeDotFileRec(writer, newVisitedCountLeft) writer.write(s" $parentIdn -> $leftBranchIdn[label=\"F\"];\n") visitedCountLeft_ case Leaf => @@ -235,9 +242,9 @@ class Tree extends BranchTree { } val newVisitedCountRight = visitedCountLeft + 1 val visitedCountRight = right match { - case b2 : Branch => + case _ : Branch => val rightBranchIdn = s"B$newVisitedCountRight" - val visitedCountRight_ = b2.writeDotFileRec(writer, newVisitedCountRight) + val visitedCountRight_ = right.writeDotFileRec(writer, newVisitedCountRight) writer.write(s" $parentIdn -> $rightBranchIdn[label=\"T\"];\n") visitedCountRight_ case Leaf => @@ -250,6 +257,7 @@ class Tree extends BranchTree { case _ => 0 } } + def toDotFile(): Unit = { val writer = PrintWriter(new java.io.File(Tree.DotFilePath),true) writer.write("digraph {\n") @@ -284,8 +292,8 @@ private object Leaf extends Tree case class Branch(var exp : Exp, var left: Tree, var right: Tree, - var leftResFatalCount: Int, - var rightResFatalCount: Int) extends Tree { + protected[state] var leftResFatalCount: Int, + protected[state] var rightResFatalCount: Int) extends Tree { def isLeftFatal = leftResFatalCount > 0 def isRightFatal = rightResFatalCount > 0 } \ No newline at end of file From 692e9e2b09bf188f2a8fd338486e7c1fd38083b3 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Sun, 9 Mar 2025 11:46:34 +0100 Subject: [PATCH 33/39] Refactoring --- src/main/scala/state/BranchTree.scala | 29 +++++++++---------- .../scala/supporters/MethodSupporter.scala | 2 +- 2 files changed, 15 insertions(+), 16 deletions(-) diff --git a/src/main/scala/state/BranchTree.scala b/src/main/scala/state/BranchTree.scala index 6173c2b6..9a9b5c11 100644 --- a/src/main/scala/state/BranchTree.scala +++ b/src/main/scala/state/BranchTree.scala @@ -27,8 +27,8 @@ class Tree extends BranchTree { private def incrementIfFatal(currBranchResultFatal: Int, isResultFatal: Boolean) : Int = if (isResultFatal) Math.max(currBranchResultFatal,0)+1 else currBranchResultFatal - def extend(branchConditions : Seq[Exp], isResultFatal: Boolean) = { - if (branchConditions.length > 0) { + def extend(branchConditions : Seq[Exp], isResultFatal: Boolean) : Unit = { + if (branchConditions.nonEmpty) { var currNode = this var currBranch = currNode.asInstanceOf[Branch] var negated = branchConditions.head match { @@ -37,7 +37,7 @@ class Tree extends BranchTree { } var tail = branchConditions.tail var next = true - while (tail.length != 0 && next) { + while (tail.nonEmpty && next) { next = false val headExp = tail.head match { case ast.Not(exp) => exp @@ -64,13 +64,12 @@ class Tree extends BranchTree { } } val errorCount = if (isResultFatal) 1 else -1 // -1 for successful result - negated match { - case true => - currBranch.left = Tree.generate(tail, errorCount) - currBranch.leftResFatalCount = errorCount - case _ => - currBranch.right = Tree.generate(tail, errorCount) - currBranch.rightResFatalCount = errorCount + if (negated) { + currBranch.left = Tree.generate(tail, errorCount) + currBranch.leftResFatalCount = errorCount + } else { + currBranch.right = Tree.generate(tail, errorCount) + currBranch.rightResFatalCount = errorCount } } } @@ -198,7 +197,7 @@ class Tree extends BranchTree { .reduce((str, s) => str + s) } - def getErrorCount(): Int = { + def getErrorCount: Int = { this match { case Branch(_,_,_,lf,rf) => Math.max(lf,0) + Math.max(rf,0) case _ => 0 @@ -206,7 +205,7 @@ class Tree extends BranchTree { } def prettyPrint() : String = { - if (Verifier.config.numberOfErrorsToReport() == 1 || this.getErrorCount() == 1) { + if (Verifier.config.numberOfErrorsToReport() == 1 || this.getErrorCount == 1) { this.buildPathStr() } else { this.buildTreeStr()._1.reduce((str, s) => str + "\n" + s) + "\n" @@ -259,7 +258,7 @@ class Tree extends BranchTree { } def toDotFile(): Unit = { - val writer = PrintWriter(new java.io.File(Tree.DotFilePath),true) + val writer = PrintWriter(new java.io.File(Tree.DotFilePath),append=true) writer.write("digraph {\n") this.writeDotFileRec(writer) writer.write("}\n") @@ -294,6 +293,6 @@ case class Branch(var exp : Exp, var right: Tree, protected[state] var leftResFatalCount: Int, protected[state] var rightResFatalCount: Int) extends Tree { - def isLeftFatal = leftResFatalCount > 0 - def isRightFatal = rightResFatalCount > 0 + def isLeftFatal : Boolean = leftResFatalCount > 0 + def isRightFatal : Boolean = rightResFatalCount > 0 } \ No newline at end of file diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index 0457496f..3b35e8d8 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/src/main/scala/supporters/MethodSupporter.scala @@ -122,7 +122,7 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif symbExLog.closeMemberScope() Option(branchTreeMap.get(method.name)).collect({ - case branchTree : Branch if branchTree.getErrorCount() > 0 => + case branchTree : Branch if branchTree.getErrorCount > 0 => val method = s.currentMember.get.asInstanceOf[ast.Method] Seq(result, Failure( BranchFailed( From 9a7006080c61550fcd2c42bef798cf70f483179f Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Mon, 10 Mar 2025 00:19:46 +0100 Subject: [PATCH 34/39] Refactoring --- src/main/scala/interfaces/Verification.scala | 13 +- src/main/scala/rules/Consumer.scala | 2 +- .../scala/rules/SymbolicExecutionRules.scala | 7 +- src/main/scala/state/BranchTree.scala | 165 +++++++++--------- src/main/scala/state/State.scala | 22 +-- .../scala/supporters/MethodSupporter.scala | 18 +- .../default/firstPathFails_expected | 10 -- .../default/multipleMethods_expected | 21 --- .../branchTreeTests/default/onlyIf_expected | 6 - .../reportAllErrors/firstPathFails_expected | 9 - .../reportAllErrors/lastPathFails_expected | 9 - .../reportAllErrors/onlyIf_expected | 5 - .../reportAllErrors/while_expected | 6 - .../reportTwoErrors/firstPathFails_expected | 9 - .../reportTwoErrors/lastPathFails_expected | 9 - src/test/scala/BranchTreeTests.scala | 4 +- 16 files changed, 113 insertions(+), 202 deletions(-) delete mode 100644 src/test/resources/branchTreeTests/default/firstPathFails_expected delete mode 100644 src/test/resources/branchTreeTests/default/multipleMethods_expected delete mode 100644 src/test/resources/branchTreeTests/default/onlyIf_expected delete mode 100644 src/test/resources/branchTreeTests/reportAllErrors/firstPathFails_expected delete mode 100644 src/test/resources/branchTreeTests/reportAllErrors/lastPathFails_expected delete mode 100644 src/test/resources/branchTreeTests/reportAllErrors/onlyIf_expected delete mode 100644 src/test/resources/branchTreeTests/reportAllErrors/while_expected delete mode 100644 src/test/resources/branchTreeTests/reportTwoErrors/firstPathFails_expected delete mode 100644 src/test/resources/branchTreeTests/reportTwoErrors/lastPathFails_expected diff --git a/src/main/scala/interfaces/Verification.scala b/src/main/scala/interfaces/Verification.scala index ad52d3bf..96b67801 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,18 @@ 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.map(x => x.previous.length match { + case 0 => x.exploredBranchPaths + case _ => + val recRes = x.previous.map(getExploredBranchPaths).flatten + x.exploredBranchPaths ++ recRes + }).flatten} + def isFatal: Boolean def &&(other: => VerificationResult): VerificationResult @@ -61,7 +70,6 @@ sealed abstract class VerificationResult { } this } - } } @@ -100,7 +108,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 ceca9c63..8231a78c 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -620,7 +620,7 @@ object consumer extends ConsumptionRules { case true => v2.decider.assume(t, Option.when(withExp)(e), eNew) val r = QS(s3, v2) - s.storeIntoTree(v.decider.pcs.getBranchConditionsExp(),false) + r.exploredBranchPaths +:= (v.decider.pcs.getBranchConditionsExp(),false) r case false => val failure = createFailure(pve dueTo AssertionFalse(e), v2, s3, termToAssert, eNew) diff --git a/src/main/scala/rules/SymbolicExecutionRules.scala b/src/main/scala/rules/SymbolicExecutionRules.scala index ba76c203..d8ce63f0 100644 --- a/src/main/scala/rules/SymbolicExecutionRules.scala +++ b/src/main/scala/rules/SymbolicExecutionRules.scala @@ -8,7 +8,7 @@ package viper.silicon.rules import viper.silicon.debugger.DebugExp import viper.silicon.interfaces.{Failure, SiliconDebuggingFailureContext, SiliconFailureContext, SiliconMappedCounterexample, SiliconNativeCounterexample, SiliconVariableCounterexample} -import viper.silicon.state.{State} +import viper.silicon.state.State import viper.silicon.state.terms.{False, Term} import viper.silicon.verifier.Verifier import viper.silver.ast @@ -85,7 +85,6 @@ trait SymbolicExecutionRules { } val branchConditions = v.decider.pcs.getBranchConditionsExp() - s.storeIntoTree(branchConditions, true) if (Verifier.config.enableDebugging()){ val assumptions = v.decider.pcs.assumptionExps @@ -97,6 +96,8 @@ trait SymbolicExecutionRules { 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/state/BranchTree.scala b/src/main/scala/state/BranchTree.scala index 9a9b5c11..c6cca5c4 100644 --- a/src/main/scala/state/BranchTree.scala +++ b/src/main/scala/state/BranchTree.scala @@ -1,82 +1,65 @@ -package viper.silicon.state +package viper.silicon.state.branchTree import viper.silicon.common.io.PrintWriter import viper.silicon.verifier.Verifier import viper.silver.ast import viper.silver.ast.Exp -import viper.silver.verifier.errors.BranchTree -import java.util.concurrent.{ConcurrentHashMap, ConcurrentMap} - -class BranchTreeMap { - private val map : ConcurrentMap[String, Tree] = new ConcurrentHashMap[String,Tree]() - - def get(method: String) : Tree = map.get(method) - def storeIntoTree(method: String, branchConditions : Seq[Exp], isResultFatal: Boolean): Unit = { - if (map.containsKey(method)) { - val branchTree = map.get(method) - branchTree.extend(branchConditions, isResultFatal) - } else { - map.put(method, Tree.generate(branchConditions, isResultFatal)) - } - } -} - -class Tree extends BranchTree { +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 - def extend(branchConditions : Seq[Exp], isResultFatal: Boolean) : Unit = { - if (branchConditions.nonEmpty) { - var currNode = this - var currBranch = currNode.asInstanceOf[Branch] - 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 (Branch(exp,_,_,_,_),_) if headExp.toString == exp.toString && negated => - currNode = currBranch.left - currBranch.leftResFatalCount = incrementIfFatal(currBranch.leftResFatalCount,isResultFatal) - next = true - case (_,Branch(exp,_,_,_,_)) if headExp.toString == exp.toString && !negated => - currNode = currBranch.right - currBranch.rightResFatalCount = incrementIfFatal(currBranch.rightResFatalCount,isResultFatal) - next = true - case _ => + 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 } - if (next) { - currBranch = currNode.asInstanceOf[Branch] - negated = tail.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 } - tail = tail.tail } - } - val errorCount = if (isResultFatal) 1 else -1 // -1 for successful result - if (negated) { - currBranch.left = Tree.generate(tail, errorCount) - currBranch.leftResFatalCount = errorCount - } else { - currBranch.right = Tree.generate(tail, errorCount) - currBranch.rightResFatalCount = errorCount - } + val errorCount = if (isResultFatal) 1 else -1 + val subTree = BranchTree.generate(Vector((tail, isResultFatal)))// -1 for successful result // TODO + 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) @@ -85,7 +68,6 @@ class Tree extends BranchTree { case _ => (Vector("?"), 0, 0) } } - private def buildTreeStr() : (Vector[String], Int, Int) = { this match { case Branch(exp, left, right, leftErrCount, rightErrCount) => @@ -155,9 +137,8 @@ class Tree extends BranchTree { ) }).toVector } - private def buildPathStr() : String = { - var currTree : Tree = this + var currTree : BranchTree = this var maxBoxLen = 5 // for 'Error' var path = Vector[String]() var side = Vector[String]() @@ -166,8 +147,7 @@ class Tree extends BranchTree { case b@Branch(e, l, r, lc, rc) => val expStr = e.toString val halfExpStrLen = expStr.length / 2 - val pathTaken = if (b.isLeftFatal) "F" else "T" - val pathNotTaken = if (b.isLeftFatal) "T" else "F" + 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 "") + " ├──" @@ -180,14 +160,14 @@ class Tree extends BranchTree { if (maxBoxLen > boxLen) box = fill(box, filler) else path = fill(path, filler) maxBoxLen = Math.max(maxBoxLen, boxLen) - (if(b.isLeftFatal) rc else lc) match { + (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.isLeftFatal) l else r + currTree = if (b.isRightFatal) r else l // influenced by order of verification results (true branch results before left) case _ => currTree = Leaf } } @@ -212,7 +192,6 @@ class Tree extends BranchTree { } } - private def leafToDotNodeContent(fatalCount : Int): String = { fatalCount match { case -1 => "label=\"✔\",shape=\"octagon\",style=\"filled\", fillcolor=\"palegreen\"" @@ -220,7 +199,6 @@ class Tree extends BranchTree { 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) => @@ -258,7 +236,7 @@ class Tree extends BranchTree { } def toDotFile(): Unit = { - val writer = PrintWriter(new java.io.File(Tree.DotFilePath),append=true) + val writer = PrintWriter(new java.io.File(BranchTree.DotFilePath),append=true) writer.write("digraph {\n") this.writeDotFileRec(writer) writer.write("}\n") @@ -266,33 +244,50 @@ class Tree extends BranchTree { } } -object Tree { +object BranchTree { val DotFilePath = s"${System.getProperty("user.dir")}/${Verifier.config.tempDirectory()}/BranchTree.dot" - private def generate(expressions : Seq[Exp], errorCount: Int) : Tree = { + private def generatePathRec(expressions: Seq[Exp], errorCount: Int, result: BranchTree): BranchTree = { expressions.length match { - case 0 => Leaf + case 0 => result case _ => - val subtree = generate(expressions.tail, errorCount) - expressions.head match { + val lastExp = expressions.last + lastExp match { case ast.Not(exp) => - Branch(exp, subtree, Leaf, errorCount, 0) + generatePathRec(expressions.init, errorCount, Branch(exp, result, Leaf, errorCount, 0)) case _ => - Branch(expressions.head, Leaf, subtree, 0, errorCount) + generatePathRec(expressions.init, errorCount, Branch(lastExp, Leaf, result, 0, errorCount)) } } } - def generate(expressions : Seq[Exp], isFatal: Boolean) : Tree = - generate(expressions, if (isFatal) 1 else -1) // -1 or distinguishing successful from no result at leaves + 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)) + } + } } -private object Leaf extends Tree +object Leaf extends BranchTree case class Branch(var exp : Exp, - var left: Tree, - var right: Tree, - protected[state] var leftResFatalCount: Int, - protected[state] var rightResFatalCount: Int) extends Tree { + 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/state/State.scala b/src/main/scala/state/State.scala index e05406dc..88fabb55 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -81,10 +81,8 @@ final case class State(g: Store = Store(), /* ast.Field, ast.Predicate, or MagicWandIdentifier */ heapDependentTriggers: InsertionOrderedSet[Any] = InsertionOrderedSet.empty, moreCompleteExhale: Boolean = false, - moreJoins: JoinMode = JoinMode.Off, - - branchTreeMap: Option[BranchTreeMap] = None) - extends Mergeable[State] { + moreJoins: JoinMode = JoinMode.Off) + extends Mergeable[State] { val isMethodVerification: Boolean = { // currentMember being None means we're verifying a CFG; this should behave like verifying a method. @@ -152,14 +150,6 @@ Verifier.config.respectFunctionPrePermAmounts() lazy val relevantQuantifiedVariables: Seq[(Var, Option[ast.AbstractLocalVar])] = relevantQuantifiedVariables(_ => true) - def storeIntoTree(branchConditions: Seq[Exp], isResultFatal: Boolean) = { - if (this.branchTreeMap.isDefined && this.currentMember.isDefined){ - if (branchConditions.nonEmpty) { - this.branchTreeMap.get.storeIntoTree(this.currentMember.get.name, branchConditions, isResultFatal) - } - } - } - override val toString = s"${this.getClass.getSimpleName}(...)" } @@ -191,7 +181,7 @@ object State { ssCache1, assertReadAccessOnly1, qpFields1, qpPredicates1, qpMagicWands1, permResources1, smCache1, pmCache1, smDomainNeeded1, predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers, - moreCompleteExhale, moreJoins, branchTreeMap) => + moreCompleteExhale, moreJoins) => /* Decompose state s2: most values must match those of s1 */ s2 match { @@ -216,7 +206,7 @@ object State { ssCache2, `assertReadAccessOnly1`, `qpFields1`, `qpPredicates1`, `qpMagicWands1`, `permResources1`, smCache2, pmCache2, `smDomainNeeded1`, `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`, - moreCompleteExhale2, `moreJoins`, `branchTreeMap`) => + moreCompleteExhale2, `moreJoins`) => val functionRecorder3 = functionRecorder1.merge(functionRecorder2) val triggerExp3 = triggerExp1 && triggerExp2 @@ -347,7 +337,7 @@ object State { ssCache1, assertReadAccessOnly1, qpFields1, qpPredicates1, qpMagicWands1, permResources1, smCache1, pmCache1, smDomainNeeded1, predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers, - moreCompleteExhale, moreJoins, branchTreeMap) => + moreCompleteExhale, moreJoins) => /* Decompose state s2: most values must match those of s1 */ s2 match { @@ -371,7 +361,7 @@ object State { ssCache2, `assertReadAccessOnly1`, `qpFields1`, `qpPredicates1`, `qpMagicWands1`, `permResources1`, smCache2, pmCache2, smDomainNeeded2, `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`, - moreCompleteExhale2, `moreJoins`, `branchTreeMap`) => + moreCompleteExhale2, `moreJoins`) => val functionRecorder3 = functionRecorder1.merge(functionRecorder2) val triggerExp3 = triggerExp1 && triggerExp2 diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index 3b35e8d8..1e01d3f1 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/src/main/scala/supporters/MethodSupporter.scala @@ -14,8 +14,9 @@ import viper.silicon.interfaces.{Failure, _} import viper.silicon.decider.Decider import viper.silicon.logger.records.data.WellformednessCheckRecord import viper.silicon.rules.{consumer, executionFlowController, executor, producer} -import viper.silicon.state.{Branch, BranchTreeMap, Heap, State, Store} +import viper.silicon.state.{Heap, State, Store} import viper.silicon.state.State.OldHeaps +import viper.silicon.state.branchTree.{Branch, BranchTree} import viper.silicon.verifier.{Verifier, VerifierComponent} import viper.silicon.utils.freshSnap import viper.silver.reporter.AnnotationWarning @@ -82,12 +83,10 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif ++ outs.map(x => (x, decider.fresh(x))) ++ method.scopedDecls.collect { case l: ast.LocalVarDecl => l }.map(_.localVar).map(x => (x, decider.fresh(x)))) - val branchTreeMap = new BranchTreeMap() val s = sInit.copy(g = g, h = Heap(), oldHeaps = OldHeaps(), - methodCfg = body, - branchTreeMap = Some(branchTreeMap)) + methodCfg = body) if (Verifier.config.printMethodCFGs()) { viper.silicon.common.io.toFile( @@ -121,8 +120,8 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif symbExLog.closeMemberScope() - Option(branchTreeMap.get(method.name)).collect({ - case branchTree : Branch if branchTree.getErrorCount > 0 => + 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( @@ -130,12 +129,15 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif BranchFails( method, branchTree, - Seq(BeamInfo(branchTree.exp, branchTree.isLeftFatal, branchTree.isRightFatal)) + Seq(BeamInfo(branchTree.exp, + branchTree.isLeftFatal, + branchTree.isRightFatal) + ) ) ) )) case _=> Seq(result) - }).getOrElse(Seq(result)) + } } /* Lifetime */ diff --git a/src/test/resources/branchTreeTests/default/firstPathFails_expected b/src/test/resources/branchTreeTests/default/firstPathFails_expected deleted file mode 100644 index 118145ee..00000000 --- a/src/test/resources/branchTreeTests/default/firstPathFails_expected +++ /dev/null @@ -1,10 +0,0 @@ - │ - ┌─┴─┐ F - │ a ├──── ? - └─┬─┘ - │T -┌───┴───┐ F -│ bcde ├── ? -└───┬───┘ - │T - Error diff --git a/src/test/resources/branchTreeTests/default/multipleMethods_expected b/src/test/resources/branchTreeTests/default/multipleMethods_expected deleted file mode 100644 index 360dffef..00000000 --- a/src/test/resources/branchTreeTests/default/multipleMethods_expected +++ /dev/null @@ -1,21 +0,0 @@ - │ - ┌─┴─┐ F - │ a ├──── ? - └─┬─┘ - │T -┌───┴───┐ F -│ bcde ├── ? -└───┬───┘ - │T - Error - - │ -┌─┴─┐ T -│ a ├── ✔ -└─┬─┘ - │F -┌─┴─┐ T -│ c ├── ✔ -└─┬─┘ - │F -Error diff --git a/src/test/resources/branchTreeTests/default/onlyIf_expected b/src/test/resources/branchTreeTests/default/onlyIf_expected deleted file mode 100644 index 2035a798..00000000 --- a/src/test/resources/branchTreeTests/default/onlyIf_expected +++ /dev/null @@ -1,6 +0,0 @@ - │ -┌─┴─┐ F -│ d ├── ? -└─┬─┘ - │T -Error diff --git a/src/test/resources/branchTreeTests/reportAllErrors/firstPathFails_expected b/src/test/resources/branchTreeTests/reportAllErrors/firstPathFails_expected deleted file mode 100644 index ef79e48e..00000000 --- a/src/test/resources/branchTreeTests/reportAllErrors/firstPathFails_expected +++ /dev/null @@ -1,9 +0,0 @@ - ┌─┴─┐ - │ 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 deleted file mode 100644 index d12eb8ef..00000000 --- a/src/test/resources/branchTreeTests/reportAllErrors/lastPathFails_expected +++ /dev/null @@ -1,9 +0,0 @@ - ┌─┴─┐ - │ a │ - └─┬─┘ - F┌──┴────┐T - ┌─┴─┐ ┌───┴───┐ - │ c │ │ bcde │ - └─┬─┘ └───┬───┘ - F┌──┴┐T F┌┴┐T -Error ✔ ✔ ✔ diff --git a/src/test/resources/branchTreeTests/reportAllErrors/onlyIf_expected b/src/test/resources/branchTreeTests/reportAllErrors/onlyIf_expected deleted file mode 100644 index b43faf03..00000000 --- a/src/test/resources/branchTreeTests/reportAllErrors/onlyIf_expected +++ /dev/null @@ -1,5 +0,0 @@ - ┌─┴─┐ - │ d │ - └─┬─┘ - F┌──┴──┐T -Error Error diff --git a/src/test/resources/branchTreeTests/reportAllErrors/while_expected b/src/test/resources/branchTreeTests/reportAllErrors/while_expected deleted file mode 100644 index 3b4a031d..00000000 --- a/src/test/resources/branchTreeTests/reportAllErrors/while_expected +++ /dev/null @@ -1,6 +0,0 @@ - │ -┌─┴─┐ T -│ a ├── ? -└─┬─┘ - │F -Error diff --git a/src/test/resources/branchTreeTests/reportTwoErrors/firstPathFails_expected b/src/test/resources/branchTreeTests/reportTwoErrors/firstPathFails_expected deleted file mode 100644 index 4e978087..00000000 --- a/src/test/resources/branchTreeTests/reportTwoErrors/firstPathFails_expected +++ /dev/null @@ -1,9 +0,0 @@ -┌─┴─┐ -│ 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 deleted file mode 100644 index d12eb8ef..00000000 --- a/src/test/resources/branchTreeTests/reportTwoErrors/lastPathFails_expected +++ /dev/null @@ -1,9 +0,0 @@ - ┌─┴─┐ - │ a │ - └─┬─┘ - F┌──┴────┐T - ┌─┴─┐ ┌───┴───┐ - │ c │ │ bcde │ - └─┬─┘ └───┬───┘ - F┌──┴┐T F┌┴┐T -Error ✔ ✔ ✔ diff --git a/src/test/scala/BranchTreeTests.scala b/src/test/scala/BranchTreeTests.scala index b7d53720..3e4a82f5 100644 --- a/src/test/scala/BranchTreeTests.scala +++ b/src/test/scala/BranchTreeTests.scala @@ -57,10 +57,10 @@ class BranchTreeTests extends AnyFunSuite { def executeTestReportTwoErrors(fileName: String) : Unit = executeTest(fileName, "reportTwoErrors", List("--numberOfErrorsToReport", "2")) - test("FirstPathFailsTree") { + test("FirstPathFailsTreeTwo") { executeTestReportTwoErrors("firstPathFails") } - test("LastPathFailsTree") { + test("LastPathFailsTreeTwo") { executeTestReportTwoErrors("lastPathFails") } From 1a04d4f2bca75466f98fc6c9e6d4dd72099c3512 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Mon, 10 Mar 2025 00:26:40 +0100 Subject: [PATCH 35/39] Refactoring --- src/main/scala/interfaces/Verification.scala | 13 +++++++------ src/main/scala/state/BranchTree.scala | 4 ++++ 2 files changed, 11 insertions(+), 6 deletions(-) diff --git a/src/main/scala/interfaces/Verification.scala b/src/main/scala/interfaces/Verification.scala index 96b67801..caa71711 100644 --- a/src/main/scala/interfaces/Verification.scala +++ b/src/main/scala/interfaces/Verification.scala @@ -33,12 +33,13 @@ sealed abstract class VerificationResult { var isReported: Boolean = false def getExploredBranchPaths(r: VerificationResult = this) : Vector[(Seq[Exp], Boolean)] = { - r.exploredBranchPaths ++ r.previous.map(x => x.previous.length match { - case 0 => x.exploredBranchPaths - case _ => - val recRes = x.previous.map(getExploredBranchPaths).flatten - x.exploredBranchPaths ++ recRes - }).flatten} + 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 diff --git a/src/main/scala/state/BranchTree.scala b/src/main/scala/state/BranchTree.scala index c6cca5c4..8e52bc82 100644 --- a/src/main/scala/state/BranchTree.scala +++ b/src/main/scala/state/BranchTree.scala @@ -5,6 +5,8 @@ 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 = @@ -247,6 +249,7 @@ class BranchTree extends viper.silver.verifier.errors.BranchTree { 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 @@ -261,6 +264,7 @@ object BranchTree { } } + @tailrec private def generateRec(exploredPaths: Vector[(Seq[Exp], Boolean)], result: BranchTree): BranchTree = { // result.instanceOf[Branch] must hold exploredPaths.length match { case 0 => result From 11f2d7a5b03f4bfb28980fa733577ef6cffa900a Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Mon, 10 Mar 2025 01:04:10 +0100 Subject: [PATCH 36/39] Undo changes --- src/main/scala/state/State.scala | 6 ++--- .../scala/verifier/DefaultMainVerifier.scala | 23 ++----------------- 2 files changed, 4 insertions(+), 25 deletions(-) diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index 88fabb55..6dc4c494 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -23,7 +23,6 @@ import viper.silicon.supporters.functions.{FunctionData, FunctionRecorder, NoopF import viper.silicon.utils.ast.BigAnd import viper.silicon.verifier.Verifier import viper.silicon.{Map, Stack} -import viper.silver.ast.Exp import viper.silver.utility.Sanitizer final case class State(g: Store = Store(), @@ -82,7 +81,7 @@ final case class State(g: Store = Store(), heapDependentTriggers: InsertionOrderedSet[Any] = InsertionOrderedSet.empty, moreCompleteExhale: Boolean = false, moreJoins: JoinMode = JoinMode.Off) - extends Mergeable[State] { + extends Mergeable[State] { val isMethodVerification: Boolean = { // currentMember being None means we're verifying a CFG; this should behave like verifying a method. @@ -90,8 +89,7 @@ final case class State(g: Store = Store(), } val mayAssumeUpperBounds: Boolean = { - currentMember.isEmpty || !currentMember.get.isInstanceOf[ast.Function] || -Verifier.config.respectFunctionPrePermAmounts() + currentMember.isEmpty || !currentMember.get.isInstanceOf[ast.Function] || Verifier.config.respectFunctionPrePermAmounts() } val isLastRetry: Boolean = retryLevel == 0 diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index 724e6102..84df895b 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -36,8 +36,6 @@ import viper.silver.cfg.silver.SilverCfg import viper.silver.frontend.FrontendStateCache import viper.silver.reporter._ import viper.silver.verifier.VerifierWarning -import viper.silver.verifier.errors.PostconditionViolatedBranch -import viper.silver.verifier.reasons.BranchFailure /* TODO: Extract a suitable MainVerifier interface, probably including * - def verificationPoolManager: VerificationPoolManager) @@ -260,31 +258,14 @@ class DefaultMainVerifier(config: Config, program.methods.filterNot(excludeMethod).map(method => { val s = createInitialState(method, program, functionData, predicateData).copy(parallelizeBranches = - Verifier.config.parallelizeBranches(), branchTreeMap = Some(new BranchTreeMap())) /* [BRANCH-PARALLELISATION] */ + Verifier.config.parallelizeBranches()) /* [BRANCH-PARALLELISATION] */ _verificationPoolManager.queueVerificationTask(v => { val startTime = System.currentTimeMillis() - var results = v.methodSupporter.verify(s, method) + val results = v.methodSupporter.verify(s, method) .flatMap(extractAllVerificationResults) val elapsed = System.currentTimeMillis() - startTime - val branchTree = s.branchTreeMap.get.Map.get(method.name) - if (branchTree.isDefined) { - val branch = branchTree.get.asInstanceOf[Branch] - if (branch.isLeftFatal || branch.isRightFatal) { - val firstCond = branchTree.get.asInstanceOf[Branch].exp - results +:= Failure( - PostconditionViolatedBranch( - firstCond, - BranchFailure( - firstCond, - branchTree.get.prettyPrint() - ), - branch.isLeftFatal, - branch.isRightFatal) - ) - } - } reporter report VerificationResultMessage(s"silicon", method, elapsed, condenseToViperResult(results)) logger debug s"Silicon finished verification of method `${method.name}` in ${viper.silver.reporter.format.formatMillisReadably(elapsed)} seconds with the following result: ${condenseToViperResult(results).toString}" From 3f113845fd3262a1b92f3e805721e10f6403e90e Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Mon, 10 Mar 2025 01:14:17 +0100 Subject: [PATCH 37/39] Remove TODO --- src/main/scala/state/BranchTree.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/state/BranchTree.scala b/src/main/scala/state/BranchTree.scala index 8e52bc82..c095f98a 100644 --- a/src/main/scala/state/BranchTree.scala +++ b/src/main/scala/state/BranchTree.scala @@ -48,7 +48,7 @@ class BranchTree extends viper.silver.verifier.errors.BranchTree { } } val errorCount = if (isResultFatal) 1 else -1 - val subTree = BranchTree.generate(Vector((tail, isResultFatal)))// -1 for successful result // TODO + val subTree = BranchTree.generate(Vector((tail, isResultFatal)))// -1 for successful result if (negated) { currBranch.left = subTree.get currBranch.leftResFatalCount = errorCount From d35072c0cc23e43d52288856077f5e1aa3f56a56 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Mon, 10 Mar 2025 10:30:39 +0100 Subject: [PATCH 38/39] Readd missing files --- .../default/firstPathFails_expected | 10 +++++++++ .../default/multipleMethods_expected | 21 +++++++++++++++++++ .../branchTreeTests/default/onlyIf_expected | 6 ++++++ .../reportAllErrors/firstPathFails_expected | 9 ++++++++ .../reportAllErrors/lastPathFails_expected | 10 +++++++++ .../reportAllErrors/onlyIf_expected | 5 +++++ .../reportAllErrors/while_expected | 6 ++++++ .../reportTwoErrors/firstPathFails_expected | 9 ++++++++ .../reportTwoErrors/lastPathFails_expected | 10 +++++++++ 9 files changed, 86 insertions(+) create mode 100644 src/test/resources/branchTreeTests/default/firstPathFails_expected create mode 100644 src/test/resources/branchTreeTests/default/multipleMethods_expected create mode 100644 src/test/resources/branchTreeTests/default/onlyIf_expected create mode 100644 src/test/resources/branchTreeTests/reportAllErrors/firstPathFails_expected create mode 100644 src/test/resources/branchTreeTests/reportAllErrors/lastPathFails_expected create mode 100644 src/test/resources/branchTreeTests/reportAllErrors/onlyIf_expected create mode 100644 src/test/resources/branchTreeTests/reportAllErrors/while_expected create mode 100644 src/test/resources/branchTreeTests/reportTwoErrors/firstPathFails_expected create mode 100644 src/test/resources/branchTreeTests/reportTwoErrors/lastPathFails_expected 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/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/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/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/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 From 2a563d1fff73df14f1a66336c7d858e9545870cb Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Mon, 10 Mar 2025 11:57:02 +0100 Subject: [PATCH 39/39] Move BranchTree --- src/main/scala/{state => branchTree}/BranchTree.scala | 2 +- src/main/scala/supporters/MethodSupporter.scala | 4 ++-- src/test/scala/tests.scala | 1 - 3 files changed, 3 insertions(+), 4 deletions(-) rename src/main/scala/{state => branchTree}/BranchTree.scala (99%) diff --git a/src/main/scala/state/BranchTree.scala b/src/main/scala/branchTree/BranchTree.scala similarity index 99% rename from src/main/scala/state/BranchTree.scala rename to src/main/scala/branchTree/BranchTree.scala index c095f98a..7204ac3a 100644 --- a/src/main/scala/state/BranchTree.scala +++ b/src/main/scala/branchTree/BranchTree.scala @@ -1,4 +1,4 @@ -package viper.silicon.state.branchTree +package viper.silicon.branchTree import viper.silicon.common.io.PrintWriter import viper.silicon.verifier.Verifier diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index 1e01d3f1..604ce311 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/src/main/scala/supporters/MethodSupporter.scala @@ -10,13 +10,13 @@ import com.typesafe.scalalogging.Logger import viper.silver.ast import viper.silver.components.StatefulComponent import viper.silver.verifier.errors._ -import viper.silicon.interfaces.{Failure, _} +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} import viper.silicon.state.State.OldHeaps -import viper.silicon.state.branchTree.{Branch, BranchTree} import viper.silicon.verifier.{Verifier, VerifierComponent} import viper.silicon.utils.freshSnap import viper.silver.reporter.AnnotationWarning diff --git a/src/test/scala/tests.scala b/src/test/scala/tests.scala index a41a4363..35197277 100644 --- a/src/test/scala/tests.scala +++ b/src/test/scala/tests.scala @@ -9,7 +9,6 @@ import viper.silver.ast.Program import viper.silver.frontend.{DefaultStates, SilFrontend, SilFrontendConfig} import viper.silver.verifier.{AbstractError, AbstractVerificationError, VerificationResult, Verifier, Failure => SilFailure} import viper.silicon.Silicon -import viper.silver.reporter.Reporter package object tests { class DummyFrontend extends SilFrontend {