Fix macro transfer between verifiers in parallel branch verification

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()

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
   }

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())