From 06850e831af2f41fb3583ae4685894a17fc78b7d Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 20 Jul 2022 20:52:10 +0200
Subject: [PATCH 01/11] Attempting to remove global state from parser

---
 .../scala/viper/silver/ast/Position.scala     |   4 +-
 .../silver/ast/utility/Consistency.scala      |   4 +-
 src/main/scala/viper/silver/cfg/CfgTest.scala |   2 +-
 .../viper/silver/frontend/SilFrontend.scala   |   5 +-
 .../viper/silver/parser/FastParser.scala      | 155 ++++++++++--------
 .../viper/silver/verifier/ModelParser.scala   |   2 +-
 6 files changed, 95 insertions(+), 77 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/Position.scala b/src/main/scala/viper/silver/ast/Position.scala
index 11146cf32..82c143232 100644
--- a/src/main/scala/viper/silver/ast/Position.scala
+++ b/src/main/scala/viper/silver/ast/Position.scala
@@ -89,10 +89,10 @@ class IdentifierPosition(val file: Path, val start: HasLineColumn, val end: Opti
     file :: start :: end :: id :: Nil
 }
 
-object LineCol {
+class LineCol(fp: FastParser) {
   def apply(index: Int): (Int, Int) = {
     // val Array(line, col) = ctx.input.prettyIndex(index).split(":").map(_.toInt)
-    val line_offset = FastParser._line_offset
+    val line_offset = fp._line_offset
     val result = java.util.Arrays.binarySearch(line_offset, index)
     if (result >= 0) {
       // Exact match
diff --git a/src/main/scala/viper/silver/ast/utility/Consistency.scala b/src/main/scala/viper/silver/ast/utility/Consistency.scala
index 6cf495175..00c8eefe4 100644
--- a/src/main/scala/viper/silver/ast/utility/Consistency.scala
+++ b/src/main/scala/viper/silver/ast/utility/Consistency.scala
@@ -8,7 +8,7 @@ package viper.silver.ast.utility
 
 import viper.silver.ast._
 import viper.silver.ast.utility.rewriter.Traverse
-import viper.silver.parser.FastParser
+import viper.silver.parser.{FastParser, FastParserCompanion}
 import viper.silver.verifier.ConsistencyError
 import viper.silver.{FastMessage, FastMessaging}
 
@@ -29,7 +29,7 @@ object Consistency {
     recordIfNot(suspect, !property, message)
 
   /** Names that are not allowed for use in programs. */
-  def reservedNames: Seq[String] = FastParser.keywords.toSeq
+  def reservedNames: Seq[String] = FastParserCompanion.keywords.toSeq
 
   /** Returns true iff the string `name` is a valid identifier. */
   val identFirstLetter = "[a-zA-Z$_]"
diff --git a/src/main/scala/viper/silver/cfg/CfgTest.scala b/src/main/scala/viper/silver/cfg/CfgTest.scala
index a07866420..f68961b83 100644
--- a/src/main/scala/viper/silver/cfg/CfgTest.scala
+++ b/src/main/scala/viper/silver/cfg/CfgTest.scala
@@ -36,7 +36,7 @@ object CfgTest {
   }
 
   private def parse[_: P](input: String, file: Path): Option[PProgram] = {
-    val result = FastParser.parse(input, file)
+    val result = new FastParser().parse(input, file)
     result match {
       case Parsed.Success(program@PProgram(_, _, _, _, _, _, _,_, errors), _) =>
         if (errors.isEmpty || errors.forall(_.isInstanceOf[ParseWarning])) Some(program)
diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala
index 29c2138ec..f3a3a827c 100644
--- a/src/main/scala/viper/silver/frontend/SilFrontend.scala
+++ b/src/main/scala/viper/silver/frontend/SilFrontend.scala
@@ -233,7 +233,8 @@ trait SilFrontend extends DefaultFrontend {
     val file = _inputFile.get
     _plugins.beforeParse(input, isImported = false) match {
       case Some(inputPlugin) =>
-        val result = FastParser.parse(inputPlugin, file, Some(_plugins))
+        val fp = new FastParser()
+        val result = fp.parse(inputPlugin, file, Some(_plugins))
           result match {
             case Parsed.Success(e@ PProgram(_, _, _, _, _, _, _, _, err_list), _) =>
               if (err_list.isEmpty || err_list.forall(p => p.isInstanceOf[ParseWarning])) {
@@ -243,7 +244,7 @@ trait SilFrontend extends DefaultFrontend {
               else Fail(err_list)
             case fail @ Parsed.Failure(_, index, extra) =>
               val msg = fail.trace().longAggregateMsg
-              val (line, col) = LineCol(index)
+              val (line, col) = fp.lineCol(index)
               Fail(List(ParseError(s"Expected $msg", SourcePosition(file, line, col))))
             //? val pos = extra.input.prettyIndex(index).split(":").map(_.toInt)
               //? Fail(List(ParseError(s"Expected $msg", SourcePosition(file, pos(0), pos(1)))))
diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index 15d616c2e..4b56bc42c 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -8,8 +8,11 @@ package viper.silver.parser
 
 import java.net.URL
 import java.nio.file.{Files, Path, Paths}
+
+import fastparse.{CharsWhile, Implicits, NoTrace, NoWhitespace, P, ParsingRun, Pass, StringIn}
 import viper.silver.ast.{FilePosition, LabelledOld, LineCol, NoPosition, Position, SourcePosition}
 import viper.silver.ast.utility.rewriter.{ContextA, PartialContextC, StrategyBuilder}
+import viper.silver.parser.FastParserCompanion.{LW, LeadingWhitespace}
 import viper.silver.parser.Transformer.ParseTreeDuplicationError
 import viper.silver.plugin.SilverPluginManager
 import viper.silver.verifier.{ParseError, ParseWarning}
@@ -23,7 +26,7 @@ case class SuffixedExpressionGenerator[E <: PExp](func: PExp => E) extends (PExp
   override def apply(v1: PExp): E = func(v1)
 }
 
-object FastParser {
+object FastParserCompanion {
   import fastparse._
 
   implicit val whitespace = {
@@ -32,6 +35,83 @@ object FastParser {
       NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
   }
 
+  class LeadingWhitespace[T](val p: () => P[T]) extends AnyVal {
+    /**
+      * Using `p.lw` is shorthand for `Pass ~ p` (the same parser but with possibly leading whitespace).
+      *
+      * A parser of the form `FP(p0 ~ p1.?)` or `FP(p0 ~ p2.rep)` may return an end position which
+      * includes trailing whitespaces (incl. comments, newlines) if `p1` or `p2` fail to match (the `~` does this).
+      * Instead we would like to use `FP(p0 ~~ (Pass ~ p1).?)` or `FP(p0 ~~ (Pass ~ p2).rep)`, which avoids this issue.
+      */
+    def lw(implicit ctx: P[Any]): LW[T] = new LW(() => Pass ~ p())
+    def ~~~[V, R](other: LW[V])(implicit s: Implicits.Sequencer[T, V, R], ctx: P[Any]): P[R] = (p() ~~ other.p()).asInstanceOf[P[R]]
+    def ~~~/[V, R](other: LW[V])(implicit s: Implicits.Sequencer[T, V, R], ctx: P[Any]): P[R] = (p() ~~/ other.p()).asInstanceOf[P[R]]
+  }
+  /**
+    * A parser which matches leading whitespaces. See `LeadingWhitespace.lw` for more info. Can only be operated on in
+    * restricted ways (e.g. `?`, `rep`, `|` or `map`), requiring that it is eventually appened to a normal parser (of type `P[V]`).
+    *
+    * For example, the following two are equivalent:
+    * {{{FP("hello" ~~~ "world".lw.?)
+    * FP("hello" ~~ (Pass ~ "world").?)}}}
+    * The type system prevents one from erroneously writing:
+    * {{{FP("hello" ~ "world".lw.?)}}}
+    */
+  class LW[T](val p: () => P[T]) {
+    def ?[V](implicit optioner: Implicits.Optioner[T, V], ctx: P[Any]): LW[V] = new LW(() => p().?.asInstanceOf[P[V]])
+    def rep[V](implicit repeater: Implicits.Repeater[T, V], ctx: P[Any]): LW[V] = new LW(() => p().rep.asInstanceOf[P[V]])
+    def |[V >: T](other: LW[V])(implicit ctx: P[Any]): LW[V] = new LW(() => (p() | other.p()).asInstanceOf[P[V]])
+    def map[V](f: T => V): LW[V] = new LW(() => p().map(f))
+  }
+
+  lazy val keywords = Set("result",
+    // types
+    "Int", "Perm", "Bool", "Ref", "Rational",
+    // boolean constants
+    "true", "false",
+    // null
+    "null",
+    // preamble importing
+    "import",
+    // declaration keywords
+    "method", "function", "predicate", "program", "domain", "axiom", "var", "returns", "field", "define",
+    // specifications
+    "requires", "ensures", "invariant",
+    // statements
+    "fold", "unfold", "inhale", "exhale", "new", "assert", "assume", "package", "apply",
+    // control flow
+    "while", "if", "elseif", "else", "goto", "label",
+    // sequences
+    "Seq",
+    // sets and multisets
+    "Set", "Multiset", "union", "intersection", "setminus", "subset",
+    // maps
+    "Map", "range",
+    // prover hint expressions
+    "unfolding", "in", "applying",
+    // old expression
+    "old", "lhs",
+    // other expressions
+    "let",
+    // quantification
+    "forall", "exists", "forperm",
+    // permission syntax
+    "acc", "wildcard", "write", "none", "epsilon", "perm",
+    // modifiers
+    "unique") | ParserExtension.extendedKeywords
+}
+
+class FastParser {
+  import fastparse._
+
+  implicit val whitespace = {
+    import NoWhitespace._
+    implicit ctx: ParsingRun[_] =>
+      NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
+  }
+
+  val lineCol = new LineCol(this)
+
   /* When importing a file from standard library, e.g. `include <inc.vpr>`, the file is expected
    * to be located in `resources/${standard_import_directory}`, e.g. `resources/import/inv.vpr`.
    */
@@ -183,43 +263,16 @@ object FastParser {
     * Function that wraps a parser to provide start and end positions if the wrapped parser succeeds.
     */
   def FP[T](t: => P[T])(implicit ctx: P[_]): P[((FilePosition, FilePosition), T)] = {
-    val startPos = LineCol(ctx.index)
+    val startPos = lineCol.apply(ctx.index)
     val res: P[T] = t
-    val finishPos = LineCol(ctx.index)
+    val finishPos = lineCol.apply(ctx.index)
     res.map({ parsed => ((FilePosition(_file, startPos._1, startPos._2), FilePosition(_file, finishPos._1, finishPos._2)), parsed) })
   }
 
   import scala.language.implicitConversions
   implicit def LeadingWhitespaceStr(p: String)(implicit ctx: P[Any]): LeadingWhitespace[Unit] = new LeadingWhitespace(() => P(p))
   implicit def LeadingWhitespace[T](p: => P[T]) = new LeadingWhitespace(() => p)
-  class LeadingWhitespace[T](val p: () => P[T]) extends AnyVal {
-  /**
-    * Using `p.lw` is shorthand for `Pass ~ p` (the same parser but with possibly leading whitespace).
-    *
-    * A parser of the form `FP(p0 ~ p1.?)` or `FP(p0 ~ p2.rep)` may return an end position which
-    * includes trailing whitespaces (incl. comments, newlines) if `p1` or `p2` fail to match (the `~` does this).
-    * Instead we would like to use `FP(p0 ~~ (Pass ~ p1).?)` or `FP(p0 ~~ (Pass ~ p2).rep)`, which avoids this issue.
-    */
-    def lw(implicit ctx: P[Any]): LW[T] = new LW(() => Pass ~ p())
-    def ~~~[V, R](other: LW[V])(implicit s: Implicits.Sequencer[T, V, R], ctx: P[Any]): P[R] = (p() ~~ other.p()).asInstanceOf[P[R]]
-    def ~~~/[V, R](other: LW[V])(implicit s: Implicits.Sequencer[T, V, R], ctx: P[Any]): P[R] = (p() ~~/ other.p()).asInstanceOf[P[R]]
-  }
-  /**
-    * A parser which matches leading whitespaces. See `LeadingWhitespace.lw` for more info. Can only be operated on in
-    * restricted ways (e.g. `?`, `rep`, `|` or `map`), requiring that it is eventually appened to a normal parser (of type `P[V]`).
-    * 
-    * For example, the following two are equivalent:
-    * {{{FP("hello" ~~~ "world".lw.?)
-    * FP("hello" ~~ (Pass ~ "world").?)}}}
-    * The type system prevents one from erroneously writing:
-    * {{{FP("hello" ~ "world".lw.?)}}}
-    */
-  class LW[T](val p: () => P[T]) {
-    def ?[V](implicit optioner: Implicits.Optioner[T, V], ctx: P[Any]): LW[V] = new LW(() => p().?.asInstanceOf[P[V]])
-    def rep[V](implicit repeater: Implicits.Repeater[T, V], ctx: P[Any]): LW[V] = new LW(() => p().rep.asInstanceOf[P[V]])
-    def |[V >: T](other: LW[V])(implicit ctx: P[Any]): LW[V] = new LW(() => (p() | other.p()).asInstanceOf[P[V]])
-    def map[V](f: T => V): LW[V] = new LW(() => p().map(f))
-  }
+
 
   // Actual Parser starts from here
   def identContinues[_: P] = CharIn("0-9", "A-Z", "a-z", "$_")
@@ -264,7 +317,7 @@ object FastParser {
       case fastparse.Parsed.Success(prog, _) => prog
       case fail @ fastparse.Parsed.Failure(_, index, _) =>
         val msg = fail.trace().longMsg
-        val (line, col) = LineCol(index)
+        val (line, col) = lineCol.apply(index)
         throw ParseException(s"Expected $msg", FilePosition(path, line, col))
     }
   }
@@ -732,42 +785,6 @@ object FastParser {
   /** The file we are currently parsing (for creating positions later). */
   def file: Path = _file
 
-  lazy val keywords = Set("result",
-    // types
-    "Int", "Perm", "Bool", "Ref", "Rational",
-    // boolean constants
-    "true", "false",
-    // null
-    "null",
-    // preamble importing
-    "import",
-    // declaration keywords
-    "method", "function", "predicate", "program", "domain", "axiom", "var", "returns", "field", "define",
-    // specifications
-    "requires", "ensures", "invariant",
-    // statements
-    "fold", "unfold", "inhale", "exhale", "new", "assert", "assume", "package", "apply",
-    // control flow
-    "while", "if", "elseif", "else", "goto", "label",
-    // sequences
-    "Seq",
-    // sets and multisets
-    "Set", "Multiset", "union", "intersection", "setminus", "subset",
-    // maps
-    "Map", "range",
-    // prover hint expressions
-    "unfolding", "in", "applying",
-    // old expression
-    "old", "lhs",
-    // other expressions
-    "let",
-    // quantification
-    "forall", "exists", "forperm",
-    // permission syntax
-    "acc", "wildcard", "write", "none", "epsilon", "perm",
-    // modifiers
-    "unique") | ParserExtension.extendedKeywords
-
 
   // Note that `typedFapp` is before `"(" ~ exp ~ ")"` to ensure that the latter doesn't gobble up the brackets for the former
   // and then look like an `fapp` up untill the `: type` part, after which we need to backtrack all the way back (or error if cut)
@@ -795,7 +812,7 @@ object FastParser {
 
   def identifier[_: P]: P[Unit] = CharIn("A-Z", "a-z", "$_") ~~ CharIn("0-9", "A-Z", "a-z", "$_").repX
 
-  def ident[_: P]: P[String] = identifier.!.filter(a => !keywords.contains(a)).opaque("invalid identifier (could be a keyword)")
+  def ident[_: P]: P[String] = identifier.!.filter(a => !FastParserCompanion.keywords.contains(a)).opaque("invalid identifier (could be a keyword)")
 
   def idnuse[_: P]: P[PIdnUse] = FP(ident).map { case (pos, id) => PIdnUse(id)(pos) }
 
diff --git a/src/main/scala/viper/silver/verifier/ModelParser.scala b/src/main/scala/viper/silver/verifier/ModelParser.scala
index 0a8d5c7e8..01a89c5c0 100644
--- a/src/main/scala/viper/silver/verifier/ModelParser.scala
+++ b/src/main/scala/viper/silver/verifier/ModelParser.scala
@@ -1,7 +1,7 @@
 package viper.silver.verifier
 
 import fastparse._
-import viper.silver.parser.FastParser.whitespace
+import viper.silver.parser.FastParserCompanion.whitespace
 
 object ModelParser {
   // note that the dash/minus character '-' needs to be escaped by double backslashes such that it is not interpreted as a range

From 700cc46fc2044d3bd84425933f5face15f105310 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 18 Aug 2022 13:54:13 +0200
Subject: [PATCH 02/11] WIP

---
 .../viper/silver/frontend/SilFrontend.scala   |  6 +++---
 .../scala/viper/silver/parser/ParseAst.scala  | 20 ++++++++++---------
 .../silver/plugin/SilverPluginManager.scala   | 17 ++++++++--------
 .../plugin/standard/adt/AdtPlugin.scala       |  7 +++++--
 .../PredicateInstancePlugin.scala             | 10 +++++++---
 .../plugin/standard/refute/RefutePlugin.scala | 11 +++++++---
 .../termination/TerminationPlugin.scala       |  7 ++++---
 7 files changed, 47 insertions(+), 31 deletions(-)

diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala
index f3a3a827c..0653269e2 100644
--- a/src/main/scala/viper/silver/frontend/SilFrontend.scala
+++ b/src/main/scala/viper/silver/frontend/SilFrontend.scala
@@ -89,11 +89,12 @@ trait SilFrontend extends DefaultFrontend {
   /** For testing of plugin import feature */
   def defaultPluginCount: Int = defaultPlugins.size
 
+  protected val fp = new FastParser()
 
   protected var _plugins: SilverPluginManager = SilverPluginManager(defaultPlugins match {
     case Seq() => None
     case s => Some(s.mkString(":"))
-  })(reporter, logger, _config)
+  })(reporter, logger, _config, fp)
 
   def plugins: SilverPluginManager = _plugins
 
@@ -187,7 +188,7 @@ trait SilFrontend extends DefaultFrontend {
         val list = _config.plugin.toOption ++ defaultPlugins
         if (list.isEmpty) { None } else { Some(list.mkString(":")) }
       }
-      _plugins = SilverPluginManager(plugins)(reporter, logger, _config)
+      _plugins = SilverPluginManager(plugins)(reporter, logger, _config, fp)
     }
   }
 
@@ -233,7 +234,6 @@ trait SilFrontend extends DefaultFrontend {
     val file = _inputFile.get
     _plugins.beforeParse(input, isImported = false) match {
       case Some(inputPlugin) =>
-        val fp = new FastParser()
         val result = fp.parse(inputPlugin, file, Some(_plugins))
           result match {
             case Parsed.Success(e@ PProgram(_, _, _, _, _, _, _, _, err_list), _) =>
diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala
index 26595c030..a6dc49cbe 100644
--- a/src/main/scala/viper/silver/parser/ParseAst.scala
+++ b/src/main/scala/viper/silver/parser/ParseAst.scala
@@ -6,6 +6,8 @@
 
 package viper.silver.parser
 
+import java.util.concurrent.atomic.{AtomicInteger, AtomicLong}
+
 import viper.silver.ast.utility.Visitor
 import viper.silver.ast.utility.rewriter.{Rewritable, StrategyBuilder}
 import viper.silver.ast.{Exp, MagicWandOp, Member, NoPosition, Position, Stmt, Type}
@@ -264,23 +266,24 @@ object PTypeVar{
   val sep = "#"
   //TODO: do this properly
   def isFreePTVName(s : String) = s.contains(sep)
-  private var lastIndex = 0
+  private val lastIndex = new AtomicInteger(0)
   //Generate a unique fresh version of old
   def fresh(old: PDomainType) = {
     require(old.isTypeVar)
-    val freshName = getFreshName(old.domain.name)
-    lastIndex+=1
+    val ind = lastIndex.getAndIncrement()
+    val freshName = getFreshName(old.domain.name, ind)
     PTypeVar(freshName)
   }
-  private def getFreshName(name:String) = name+sep+lastIndex
+  private def getFreshName(name:String, ind: Int) = name+sep+ind
+
   def freshTypeSubstitutionPTVs(tvs : Seq[PDomainType]) : PTypeRenaming = {
     require(tvs.forall(_.isTypeVar))
     freshTypeSubstitution(tvs map (tv=>tv.domain.name))
   }
   def freshTypeSubstitution(tvns : Seq[String]) : PTypeRenaming =
     {
-      lastIndex+=1
-      new PTypeRenaming((tvns map (tv=>tv->getFreshName(tv))).toMap)
+      val ind = lastIndex.getAndIncrement()
+      new PTypeRenaming((tvns map (tv=>tv->getFreshName(tv, ind))).toMap)
     }
 }
 
@@ -1104,11 +1107,10 @@ sealed trait PScope extends PNode {
 object PScope {
   type Id = Long
 
-  private[this] var counter: Id = 0L
+  private[this] val counter = new AtomicLong(0)
 
   private def uniqueId() = {
-    val id = counter
-    counter = counter + 1
+    val id = counter.getAndIncrement()
 
     id
   }
diff --git a/src/main/scala/viper/silver/plugin/SilverPluginManager.scala b/src/main/scala/viper/silver/plugin/SilverPluginManager.scala
index 7e6cac4bb..e30c8773b 100644
--- a/src/main/scala/viper/silver/plugin/SilverPluginManager.scala
+++ b/src/main/scala/viper/silver/plugin/SilverPluginManager.scala
@@ -9,7 +9,7 @@ package viper.silver.plugin
 import ch.qos.logback.classic.Logger
 import viper.silver.ast._
 import viper.silver.frontend.SilFrontendConfig
-import viper.silver.parser.PProgram
+import viper.silver.parser.{FastParser, PProgram}
 import viper.silver.reporter.Reporter
 import viper.silver.verifier.{AbstractError, VerificationResult}
 
@@ -77,10 +77,10 @@ class SilverPluginManager(val plugins: Seq[SilverPlugin]) {
 object SilverPluginManager {
 
   def apply(pluginArg: Option[String])
-           (reporter: Reporter, logger: Logger, cmdArgs: SilFrontendConfig): SilverPluginManager =
+           (reporter: Reporter, logger: Logger, cmdArgs: SilFrontendConfig, fp: FastParser): SilverPluginManager =
     pluginArg match {
       case Some(plugins) =>
-        new SilverPluginManager(resolveAll(plugins)(reporter, logger, cmdArgs))
+        new SilverPluginManager(resolveAll(plugins)(reporter, logger, cmdArgs, fp))
       case None =>
         new SilverPluginManager(Seq())
     }
@@ -88,8 +88,8 @@ object SilverPluginManager {
   def apply() = new SilverPluginManager(Seq())
 
   def resolveAll(pluginArg: String)
-                (reporter: Reporter, logger: Logger, cmdArgs: SilFrontendConfig): Seq[SilverPlugin] =
-    pluginArg.split(":").toSeq.map(resolve(_, reporter, logger, cmdArgs)).filter(_.isDefined).map(_.get)
+                (reporter: Reporter, logger: Logger, cmdArgs: SilFrontendConfig, fp: FastParser): Seq[SilverPlugin] =
+    pluginArg.split(":").toSeq.map(resolve(_, reporter, logger, cmdArgs, fp)).filter(_.isDefined).map(_.get)
 
   /** Tries to create an instance of the plugin class.
     *
@@ -122,13 +122,14 @@ object SilverPluginManager {
     * @throws PluginWrongTypeException if the plugin class does not extend [[viper.silver.plugin.SilverPlugin]]
     * @throws PluginWrongArgsException if the plugin does not provide a constructor with the expected arguments.
     */
-  def resolve(clazzName: String, reporter: Reporter, logger: Logger, cmdArgs: SilFrontendConfig): Option[SilverPlugin] = {
+  def resolve(clazzName: String, reporter: Reporter, logger: Logger, cmdArgs: SilFrontendConfig, fp: FastParser): Option[SilverPlugin] = {
     val clazz = try {
       val constructor = Class.forName(clazzName).getConstructor(
         classOf[viper.silver.reporter.Reporter],
         classOf[ch.qos.logback.classic.Logger],
-        classOf[viper.silver.frontend.SilFrontendConfig])
-      Some(constructor.newInstance(reporter, logger, cmdArgs))
+        classOf[viper.silver.frontend.SilFrontendConfig],
+        classOf[viper.silver.parser.FastParser])
+      Some(constructor.newInstance(reporter, logger, cmdArgs, fp))
     } catch {
       case _: NoSuchMethodException =>
         try {
diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
index 19091f525..5b4c65668 100644
--- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
@@ -9,7 +9,7 @@ package viper.silver.plugin.standard.adt
 import fastparse._
 import viper.silver.ast.Program
 import viper.silver.ast.utility.rewriter.StrategyBuilder
-import viper.silver.parser.FastParser.{FP, formalArg, idndef, idnuse, typ, whitespace}
+import viper.silver.parser.FastParserCompanion.whitespace
 import viper.silver.parser._
 import viper.silver.plugin.standard.adt.encoding.AdtEncoder
 import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin}
@@ -17,7 +17,10 @@ import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin}
 
 class AdtPlugin(reporter: viper.silver.reporter.Reporter,
                 logger: ch.qos.logback.classic.Logger,
-                config: viper.silver.frontend.SilFrontendConfig) extends SilverPlugin with ParserPluginTemplate {
+                config: viper.silver.frontend.SilFrontendConfig,
+                fp: FastParser) extends SilverPlugin with ParserPluginTemplate {
+
+  import fp.{FP, formalArg, idndef, idnuse, typ}
 
   /**
     * Keywords used to define ADT's
diff --git a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala b/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala
index 039952d94..42b1e8026 100644
--- a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala
@@ -9,17 +9,21 @@ package viper.silver.plugin.standard.predicateinstance
 import viper.silver.ast.{Domain, DomainType, ErrTrafo, FuncApp, Function, Position, PredicateAccess, PredicateAccessPredicate, Program, WildcardPerm}
 import viper.silver.ast.utility.ViperStrategy
 import viper.silver.ast.utility.rewriter.Traverse
-import viper.silver.parser.FastParser._
 import viper.silver.parser._
 import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin}
 import viper.silver.verifier.{ConsistencyError, Failure, Success, VerificationResult}
 import viper.silver.verifier.errors.PreconditionInAppFalse
 import fastparse._
-import viper.silver.parser.FastParser.whitespace
+import viper.silver.parser.FastParserCompanion.whitespace
 
 import scala.collection.immutable.ListMap
 
-class PredicateInstancePlugin  extends SilverPlugin with ParserPluginTemplate {
+class PredicateInstancePlugin(reporter: viper.silver.reporter.Reporter,
+                              logger: ch.qos.logback.classic.Logger,
+                              config: viper.silver.frontend.SilFrontendConfig,
+                              fp: FastParser)  extends SilverPlugin with ParserPluginTemplate {
+
+  import fp.{FP, predAcc}
 
   /**
    * Syntactic marker for predicate instances
diff --git a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
index a9c9d5728..7b83a8cad 100644
--- a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
@@ -9,13 +9,18 @@ package viper.silver.plugin.standard.refute
 import fastparse.P
 import viper.silver.ast.utility.ViperStrategy
 import viper.silver.ast._
-import viper.silver.parser.FastParser.{FP, exp, keyword, whitespace}
-import viper.silver.parser.ParserExtension
+import viper.silver.parser.FastParserCompanion.whitespace
+import viper.silver.parser.{FastParser, ParserExtension}
 import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin}
 import viper.silver.verifier._
 import viper.silver.verifier.errors.AssertFailed
 
-class RefutePlugin extends SilverPlugin with ParserPluginTemplate {
+class RefutePlugin(reporter: viper.silver.reporter.Reporter,
+                   logger: ch.qos.logback.classic.Logger,
+                   config: viper.silver.frontend.SilFrontendConfig,
+                   fp: FastParser) extends SilverPlugin with ParserPluginTemplate {
+
+  import fp.{FP, keyword, exp}
 
   /** Keyword used to define refute statements. */
   private val refuteKeyword: String = "refute"
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
index af1c9a81e..2b4f95a8c 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
@@ -9,7 +9,6 @@ package viper.silver.plugin.standard.termination
 import viper.silver.ast.utility.ViperStrategy
 import viper.silver.ast.utility.rewriter.{SimpleContext, Strategy, StrategyBuilder}
 import viper.silver.ast.{Applying, Assert, CondExp, CurrentPerm, Exp, Function, InhaleExhaleExp, MagicWand, Method, Node, Program, Unfolding, While}
-import viper.silver.parser.FastParser._
 import viper.silver.parser._
 import viper.silver.plugin.standard.predicateinstance.PPredicateInstance
 import viper.silver.plugin.standard.termination.transformation.Trafo
@@ -17,11 +16,13 @@ import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin}
 import viper.silver.verifier.errors.AssertFailed
 import viper.silver.verifier._
 import fastparse._
-import viper.silver.parser.FastParser.whitespace
+import viper.silver.parser.FastParserCompanion.whitespace
 
 class TerminationPlugin(reporter: viper.silver.reporter.Reporter,
                         logger: ch.qos.logback.classic.Logger,
-                        config: viper.silver.frontend.SilFrontendConfig) extends SilverPlugin with ParserPluginTemplate {
+                        config: viper.silver.frontend.SilFrontendConfig,
+                        fp: FastParser) extends SilverPlugin with ParserPluginTemplate {
+  import fp.{FP, keyword, exp}
 
   private def deactivated: Boolean = config != null && config.terminationPlugin.toOption.getOrElse(false)
 

From feb40b3248b5ab2a9a20e9fb9c20095bbaae52ab Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 18 Aug 2022 16:41:11 +0200
Subject: [PATCH 03/11] One ParseExtension object per parser

---
 .../silver/ast/utility/Consistency.scala      |   2 +-
 .../viper/silver/parser/FastParser.scala      | 141 +++++++++++++++++-
 .../viper/silver/parser/ParserExtension.scala | 137 -----------------
 .../plugin/standard/adt/AdtPlugin.scala       |   2 +-
 .../PredicateInstancePlugin.scala             |   2 +-
 .../plugin/standard/refute/RefutePlugin.scala |   4 +-
 .../termination/TerminationPlugin.scala       |   2 +-
 7 files changed, 142 insertions(+), 148 deletions(-)
 delete mode 100644 src/main/scala/viper/silver/parser/ParserExtension.scala

diff --git a/src/main/scala/viper/silver/ast/utility/Consistency.scala b/src/main/scala/viper/silver/ast/utility/Consistency.scala
index 00c8eefe4..c800ca67b 100644
--- a/src/main/scala/viper/silver/ast/utility/Consistency.scala
+++ b/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: Seq[String] = FastParserCompanion.keywords.toSeq
+  def reservedNames: Seq[String] = FastParserCompanion.basicKeywords.toSeq
 
   /** Returns true iff the string `name` is a valid identifier. */
   val identFirstLetter = "[a-zA-Z$_]"
diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index 4b56bc42c..5cabaf5fe 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -14,10 +14,11 @@ import viper.silver.ast.{FilePosition, LabelledOld, LineCol, NoPosition, Positio
 import viper.silver.ast.utility.rewriter.{ContextA, PartialContextC, StrategyBuilder}
 import viper.silver.parser.FastParserCompanion.{LW, LeadingWhitespace}
 import viper.silver.parser.Transformer.ParseTreeDuplicationError
-import viper.silver.plugin.SilverPluginManager
+import viper.silver.plugin.ParserPluginTemplate.{Extension, combine}
+import viper.silver.plugin.{ParserPluginTemplate, SilverPluginManager}
 import viper.silver.verifier.{ParseError, ParseWarning}
 
-import scala.collection.mutable
+import scala.collection.{Set, mutable}
 
 
 case class ParseException(msg: String, pos: Position) extends Exception
@@ -64,7 +65,7 @@ object FastParserCompanion {
     def map[V](f: T => V): LW[V] = new LW(() => p().map(f))
   }
 
-  lazy val keywords = Set("result",
+  lazy val basicKeywords = Set("result",
     // types
     "Int", "Perm", "Bool", "Ref", "Rational",
     // boolean constants
@@ -98,7 +99,7 @@ object FastParserCompanion {
     // permission syntax
     "acc", "wildcard", "write", "none", "epsilon", "perm",
     // modifiers
-    "unique") | ParserExtension.extendedKeywords
+    "unique")
 }
 
 class FastParser {
@@ -785,6 +786,8 @@ class FastParser {
   /** The file we are currently parsing (for creating positions later). */
   def file: Path = _file
 
+  lazy val keywords = FastParserCompanion.basicKeywords | ParserExtension.extendedKeywords
+
 
   // Note that `typedFapp` is before `"(" ~ exp ~ ")"` to ensure that the latter doesn't gobble up the brackets for the former
   // and then look like an `fapp` up untill the `: type` part, after which we need to backtrack all the way back (or error if cut)
@@ -812,7 +815,7 @@ class FastParser {
 
   def identifier[_: P]: P[Unit] = CharIn("A-Z", "a-z", "$_") ~~ CharIn("0-9", "A-Z", "a-z", "$_").repX
 
-  def ident[_: P]: P[String] = identifier.!.filter(a => !FastParserCompanion.keywords.contains(a)).opaque("invalid identifier (could be a keyword)")
+  def ident[_: P]: P[String] = identifier.!.filter(a => !keywords.contains(a)).opaque("invalid identifier (could be a keyword)")
 
   def idnuse[_: P]: P[PIdnUse] = FP(ident).map { case (pos, id) => PIdnUse(id)(pos) }
 
@@ -1264,4 +1267,132 @@ class FastParser {
   def methodSignature[_: P] = P("method" ~/ idndef ~ "(" ~ formalArgList ~ ")" ~~~ ("returns" ~ "(" ~ formalArgList ~ ")").lw.?)
 
   def entireProgram[_: P]: P[PProgram] = P(Start ~ programDecl ~ End)
+
+
+  object ParserExtension extends ParserPluginTemplate {
+
+    import ParserPluginTemplate._
+
+    /**
+      * These private variables are the storage variables for each of the extensions.
+      * As the parser are evaluated lazily, it is possible for us to stores extra parsing sequences in these variables
+      * and after the plugins are loaded, the parsers are added to these variables and when any parser is required,
+      * can be referenced back.
+      */
+    private var _newDeclAtEnd: Option[Extension[PExtender]] = None
+    private var _newDeclAtStart: Option[Extension[PExtender]] = None
+
+    private var _newExpAtEnd: Option[Extension[PExp]] = None
+    private var _newExpAtStart: Option[Extension[PExp]] = None
+
+    private var _newStmtAtEnd: Option[Extension[PStmt]] = None
+    private var _newStmtAtStart: Option[Extension[PStmt]] = None
+
+    private var _preSpecification: Option[Extension[PExp]] = None
+    private var _postSpecification: Option[Extension[PExp]] = None
+    private var _invSpecification: Option[Extension[PExp]] = None
+
+    private var _extendedKeywords: Set[String] = Set()
+
+
+    /**
+      * For more details regarding the functionality of each of these initial parser extensions
+      * and other hooks for the parser extension, please refer to ParserPluginTemplate.scala
+      */
+    override def newDeclAtStart : Extension[PExtender] = _newDeclAtStart match {
+      case None => ParserPluginTemplate.defaultExtension
+      case Some(ext) => ext
+    }
+
+    override def newDeclAtEnd : Extension[PExtender] = _newDeclAtEnd match {
+      case None => ParserPluginTemplate.defaultExtension
+      case Some(ext) => ext
+    }
+
+    override def newStmtAtEnd : Extension[PStmt] = _newStmtAtEnd match {
+      case None => ParserPluginTemplate.defaultStmtExtension
+      case Some(ext) => ext
+    }
+
+    override def newStmtAtStart : Extension[PStmt] = _newStmtAtStart match {
+      case None => ParserPluginTemplate.defaultStmtExtension
+      case Some(ext) => ext
+    }
+
+    override def newExpAtEnd : Extension[PExp] = _newExpAtEnd match {
+      case None => ParserPluginTemplate.defaultExpExtension
+      case Some(ext) => ext
+    }
+
+    override def newExpAtStart : Extension[PExp] = _newExpAtStart match {
+      case None => ParserPluginTemplate.defaultExpExtension
+      case Some(ext) => ext
+    }
+
+    override def postSpecification : Extension[PExp] = _postSpecification match {
+      case None => ParserPluginTemplate.defaultExpExtension
+      case Some(ext) => ext
+    }
+
+    override def preSpecification : Extension[PExp] = _preSpecification match {
+      case None => ParserPluginTemplate.defaultExpExtension
+      case Some(ext) => ext
+    }
+
+    override def invSpecification : Extension[PExp] = _invSpecification match {
+      case None => ParserPluginTemplate.defaultExpExtension
+      case Some(ext) => ext
+    }
+
+    override def extendedKeywords : Set[String] = _extendedKeywords
+
+    def addNewDeclAtEnd(t: Extension[PExtender]) : Unit = _newDeclAtEnd match {
+      case None => _newDeclAtEnd = Some(t)
+      case Some(s) => _newDeclAtEnd = Some(combine(s, t))
+    }
+
+    def addNewDeclAtStart(t: Extension[PExtender]) : Unit = _newDeclAtStart match {
+      case None => _newDeclAtStart = Some(t)
+      case Some(s) => _newDeclAtStart = Some(combine(s, t))
+    }
+
+    def addNewExpAtEnd(t: Extension[PExp]) : Unit = _newExpAtEnd match {
+      case None => _newExpAtEnd = Some(t)
+      case Some(s) => _newExpAtEnd = Some(combine(s, t))
+    }
+
+    def addNewExpAtStart(t: Extension[PExp]) : Unit = _newExpAtStart match {
+      case None => _newExpAtStart = Some(t)
+      case Some(s) => _newExpAtStart = Some(combine(s, t))
+    }
+
+    def addNewStmtAtEnd(t: Extension[PStmt]) : Unit = _newStmtAtEnd match {
+      case None => _newStmtAtEnd = Some(t)
+      case Some(s) => _newStmtAtEnd = Some(combine(s, t))
+    }
+
+    def addNewStmtAtStart(t: Extension[PStmt]) : Unit = _newStmtAtStart match {
+      case None => _newStmtAtStart = Some(t)
+      case Some(s) => _newStmtAtStart = Some(combine(s, t))
+    }
+
+    def addNewPreCondition(t: Extension[PExp]) : Unit = _preSpecification match {
+      case None => _preSpecification = Some(t)
+      case Some(s) => _preSpecification = Some(combine(s, t))
+    }
+
+    def addNewPostCondition(t: Extension[PExp]) : Unit = _postSpecification match {
+      case None => _postSpecification = Some(t)
+      case Some(s) => _postSpecification = Some(combine(s, t))
+    }
+
+    def addNewInvariantCondition(t: Extension[PExp]) : Unit = _invSpecification match {
+      case None => _invSpecification = Some(t)
+      case Some(s) => _invSpecification = Some(combine(s, t))
+    }
+
+    def addNewKeywords(t : Set[String]) : Unit = {
+      _extendedKeywords ++= t
+    }
+  }
 }
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/parser/ParserExtension.scala b/src/main/scala/viper/silver/parser/ParserExtension.scala
deleted file mode 100644
index fd17fd894..000000000
--- a/src/main/scala/viper/silver/parser/ParserExtension.scala
+++ /dev/null
@@ -1,137 +0,0 @@
-// This Source Code Form is subject to the terms of the Mozilla Public
-// License, v. 2.0. If a copy of the MPL was not distributed with this
-// file, You can obtain one at http://mozilla.org/MPL/2.0/.
-//
-// Copyright (c) 2011-2019 ETH Zurich.
-
-package viper.silver.parser
-
-import viper.silver.plugin._
-import scala.collection.Set
-
-object ParserExtension extends ParserPluginTemplate {
-
-  import ParserPluginTemplate._
-
-  /**
-    * These private variables are the storage variables for each of the extensions.
-    * As the parser are evaluated lazily, it is possible for us to stores extra parsing sequences in these variables
-    * and after the plugins are loaded, the parsers are added to these variables and when any parser is required,
-    * can be referenced back.
-    */
-  private var _newDeclAtEnd: Option[Extension[PExtender]] = None
-  private var _newDeclAtStart: Option[Extension[PExtender]] = None
-
-  private var _newExpAtEnd: Option[Extension[PExp]] = None
-  private var _newExpAtStart: Option[Extension[PExp]] = None
-
-  private var _newStmtAtEnd: Option[Extension[PStmt]] = None
-  private var _newStmtAtStart: Option[Extension[PStmt]] = None
-
-  private var _preSpecification: Option[Extension[PExp]] = None
-  private var _postSpecification: Option[Extension[PExp]] = None
-  private var _invSpecification: Option[Extension[PExp]] = None
-
-  private var _extendedKeywords: Set[String] = Set()
-
-
-  /**
-    * For more details regarding the functionality of each of these initial parser extensions
-    * and other hooks for the parser extension, please refer to ParserPluginTemplate.scala
-    */
-  override def newDeclAtStart : Extension[PExtender] = _newDeclAtStart match {
-    case None => ParserPluginTemplate.defaultExtension
-    case Some(ext) => ext
-  }
-
-  override def newDeclAtEnd : Extension[PExtender] = _newDeclAtEnd match {
-    case None => ParserPluginTemplate.defaultExtension
-    case Some(ext) => ext
-  }
-
-  override def newStmtAtEnd : Extension[PStmt] = _newStmtAtEnd match {
-    case None => ParserPluginTemplate.defaultStmtExtension
-    case Some(ext) => ext
-  }
-
-  override def newStmtAtStart : Extension[PStmt] = _newStmtAtStart match {
-    case None => ParserPluginTemplate.defaultStmtExtension
-    case Some(ext) => ext
-  }
-
-  override def newExpAtEnd : Extension[PExp] = _newExpAtEnd match {
-    case None => ParserPluginTemplate.defaultExpExtension
-    case Some(ext) => ext
-  }
-
-  override def newExpAtStart : Extension[PExp] = _newExpAtStart match {
-    case None => ParserPluginTemplate.defaultExpExtension
-    case Some(ext) => ext
-  }
-
-  override def postSpecification : Extension[PExp] = _postSpecification match {
-    case None => ParserPluginTemplate.defaultExpExtension
-    case Some(ext) => ext
-  }
-
-  override def preSpecification : Extension[PExp] = _preSpecification match {
-    case None => ParserPluginTemplate.defaultExpExtension
-    case Some(ext) => ext
-  }
-
-  override def invSpecification : Extension[PExp] = _invSpecification match {
-    case None => ParserPluginTemplate.defaultExpExtension
-    case Some(ext) => ext
-  }
-
-  override def extendedKeywords : Set[String] = _extendedKeywords
-
-  def addNewDeclAtEnd(t: Extension[PExtender]) : Unit = _newDeclAtEnd match {
-    case None => _newDeclAtEnd = Some(t)
-    case Some(s) => _newDeclAtEnd = Some(combine(s, t))
-  }
-
-  def addNewDeclAtStart(t: Extension[PExtender]) : Unit = _newDeclAtStart match {
-    case None => _newDeclAtStart = Some(t)
-    case Some(s) => _newDeclAtStart = Some(combine(s, t))
-  }
-
-  def addNewExpAtEnd(t: Extension[PExp]) : Unit = _newExpAtEnd match {
-    case None => _newExpAtEnd = Some(t)
-    case Some(s) => _newExpAtEnd = Some(combine(s, t))
-  }
-
-  def addNewExpAtStart(t: Extension[PExp]) : Unit = _newExpAtStart match {
-    case None => _newExpAtStart = Some(t)
-    case Some(s) => _newExpAtStart = Some(combine(s, t))
-  }
-
-  def addNewStmtAtEnd(t: Extension[PStmt]) : Unit = _newStmtAtEnd match {
-    case None => _newStmtAtEnd = Some(t)
-    case Some(s) => _newStmtAtEnd = Some(combine(s, t))
-  }
-
-  def addNewStmtAtStart(t: Extension[PStmt]) : Unit = _newStmtAtStart match {
-    case None => _newStmtAtStart = Some(t)
-    case Some(s) => _newStmtAtStart = Some(combine(s, t))
-  }
-
-  def addNewPreCondition(t: Extension[PExp]) : Unit = _preSpecification match {
-    case None => _preSpecification = Some(t)
-    case Some(s) => _preSpecification = Some(combine(s, t))
-  }
-
-  def addNewPostCondition(t: Extension[PExp]) : Unit = _postSpecification match {
-    case None => _postSpecification = Some(t)
-    case Some(s) => _postSpecification = Some(combine(s, t))
-  }
-
-  def addNewInvariantCondition(t: Extension[PExp]) : Unit = _invSpecification match {
-    case None => _invSpecification = Some(t)
-    case Some(s) => _invSpecification = Some(combine(s, t))
-  }
-
-  def addNewKeywords(t : Set[String]) : Unit = {
-    _extendedKeywords ++= t
-  }
-}
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
index 5b4c65668..6618ae3d7 100644
--- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
@@ -20,7 +20,7 @@ class AdtPlugin(reporter: viper.silver.reporter.Reporter,
                 config: viper.silver.frontend.SilFrontendConfig,
                 fp: FastParser) extends SilverPlugin with ParserPluginTemplate {
 
-  import fp.{FP, formalArg, idndef, idnuse, typ}
+  import fp.{FP, formalArg, idndef, idnuse, typ, ParserExtension}
 
   /**
     * Keywords used to define ADT's
diff --git a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala b/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala
index 42b1e8026..167508e01 100644
--- a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala
@@ -23,7 +23,7 @@ class PredicateInstancePlugin(reporter: viper.silver.reporter.Reporter,
                               config: viper.silver.frontend.SilFrontendConfig,
                               fp: FastParser)  extends SilverPlugin with ParserPluginTemplate {
 
-  import fp.{FP, predAcc}
+  import fp.{FP, predAcc, ParserExtension}
 
   /**
    * Syntactic marker for predicate instances
diff --git a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
index 7b83a8cad..7164a90a4 100644
--- a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
@@ -10,7 +10,7 @@ import fastparse.P
 import viper.silver.ast.utility.ViperStrategy
 import viper.silver.ast._
 import viper.silver.parser.FastParserCompanion.whitespace
-import viper.silver.parser.{FastParser, ParserExtension}
+import viper.silver.parser.FastParser
 import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin}
 import viper.silver.verifier._
 import viper.silver.verifier.errors.AssertFailed
@@ -20,7 +20,7 @@ class RefutePlugin(reporter: viper.silver.reporter.Reporter,
                    config: viper.silver.frontend.SilFrontendConfig,
                    fp: FastParser) extends SilverPlugin with ParserPluginTemplate {
 
-  import fp.{FP, keyword, exp}
+  import fp.{FP, keyword, exp, ParserExtension}
 
   /** Keyword used to define refute statements. */
   private val refuteKeyword: String = "refute"
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
index 2b4f95a8c..ddca26499 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
@@ -22,7 +22,7 @@ class TerminationPlugin(reporter: viper.silver.reporter.Reporter,
                         logger: ch.qos.logback.classic.Logger,
                         config: viper.silver.frontend.SilFrontendConfig,
                         fp: FastParser) extends SilverPlugin with ParserPluginTemplate {
-  import fp.{FP, keyword, exp}
+  import fp.{FP, keyword, exp, ParserExtension}
 
   private def deactivated: Boolean = config != null && config.terminationPlugin.toOption.getOrElse(false)
 

From ff430f7e63b4a102369d9c89e594332df9248201 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Mon, 22 Aug 2022 14:41:53 +0200
Subject: [PATCH 04/11] Cleanup

---
 src/main/scala/viper/silver/ast/Position.scala         | 2 +-
 src/main/scala/viper/silver/frontend/SilFrontend.scala | 2 +-
 src/main/scala/viper/silver/parser/FastParser.scala    | 6 +++---
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/Position.scala b/src/main/scala/viper/silver/ast/Position.scala
index 82c143232..95ea4efcb 100644
--- a/src/main/scala/viper/silver/ast/Position.scala
+++ b/src/main/scala/viper/silver/ast/Position.scala
@@ -90,7 +90,7 @@ class IdentifierPosition(val file: Path, val start: HasLineColumn, val end: Opti
 }
 
 class LineCol(fp: FastParser) {
-  def apply(index: Int): (Int, Int) = {
+  def getPos(index: Int): (Int, Int) = {
     // val Array(line, col) = ctx.input.prettyIndex(index).split(":").map(_.toInt)
     val line_offset = fp._line_offset
     val result = java.util.Arrays.binarySearch(line_offset, index)
diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala
index 0653269e2..e706cf048 100644
--- a/src/main/scala/viper/silver/frontend/SilFrontend.scala
+++ b/src/main/scala/viper/silver/frontend/SilFrontend.scala
@@ -244,7 +244,7 @@ trait SilFrontend extends DefaultFrontend {
               else Fail(err_list)
             case fail @ Parsed.Failure(_, index, extra) =>
               val msg = fail.trace().longAggregateMsg
-              val (line, col) = fp.lineCol(index)
+              val (line, col) = fp.lineCol.getPos(index)
               Fail(List(ParseError(s"Expected $msg", SourcePosition(file, line, col))))
             //? val pos = extra.input.prettyIndex(index).split(":").map(_.toInt)
               //? Fail(List(ParseError(s"Expected $msg", SourcePosition(file, pos(0), pos(1)))))
diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index 5cabaf5fe..8d23b7453 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -264,9 +264,9 @@ class FastParser {
     * Function that wraps a parser to provide start and end positions if the wrapped parser succeeds.
     */
   def FP[T](t: => P[T])(implicit ctx: P[_]): P[((FilePosition, FilePosition), T)] = {
-    val startPos = lineCol.apply(ctx.index)
+    val startPos = lineCol.getPos(ctx.index)
     val res: P[T] = t
-    val finishPos = lineCol.apply(ctx.index)
+    val finishPos = lineCol.getPos(ctx.index)
     res.map({ parsed => ((FilePosition(_file, startPos._1, startPos._2), FilePosition(_file, finishPos._1, finishPos._2)), parsed) })
   }
 
@@ -318,7 +318,7 @@ class FastParser {
       case fastparse.Parsed.Success(prog, _) => prog
       case fail @ fastparse.Parsed.Failure(_, index, _) =>
         val msg = fail.trace().longMsg
-        val (line, col) = lineCol.apply(index)
+        val (line, col) = lineCol.getPos(index)
         throw ParseException(s"Expected $msg", FilePosition(path, line, col))
     }
   }

From 9c0f62206f3f148b25997c0f186879f27a55997a Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 25 Aug 2022 17:12:33 +0200
Subject: [PATCH 05/11] Updated docomentation for plugins

---
 src/main/scala/viper/silver/plugin/SilverPlugin.scala |  8 +++++---
 .../viper/silver/plugin/SilverPluginManager.scala     | 11 +++++++----
 2 files changed, 12 insertions(+), 7 deletions(-)

diff --git a/src/main/scala/viper/silver/plugin/SilverPlugin.scala b/src/main/scala/viper/silver/plugin/SilverPlugin.scala
index e69269143..63442fced 100644
--- a/src/main/scala/viper/silver/plugin/SilverPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/SilverPlugin.scala
@@ -9,20 +9,22 @@ package viper.silver.plugin
 import ch.qos.logback.classic.Logger
 import viper.silver.ast.Program
 import viper.silver.frontend.SilFrontendConfig
-import viper.silver.parser.PProgram
+import viper.silver.parser.{FastParser, PProgram}
 import viper.silver.reporter.Reporter
 import viper.silver.verifier.{AbstractError, VerificationResult}
 
 /** Implement this abstract class in order to give your plugin access to SilFrontend's IO:
   * 1. Reporter,
-  * 2. Logger, and
-  * 2. Command line arguments
+  * 2. Logger,
+  * 3. Command line arguments, and
+  * 4. Parser.
   * Has to be set as an explicit parameter for the plugin constructor.
   */
 trait IOAwarePlugin {
   val reporter: Reporter
   val logger: Logger
   val cmdArgs: SilFrontendConfig
+  val fp: FastParser
 }
 
 /** Trait to be extended by plugins. A plugin can change the current structure of the program under verification
diff --git a/src/main/scala/viper/silver/plugin/SilverPluginManager.scala b/src/main/scala/viper/silver/plugin/SilverPluginManager.scala
index e30c8773b..a8cd615ce 100644
--- a/src/main/scala/viper/silver/plugin/SilverPluginManager.scala
+++ b/src/main/scala/viper/silver/plugin/SilverPluginManager.scala
@@ -93,17 +93,19 @@ object SilverPluginManager {
 
   /** Tries to create an instance of the plugin class.
     *
-    * The plugin constructor is expected to take either zero or three arguments (as specified in [[viper.silver.plugin.IOAwarePlugin]]):
+    * The plugin constructor is expected to take either zero or four arguments (as specified in [[viper.silver.plugin.IOAwarePlugin]]):
     *  [[viper.silver.reporter.Reporter]],
     *  [[ch.qos.logback.classic.Logger]],
-    *  [[viper.silver.frontend.SilFrontendConfig]].
+    *  [[viper.silver.frontend.SilFrontendConfig]],
+    *  [[viper.silver.parser.FastParser]].
     *
     * Example plugin class declarations:
     * <pre>
     * class MyPlugin(val _reporter: Reporter,
     *                val _logger: Logger,
-    *                val _cmdArgs: SilFrontendConfig)
-    *                extends IOAwarePlugin(_reporter, _logger, _cmdArgs) with SilverPlugin
+    *                val _cmdArgs: SilFrontendConfig,
+    *                val _fp: FastParser)
+    *                extends IOAwarePlugin(_reporter, _logger, _cmdArgs, _fp) with SilverPlugin
     * </pre>
     * <pre>
     * class MyPlugin extends SilverPlugin
@@ -115,6 +117,7 @@ object SilverPluginManager {
     * @param reporter  The reporter to be used in the plugin.
     * @param logger    The logger to be used in the plugin.
     * @param cmdArgs   The config object to be accessible from the plugin.
+    * @param fp        The parser object to be used by the plugin.
     *
     * @return A fresh instance of the plugin class
     *

From b012f2c541009685c2cf17a582559eccf5fd51ac Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Mon, 29 Aug 2022 15:03:13 +0200
Subject: [PATCH 06/11] Ignore quantified fields/predicates in bodies of called
 methods, only use their spec

---
 .../ast/utility/QuantifiedPermissions.scala   | 74 ++++++++++++-------
 1 file changed, 46 insertions(+), 28 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
index 11324e86b..ebc6820f2 100644
--- a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
+++ b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
@@ -53,19 +53,16 @@ object QuantifiedPermissions {
    *       e.g. someMethod.quantifiedFields.
    */
 
-  def quantifiedFields(root: Node, program: Program): collection.Set[Field] = {
+  def quantifiedFields(root: Member, program: Program): collection.Set[Field] = {
     val collected = mutable.LinkedHashSet[Field]()
     val visited = mutable.Set[Member]()
     val toVisit = mutable.Queue[Member]()
 
-    root match {
-      case m: Member => toVisit += m
-      case _ =>
-    }
+    toVisit += root
 
     toVisit ++= Nodes.referencedMembers(root, program)
 
-    quantifiedFields(toVisit, collected, visited, program)
+    quantifiedFields(toVisit, root, collected, visited, program)
 
     collected
   }
@@ -73,19 +70,16 @@ object QuantifiedPermissions {
   /* TODO: See comment above about caching
    * TODO: Unify with corresponding code for fields
    */
-  def quantifiedPredicates(root: Node, program: Program): collection.Set[Predicate] = {
+  def quantifiedPredicates(root: Member, program: Program): collection.Set[Predicate] = {
     val collected = mutable.LinkedHashSet[Predicate]()
     val visited = mutable.Set[Member]()
     val toVisit = mutable.Queue[Member]()
 
-    root match {
-      case m: Member => toVisit += m
-      case _ =>
-    }
+    toVisit += root
 
     toVisit ++= Nodes.referencedMembers(root, program)
 
-    quantifiedPredicates(toVisit, collected, visited, program)
+    quantifiedPredicates(toVisit, root, collected, visited, program)
 
     collected
   }
@@ -98,44 +92,68 @@ object QuantifiedPermissions {
   }
 
   private def quantifiedFields(toVisit: mutable.Queue[Member],
+                               root: Member,
                                collected: mutable.LinkedHashSet[Field],
                                visited: mutable.Set[Member],
                                program: Program): Unit = {
 
     while (toVisit.nonEmpty) {
-      val root = toVisit.dequeue()
+      val currentRoot = toVisit.dequeue()
 
-      root visit {
-        case QuantifiedPermissionAssertion(_, _, acc: FieldAccessPredicate) =>
-          collected += acc.loc.field
-        case Forall(_,triggers,_) => collected ++= triggers flatMap (_.exps) collect {case fa: FieldAccess => fa.field}
+      val relevantNodes: Map[Member, Seq[Node]] = currentRoot match {
+        case m@Method(_, _, _, pres, posts, _) if m != root =>
+          // use only specification of called methods
+          Map(m -> (pres ++ posts))
+        case _ => Map(currentRoot -> Seq(currentRoot))
       }
 
-      visited += root
+      for ((member, ns) <- relevantNodes.toIndexedSeq) {
+        visited += member
+
+        for (n <- ns){
+          n visit {
+            case QuantifiedPermissionAssertion(_, _, acc: FieldAccessPredicate) =>
+              collected += acc.loc.field
+            case Forall(_,triggers,_) => collected ++= triggers flatMap (_.exps) collect {case fa: FieldAccess => fa.field}
+          }
+          utility.Nodes.referencedMembers(n, program) foreach (m =>
+            if (!visited.contains(m)) toVisit += m)
 
-      utility.Nodes.referencedMembers(root, program) foreach (m =>
-        if (!visited.contains(m)) toVisit += m)
+        }
+      }
     }
   }
 
   private def quantifiedPredicates(toVisit: mutable.Queue[Member],
+                                   root: Member,
                                    collected: mutable.LinkedHashSet[Predicate],
                                    visited: mutable.Set[Member],
                                    program: Program): Unit = {
 
     while (toVisit.nonEmpty) {
-      val root = toVisit.dequeue()
+      val currentRoot = toVisit.dequeue()
 
-      root visit {
-        case QuantifiedPermissionAssertion(_, _, acc: PredicateAccessPredicate) =>
-          collected += program.findPredicate(acc.loc.predicateName)
-        case Forall(_,triggers,_) => collected ++= triggers flatMap (_.exps) collect {case pa: PredicateAccess => pa.loc(program)}
+      val relevantNodes: Map[Member, Seq[Node]] = currentRoot match {
+        case m@Method(_, _, _, pres, posts, _) if m != root =>
+          // use only specification of called methods
+          Map(m -> (pres ++ posts))
+        case _ => Map(currentRoot -> Seq(currentRoot))
       }
 
-      visited += root
+      for ((member, ns) <- relevantNodes.toIndexedSeq) {
+        visited += member
+
+        for (n <- ns){
+          n visit {
+            case QuantifiedPermissionAssertion(_, _, acc: PredicateAccessPredicate) =>
+              collected += program.findPredicate(acc.loc.predicateName)
+            case Forall(_,triggers,_) => collected ++= triggers flatMap (_.exps) collect {case pa: PredicateAccess => pa.loc(program)}
+          }
+          utility.Nodes.referencedMembers(n, program) foreach (m =>
+            if (!visited.contains(m)) toVisit += m)
 
-      utility.Nodes.referencedMembers(root, program) foreach (m =>
-        if (!visited.contains(m)) toVisit += m)
+        }
+      }
     }
   }
 

From 4a5782916dd80a21c2a5e4730b8595dc7ed529f4 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 31 Aug 2022 11:51:22 +0200
Subject: [PATCH 07/11] Simplified after review

---
 .../ast/utility/QuantifiedPermissions.scala   | 51 +++++++++----------
 1 file changed, 23 insertions(+), 28 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
index ebc6820f2..76e589655 100644
--- a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
+++ b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
@@ -100,26 +100,23 @@ object QuantifiedPermissions {
     while (toVisit.nonEmpty) {
       val currentRoot = toVisit.dequeue()
 
-      val relevantNodes: Map[Member, Seq[Node]] = currentRoot match {
+      val relevantNodes: Seq[Node] = currentRoot match {
         case m@Method(_, _, _, pres, posts, _) if m != root =>
           // use only specification of called methods
-          Map(m -> (pres ++ posts))
-        case _ => Map(currentRoot -> Seq(currentRoot))
+          pres ++ posts
+        case _ => Seq(currentRoot)
       }
 
-      for ((member, ns) <- relevantNodes.toIndexedSeq) {
-        visited += member
-
-        for (n <- ns){
-          n visit {
-            case QuantifiedPermissionAssertion(_, _, acc: FieldAccessPredicate) =>
-              collected += acc.loc.field
-            case Forall(_,triggers,_) => collected ++= triggers flatMap (_.exps) collect {case fa: FieldAccess => fa.field}
-          }
-          utility.Nodes.referencedMembers(n, program) foreach (m =>
-            if (!visited.contains(m)) toVisit += m)
+      visited += currentRoot
 
+      for (n <- relevantNodes){
+        n visit {
+          case QuantifiedPermissionAssertion(_, _, acc: FieldAccessPredicate) =>
+            collected += acc.loc.field
+          case Forall(_,triggers,_) => collected ++= triggers flatMap (_.exps) collect {case fa: FieldAccess => fa.field}
         }
+        utility.Nodes.referencedMembers(n, program) foreach (m =>
+          if (!visited.contains(m)) toVisit += m)
       }
     }
   }
@@ -133,26 +130,24 @@ object QuantifiedPermissions {
     while (toVisit.nonEmpty) {
       val currentRoot = toVisit.dequeue()
 
-      val relevantNodes: Map[Member, Seq[Node]] = currentRoot match {
+      val relevantNodes: Seq[Node] = currentRoot match {
         case m@Method(_, _, _, pres, posts, _) if m != root =>
           // use only specification of called methods
-          Map(m -> (pres ++ posts))
-        case _ => Map(currentRoot -> Seq(currentRoot))
+          pres ++ posts
+        case _ => Seq(currentRoot)
       }
 
-      for ((member, ns) <- relevantNodes.toIndexedSeq) {
-        visited += member
-
-        for (n <- ns){
-          n visit {
-            case QuantifiedPermissionAssertion(_, _, acc: PredicateAccessPredicate) =>
-              collected += program.findPredicate(acc.loc.predicateName)
-            case Forall(_,triggers,_) => collected ++= triggers flatMap (_.exps) collect {case pa: PredicateAccess => pa.loc(program)}
-          }
-          utility.Nodes.referencedMembers(n, program) foreach (m =>
-            if (!visited.contains(m)) toVisit += m)
+      visited += currentRoot
 
+      for (n <- relevantNodes){
+        n visit {
+          case QuantifiedPermissionAssertion(_, _, acc: PredicateAccessPredicate) =>
+            collected += program.findPredicate(acc.loc.predicateName)
+          case Forall(_,triggers,_) => collected ++= triggers flatMap (_.exps) collect {case pa: PredicateAccess => pa.loc(program)}
         }
+        utility.Nodes.referencedMembers(n, program) foreach (m =>
+          if (!visited.contains(m)) toVisit += m)
+
       }
     }
   }

From 4181ac6e6192eed05d45c6678252c5335dc1bdad Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 1 Sep 2022 14:28:43 +0200
Subject: [PATCH 08/11] Changes after code review

---
 src/main/scala/viper/silver/ast/utility/Consistency.scala  | 2 +-
 src/main/scala/viper/silver/parser/FastParser.scala        | 2 +-
 src/main/scala/viper/silver/utility/SilNameGenerator.scala | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/utility/Consistency.scala b/src/main/scala/viper/silver/ast/utility/Consistency.scala
index c800ca67b..a179539ad 100644
--- a/src/main/scala/viper/silver/ast/utility/Consistency.scala
+++ b/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: Seq[String] = FastParserCompanion.basicKeywords.toSeq
+  def reservedNames: Set[String] = FastParserCompanion.basicKeywords
 
   /** Returns true iff the string `name` is a valid identifier. */
   val identFirstLetter = "[a-zA-Z$_]"
diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index 8d23b7453..d591a84f3 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -65,7 +65,7 @@ object FastParserCompanion {
     def map[V](f: T => V): LW[V] = new LW(() => p().map(f))
   }
 
-  lazy val basicKeywords = Set("result",
+  val basicKeywords = Set("result",
     // types
     "Int", "Perm", "Bool", "Ref", "Rational",
     // boolean constants
diff --git a/src/main/scala/viper/silver/utility/SilNameGenerator.scala b/src/main/scala/viper/silver/utility/SilNameGenerator.scala
index 6e7bb2ea5..087386286 100644
--- a/src/main/scala/viper/silver/utility/SilNameGenerator.scala
+++ b/src/main/scala/viper/silver/utility/SilNameGenerator.scala
@@ -15,7 +15,7 @@ class SilNameGenerator extends DefaultNameGenerator {
   val identFirstLetter = "[a-zA-Z$_]"
   val identOtherLetterChars = "a-zA-Z0-9$_'"
   val identOtherLetter = s"[$identOtherLetterChars]"
-  val reservedNames = Consistency.reservedNames.toSet
+  val reservedNames = Consistency.reservedNames
   val separator = "_"
   val firstCharacter = identFirstLetter.r
   val otherCharacter = identOtherLetter.r

From fdcaed397a1deedf64d3e371b863fcb134818a66 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 1 Sep 2022 14:58:11 +0200
Subject: [PATCH 09/11] Fixed error with different set types

---
 src/main/scala/viper/silver/parser/FastParser.scala | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index d591a84f3..e220d4cb9 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -9,16 +9,14 @@ package viper.silver.parser
 import java.net.URL
 import java.nio.file.{Files, Path, Paths}
 
-import fastparse.{CharsWhile, Implicits, NoTrace, NoWhitespace, P, ParsingRun, Pass, StringIn}
 import viper.silver.ast.{FilePosition, LabelledOld, LineCol, NoPosition, Position, SourcePosition}
 import viper.silver.ast.utility.rewriter.{ContextA, PartialContextC, StrategyBuilder}
 import viper.silver.parser.FastParserCompanion.{LW, LeadingWhitespace}
 import viper.silver.parser.Transformer.ParseTreeDuplicationError
-import viper.silver.plugin.ParserPluginTemplate.{Extension, combine}
 import viper.silver.plugin.{ParserPluginTemplate, SilverPluginManager}
 import viper.silver.verifier.{ParseError, ParseWarning}
 
-import scala.collection.{Set, mutable}
+import scala.collection.{Set, immutable, mutable}
 
 
 case class ParseException(msg: String, pos: Position) extends Exception
@@ -65,7 +63,7 @@ object FastParserCompanion {
     def map[V](f: T => V): LW[V] = new LW(() => p().map(f))
   }
 
-  val basicKeywords = Set("result",
+  val basicKeywords = immutable.Set("result",
     // types
     "Int", "Perm", "Bool", "Ref", "Rational",
     // boolean constants

From ecc03b5360ad4983451b99981151b2fafd51da76 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Fri, 2 Sep 2022 17:29:14 +0200
Subject: [PATCH 10/11] Ignoring function bodies as well for finding
 qpFields/qpPredicates

---
 .../viper/silver/ast/utility/QuantifiedPermissions.scala    | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
index 76e589655..7568e05c4 100644
--- a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
+++ b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
@@ -104,6 +104,9 @@ object QuantifiedPermissions {
         case m@Method(_, _, _, pres, posts, _) if m != root =>
           // use only specification of called methods
           pres ++ posts
+        case Function(_, _, _, pres, posts, _) =>
+          // use only specification of called functions
+          pres ++ posts
         case _ => Seq(currentRoot)
       }
 
@@ -134,6 +137,9 @@ object QuantifiedPermissions {
         case m@Method(_, _, _, pres, posts, _) if m != root =>
           // use only specification of called methods
           pres ++ posts
+        case Function(_, _, _, pres, posts, _) =>
+          // use only specification of called functions
+          pres ++ posts
         case _ => Seq(currentRoot)
       }
 

From bac52241529d58f6a572cb3ac05d3fc57710240a Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Fri, 2 Sep 2022 17:59:51 +0200
Subject: [PATCH 11/11] Forgot to always include body of root function

---
 .../viper/silver/ast/utility/QuantifiedPermissions.scala      | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
index 7568e05c4..6b994cef9 100644
--- a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
+++ b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
@@ -104,7 +104,7 @@ object QuantifiedPermissions {
         case m@Method(_, _, _, pres, posts, _) if m != root =>
           // use only specification of called methods
           pres ++ posts
-        case Function(_, _, _, pres, posts, _) =>
+        case f@Function(_, _, _, pres, posts, _) if f != root=>
           // use only specification of called functions
           pres ++ posts
         case _ => Seq(currentRoot)
@@ -137,7 +137,7 @@ object QuantifiedPermissions {
         case m@Method(_, _, _, pres, posts, _) if m != root =>
           // use only specification of called methods
           pres ++ posts
-        case Function(_, _, _, pres, posts, _) =>
+        case f@Function(_, _, _, pres, posts, _) if f != root =>
           // use only specification of called functions
           pres ++ posts
         case _ => Seq(currentRoot)