Skip to content

Commit b737e36

Browse files
marcoeilersmarcoeilers
authored
Fix macro transfer between verifiers in parallel branch verification (#872)
1 parent 768a8b6 commit b737e36

3 files changed

Lines changed: 39 additions & 72 deletions

File tree

‎src/main/scala/decider/Decider.scala‎

Lines changed: 17 additions & 59 deletions
Original file line numberDiff line numberDiff line change
@@ -96,10 +96,8 @@ trait Decider {
9696
// slower, so this tradeoff seems worth it.
9797
def freshFunctions: Set[FunctionDecl]
9898
def freshMacros: Vector[MacroDecl]
99-
def declareAndRecordAsFreshFunctions(functions: Set[FunctionDecl], toStack: Boolean): Unit
100-
def declareAndRecordAsFreshMacros(functions: Seq[MacroDecl], toStack: Boolean): Unit
101-
def pushSymbolStack(): Unit
102-
def popSymbolStack(): (Set[FunctionDecl], Seq[MacroDecl])
99+
def declareAndRecordAsFreshFunctions(functions: Set[FunctionDecl]): Unit
100+
def declareAndRecordAsFreshMacros(functions: Seq[MacroDecl]): Unit
103101
def setPcs(other: PathConditionStack): Unit
104102

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

127125
private var _declaredFreshFunctions: Set[FunctionDecl] = _ /* [BRANCH-PARALLELISATION] */
128126
private var _declaredFreshMacros: Vector[MacroDecl] = _
129-
130-
private var _freshFunctionStack: Stack[mutable.HashSet[FunctionDecl]] = _
131-
private var _freshMacroStack: Stack[mutable.ListBuffer[MacroDecl]] = _
127+
private var _declaredFreshMacroNames: Set[String] = _ /* contains names of _declaredFreshMacros for faster lookup */
132128

133129
private var _proverOptions: Map[String, String] = Map.empty
134130
private var _proverResetOptions: Map[String, String] = Map.empty
135131
private val _debuggerAssumedTerms: mutable.Set[Term] = mutable.Set.empty
136-
137-
138-
//private val TODODELETEtermSources = mutable.Map.empty[Term, DebugExp]
139-
132+
140133
def functionDecls: Set[FunctionDecl] = _declaredFreshFunctions
141134
def macroDecls: Vector[MacroDecl] = _declaredFreshMacros
142135

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

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

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

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

471462
macroDecl
472463
}
@@ -504,7 +495,6 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
504495

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

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

517-
def declareAndRecordAsFreshFunctions(functions: Set[FunctionDecl], toSymbolStack: Boolean): Unit = {
518-
if (!toSymbolStack) {
519-
for (f <- functions) {
520-
if (!_declaredFreshFunctions.contains(f))
521-
prover.declare(f)
522-
523-
_declaredFreshFunctions = _declaredFreshFunctions + f
524-
}
525-
} else {
526-
for (f <- functions) {
527-
if (!_declaredFreshFunctions.contains(f))
528-
prover.declare(f)
529-
507+
def declareAndRecordAsFreshFunctions(functions: Set[FunctionDecl]): Unit = {
508+
for (f <- functions) {
509+
if (!_declaredFreshFunctions.contains(f)) {
510+
prover.declare(f)
530511
_declaredFreshFunctions = _declaredFreshFunctions + f
531-
_freshFunctionStack.foreach(s => s.add(f))
532512
}
533513
}
534514
}
535515

536-
def declareAndRecordAsFreshMacros(macros: Seq[MacroDecl], toStack: Boolean): Unit = {
537-
if (!toStack) {
538-
for (m <- macros) {
539-
if (!_declaredFreshMacros.contains(m)) {
540-
prover.declare(m)
541-
_declaredFreshMacros = _declaredFreshMacros.appended(m)
542-
}
543-
}
544-
} else {
545-
for (m <- macros) {
546-
if (!_declaredFreshMacros.contains(m)) {
547-
prover.declare(m)
548-
_declaredFreshMacros = _declaredFreshMacros.appended(m)
549-
}
550-
_freshMacroStack.foreach(l => l.append(m))
516+
def declareAndRecordAsFreshMacros(macros: Seq[MacroDecl]): Unit = {
517+
for (m <- macros) {
518+
if (!_declaredFreshMacroNames.contains(m.id.name)) {
519+
prover.declare(m)
520+
_declaredFreshMacros = _declaredFreshMacros.appended(m)
521+
_declaredFreshMacroNames = _declaredFreshMacroNames + m.id.name
551522
}
552523
}
553524
}
554525

555-
def pushSymbolStack(): Unit = {
556-
_freshFunctionStack = _freshFunctionStack.prepended(mutable.HashSet())
557-
_freshMacroStack = _freshMacroStack.prepended(mutable.ListBuffer())
558-
}
559-
560-
def popSymbolStack(): (Set[FunctionDecl], Seq[MacroDecl]) = {
561-
val funcDecls = _freshFunctionStack.head.toSet
562-
_freshFunctionStack = _freshFunctionStack.tail
563-
val macroDecls = _freshMacroStack.head.toSeq
564-
_freshMacroStack = _freshMacroStack.tail
565-
(funcDecls, macroDecls)
566-
}
567-
568526
/* Misc */
569527

570528
def statistics(): Map[String, String] = prover.statistics()

‎src/main/scala/rules/Brancher.scala‎

Lines changed: 21 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,8 @@
66

77
package viper.silicon.rules
88

9+
import viper.silicon.common.collections.immutable.InsertionOrderedSet
10+
911
import java.util.concurrent._
1012
import viper.silicon.common.concurrency._
1113
import viper.silicon.decider.PathConditionStack
@@ -18,6 +20,8 @@ import viper.silver.ast
1820
import viper.silver.reporter.BranchFailureMessage
1921
import viper.silver.verifier.Failure
2022

23+
import scala.collection.immutable.HashSet
24+
2125
trait BranchingRules extends SymbolicExecutionRules {
2226
def branch(s: State,
2327
condition: Term,
@@ -120,19 +124,18 @@ object brancher extends BranchingRules {
120124
// executing the else branch on a different verifier, need to adapt the state
121125
wasElseExecutedOnDifferentVerifier = true
122126

123-
if (s.underJoin)
124-
v0.decider.pushSymbolStack()
125127
val newFunctions = functionsOfCurrentDecider -- v0.decider.freshFunctions
126-
val newMacros = macrosOfCurrentDecider.diff(v0.decider.freshMacros)
128+
val v0FreshMacros = HashSet.from(v0.decider.freshMacros)
129+
val newMacros = macrosOfCurrentDecider.filter(m => !v0FreshMacros.contains(m))
127130

128131
v0.decider.prover.comment(s"[Shifting execution from ${v.uniqueId} to ${v0.uniqueId}]")
129132
proverArgsOfElseBranchDecider = v0.decider.getProverOptions()
130133
v0.decider.resetProverOptions()
131134
v0.decider.setProverOptions(proverArgsOfCurrentDecider)
132135
v0.decider.prover.comment(s"Bulk-declaring functions")
133-
v0.decider.declareAndRecordAsFreshFunctions(newFunctions, false)
136+
v0.decider.declareAndRecordAsFreshFunctions(newFunctions)
134137
v0.decider.prover.comment(s"Bulk-declaring macros")
135-
v0.decider.declareAndRecordAsFreshMacros(newMacros, false)
138+
v0.decider.declareAndRecordAsFreshMacros(newMacros)
136139

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

147-
if (v.uniqueId != v0.uniqueId)
150+
var functionsOfElseBranchdDeciderBefore: Set[FunctionDecl] = null
151+
var nMacrosOfElseBranchDeciderBefore: Int = 0
152+
153+
if (v.uniqueId != v0.uniqueId) {
148154
v1.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract)
155+
if (s.underJoin) {
156+
nMacrosOfElseBranchDeciderBefore = v1.decider.freshMacros.size
157+
functionsOfElseBranchdDeciderBefore = v1.decider.freshFunctions
158+
}
159+
}
149160

150161
val result = fElse(v1.stateConsolidator(s1).consolidateOptionally(s1, v1), v1)
151162
if (wasElseExecutedOnDifferentVerifier) {
152163
v1.decider.resetProverOptions()
153164
v1.decider.setProverOptions(proverArgsOfElseBranchDecider)
154165
if (s.underJoin) {
155-
val newSymbols = v1.decider.popSymbolStack()
156-
functionsOfElseBranchDecider = newSymbols._1
157-
macrosOfElseBranchDecider = newSymbols._2
166+
functionsOfElseBranchDecider = v1.decider.freshFunctions -- functionsOfElseBranchdDeciderBefore
167+
macrosOfElseBranchDecider = v1.decider.freshMacros.drop(nMacrosOfElseBranchDeciderBefore)
158168
}
159169
}
160170
result
@@ -243,10 +253,9 @@ object brancher extends BranchingRules {
243253

244254
v.decider.prover.comment(s"[To continue after join, adding else branch functions and macros to current verifier.]")
245255
v.decider.prover.comment(s"Bulk-declaring functions")
246-
v.decider.declareAndRecordAsFreshFunctions(functionsOfElseBranchDecider, true)
256+
v.decider.declareAndRecordAsFreshFunctions(functionsOfElseBranchDecider)
247257
v.decider.prover.comment(s"Bulk-declaring macros")
248-
// Declare macros without duplicates; we keep only the last occurrence of every declaration to avoid errors.
249-
v.decider.declareAndRecordAsFreshMacros(macrosOfElseBranchDecider.reverse.distinct.reverse, true)
258+
v.decider.declareAndRecordAsFreshMacros(macrosOfElseBranchDecider)
250259
}
251260
res
252261
}

‎src/main/scala/rules/Executor.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -275,7 +275,7 @@ object executor extends ExecutionRules {
275275
case (intermediateResult, (s1, pcs, ff1)) => /* [BRANCH-PARALLELISATION] ff1 */
276276
val s2 = s1.copy(invariantContexts = sLeftover.h +: s1.invariantContexts)
277277
intermediateResult combine executionFlowController.locally(s2, v1)((s3, v2) => {
278-
v2.decider.declareAndRecordAsFreshFunctions(ff1 -- v2.decider.freshFunctions, true) /* [BRANCH-PARALLELISATION] */
278+
v2.decider.declareAndRecordAsFreshFunctions(ff1 -- v2.decider.freshFunctions) /* [BRANCH-PARALLELISATION] */
279279
v2.decider.assume(pcs.assumptions, Option.when(withExp)(DebugExp.createInstance("Loop invariant", pcs.assumptionExps)), false)
280280
v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract)
281281
if (v2.decider.checkSmoke())

0 commit comments

Comments
 (0)
⚡