diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala index d4d8afe3..fbf93b06 100644 --- a/src/main/scala/decider/Decider.scala +++ b/src/main/scala/decider/Decider.scala @@ -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] @@ -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 @@ -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) } @@ -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 } @@ -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 } @@ -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 } @@ -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() diff --git a/src/main/scala/rules/Brancher.scala b/src/main/scala/rules/Brancher.scala index 62b18d43..444c6118 100644 --- a/src/main/scala/rules/Brancher.scala +++ b/src/main/scala/rules/Brancher.scala @@ -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 @@ -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, @@ -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) @@ -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 @@ -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 } diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index d07c1e5f..a19e85d6 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -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())