Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Use ordered set to track declared macros, avoid double-declarations #807

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Use ordered set to track declared macros, avoid double-declarations #807

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 16 additions & 13 deletions src/main/scala/decider/Decider.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand All @@ -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]] = _
Expand Down Expand Up @@ -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()
Expand All @@ -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
}
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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) {
Expand All @@ -424,19 +424,22 @@ 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)
}
Comment on lines +429 to +432
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am bit afraid that using InsertionOrderedSet may hurt performance quite a lot. From what I gathered, this data structure is very inneficient and this may hurt us if the lists are very big.

I wonder if we really are making use of the fact that _declaredFreshMacros only stores once each value. If that is not necessary, could we keep the implementation using a vector and keep this check? ((!_declaredFreshMacros.contains(m)))

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure the Vectors will do much better; checking many times if a vector contains a specific value isn't going to be efficient either, right. We just need a good InsertionOrderedSet implementation. But I made a PR for now to just add perform the check.


_declaredFreshMacros = _declaredFreshMacros ++ macros
} else {
for (m <- macros) {
if (!_declaredFreshMacros.contains(m))
prover.declare(m)

_declaredFreshMacros = _declaredFreshMacros.appended(m)
_freshMacroStack.foreach(l => l.append(m))
}
_declaredFreshMacros = _declaredFreshMacros ++ macros
}
}

Expand All @@ -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)
}
Expand Down
8 changes: 5 additions & 3 deletions src/main/scala/rules/Brancher.scala
View file
Open in desktop
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 @@ -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 {
Expand Down Expand Up @@ -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

Expand Down
Loading