Skip to content

Faster NameAnalyser implementation #631

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

Merged
marcoeilers merged 4 commits into from
Nov 30, 2022
Merged

Faster NameAnalyser implementation #631

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
66cac20
Attempt to make the resolver faster
marcoeilers Nov 29, 2022
bbe025e
Analyzing top level declarations first, then bodies.
marcoeilers Nov 30, 2022
7cac3b3
Rewrote to avoid flag
marcoeilers Nov 30, 2022
4980de4
Merge branch 'master' into meilers_faster_resolver
marcoeilers Nov 30, 2022
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
2 changes: 2 additions & 0 deletions src/main/scala/viper/silver/ast/Program.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -484,6 +484,8 @@ case class Function(name: String, formalArgs: Seq[LocalVarDecl], typ: Type, pres

def isAbstract = body.isEmpty

lazy val isPure = pres.forall(_.isPure)

override def isValid : Boolean /* Option[Message] */ = this match {
case _ if (for (e <- pres ++ posts) yield e.contains[MagicWand]).contains(true) => false
case _ if (for (e <- body) yield e.contains[MagicWand]).contains(true) => false
Expand Down
106 changes: 41 additions & 65 deletions src/main/scala/viper/silver/parser/Resolver.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@
package viper.silver.parser

import viper.silver.FastMessaging
import viper.silver.ast.utility.Visitor
import viper.silver.ast.{LabelledOld, MagicWandOp}

import scala.collection.mutable
Expand Down Expand Up @@ -857,6 +856,9 @@ case class NameAnalyser() {
n match {
case d: PDeclaration =>
getMap(d).get(d.idndef.name) match {
case Some(m: PMember) if d eq m =>
// We re-encountered a member we already looked at in the previous run.
// This is expected, nothing to do.
case Some(e: PDeclaration) =>
messages ++= FastMessaging.message(e.idndef, "Duplicate identifier `" + e.idndef.name + "' at " + e.idndef.pos._1 + " and at " + d.idndef.pos._1)
case Some(_: PErrorEntity) =>
Expand All @@ -870,6 +872,22 @@ case class NameAnalyser() {
getMap(d).put(d.idndef.name, d)
}
}
case i@PIdnUse(name) =>
// look up in both maps (if we are not in a method currently, we look in the same map twice, but that is ok)
getCurrentMap.getOrElse(name, globalDeclarationMap.getOrElse(name, PUnknownEntity())) match {
case PUnknownEntity() =>
// domain types can also be type variables, which need not be declared
// goto and state labels may exist out of scope (but must exist in method, this is checked in final AST in checkIdentifiers)
if (i.parent.isDefined) {
val parent = i.parent.get
if (!parent.isInstanceOf[PDomainType] && !parent.isInstanceOf[PGoto] &&
!(parent.isInstanceOf[PLabelledOld] && i == parent.asInstanceOf[PLabelledOld].label) &&
!(name == LabelledOld.LhsOldLabel && parent.isInstanceOf[PLabelledOld])) {
messages ++= FastMessaging.message(i, s"identifier $name not defined.")
}
}
case _ =>
}
case _ =>
}

Expand All @@ -892,6 +910,7 @@ case class NameAnalyser() {
n match {
case _: PDeclaration => true
case _: PScope => true
case _: PIdnUse => true
case _ => target.isDefined
}
}
Expand All @@ -913,74 +932,31 @@ case class NameAnalyser() {
}
}

def containsSubnodeBefore(container: PNode, toFind: PNode, before: PNode) : Boolean = {
var beforeFound = false
val pred = new PartialFunction[PNode, PNode] {
def isDefinedAt(node: PNode): Boolean = {
if (!beforeFound){
if (node eq before){
beforeFound = true
}
}
(node eq toFind) && node != container && !beforeFound
n match {
case prog: PProgram =>
// find all global names first
for (d <- prog.domains) {
nodeDownNameCollectorVisitor(d)
d.funcs.foreach(f => {nodeDownNameCollectorVisitor(f); nodeUpNameCollectorVisitor(f)})
nodeUpNameCollectorVisitor(d)
}
prog.fields.foreach(f => f.visit(nodeDownNameCollectorVisitor,nodeUpNameCollectorVisitor))
prog.functions.foreach(f => {nodeDownNameCollectorVisitor(f); nodeUpNameCollectorVisitor(f)})
prog.predicates.foreach(f => {nodeDownNameCollectorVisitor(f); nodeUpNameCollectorVisitor(f)})
prog.methods.foreach(m => {nodeDownNameCollectorVisitor(m); nodeUpNameCollectorVisitor(m)})
prog.extensions.foreach(e => e.visit(nodeDownNameCollectorVisitor,nodeUpNameCollectorVisitor))

// now completely walk through all axioms, functions, predicates, and methods
prog.domains.foreach(d => d.visit(nodeDownNameCollectorVisitor,nodeUpNameCollectorVisitor))
prog.functions.foreach(f => f.visit(nodeDownNameCollectorVisitor,nodeUpNameCollectorVisitor))
prog.predicates.foreach(f => f.visit(nodeDownNameCollectorVisitor,nodeUpNameCollectorVisitor))
prog.methods.foreach(m => m.visit(nodeDownNameCollectorVisitor,nodeUpNameCollectorVisitor))

def apply(node: PNode) = node
}
Visitor.existsDefined(container, Nodes.subnodes)(pred)
}

def getContainingMethod(node : PNode) : Option[PMethod] = {
node match {
case null => None
case method : PMethod => Some(method)
case nonMethod =>
nonMethod.parent match {
case Some(parentNode) => getContainingMethod(parentNode)
case None => None
}
}
case _ =>
// find all declarations
n.visit(nodeDownNameCollectorVisitor,nodeUpNameCollectorVisitor)
}

// find all declarations
n.visit(nodeDownNameCollectorVisitor,nodeUpNameCollectorVisitor)
clearUniversalDeclarationsMap()
/* Check all identifier uses. */
n.visit({
case m: PScope =>
scopeStack.push(curMember)
curMember = m
case i@PIdnUse(name) =>
// look up in both maps (if we are not in a method currently, we look in the same map twice, but that is ok)
getCurrentMap.getOrElse(name, globalDeclarationMap.getOrElse(name, PUnknownEntity())) match {
case PUnknownEntity() =>
// domain types can also be type variables, which need not be declared
// goto and state labels may exist out of scope (but must exist in method, this is checked in final AST in checkIdentifiers)
if (i.parent.isDefined) {
val parent = i.parent.get
if (!parent.isInstanceOf[PDomainType] && !parent.isInstanceOf[PGoto] &&
!(parent.isInstanceOf[PLabelledOld] && i==parent.asInstanceOf[PLabelledOld].label) &&
!(name == LabelledOld.LhsOldLabel && parent.isInstanceOf[PLabelledOld])) {
messages ++= FastMessaging.message(i, s"identifier $name not defined.")
}
}
case localVar : PLocalVarDecl =>
getContainingMethod(localVar) match {
case Some(PMethod(_, _, _, _, _, Some(actualBody))) =>
// Variables must not be used before they are declared
if (containsSubnodeBefore(actualBody, i, localVar)){
messages ++= FastMessaging.message(i, s"local variable $name cannot be accessed before it is declared.")
}
case _ =>
}
case _ =>
}
case _ =>
}, {
case _: PScope =>
curMember = scopeStack.pop()
case _ =>
})
}

def run(p: PProgram): Boolean = {
Expand Down
⚡