Skip to content

Commit

Permalink
Fix macro transfer between verifiers in parallel branch verification (#…
Browse files Browse the repository at this point in the history 
…872)
  • Loading branch information
@marcoeilers
marcoeilers authored Sep 17, 2024
1 parent 768a8b6 commit b737e36
Show file tree
Hide file tree
Showing 3 changed files with 39 additions and 72 deletions.
76 changes: 17 additions & 59 deletions src/main/scala/decider/Decider.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -96,10 +96,8 @@ trait Decider {
// slower, so this tradeoff seems worth it.
def freshFunctions: Set[FunctionDecl]
def freshMacros: Vector[MacroDecl]
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 declareAndRecordAsFreshFunctions(functions: Set[FunctionDecl]): Unit
def declareAndRecordAsFreshMacros(functions: Seq[MacroDecl]): Unit
def setPcs(other: PathConditionStack): Unit

def statistics(): Map[String, String]
Expand All @@ -126,17 +124,12 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>

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]] = _
private var _declaredFreshMacroNames: Set[String] = _ /* contains names of _declaredFreshMacros for faster lookup */

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


//private val TODODELETEtermSources = mutable.Map.empty[Term, DebugExp]


def functionDecls: Set[FunctionDecl] = _declaredFreshFunctions
def macroDecls: Vector[MacroDecl] = _declaredFreshMacros

Expand Down Expand Up @@ -221,8 +214,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
pathConditions = new LayeredPathConditionStack()
_declaredFreshFunctions = if (Verifier.config.parallelizeBranches()) HashSet.empty else InsertionOrderedSet.empty /* [BRANCH-PARALLELISATION] */
_declaredFreshMacros = Vector.empty
_freshMacroStack = Stack.empty
_freshFunctionStack = Stack.empty
_declaredFreshMacroNames = HashSet.empty
createProver(Verifier.config.prover(), Verifier.config.proverArgs)
}

Expand All @@ -231,8 +223,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
pathConditions = new LayeredPathConditionStack()
_declaredFreshFunctions = if (Verifier.config.parallelizeBranches()) HashSet.empty else InsertionOrderedSet.empty /* [BRANCH-PARALLELISATION] */
_declaredFreshMacros = Vector.empty
_freshMacroStack = Stack.empty
_freshFunctionStack = Stack.empty
_declaredFreshMacroNames = HashSet.empty
_proverOptions = Map.empty
}

Expand Down Expand Up @@ -466,7 +457,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
prover.declare(macroDecl)

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

macroDecl
}
Expand Down Expand Up @@ -504,7 +495,6 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>

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

fun
}
Expand All @@ -514,57 +504,25 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
def freshFunctions: Set[FunctionDecl] = _declaredFreshFunctions
def freshMacros: Vector[MacroDecl] = _declaredFreshMacros

