Add information required for LSP features to Parse AST

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

@@ -12,10 +12,13 @@ import java.nio.file.Path
 import viper.silver.parser.FastParser
 
 /** A trait describing the position of occurrence of an AST node. */
-sealed trait Position
+sealed trait Position {
+  def deltaColumn(delta: Int): Position
+}
 
 /** Describes ''no location'' for cases where a `Position` is expected, but not available. */
 case object NoPosition extends Position {
+  override def deltaColumn(delta: Int) = this
   override def toString = "<no position>"
 }
 
@@ -25,6 +28,13 @@ trait HasLineColumn extends Position {
 
   def column: Int
 
+  def <=(other: HasLineColumn): Boolean = {
+    if (line < other.line) true
+    else if (line > other.line) false
+    else column <= other.column
+  }
+
+  def deltaColumn(delta: Int): HasLineColumn
   override def toString = s"$line.$column"
 }
 
@@ -35,7 +45,9 @@ trait HasIdentifier extends HasLineColumn {
   def id: String
 }
 
-case class LineColumnPosition(line: Int, column: Int) extends HasLineColumn
+case class LineColumnPosition(line: Int, column: Int) extends HasLineColumn {
+  override def deltaColumn(delta: Int) = LineColumnPosition(line, column + delta)
+}
 
 /** Represents a source code position by referencing a file, a line and a column.
   * Optionally, an additional end position can be specified.
@@ -57,6 +69,7 @@ trait AbstractSourcePosition extends HasLineColumn {
   private def lineColComponent(lc_pos: HasLineColumn) =
     s"${lc_pos.line}.${lc_pos.column}"
 
+  override def deltaColumn(delta: Int): AbstractSourcePosition
   override def toString: String = end match {
     case None =>
       s"$fileComponent${lineColComponent(start)}"
@@ -79,12 +92,16 @@ object AbstractSourcePosition {
 class SourcePosition(val file: Path, val start: HasLineColumn, val end: Option[HasLineColumn])
   extends AbstractSourcePosition with StructuralEquality {
 
+  override def deltaColumn(delta: Int): SourcePosition =
+    new SourcePosition(file, start.deltaColumn(delta), end.map(_.deltaColumn(delta)))
   protected val equalityDefiningMembers: Seq[Object] =
     file :: start :: end :: Nil
 }
 
 class IdentifierPosition(val file: Path, val start: HasLineColumn, val end: Option[HasLineColumn], val id: String)
   extends AbstractSourcePosition with StructuralEquality with HasIdentifier {
+  override def deltaColumn(delta: Int): IdentifierPosition =
+    new IdentifierPosition(file, start.deltaColumn(delta), end.map(_.deltaColumn(delta)), id)
   protected val equalityDefiningMembers: Seq[Object] =
     file :: start :: end :: id :: Nil
 }
@@ -122,13 +139,19 @@ case class TranslatedPosition(pos: AbstractSourcePosition) extends AbstractSourc
   val file: Path = pos.file
   val start: HasLineColumn = pos.start
   val end: Option[HasLineColumn] = pos.end
+  override def deltaColumn(delta: Int): TranslatedPosition =
+    new TranslatedPosition(pos.deltaColumn(delta))
 }
 
 case class FilePosition(file: Path, vline: Int, col: Int) extends util.parsing.input.Position with HasLineColumn {
   override lazy val line: Int = vline
   override lazy val column: Int = col
   override lazy val lineContents: String = toString
   override lazy val toString: String = s"${file.getFileName}@$vline.$col"
+  override def deltaColumn(delta: Int): FilePosition = FilePosition(file, vline, col + delta)
+}
+object FilePosition {
+  def apply(pos: (Int, Int))(implicit file: Path): FilePosition = FilePosition(file, pos._1, pos._2)
 }
 
 /**
@@ -138,4 +161,5 @@ case class FilePosition(file: Path, vline: Int, col: Int) extends util.parsing.i
   */
 case class VirtualPosition(identifier: String) extends Position {
   override def toString: String = identifier
+  override def deltaColumn(delta: Int): VirtualPosition = this
 }

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

