Parses all inputs to 'GobraTests' in parallel before actually startin…

…g the unit tests
koflin · Mar 30, 2023 · 686b53d · 686b53d
1 parent c00c636
commit 686b53d
Show file tree

Hide file tree

Showing 2 changed files with 39 additions and 5 deletions.
diff --git a/src/main/scala/viper/gobra/frontend/Parser.scala b/src/main/scala/viper/gobra/frontend/Parser.scala
@@ -57,6 +57,18 @@ object Parser {
       }
     }
 
+    /** this is only used for unit testing to fill the parse cache */
+    def parseAll(pkgInfos: Vector[PackageInfo]): Map[PackageInfo, ParseResult] = {
+      val createdFuts = pkgInfos.map(pkgInfo => {
+        val pkg = RegularPackage(pkgInfo.id)
+        val parseJob = ParallelParseInfoJob(pkgInfo)
+        parallelManager.addIfAbsent(pkg, parseJob)(executionContext)
+          .map(res => (pkgInfo, res))(executionContext)
+      })
+      implicit val executor: GobraExecutionContext = executionContext
+      Await.result(Future.sequence(createdFuts), Duration.Inf).toMap
+    }
+
     trait ImportResolver {
       def pkgInfo: PackageInfo
 

diff --git a/src/test/scala/viper/gobra/GobraTests.scala b/src/test/scala/viper/gobra/GobraTests.scala
@@ -8,9 +8,11 @@ package viper.gobra
 
 import java.nio.file.Path
 import ch.qos.logback.classic.Level
-import org.scalatest.BeforeAndAfterAll
+import org.bitbucket.inkytonik.kiama.util.Source
+import org.scalatest.{Args, BeforeAndAfterAll, Status}
+import viper.gobra.frontend.Parser.ParseManager
 import viper.gobra.frontend.Source.FromFileSource
-import viper.gobra.frontend.{Config, PackageResolver, Source}
+import viper.gobra.frontend.{Config, PackageInfo, PackageResolver, Source}
 import viper.gobra.reporting.VerifierResult.{Failure, Success}
 import viper.gobra.reporting.{NoopReporter, VerifierError}
 import viper.silver.testing.{AbstractOutput, AnnotatedTestInput, ProjectInfo, SystemUnderTest}
@@ -30,12 +32,30 @@ class GobraTests extends AbstractGobraTests with BeforeAndAfterAll {
 
   var gobraInstance: Gobra = _
   var executor: GobraExecutionContext = _
+  var inputMapping: Vector[(PackageInfo, Vector[Source])] = Vector.empty
+  val cacheParser = true
 
   override def beforeAll(): Unit = {
     executor = new DefaultGobraExecutionContext()
     gobraInstance = new Gobra()
   }
 
+  override def registerTest(input: AnnotatedTestInput): Unit = {
+    super.registerTest(input)
+    val source = FromFileSource(input.file)
+    inputMapping = inputMapping :+ (Source.getPackageInfo(source, Path.of("")) -> Vector(source))
+  }
+
+  override def runTests(testName: Option[String], args: Args): Status = {
+    val inputMap = inputMapping.toMap
+    if (cacheParser) {
+      val config = Config(packageInfoInputMap = inputMap, cacheParser = true)
+      val parseManager = new ParseManager(config, executor)
+      parseManager.parseAll(inputMap.keys.toVector)
+    }
+    super.runTests(testName, args)
+  }
+
   override def afterAll(): Unit = {
     executor.terminateAndAssertInexistanceOfTimeout()
     gobraInstance = null
@@ -48,16 +68,18 @@ class GobraTests extends AbstractGobraTests with BeforeAndAfterAll {
 
       override def run(input: AnnotatedTestInput): Seq[AbstractOutput] = {
 
-        val source = FromFileSource(input.file)
         val config = Config(
           logLevel = Level.INFO,
           reporter = NoopReporter,
-          packageInfoInputMap = Map(Source.getPackageInfo(source, Path.of("")) -> Vector(source)),
+          packageInfoInputMap = inputMapping.toMap,
           checkConsistency = true,
+          cacheParser = cacheParser,
           z3Exe = z3Exe
         )
 
-        val (result, elapsedMilis) = time(() => Await.result(gobraInstance.verify(config.packageInfoInputMap.keys.head, config)(executor), Duration.Inf))
+        val source = FromFileSource(input.file)
+        val pkgInfo = Source.getPackageInfo(source, Path.of(""))
+        val (result, elapsedMilis) = time(() => Await.result(gobraInstance.verify(pkgInfo, config)(executor), Duration.Inf))
 
         info(s"Time required: $elapsedMilis ms")