Skip to content

Commit

Permalink
Merge pull request #730 from viperproject/meilers_more_joins
Browse files Browse the repository at this point in the history 
Add experimental --moreJoins option
  • Loading branch information
@marcoeilers
marcoeilers authored Oct 18, 2023
2 parents 36c611f + e785d26 commit 1e3e961
Show file tree
Hide file tree
Showing 11 changed files with 610 additions and 124 deletions.
6 changes: 6 additions & 0 deletions src/main/scala/Config.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -656,6 +656,12 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
noshort = true
)

val moreJoins: ScallopOption[Boolean] = opt[Boolean]("moreJoins",
descr = "Enable more joins using a more complete implementation of state merging.",
default = Some(false),
noshort = true
)

val exhaleModeOption: ScallopOption[ExhaleMode] = opt[ExhaleMode]("exhaleMode",
descr = "Exhale mode. Options are 0 (greedy, default), 1 (more complete exhale), 2 (more complete exhale on demand).",
default = None,
Expand Down
82 changes: 64 additions & 18 deletions src/main/scala/decider/Decider.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ import viper.silicon.verifier.{Verifier, VerifierComponent}
import viper.silver.reporter.{ConfigurationConfirmation, InternalWarningMessage}

import scala.collection.immutable.HashSet
import scala.collection.mutable

/*
* Interfaces
Expand Down Expand Up @@ -73,8 +74,10 @@ trait Decider {
// slower, so this tradeoff seems worth it.
def freshFunctions: Set[FunctionDecl]
def freshMacros: Vector[MacroDecl]
def declareAndRecordAsFreshFunctions(functions: Set[FunctionDecl]): Unit
def declareAndRecordAsFreshMacros(functions: Vector[MacroDecl]): Unit
def declareAndRecordAsFreshFunctions(functions: Set[FunctionDecl], toStack: Boolean): Unit
def declareAndRecordAsFreshMacros(functions: Seq[MacroDecl], toStack: Boolean): Unit
def pushSymbolStack(): Unit
def popSymbolStack(): (Set[FunctionDecl], Seq[MacroDecl])
def setPcs(other: PathConditionStack): Unit

def statistics(): Map[String, String]
Expand All @@ -97,8 +100,11 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
private var _prover: Prover = _
private var pathConditions: PathConditionStack = _

private var _freshFunctions: Set[FunctionDecl] = _ /* [BRANCH-PARALLELISATION] */
private var _freshMacros: Vector[MacroDecl] = _
private var _declaredFreshFunctions: Set[FunctionDecl] = _ /* [BRANCH-PARALLELISATION] */
private var _declaredFreshMacros: Vector[MacroDecl] = _

private var _freshFunctionStack: Stack[mutable.HashSet[FunctionDecl]] = _
private var _freshMacroStack: Stack[mutable.ListBuffer[MacroDecl]] = _

def prover: Prover = _prover

Expand Down Expand Up @@ -163,16 +169,20 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>

def start(): Unit = {
pathConditions = new LayeredPathConditionStack()
_freshFunctions = if (Verifier.config.parallelizeBranches()) HashSet.empty else InsertionOrderedSet.empty /* [BRANCH-PARALLELISATION] */
_freshMacros = Vector.empty
_declaredFreshFunctions = if (Verifier.config.parallelizeBranches()) HashSet.empty else InsertionOrderedSet.empty /* [BRANCH-PARALLELISATION] */
_declaredFreshMacros = Vector.empty
_freshMacroStack = Stack.empty
_freshFunctionStack = Stack.empty
createProver()
}

def reset(): Unit = {
_prover.reset()
pathConditions = new LayeredPathConditionStack()
_freshFunctions = if (Verifier.config.parallelizeBranches()) HashSet.empty else InsertionOrderedSet.empty /* [BRANCH-PARALLELISATION] */
_freshMacros = Vector.empty
_declaredFreshFunctions = if (Verifier.config.parallelizeBranches()) HashSet.empty else InsertionOrderedSet.empty /* [BRANCH-PARALLELISATION] */
_declaredFreshMacros = Vector.empty
_freshMacroStack = Stack.empty
_freshFunctionStack = Stack.empty
}

def stop(): Unit = {
Expand Down Expand Up @@ -328,7 +338,8 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>

prover.declare(macroDecl)

_freshMacros = _freshMacros :+ macroDecl /* [BRANCH-PARALLELISATION] */
_declaredFreshMacros = _declaredFreshMacros :+ macroDecl /* [BRANCH-PARALLELISATION] */
_freshMacroStack.foreach(l => l.append(macroDecl))

macroDecl
}
Expand Down Expand Up @@ -364,26 +375,61 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
HeapDepFun(proverFun.id, proverFun.argSorts, proverFun.resultSort).asInstanceOf[F]
}

