Skip to content

Commit

Permalink
Store trees & move class
Browse files Browse the repository at this point in the history
  • Loading branch information
@7i6ht
7i6ht committed Jan 30, 2025
1 parent 8c16f3d commit 1d7424d
Show file tree
Hide file tree
Showing 7 changed files with 256 additions and 122 deletions.
14 changes: 12 additions & 2 deletions src/main/scala/decider/Decider.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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 = {
Expand Down
13 changes: 12 additions & 1 deletion src/main/scala/decider/PathConditions.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
*/
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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()
}
Expand Down
160 changes: 54 additions & 106 deletions src/main/scala/rules/Brancher.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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) {

Expand Down
9 changes: 8 additions & 1 deletion src/main/scala/rules/Consumer.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
8 changes: 1 addition & 7 deletions src/main/scala/rules/SymbolicExecutionRules.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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()){
Expand Down
Loading

0 comments on commit 1d7424d

Please sign in to comment.