Removing global state

src/main/scala/Silicon.scala

@@ -9,6 +9,7 @@ package viper.silicon
 import java.nio.file.Paths
 import java.text.SimpleDateFormat
 import java.util.concurrent.{Callable, Executors, TimeUnit, TimeoutException}
+
 import scala.collection.immutable.ArraySeq
 import scala.util.{Left, Right}
 import ch.qos.logback.classic.{Level, Logger}
@@ -20,11 +21,12 @@ import viper.silver.reporter._
 import viper.silver.verifier.{AbstractVerificationError => SilAbstractVerificationError, Failure => SilFailure, Success => SilSuccess, TimeoutOccurred => SilTimeoutOccurred, VerificationResult => SilVerificationResult, Verifier => SilVerifier}
 import viper.silicon.interfaces.Failure
 import viper.silicon.logger.SymbExLogger
-import viper.silicon.reporting.condenseToViperResult
+import viper.silicon.reporting.{MultiRunRecorders, condenseToViperResult}
 import viper.silicon.verifier.DefaultMasterVerifier
-import viper.silicon.decider.{Z3ProverStdIO, Cvc5ProverStdIO}
+import viper.silicon.decider.{Cvc5ProverStdIO, Z3ProverStdIO}
 import viper.silver.cfg.silver.SilverCfg
 import viper.silver.logger.ViperStdOutLogger
+
 import scala.util.chaining._
 
 object Silicon {
@@ -167,20 +169,16 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)]
 
     logger.debug(s"$name started ${new SimpleDateFormat("yyyy-MM-dd HH:mm:ss z").format(System.currentTimeMillis())}")
 
-    /* If available, save the filename corresponding to the program under verification in Verifier.inputFile.
-     * See also src/test/scala/SiliconTests.scala, where the analogous happens if Silicon is executed while
-     * running the test suite.
-     * Do not save the filename if the filename corresponds to the dummy one or `--ignoreFile` has been specified.
+    /* Do not save the filename if the filename corresponds to the dummy one or `--ignoreFile` has been specified.
      * Clients assume that the filename is ignored if `--ignoreFile` is used but calling `Paths.get` on it effectively
      * tries to parse the given string as path. For example, the following string causes an exception on Windows (and
      * only on Windows): `_programID_d:\a\test`
      *
      * TODO: Figure out what happens when ViperServer is used. */
-    config.file.foreach(filename => {
-      if (filename != Silicon.dummyInputFilename && !config.ignoreFile.getOrElse(false)) {
-        viper.silicon.verifier.Verifier.inputFile = Some(Paths.get(filename))
-      }
-    })
+    val inputFile: Option[String] =
+      if (config.file() != Silicon.dummyInputFilename && !config.ignoreFile.getOrElse(false)) Some(config.file())
+      else None
+    MultiRunRecorders.source = inputFile
 
     // TODO: Check consistency of cfgs.
     val consistencyErrors = utils.consistency.check(program)
@@ -192,7 +190,7 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)]
       val executor = Executors.newSingleThreadExecutor()
 
       val future = executor.submit(new Callable[List[Failure]] {
-        def call(): List[Failure] = runVerifier(program, cfgs)
+        def call(): List[Failure] = runVerifier(program, cfgs, inputFile)
       })
 
       try {
@@ -235,11 +233,11 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)]
     }
   }
 
