From 3f8ff57535c1a3cccdd5c7451e2c5469b7ac2451 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 23 Feb 2024 17:21:59 +0100 Subject: [PATCH] Use ordered set to track declared macros, avoid double-declarations --- src/main/scala/decider/Decider.scala | 29 +++++++++++++++------------- src/main/scala/rules/Brancher.scala | 8 +++++--- 2 files changed, 21 insertions(+), 16 deletions(-) diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala index 6f9814d33..88c483ad7 100644 --- a/src/main/scala/decider/Decider.scala +++ b/src/main/scala/decider/Decider.scala @@ -77,11 +77,11 @@ trait Decider { // states anyway (and Scala does not seem to have efficient order-preserving sets). ListSets are significantly // slower, so this tradeoff seems worth it. def freshFunctions: Set[FunctionDecl] - def freshMacros: Vector[MacroDecl] + def freshMacros: InsertionOrderedSet[MacroDecl] def declareAndRecordAsFreshFunctions(functions: Set[FunctionDecl], toStack: Boolean): Unit - def declareAndRecordAsFreshMacros(functions: Seq[MacroDecl], toStack: Boolean): Unit + def declareAndRecordAsFreshMacros(functions: InsertionOrderedSet[MacroDecl], toStack: Boolean): Unit def pushSymbolStack(): Unit - def popSymbolStack(): (Set[FunctionDecl], Seq[MacroDecl]) + def popSymbolStack(): (Set[FunctionDecl], InsertionOrderedSet[MacroDecl]) def setPcs(other: PathConditionStack): Unit def statistics(): Map[String, String] @@ -105,7 +105,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => private var pathConditions: PathConditionStack = _ private var _declaredFreshFunctions: Set[FunctionDecl] = _ /* [BRANCH-PARALLELISATION] */ - private var _declaredFreshMacros: Vector[MacroDecl] = _ + private var _declaredFreshMacros: InsertionOrderedSet[MacroDecl] = _ private var _freshFunctionStack: Stack[mutable.HashSet[FunctionDecl]] = _ private var _freshMacroStack: Stack[mutable.ListBuffer[MacroDecl]] = _ @@ -191,7 +191,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => def start(): Unit = { pathConditions = new LayeredPathConditionStack() _declaredFreshFunctions = if (Verifier.config.parallelizeBranches()) HashSet.empty else InsertionOrderedSet.empty /* [BRANCH-PARALLELISATION] */ - _declaredFreshMacros = Vector.empty + _declaredFreshMacros = InsertionOrderedSet.empty _freshMacroStack = Stack.empty _freshFunctionStack = Stack.empty createProver() @@ -201,7 +201,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => _prover.reset() pathConditions = new LayeredPathConditionStack() _declaredFreshFunctions = if (Verifier.config.parallelizeBranches()) HashSet.empty else InsertionOrderedSet.empty /* [BRANCH-PARALLELISATION] */ - _declaredFreshMacros = Vector.empty + _declaredFreshMacros = InsertionOrderedSet.empty _freshMacroStack = Stack.empty _freshFunctionStack = Stack.empty } @@ -359,7 +359,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => prover.declare(macroDecl) - _declaredFreshMacros = _declaredFreshMacros :+ macroDecl /* [BRANCH-PARALLELISATION] */ + _declaredFreshMacros = _declaredFreshMacros + macroDecl /* [BRANCH-PARALLELISATION] */ _freshMacroStack.foreach(l => l.append(macroDecl)) macroDecl @@ -406,7 +406,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => /* [BRANCH-PARALLELISATION] */ def freshFunctions: Set[FunctionDecl] = _declaredFreshFunctions - def freshMacros: Vector[MacroDecl] = _declaredFreshMacros + def freshMacros: InsertionOrderedSet[MacroDecl] = _declaredFreshMacros def declareAndRecordAsFreshFunctions(functions: Set[FunctionDecl], toSymbolStack: Boolean): Unit = { if (!toSymbolStack) { @@ -424,9 +424,12 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => } } - def declareAndRecordAsFreshMacros(macros: Seq[MacroDecl], toStack: Boolean): Unit = { + def declareAndRecordAsFreshMacros(macros: InsertionOrderedSet[MacroDecl], toStack: Boolean): Unit = { if (!toStack) { - macros foreach prover.declare + for (m <- macros) { + if (!_declaredFreshMacros.contains(m)) + prover.declare(m) + } _declaredFreshMacros = _declaredFreshMacros ++ macros } else { @@ -434,9 +437,9 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => if (!_declaredFreshMacros.contains(m)) prover.declare(m) - _declaredFreshMacros = _declaredFreshMacros.appended(m) _freshMacroStack.foreach(l => l.append(m)) } + _declaredFreshMacros = _declaredFreshMacros ++ macros } } @@ -445,10 +448,10 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => _freshMacroStack = _freshMacroStack.prepended(mutable.ListBuffer()) } - def popSymbolStack(): (Set[FunctionDecl], Seq[MacroDecl]) = { + def popSymbolStack(): (Set[FunctionDecl], InsertionOrderedSet[MacroDecl]) = { val funcDecls = _freshFunctionStack.head.toSet _freshFunctionStack = _freshFunctionStack.tail - val macroDecls = _freshMacroStack.head.toSeq + val macroDecls = InsertionOrderedSet(_freshMacroStack.head.toSeq) _freshMacroStack = _freshMacroStack.tail (funcDecls, macroDecls) } diff --git a/src/main/scala/rules/Brancher.scala b/src/main/scala/rules/Brancher.scala index 40afdbf78..0704df520 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 @@ -15,7 +17,7 @@ import viper.silicon.state.State import viper.silicon.state.terms.{FunctionDecl, MacroDecl, Not, Term} import viper.silicon.verifier.Verifier import viper.silver.ast -import viper.silver.reporter.{BranchFailureMessage} +import viper.silver.reporter.BranchFailureMessage import viper.silver.verifier.Failure trait BranchingRules extends SymbolicExecutionRules { @@ -84,12 +86,12 @@ object brancher extends BranchingRules { val uidBranchPoint = v.symbExLog.insertBranchPoint(2, Some(condition), conditionExp) var functionsOfCurrentDecider: Set[FunctionDecl] = null - var macrosOfCurrentDecider: Vector[MacroDecl] = null + var macrosOfCurrentDecider: InsertionOrderedSet[MacroDecl] = null var proverArgsOfCurrentDecider: viper.silicon.Map[String, String] = null var wasElseExecutedOnDifferentVerifier = false var functionsOfElseBranchDecider: Set[FunctionDecl] = null var proverArgsOfElseBranchDecider: viper.silicon.Map[String, String] = null - var macrosOfElseBranchDecider: Seq[MacroDecl] = null + var macrosOfElseBranchDecider: InsertionOrderedSet[MacroDecl] = null var pcsForElseBranch: PathConditionStack = null var noOfErrors = 0