From 1d7424d89528d7ba11480fe67d86b76d318c23a4 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Thu, 30 Jan 2025 16:24:21 +0100 Subject: [PATCH] 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 fbf93b066..6b2a90b87 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 de38c28cd..017838618 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 3c2885e9a..8ea4c9b67 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 fd3e34b94..9ce2e66cd 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 6f18728d5..eb3873ab2 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 000000000..751ffb7ca --- /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 b395ed213..a3dd7d882 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}"