-  private def runVerifier(program: ast.Program, cfgs: Seq[SilverCfg]): List[Failure] = {
+  private def runVerifier(program: ast.Program, cfgs: Seq[SilverCfg], inputFile: Option[String]): List[Failure] = {
 //    verifier.bookkeeper.branches = 1
     /*verifier.bookkeeper.*/startTime = System.currentTimeMillis()
 
-    val results = verifier.verify(program, cfgs)
+    val results = verifier.verify(program, cfgs, inputFile)
 
     /*verifier.bookkeeper.*/elapsedMillis = System.currentTimeMillis() - /*verifier.bookkeeper.*/startTime
 
@@ -373,8 +371,14 @@ class SiliconFrontend(override val reporter: Reporter,
   }
 }
 
-object SiliconRunner extends SiliconFrontend(StdIOReporter()) {
+object SiliconRunner extends SiliconRunnerInstance {
   def main(args: Array[String]): Unit = {
+    runMain(args)
+  }
+}
+
+class SiliconRunnerInstance extends SiliconFrontend(StdIOReporter()) {
+  def runMain(args: Array[String]): Unit = {
     var exitCode = 1 /* Only 0 indicates no error - we're pessimistic here */
 
     try {

src/main/scala/extensions/TryBlockParserPlugin.scala

@@ -6,13 +6,13 @@
 
 package viper.silicon.extensions
 
-import viper.silver.parser.FastParser._
-import viper.silver.parser.ParserExtension
+import viper.silver.parser.FastParser
 import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin}
 
-class TryBlockParserPlugin extends SilverPlugin with ParserPluginTemplate {
+class TryBlockParserPlugin(fp: FastParser) extends SilverPlugin with ParserPluginTemplate {
   import fastparse._
-  import viper.silver.parser.FastParser.whitespace
+  import viper.silver.parser.FastParserCompanion.whitespace
+  import fp.{FP, block, ParserExtension}
 
 
   private val tryKeyword = "try"

src/main/scala/interfaces/Preamble.scala

@@ -34,8 +34,6 @@ trait PreambleContributor[+SO, +SY, +AX] extends StatefulComponent {
 
   def axiomsAfterAnalysis: Iterable[AX]
   def emitAxiomsAfterAnalysis(sink: ProverLike): Unit
-
-  def updateGlobalStateAfterAnalysis(): Unit
 }
 
 trait VerifyingPreambleContributor[+SO, +SY, +AX, U <: ast.Node]
@@ -50,6 +48,4 @@ trait VerifyingPreambleContributor[+SO, +SY, +AX, U <: ast.Node]
 
   def axiomsAfterVerification: Iterable[AX]
   def emitAxiomsAfterVerification(sink: ProverLike): Unit
-
-  def contributeToGlobalStateAfterVerification(): Unit
 }

src/main/scala/interfaces/Verification.scala

@@ -7,13 +7,13 @@
 package viper.silicon.interfaces
 
 import viper.silicon.interfaces.state.Chunk
-import viper.silicon.reporting.{Converter, ExtractedModel, ExtractedModelEntry, GenericDomainInterpreter, 
-  ModelInterpreter, ExtractedFunction, DomainEntry, VarEntry, RefEntry, NullRefEntry, UnprocessedModelEntry}
+import viper.silicon.reporting.{Converter, DomainEntry, ExtractedFunction, ExtractedModel, ExtractedModelEntry, GenericDomainInterpreter, ModelInterpreter, NullRefEntry, RefEntry, UnprocessedModelEntry, VarEntry}
 import viper.silicon.state.{State, Store}
-import viper.silver.verifier.{Counterexample, FailureContext, Model, VerificationError, ValueEntry, ApplicationEntry, ConstantEntry}
+import viper.silver.verifier.{ApplicationEntry, ConstantEntry, Counterexample, FailureContext, Model, ValueEntry, VerificationError}
 import viper.silicon.state.terms.Term
 import viper.silicon.verifier.Verifier
 import viper.silver.ast
+import viper.silver.ast.Program
 
 /*
  * Results
@@ -144,11 +144,12 @@ case class SiliconVariableCounterexample(internalStore: Store, nativeModel: Mode
 case class SiliconMappedCounterexample(internalStore: Store,
                                        heap: Iterable[Chunk],
                                        oldHeaps: State.OldHeaps,
-                                       nativeModel: Model)
+                                       nativeModel: Model,
+                                       program: Program)
     extends SiliconCounterexample {
 
   val converter: Converter =
-    Converter(nativeModel, internalStore, heap, oldHeaps, Verifier.program)
+    Converter(nativeModel, internalStore, heap, oldHeaps, program)
 
   val model: Model = nativeModel
   val interpreter: ModelInterpreter[ExtractedModelEntry, Seq[ExtractedModelEntry]] = GenericDomainInterpreter(converter)
@@ -226,6 +227,6 @@ case class SiliconMappedCounterexample(internalStore: Store,
   }
 
   override def withStore(s: Store): SiliconCounterexample = {
-    SiliconMappedCounterexample(s, heap, oldHeaps, nativeModel)
+    SiliconMappedCounterexample(s, heap, oldHeaps, nativeModel, program)
   }
 }

src/main/scala/reporting/Converter.scala

@@ -622,7 +622,7 @@ object Converter {
       } catch {
         case _: Throwable => Seq()
       }
-      val translatedFunctions = x._1.functions.map(y => translateFunction(model, heap, y, x._2))
+      val translatedFunctions = x._1.functions.map(y => translateFunction(model, heap, y, x._2, program))
       DomainEntry(x._1.name, types, translatedFunctions)
     }).toSeq
   }
@@ -634,7 +634,7 @@ object Converter {
     val funcs = program.collect {
       case f: ast.Function => f
     }
-    funcs.map(x => translateFunction(model, heap, x, silicon.toMap(Nil))).toSeq
+    funcs.map(x => translateFunction(model, heap, x, silicon.toMap(Nil), program)).toSeq
   }
 
   def errorfunc(problem: String): ExtractedFunction =
@@ -648,7 +648,7 @@ object Converter {
     * @param genmap map of generic types to concrete types
     * @return
     */
-  def translateFunction(model: Model, heap: ExtractedHeap, func: ast.FuncLike, genmap: Map[ast.TypeVar, ast.Type]): ExtractedFunction = {
+  def translateFunction(model: Model, heap: ExtractedHeap, func: ast.FuncLike, genmap: Map[ast.TypeVar, ast.Type], program: ast.Program): ExtractedFunction = {
     def toSort(typ: ast.Type): Either[Throwable, Sort] = Try(symbolConverter.toSort(typ)).toEither
     def toSortWithSubstitutions(typ: ast.Type, typeErrorMsg: String): Either[String, Sort] = {
       toSort(typ)
@@ -675,7 +675,7 @@ object Converter {
 
     val smtfunc = func match {
       case t: ast.Function => symbolConverter.toFunction(t).id
-      case t: ast.DomainFunc => symbolConverter.toFunction(t, argSort :+ resSort).id
+      case t: ast.DomainFunc => symbolConverter.toFunction(t, argSort :+ resSort, program).id
       case t: ast.BackendFunc => symbolConverter.toFunction(t).id
     }
     val kek = smtfunc.toString

src/main/scala/reporting/MultiRunRecorder.scala

@@ -96,7 +96,7 @@ object MultiRunRecorders extends StatefulComponent {
   private val sinks = mutable.ArrayBuffer.empty[PrintWriter]
 
   protected def config: Config = Verifier.config
-  protected def source: Option[String] = Verifier.inputFile.map(_.toString)
+  var source: Option[String] = None
 
   protected def sink(name: String): PrintWriter = {
     val writer =

src/main/scala/rules/ChunkSupporter.scala

@@ -101,7 +101,7 @@ object chunkSupporter extends ChunkSupportRules {
                       (Q: (State, Heap, Option[Term], Verifier) => VerificationResult)
                       : VerificationResult = {
 
-    val id = ChunkIdentifier(resource, Verifier.program)
+    val id = ChunkIdentifier(resource, s.program)
     if (s.exhaleExt) {
       val failure = createFailure(ve, v, s)
       magicWandSupporter.transfer(s, perms, failure, v)(consumeGreedy(_, _, id, args, _, _))((s1, optCh, v1) =>
@@ -213,7 +213,7 @@ object chunkSupporter extends ChunkSupportRules {
                           (Q: (State, Term, Verifier) => VerificationResult)
                           : VerificationResult = {
 
-    val id = ChunkIdentifier(resource, Verifier.program)
+    val id = ChunkIdentifier(resource, s.program)
 
     findChunk[NonQuantifiedChunk](h.values, id, args, v) match {
       case Some(ch) if v.decider.check(IsPositive(ch.perm), Verifier.config.checkTimeout()) =>

src/main/scala/rules/Consumer.scala

@@ -247,7 +247,7 @@ object consumer extends ConsumptionRules {
         }
 
       case QuantifiedPermissionAssertion(forall, cond, acc: ast.PredicateAccessPredicate) =>
-        val predicate = Verifier.program.findPredicate(acc.loc.predicateName)
+        val predicate = s.program.findPredicate(acc.loc.predicateName)
         /* TODO: Quantified codomain variables are used in axioms and chunks (analogous to `?r`)
          *       and need to be instantiated in several places. Hence, they need to be known,
          *       which is more complicated if fresh identifiers are used.
@@ -284,9 +284,9 @@ object consumer extends ConsumptionRules {
         }
 
       case QuantifiedPermissionAssertion(forall, cond, wand: ast.MagicWand) =>
-        val bodyVars = wand.subexpressionsToEvaluate(Verifier.program)
+        val bodyVars = wand.subexpressionsToEvaluate(s.program)
         val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ)))
-        val qid = MagicWandIdentifier(wand, Verifier.program).toString
+        val qid = MagicWandIdentifier(wand, s.program).toString
         val optTrigger =
           if (forall.triggers.isEmpty) None
           else Some(forall.triggers)
@@ -344,9 +344,9 @@ object consumer extends ConsumptionRules {
               Q(s4, h3, snap, v3)})}))
 
       case ast.AccessPredicate(loc @ ast.PredicateAccess(eArgs, predname), ePerm)
-              if s.qpPredicates.contains(Verifier.program.findPredicate(predname)) =>
+              if s.qpPredicates.contains(s.program.findPredicate(predname)) =>
 
-        val predicate = Verifier.program.findPredicate(predname)
+        val predicate = s.program.findPredicate(predname)
         val formalVars = s.predicateFormalVarMap(predicate)
 
         evals(s, eArgs, _ => pve, v)((s1, tArgs, v1) =>
@@ -383,7 +383,7 @@ object consumer extends ConsumptionRules {
         eval(s, perm, pve, v)((s1, tPerm, v1) =>
           evalLocationAccess(s1, locacc, pve, v1)((s2, _, tArgs, v2) =>
             permissionSupporter.assertNotNegative(s2, tPerm, perm, pve, v2)((s3, v3) => {
-              val resource = locacc.res(Verifier.program)
+              val resource = locacc.res(s.program)
               val loss = PermTimes(tPerm, s3.permissionScalingFactor)
               val ve = pve dueTo InsufficientPermission(locacc)
               val description = s"consume ${a.pos}: $a"
@@ -396,17 +396,17 @@ object consumer extends ConsumptionRules {
         createFailure(viper.silicon.utils.consistency.createUnexpectedInhaleExhaleExpressionError(a), v, s)
 
       /* Handle wands */
-      case wand: ast.MagicWand if s.qpMagicWands.contains(MagicWandIdentifier(wand, Verifier.program)) =>
-        val bodyVars = wand.subexpressionsToEvaluate(Verifier.program)
+      case wand: ast.MagicWand if s.qpMagicWands.contains(MagicWandIdentifier(wand, s.program)) =>
+        val bodyVars = wand.subexpressionsToEvaluate(s.program)
         val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ)))
 
         evals(s, bodyVars, _ => pve, v)((s1, tArgs, v1) => {
           val (relevantChunks, _) =
-            quantifiedChunkSupporter.splitHeap[QuantifiedMagicWandChunk](s1.h, MagicWandIdentifier(wand, Verifier.program))
+            quantifiedChunkSupporter.splitHeap[QuantifiedMagicWandChunk](s1.h, MagicWandIdentifier(wand, s.program))
           val (smDef1, smCache1) =
             quantifiedChunkSupporter.summarisingSnapshotMap(
               s1, wand, formalVars, relevantChunks, v1)
-          v1.decider.assume(PredicateTrigger(MagicWandIdentifier(wand, Verifier.program).toString, smDef1.sm, tArgs))
+          v1.decider.assume(PredicateTrigger(MagicWandIdentifier(wand, s.program).toString, smDef1.sm, tArgs))
 
           val loss = PermTimes(FullPerm(), s1.permissionScalingFactor)
           quantifiedChunkSupporter.consumeSingleLocation(