@@ -214,18 +214,20 @@ case class Program(domains: Seq[Domain], fields: Seq[Field], functions: Seq[Func
     }
 
     def checkNamesInScope(currentScope: Scope, dMap: immutable.HashMap[String, Declaration]) : Seq[ConsistencyError] = {
-      var declarationMap = dMap
+      var newMap = immutable.HashMap.empty[String, Declaration]
       var s: Seq[ConsistencyError] = Seq.empty[ConsistencyError]
       //check name declarations
       currentScope.scopedDecls.foreach(l=> {
         if(!Consistency.validUserDefinedIdentifier(l.name))
           s :+= ConsistencyError(s"${l.name} is not a valid identifier.", l.pos)
 
-        declarationMap.get(l.name) match {
-          case Some(_: Declaration) => s :+= ConsistencyError(s"Duplicate identifier ${l.name} found.", l.pos)
-          case None => declarationMap += (l.name -> l)
+        newMap.get(l.name) match {
+          case Some(_: Declaration) => s :+= ConsistencyError(s"Duplicate identifier `${l.name}` found.", l.pos)
+          case None => newMap += (l.name -> l)
         }
       })
+      // Override duplicate keys in old map
+      val declarationMap = dMap ++ newMap
 
       //check name uses
       Visitor.visitOpt(currentScope.asInstanceOf[Node], Nodes.subnodes){ n => {
@@ -268,7 +270,7 @@ case class Program(domains: Seq[Domain], fields: Seq[Field], functions: Seq[Func
 
   lazy val groundTypeInstances = DomainInstances.findNecessaryTypeInstances(this)
 
-  lazy val members: Seq[Member with Serializable] = domains ++ fields ++ functions ++ predicates ++ methods
+  val members: Seq[Member with Serializable] = domains ++ fields ++ functions ++ predicates ++ methods ++ extensions
 
   def findFieldOptionally(name: String): Option[Field] = this.fieldsByName.get(name)
 
@@ -409,11 +411,13 @@ case class Method(name: String, formalArgs: Seq[LocalVarDecl], formalReturns: Se
   }
 
   def deepCollectInBody[A](f: PartialFunction[Node, A]): Seq[A] = body match {
+    case null => Nil
+    case None => Nil
     case Some(actualBody) => actualBody.deepCollect(f)
-    case None => Seq()
   }
 
-  val scopedDecls: Seq[Declaration] = formalArgs ++ formalReturns
+  def labels: Seq[Label] = deepCollectInBody { case l: Label => l }
+  val scopedDecls: Seq[Declaration] = formalArgs ++ formalReturns ++ labels
 
   override lazy val check: Seq[ConsistencyError] =
     pres.flatMap(Consistency.checkPre) ++
@@ -444,19 +448,6 @@ case class Method(name: String, formalArgs: Seq[LocalVarDecl], formalReturns: Se
   def toCfg(simplify: Boolean = true, detect: Boolean = true): SilverCfg = CfgGenerator.methodToCfg(this, simplify, detect)
 }
 
-object MethodWithLabelsInScope {
-  def apply(name: String, formalArgs: Seq[LocalVarDecl], formalReturns: Seq[LocalVarDecl], pres: Seq[Exp], posts: Seq[Exp], body: Option[Seqn])
-                 (pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): Method = {
-    val newBody = body match {
-      case Some(actualBody) =>
-        val newScopedDecls = actualBody.scopedSeqnDeclarations ++ actualBody.deepCollect({case l: Label => l})
-        Some(actualBody.copy(scopedSeqnDeclarations = newScopedDecls)(actualBody.pos, actualBody.info, actualBody.errT))
-      case _ => body
-    }
-    Method(name, formalArgs, formalReturns, pres, posts, newBody)(pos, info, errT)
-  }
-}
-
 /** A function declaration */
 case class Function(name: String, formalArgs: Seq[LocalVarDecl], typ: Type, pres: Seq[Exp], posts: Seq[Exp], body: Option[Exp])(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Member with FuncLike with Contracted {
   override lazy val check : Seq[ConsistencyError] =
@@ -826,7 +817,7 @@ object BackendFunc {
 /**
   * The Extension Member trait provides the way to expand the Ast to include new Top Level declarations
   */
-trait ExtensionMember extends Member{
+trait ExtensionMember extends Member with Serializable {
   def extensionSubnodes: Seq[Node]
   def prettyPrint: PrettyPrintPrimitives#Cont
 }

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

@@ -29,7 +29,7 @@ object Consistency {
     recordIfNot(suspect, !property, message)
 
   /** Names that are not allowed for use in programs. */
-  def reservedNames: Set[String] = FastParserCompanion.basicKeywords
+  def reservedNames: Set[String] = FastParserCompanion.basicKeywords.map(_.keyword)
 
   /** Returns true iff the string `name` is a valid identifier. */
   val identFirstLetter = "[a-zA-Z$_]"
@@ -165,13 +165,15 @@ object Consistency {
     val argVars = args.map(_.localVar).toSet
     var s = Seq.empty[ConsistencyError]
 
-    for (a@LocalVarAssign(l, _) <- b if argVars.contains(l)) {
+    // Suppressing "pattern var a in value $anonfun is never used: use a wildcard `_` or suppress this warning with `a@_`" warning using `(true || a == a)`
+    for (a@LocalVarAssign(l, _) <- b if argVars.contains(l) && (true || a == a)) {
       s :+= ConsistencyError(s"$a is a reassignment of formal argument $l.", a.pos)
     }
     for (c@MethodCall(_, _, targets) <- b; t <- targets if argVars.contains(t)) {
       s :+= ConsistencyError(s"$c is a reassignment of formal argument $t.", c.pos)
     }
-    for (n@NewStmt(l, _) <- b if argVars.contains(l)){
+    // Suppressing "pattern var n in value $anonfun is never used: use a wildcard `_` or suppress this warning with `n@_`" warning using `(true || n == n)`
+    for (n@NewStmt(l, _) <- b if argVars.contains(l) && (true || n == n)) {
       s :+= ConsistencyError(s"$n is a reassignment of formal argument $l.", n.pos)
     }
     s

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

@@ -41,6 +41,8 @@ object Expressions {
          | _: MultisetExp
          | _: MapExp
          | _: ForPerm
+         | _: Exists
+         | _: Forall
       => true
   }
 

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

@@ -0,0 +1,17 @@
+package viper.silver.ast.utility
+
+import java.nio.file.Path
+import scala.io.Source
+import scala.util.{Using, Try}
+
+trait FileLoader {
+  def loadContent(path: Path): Try[String]
+}
+
+trait DiskLoader extends FileLoader {
+  override def loadContent(path: Path): Try[String] = {
+    Using(Source.fromFile(path.toFile()))(_.mkString)
+  }
+}
+
+object DiskLoader extends DiskLoader

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

@@ -141,9 +141,9 @@ object QuantifiedPermissions {
       val currentRoot = toVisit.dequeue()
 
       val relevantNodes: Seq[Node] = currentRoot match {
-        case m@Method(_, _, _, pres, posts, _) if m != root =>
+        case m: Method if m != root =>
           // use only specification of called methods
-          pres ++ posts
+          m.pres ++ m.posts
         case f@Function(_, _, _, pres, posts, _) if f != root =>
           // use only specification of called functions
           pres ++ posts

src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala

@@ -6,12 +6,18 @@
 
 package viper.silver.ast.utility.rewriter
 
-import viper.silver.parser.{PDomain, PDomainFunction, PFields, PFunction, PMethod, PPredicate}
-import viper.silver.parser.Transformer.ParseTreeDuplicationError
+import viper.silver.parser.PNode
 import viper.silver.ast.{AtomicType, BackendFuncApp, DomainFuncApp, ErrorTrafo, FuncApp, Info, Node, Position}
 
 import scala.reflect.runtime.{universe => reflection}
 
+trait HasExtraValList {
+  def getExtraVals: Seq[Any]
+}
+trait HasExtraVars {
+  def copyExtraVars(from: Any): Unit
+}
+
 /**
   * Trait Rewritable provides an interface that specifies which methods are required for the rewriter to work with.
   * For classes that implement product (especially case classes) everything is already implemented here and one only has to extend this base class
@@ -37,27 +43,26 @@ trait Rewritable extends Product {
         val constructorMirror = classMirror.reflectConstructor(constructorSymbol)
 
         // Add additional arguments to constructor call, besides children
-        var firstArgList = children
+        val firstArgList = children
         var secondArgList = Seq.empty[Any]
         import viper.silver.ast.{DomainType, DomainAxiom, FuncApp, DomainFunc, DomainFuncApp}
-        import viper.silver.parser.{PAxiom, PMagicWandExp, PNode, PDomainType}
         this match {
+          // TODO: remove the following cases by implementing `HasExtraValList` on the respective classes
           case dt: DomainType => secondArgList = Seq(dt.typeParameters)
           case da: DomainAxiom => secondArgList = Seq(da.pos, da.info, da.domainName, da.errT)
           case fa: FuncApp => secondArgList = Seq(fa.pos, fa.info, fa.typ, fa.errT)
           case df: DomainFunc => secondArgList = Seq(df.pos, df.info, df.domainName, df.errT)
           case df: DomainFuncApp => secondArgList = Seq(df.pos, df.info, df.typ, df.domainName, df.errT)
           case ba: BackendFuncApp => secondArgList = Seq(ba.pos, ba.info, ba.typ, ba.interpretation, ba.errT)
           case no: Node => secondArgList = no.getMetadata
-          case pa: PAxiom => secondArgList = Seq(pa.domainName) ++ Seq(pos.getOrElse(pa.pos), pa.annotations)
-          case pm: PMagicWandExp => firstArgList = Seq(children.head) ++ children.drop(2) ++ Seq(pos.getOrElse(pm.pos))
-          case pd: PDomainFunction => secondArgList = Seq(pd.domainName) ++ Seq(pos.getOrElse(pd.pos), pd.annotations)
-          case pd: PDomain => secondArgList = Seq(pos.getOrElse(pd.pos), pd.annotations)
-          case pm: PMethod => secondArgList = Seq(pos.getOrElse(pm.pos), pm.annotations)
-          case pp: PPredicate => secondArgList = Seq(pos.getOrElse(pp.pos), pp.annotations)
-          case pf: PFunction => secondArgList = Seq(pos.getOrElse(pf.pos), pf.annotations)
-          case pf: PFields => secondArgList = Seq(pos.getOrElse(pf.pos), pf.annotations)
-          case pn: PNode => secondArgList = Seq(pos.getOrElse(pn.pos))
+
+          case evl: HasExtraValList => {
+            secondArgList = evl.getExtraVals.map(ev => {
+              // Replace positions with the new one
+              val replace = pos.isDefined && ev.isInstanceOf[(_, _)] && ev.asInstanceOf[(_, _)]._1.isInstanceOf[Position] && ev.asInstanceOf[(_, _)]._2.isInstanceOf[Position]
+              if (replace) pos.get else ev
+            })
+          }
           case _ =>
         }
 
@@ -69,9 +74,9 @@ trait Rewritable extends Product {
         }
 
         // Copy member values, as they aren't in the parameters' list.
-        this match {
-          case dt: PDomainType =>
-            newNode.asInstanceOf[PDomainType].kind = dt.kind
+        newNode match {
+          case ev: HasExtraVars =>
+            ev.copyExtraVars(this)
           case _ =>
         }
 
@@ -116,4 +121,9 @@ trait Rewritable extends Product {
       newNode.asInstanceOf[this.type]
     }
   }
+
+  def initProperties(): Unit = ()
 }
+
+case class ParseTreeDuplicationError(original: PNode, newChildren: Seq[Any])
+    extends RuntimeException(s"Cannot duplicate $original with new children $newChildren")

src/main/scala/viper/silver/ast/utility/rewriter/Strategy.scala

@@ -356,6 +356,7 @@ class Strategy[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag, C
       case Traverse.Innermost => rewriteInnermost(node, contextUsed)
     }
     changed = !(result eq node)
+    result.initProperties()
     result
   }
 
@@ -424,6 +425,8 @@ class Strategy[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag, C
           rewriteTopDown(t5, context)).asInstanceOf[A]
 
         case Some(value) => Some(rewriteTopDown(value, context)).asInstanceOf[A]
+        case Left(value) => Left(rewriteTopDown(value, context)).asInstanceOf[A]
+        case Right(value) => Right(rewriteTopDown(value, context)).asInstanceOf[A]
 
         case node: N @unchecked =>
           // Rewrite node and context
@@ -477,6 +480,8 @@ class Strategy[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag, C
           rewriteBottomUp(t5, context)).asInstanceOf[A]
 
         case Some(value) => Some(rewriteBottomUp(value, context)).asInstanceOf[A]
+        case Left(value) => Left(rewriteBottomUp(value, context)).asInstanceOf[A]
+        case Right(value) => Right(rewriteBottomUp(value, context)).asInstanceOf[A]
 
         case node: N @unchecked =>
           val c = context.addAncestor(node).asInstanceOf[C]
@@ -528,6 +533,8 @@ class Strategy[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag, C
           rewriteInnermost(t5, context)).asInstanceOf[A]
 
         case Some(value) => Some(rewriteInnermost(value, context)).asInstanceOf[A]
+        case Left(value) => Left(rewriteInnermost(value, context)).asInstanceOf[A]
+        case Right(value) => Right(rewriteInnermost(value, context)).asInstanceOf[A]
 
         case node: N @unchecked =>
           // Rewrite node and context
@@ -595,12 +602,14 @@ class RepeatedStrategy[N <: Rewritable](s: StrategyInterface[N]) extends Strateg
     * @return rewritten root
     */
   override def execute[T <: N](node: N): T = {
-    val result: T = s.execute[T](node)
-    if (!s.hasChanged) {
-      result
-    } else {
-      execute[T](result)
+    var result: T = s.execute[T](node)
+    var j = 1
+    while (s.hasChanged) {
+      result = s.execute[T](result)
+      j += 1
+      assert(j < 10000, "Infinite loop detected")
     }
+    result
   }
 
   /**
@@ -616,12 +625,13 @@ class RepeatedStrategy[N <: Rewritable](s: StrategyInterface[N]) extends Strateg
       node
     }
     else {
-      val result = s.execute[T](node)
-      if (s.hasChanged) {
-        result
-      } else {
-        execute[T](result, i - 1)
+      var result: T = s.execute[T](node)
+      var j = 1
+      while (s.hasChanged && j < i) {
+        result = s.execute[T](result)
+        j += 1
       }
+      result
     }
   }