def declareAndRecordAsFreshFunctions(functions: Set[FunctionDecl], toSymbolStack: Boolean): Unit = {
if (!toSymbolStack) {
for (f <- functions) {
if (!_declaredFreshFunctions.contains(f))
prover.declare(f)

_declaredFreshFunctions = _declaredFreshFunctions + f
}
} else {
for (f <- functions) {
if (!_declaredFreshFunctions.contains(f))
prover.declare(f)

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

def declareAndRecordAsFreshMacros(macros: Seq[MacroDecl], toStack: Boolean): Unit = {
if (!toStack) {
for (m <- macros) {
if (!_declaredFreshMacros.contains(m)) {
prover.declare(m)
_declaredFreshMacros = _declaredFreshMacros.appended(m)
}
}
} else {
for (m <- macros) {
if (!_declaredFreshMacros.contains(m)) {
prover.declare(m)
_declaredFreshMacros = _declaredFreshMacros.appended(m)
}
_freshMacroStack.foreach(l => l.append(m))
def declareAndRecordAsFreshMacros(macros: Seq[MacroDecl]): Unit = {
for (m <- macros) {
if (!_declaredFreshMacroNames.contains(m.id.name)) {
prover.declare(m)
_declaredFreshMacros = _declaredFreshMacros.appended(m)
_declaredFreshMacroNames = _declaredFreshMacroNames + m.id.name
}
}
}

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

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 */

def statistics(): Map[String, String] = prover.statistics()
Expand Down
33 changes: 21 additions & 12 deletions src/main/scala/rules/Brancher.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,8 @@

package viper.silicon.rules

import viper.silicon.common.collections.immutable.InsertionOrderedSet

import java.util.concurrent._
import viper.silicon.common.concurrency._
import viper.silicon.decider.PathConditionStack
Expand All @@ -18,6 +20,8 @@ import viper.silver.ast
import viper.silver.reporter.BranchFailureMessage
import viper.silver.verifier.Failure

import scala.collection.immutable.HashSet

trait BranchingRules extends SymbolicExecutionRules {
def branch(s: State,
condition: Term,
Expand Down Expand Up @@ -120,19 +124,18 @@ object brancher extends BranchingRules {
// 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)
val v0FreshMacros = HashSet.from(v0.decider.freshMacros)
val newMacros = macrosOfCurrentDecider.filter(m => !v0FreshMacros.contains(m))

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

v0.decider.prover.comment(s"Taking path conditions from source verifier ${v.uniqueId}")
v0.decider.setPcs(pcsForElseBranch)
Expand All @@ -144,17 +147,24 @@ object brancher extends BranchingRules {
v1.decider.prover.comment(s"[else-branch: $cnt | $negatedCondition]")
v1.decider.setCurrentBranchCondition(negatedCondition, (negatedConditionExp, negatedConditionExpNew))

if (v.uniqueId != v0.uniqueId)
var functionsOfElseBranchdDeciderBefore: Set[FunctionDecl] = null
var nMacrosOfElseBranchDeciderBefore: Int = 0

if (v.uniqueId != v0.uniqueId) {
v1.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract)
if (s.underJoin) {
nMacrosOfElseBranchDeciderBefore = v1.decider.freshMacros.size
functionsOfElseBranchdDeciderBefore = v1.decider.freshFunctions
}
}

val result = fElse(v1.stateConsolidator(s1).consolidateOptionally(s1, v1), v1)
if (wasElseExecutedOnDifferentVerifier) {
v1.decider.resetProverOptions()
v1.decider.setProverOptions(proverArgsOfElseBranchDecider)
if (s.underJoin) {
val newSymbols = v1.decider.popSymbolStack()
functionsOfElseBranchDecider = newSymbols._1
macrosOfElseBranchDecider = newSymbols._2
functionsOfElseBranchDecider = v1.decider.freshFunctions -- functionsOfElseBranchdDeciderBefore
macrosOfElseBranchDecider = v1.decider.freshMacros.drop(nMacrosOfElseBranchDeciderBefore)
}
}
result
Expand Down Expand Up @@ -243,10 +253,9 @@ object brancher extends BranchingRules {

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.declareAndRecordAsFreshFunctions(functionsOfElseBranchDecider)
v.decider.prover.comment(s"Bulk-declaring macros")
// Declare macros without duplicates; we keep only the last occurrence of every declaration to avoid errors.
v.decider.declareAndRecordAsFreshMacros(macrosOfElseBranchDecider.reverse.distinct.reverse, true)
v.decider.declareAndRecordAsFreshMacros(macrosOfElseBranchDecider)
}
res
}
Expand Down
2 changes: 1 addition & 1 deletion src/main/scala/rules/Executor.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -275,7 +275,7 @@ object executor extends ExecutionRules {
case (intermediateResult, (s1, pcs, ff1)) => /* [BRANCH-PARALLELISATION] ff1 */
val s2 = s1.copy(invariantContexts = sLeftover.h +: s1.invariantContexts)
intermediateResult combine executionFlowController.locally(s2, v1)((s3, v2) => {
v2.decider.declareAndRecordAsFreshFunctions(ff1 -- v2.decider.freshFunctions, true) /* [BRANCH-PARALLELISATION] */
v2.decider.declareAndRecordAsFreshFunctions(ff1 -- v2.decider.freshFunctions) /* [BRANCH-PARALLELISATION] */
v2.decider.assume(pcs.assumptions, Option.when(withExp)(DebugExp.createInstance("Loop invariant", pcs.assumptionExps)), false)
v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract)
if (v2.decider.checkSmoke())
Expand Down

0 comments on commit b737e36

Please sign in to comment.