Avoid linear lookups in a Program (fixes #657)

Author: fpoli

src/main/scala/viper/silver/ast/Program.scala

@@ -21,6 +21,13 @@ import scala.reflect.ClassTag
 case class Program(domains: Seq[Domain], fields: Seq[Field], functions: Seq[Function], predicates: Seq[Predicate], methods: Seq[Method], extensions: Seq[ExtensionMember])(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos)
   extends Node with DependencyAware with Positioned with Infoed with Scope with TransformableErrors {
 
+  lazy val domainsByName: Map[String, Domain] = domains.map(x => (x.name, x)).toMap
+  lazy val domainFunctionsByName: Map[String, DomainFunc] = domains.flatMap(_.functions).map(x => (x.name, x)).toMap
+  lazy val fieldsByName: Map[String, Field] = fields.map(x => (x.name, x)).toMap
+  lazy val functionsByName: Map[String, Function] = functions.map(x => (x.name, x)).toMap
+  lazy val predicatesByName: Map[String, Predicate] = predicates.map(x => (x.name, x)).toMap
+  lazy val methodsByName: Map[String, Method] = methods.map(x => (x.name, x)).toMap
+
   val scopedDecls: Seq[Declaration] =
     domains ++ fields ++ functions ++ predicates ++ methods ++ extensions ++
     domains.flatMap(d => {(d.axioms.filter(_.isInstanceOf[NamedDomainAxiom])).asInstanceOf[Seq[NamedDomainAxiom]] ++ d.functions})
@@ -48,7 +55,7 @@ case class Program(domains: Seq[Domain], fields: Seq[Field], functions: Seq[Func
       case None => /* Nothing to do */
       case Some(actualBody) =>
         for (c@MethodCall(name, args, targets) <- actualBody) {
-          methods.find(_.name == name) match {
+          findMethodOptionally(name) match {
             case Some(existingMethod) =>
               if(!Consistency.areAssignable(existingMethod.formalReturns, targets))
                 s :+= ConsistencyError(s"Formal returns ${existingMethod.formalReturns} of method $name are not assignable to targets $targets.", c.pos)
@@ -69,8 +76,7 @@ case class Program(domains: Seq[Domain], fields: Seq[Field], functions: Seq[Func
     var errors = Seq.empty[ConsistencyError]
 
     def check(loc: PredicateAccess, pos: Position): Unit = {
-      predicates
-        .find(_.name == loc.predicateName)
+      findPredicateOptionally(loc.predicateName)
         .foreach(predicate => {
           if (predicate.body.isEmpty)
             errors :+= ConsistencyError(s"Cannot unfold $loc because ${loc.predicateName}  is abstract.", pos)
@@ -93,7 +99,7 @@ case class Program(domains: Seq[Domain], fields: Seq[Field], functions: Seq[Func
     var s = Seq.empty[ConsistencyError]
 
     for (funcApp@FuncApp(name, args) <- this) {
-      this.findFunctionOptionally(name) match {
+      findFunctionOptionally(name) match {
         case None => // Consistency error already reported by checkIdentifiers
         case Some(funcDef) => {
           if (!Consistency.areAssignable(args, funcDef.formalArgs)) {
@@ -121,7 +127,7 @@ case class Program(domains: Seq[Domain], fields: Seq[Field], functions: Seq[Func
     var s = Seq.empty[ConsistencyError]
 
     for (predAcc@PredicateAccess(args, name) <- this) {
-      this.findPredicateOptionally(name) match {
+      findPredicateOptionally(name) match {
         case None => // Consistency error already reported by checkIdentifiers
         case Some(predDef) => {
           if (!Consistency.areAssignable(args, predDef.formalArgs)) {
@@ -145,7 +151,7 @@ case class Program(domains: Seq[Domain], fields: Seq[Field], functions: Seq[Func
     var s = Seq.empty[ConsistencyError]
 
     for (funcApp@DomainFuncApp(name, args, typVarMap) <- this) {
-      this.findDomainFunctionOptionally(name) match {
+      findDomainFunctionOptionally(name) match {
         case None => s :+= ConsistencyError(s"No domain function named $name found in the program.", funcApp.pos)
         case Some(funcDef) => {
           if (!Consistency.areAssignable(args, funcDef.formalArgs map {
@@ -264,21 +270,25 @@ case class Program(domains: Seq[Domain], fields: Seq[Field], functions: Seq[Func
 
   lazy val members: Seq[Member with Serializable] = domains ++ fields ++ functions ++ predicates ++ methods
 
+  def findFieldOptionally(name: String): Option[Field] = this.fieldsByName.get(name)
+
   def findField(name: String): Field = {
-    this.fields.find(_.name == name) match {
+    findFieldOptionally(name) match {
       case Some(f) => f
       case None => sys.error("Field name " + name + " not found in program.")
     }
   }
 
+  def findMethodOptionally(name: String): Option[Method] = this.methodsByName.get(name)
+
   def findMethod(name: String): Method = {
-    this.methods.find(_.name == name) match {
+    findMethodOptionally(name) match {
       case Some(m) => m
       case None => sys.error("Method name " + name + " not found in program.")
     }
   }
 
-  def findFunctionOptionally(name: String): Option[Function] = this.functions.find(_.name == name)
+  def findFunctionOptionally(name: String): Option[Function] = this.functionsByName.get(name)
 
   def findFunction(name: String): Function = {
     findFunctionOptionally(name) match {
@@ -287,23 +297,25 @@ case class Program(domains: Seq[Domain], fields: Seq[Field], functions: Seq[Func
     }
   }
 
-  def findPredicateOptionally(name: String): Option[Predicate] = this.predicates.find(_.name == name)
+  def findPredicateOptionally(name: String): Option[Predicate] = this.predicatesByName.get(name)
 
   def findPredicate(name: String): Predicate = {
-    this.predicates.find(_.name == name) match {
+    findPredicateOptionally(name) match {
       case Some(p) => p
       case None => sys.error("Predicate name " + name + " not found in program.")
     }
   }
 
+  def findDomainOptionally(name: String): Option[Domain] = this.domainsByName.get(name)
+
   def findDomain(name: String): Domain = {
-    this.domains.find(_.name == name) match {
+    findDomainOptionally(name) match {
       case Some(d) => d
       case None => sys.error("Domain name " + name + " not found in program.")
     }
   }
 
-  def findDomainFunctionOptionally(name: String): Option[DomainFunc] = this.domains.flatMap(_.functions).find(_.name == name)
+  def findDomainFunctionOptionally(name: String): Option[DomainFunc] = this.domainFunctionsByName.get(name)
 
   def findDomainFunction(name: String): DomainFunc = {
     findDomainFunctionOptionally(name) match {
@@ -583,7 +595,7 @@ object Substitution{
 }
 /** Domain function which is not a binary or unary operator. */
 case class DomainFunc(name: String, formalArgs: Seq[AnyLocalVarDecl], typ: Type, unique: Boolean = false, interpretation: Option[String] = None)
-                     (val pos: Position = NoPosition, val info: Info = NoInfo,val domainName : String, val errT: ErrorTrafo = NoTrafos)
+                     (val pos: Position = NoPosition, val info: Info = NoInfo, val domainName: String, val errT: ErrorTrafo = NoTrafos)
                       extends AbstractDomainFunc with DomainMember with Declaration {
   override lazy val check : Seq[ConsistencyError] =
     if (unique && formalArgs.nonEmpty) Seq(ConsistencyError("Only constants, i.e. nullary domain functions can be unique.", pos)) else Seq()

src/main/scala/viper/silver/ast/utility/Consistency.scala

@@ -357,7 +357,7 @@ object Consistency {
         c
 
       case dt: DomainType =>
-        c.program.domains.find(_.name == dt.domainName) match {
+        c.program.findDomainOptionally(dt.domainName) match {
           case None =>
             s :+= ConsistencyError(s"DomainType references non-existent domain ${dt.domainName}.", NoPosition)
             c
@@ -368,7 +368,7 @@ object Consistency {
         }
 
       case bt: BackendType =>
-        c.program.domains.find(_.name == bt.viperName) match {
+        c.program.findDomainOptionally(bt.viperName) match {
           case None =>
             s :+= ConsistencyError(s"BackendType references non-existent domain ${bt.viperName}.", NoPosition)
             c

src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala

@@ -58,7 +58,7 @@ class PredicateInstancePlugin(@unused reporter: viper.silver.reporter.Reporter,
    * (to the respective predicate instance functions)
    */
   override def beforeVerify(input: Program): Program = {
-    val PredicateInstanceDomain: Option[Domain] =  input.domains.find(_.name == "PredicateInstance")
+    val PredicateInstanceDomain: Option[Domain] =  input.findDomainOptionally("PredicateInstance")
 
     // list of all created predicate instance functions
     var createdPIFunctions = ListMap[String, Function]()

src/main/scala/viper/silver/plugin/standard/termination/transformation/MethodCheck.scala

@@ -19,7 +19,7 @@ import viper.silver.verifier.errors.AssertFailed
 trait MethodCheck extends ProgramManager with DecreasesCheck with NestedPredicates with ErrorReporter {
 
   private def getMethodDecreasesSpecification(method: String): DecreasesSpecification = {
-    program.methods.find(_.name == method) match {
+    program.findMethodOptionally(method) match {
       case Some(f) => DecreasesSpecification.fromNode(f)
       case None => DecreasesSpecification()
     }