_freshFunctions = _freshFunctions + FunctionDecl(fun) /* [BRANCH-PARALLELISATION] */
val decl = FunctionDecl(fun)
_declaredFreshFunctions = _declaredFreshFunctions + decl /* [BRANCH-PARALLELISATION] */
_freshFunctionStack.foreach(s => s.add(decl))

fun
}


/* [BRANCH-PARALLELISATION] */
def freshFunctions: Set[FunctionDecl] = _freshFunctions
def freshMacros: Vector[MacroDecl] = _freshMacros
def freshFunctions: Set[FunctionDecl] = _declaredFreshFunctions
def freshMacros: Vector[MacroDecl] = _declaredFreshMacros

def declareAndRecordAsFreshFunctions(functions: Set[FunctionDecl], toSymbolStack: Boolean): Unit = {
if (!toSymbolStack) {
functions foreach prover.declare

def declareAndRecordAsFreshFunctions(functions: Set[FunctionDecl]): Unit = {
functions foreach prover.declare
_declaredFreshFunctions = _declaredFreshFunctions ++ functions
} else {
for (f <- functions) {
if (!_declaredFreshFunctions.contains(f))
prover.declare(f)

_freshFunctions = _freshFunctions ++ functions
_declaredFreshFunctions = _declaredFreshFunctions + f
_freshFunctionStack.foreach(s => s.add(f))
}
}
}

def declareAndRecordAsFreshMacros(macros: Vector[MacroDecl]): Unit = {
macros foreach prover.declare
def declareAndRecordAsFreshMacros(macros: Seq[MacroDecl], toStack: Boolean): Unit = {
if (!toStack) {
macros foreach prover.declare

_declaredFreshMacros = _declaredFreshMacros ++ macros
} else {
for (m <- macros) {
if (!_declaredFreshMacros.contains(m))
prover.declare(m)

_declaredFreshMacros = _declaredFreshMacros.appended(m)
_freshMacroStack.foreach(l => l.append(m))
}
}
}

def pushSymbolStack(): Unit = {
_freshFunctionStack = _freshFunctionStack.prepended(mutable.HashSet())
_freshMacroStack = _freshMacroStack.prepended(mutable.ListBuffer())
}

_freshMacros = _freshMacros ++ macros
def popSymbolStack(): (Set[FunctionDecl], Seq[MacroDecl]) = {
val funcDecls = _freshFunctionStack.head.toSet
_freshFunctionStack = _freshFunctionStack.tail
val macroDecls = _freshMacroStack.head.toSeq
_freshMacroStack = _freshMacroStack.tail
(funcDecls, macroDecls)
}

/* Misc */
Expand Down
33 changes: 29 additions & 4 deletions src/main/scala/rules/Brancher.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ object brancher extends BranchingRules {
|| skipPathFeasibilityCheck
|| !v.decider.check(condition, Verifier.config.checkTimeout()))

val parallelizeElseBranch = s.parallelizeBranches && !s.underJoin && executeThenBranch && executeElseBranch
val parallelizeElseBranch = s.parallelizeBranches && executeThenBranch && executeElseBranch

// val additionalPaths =
// if (executeThenBranch && exploreFalseBranch) 1
Expand All @@ -85,7 +85,11 @@ object brancher extends BranchingRules {
val uidBranchPoint = v.symbExLog.insertBranchPoint(2, Some(condition), conditionExp)
var functionsOfCurrentDecider: Set[FunctionDecl] = null
var macrosOfCurrentDecider: Vector[MacroDecl] = null
var wasElseExecutedOnDifferentVerifier = false
var functionsOfElseBranchDecider: Set[FunctionDecl] = null
var macrosOfElseBranchDecider: Seq[MacroDecl] = null
var pcsForElseBranch: PathConditionStack = null
var noOfErrors = 0

val elseBranchVerificationTask: Verifier => VerificationResult =
if (executeElseBranch) {
Expand All @@ -101,6 +105,7 @@ object brancher extends BranchingRules {
functionsOfCurrentDecider = v.decider.freshFunctions
macrosOfCurrentDecider = v.decider.freshMacros
pcsForElseBranch = v.decider.pcs.duplicate()
noOfErrors = v.errorsReportedSoFar.get()
}

(v0: Verifier) => {
Expand All @@ -109,18 +114,22 @@ object brancher extends BranchingRules {
if (v.uniqueId != v0.uniqueId){
/* [BRANCH-PARALLELISATION] */
// executing the else branch on a different verifier, need to adapt the state
wasElseExecutedOnDifferentVerifier = true

if (s.underJoin)
v0.decider.pushSymbolStack()
val newFunctions = functionsOfCurrentDecider -- v0.decider.freshFunctions
val newMacros = macrosOfCurrentDecider.diff(v0.decider.freshMacros)

v0.decider.prover.comment(s"[Shifting execution from ${v.uniqueId} to ${v0.uniqueId}]")
v0.decider.prover.comment(s"Bulk-declaring functions")
v0.decider.declareAndRecordAsFreshFunctions(newFunctions)
v0.decider.declareAndRecordAsFreshFunctions(newFunctions, false)
v0.decider.prover.comment(s"Bulk-declaring macros")
v0.decider.declareAndRecordAsFreshMacros(newMacros)
v0.decider.declareAndRecordAsFreshMacros(newMacros, false)

v0.decider.prover.comment(s"Taking path conditions from source verifier ${v.uniqueId}")
v0.decider.setPcs(pcsForElseBranch)
v0.errorsReportedSoFar.set(noOfErrors)
}
elseBranchVerifier = v0.uniqueId

Expand All @@ -131,7 +140,13 @@ object brancher extends BranchingRules {
if (v.uniqueId != v0.uniqueId)
v1.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract)

fElse(v1.stateConsolidator.consolidateIfRetrying(s1, v1), v1)
val result = fElse(v1.stateConsolidator.consolidateIfRetrying(s1, v1), v1)
if (wasElseExecutedOnDifferentVerifier && s.underJoin) {
val newSymbols = v1.decider.popSymbolStack()
functionsOfElseBranchDecider = newSymbols._1
macrosOfElseBranchDecider = newSymbols._2
}
result
})
}
} else {
Expand Down Expand Up @@ -179,6 +194,7 @@ object brancher extends BranchingRules {
try {
if (parallelizeElseBranch) {
val pcsAfterThenBranch = v.decider.pcs.duplicate()
val noOfErrorsAfterThenBranch = v.errorsReportedSoFar.get()

val pcsBefore = v.decider.pcs

Expand All @@ -188,6 +204,7 @@ object brancher extends BranchingRules {
// 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)
}
}else{
Expand All @@ -209,6 +226,14 @@ object brancher extends BranchingRules {

}, alwaysWaitForOther = parallelizeElseBranch)
v.symbExLog.endBranchPoint(uidBranchPoint)
if (wasElseExecutedOnDifferentVerifier && s.underJoin) {

v.decider.prover.comment(s"[To continue after join, adding else branch functions and macros to current verifier.]")
v.decider.prover.comment(s"Bulk-declaring functions")
v.decider.declareAndRecordAsFreshFunctions(functionsOfElseBranchDecider, true)
v.decider.prover.comment(s"Bulk-declaring macros")
v.decider.declareAndRecordAsFreshMacros(macrosOfElseBranchDecider, true)
}
res
}
}
4 changes: 2 additions & 2 deletions src/main/scala/rules/ChunkSupporter.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -222,8 +222,8 @@ object chunkSupporter extends ChunkSupportRules {
: VerificationResult = {

val id = ChunkIdentifier(resource, s.program)

findChunk[NonQuantifiedChunk](h.values, id, args, v) match {
val findRes = findChunk[NonQuantifiedChunk](h.values, id, args, v)
findRes match {
case Some(ch) if v.decider.check(IsPositive(ch.perm), Verifier.config.checkTimeout()) =>
Q(s, ch.snap, v)
case _ if v.decider.checkSmoke(true) =>
Expand Down
57 changes: 57 additions & 0 deletions src/main/scala/rules/Consumer.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -183,6 +183,11 @@ object consumer extends ConsumptionRules {
v.logger.debug("hR = " + s.reserveHeaps.map(v.stateFormatter.format).mkString("", ",\n ", ""))

val consumed = a match {
case imp @ ast.Implies(e0, a0) if !a.isPure && s.moreJoins =>
val impliesRecord = new ImpliesRecord(imp, s, v.decider.pcs, "consume")
val uidImplies = v.symbExLog.openScope(impliesRecord)
consumeConditionalTlcMoreJoins(s, h, e0, a0, None, uidImplies, pve, v)(Q)

case imp @ ast.Implies(e0, a0) if !a.isPure =>
val impliesRecord = new ImpliesRecord(imp, s, v.decider.pcs, "consume")
val uidImplies = v.symbExLog.openScope(impliesRecord)
Expand All @@ -198,6 +203,11 @@ object consumer extends ConsumptionRules {
Q(s2, h, Unit, v2)
}))

case ite @ ast.CondExp(e0, a1, a2) if !a.isPure && s.moreJoins =>
val condExpRecord = new CondExpRecord(ite, s, v.decider.pcs, "consume")
val uidCondExp = v.symbExLog.openScope(condExpRecord)
consumeConditionalTlcMoreJoins(s, h, e0, a1, Some(a2), uidCondExp, pve, v)(Q)

case ite @ ast.CondExp(e0, a1, a2) if !a.isPure =>
val condExpRecord = new CondExpRecord(ite, s, v.decider.pcs, "consume")
val uidCondExp = v.symbExLog.openScope(condExpRecord)
Expand Down Expand Up @@ -453,6 +463,53 @@ object consumer extends ConsumptionRules {
consumed
}

private def consumeConditionalTlcMoreJoins(s: State, h: Heap, e0: ast.Exp, a1: ast.Exp, a2: Option[ast.Exp], scopeUid: Int,
pve: PartialVerificationError, v: Verifier)
(Q: (State, Heap, Term, Verifier) => VerificationResult)
: VerificationResult = {
eval(s, e0, pve, v)((s1, t0, v1) =>
joiner.join[(Heap, Term), (Heap, Term)](s1, v1, resetState = false)((s1, v1, QB) => {
branch(s1.copy(parallelizeBranches = false), t0, Some(e0), v1)(
(s2, v2) =>
consumeR(s2.copy(parallelizeBranches = s1.parallelizeBranches), h, a1, pve, v2)((s3, h1, t1, v3) => {
v3.symbExLog.closeScope(scopeUid)
QB(s3, (h1, t1), v3)
}),
(s2, v2) =>
a2 match {
case Some(a2) => consumeR(s2.copy(parallelizeBranches = s1.parallelizeBranches), h, a2, pve, v2)((s3, h1, t1, v3) => {
v3.symbExLog.closeScope(scopeUid)
QB(s3, (h1, t1), v3)
})
case None =>
v2.symbExLog.closeScope(scopeUid)
QB(s2.copy(parallelizeBranches = s1.parallelizeBranches), (h, Unit), v2)
})
})(entries => {
val s2 = entries match {
case Seq(entry) => // One branch is dead
(entry.s, entry.data)
case Seq(entry1, entry2) => // Both branches are alive
val mergedData = (
State.mergeHeap(
entry1.data._1, And(entry1.pathConditions.branchConditions),
entry2.data._1, And(entry2.pathConditions.branchConditions),
),
// Asume that entry1.pcs is inverse of entry2.pcs
Ite(And(entry1.pathConditions.branchConditions), entry1.data._2, entry2.data._2)
)
(entry1.pathConditionAwareMerge(entry2, v1), mergedData)
case _ =>
sys.error(s"Unexpected join data entries: $entries")
}
s2
})((s4, data, v4) => {
Q(s4, data._1, data._2, v4)
})
)
}


private def evalAndAssert(s: State, e: ast.Exp, pve: PartialVerificationError, v: Verifier)
(Q: (State, Term, Verifier) => VerificationResult)
: VerificationResult = {
Expand Down
Loading

0 comments on commit 1e3e961

Please sign in to comment.