fixes compilation issue and undos parser caching for unit tests

viperproject · Jun 29, 2023 · 8d24c01 · 8d24c01
1 parent 046fe54
commit 8d24c01
Show file tree

Hide file tree

Showing 6 changed files with 19 additions and 59 deletions.
diff --git a/src/main/scala/viper/gobra/frontend/info/Info.scala b/src/main/scala/viper/gobra/frontend/info/Info.scala
@@ -206,7 +206,7 @@ object Info extends LazyLogging {
       private def typeCheck(pkgSources: Vector[Source], pkg: PPackage, dependentTypeInfo: DependentTypeInfo, isMainContext: Boolean = false, isLazy: Boolean = false): TypeCheckResult = {
         val startMs = System.currentTimeMillis()
         logger.trace(s"start type-checking ${pkg.info.id}")
-        val res = Info.checkSources(pkgSources, pkg, dependentTypeInfo, isMainContext = isMainContext)(config, executionContext)
+        val res = Info.checkSources(pkgSources, pkg, dependentTypeInfo, isMainContext = isMainContext)(config)
         logger.trace {
           val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f"
           s"type-checking ${pkg.info.id} done (took ${durationS}s with ${res.map(info => info.tree.nodes.length.toString).getOrElse("_")} nodes)"
@@ -285,12 +285,12 @@ object Info extends LazyLogging {
     typeInfoCache.clear()
   }
 
-  def checkSources(sources: Vector[Source], pkg: PPackage, dependentTypeInfo: Map[AbstractImport, () => Either[Vector[VerifierError], ExternalTypeInfo]], isMainContext: Boolean = false)(config: Config, executionContext: GobraExecutionContext): TypeCheckResult = {
+  def checkSources(sources: Vector[Source], pkg: PPackage, dependentTypeInfo: Map[AbstractImport, () => Either[Vector[VerifierError], ExternalTypeInfo]], isMainContext: Boolean = false)(config: Config): TypeCheckResult = {
     var cacheHit: Boolean = true
     def getTypeInfo(pkg: PPackage, dependentTypeInfo: Map[AbstractImport, () => Either[Vector[VerifierError], ExternalTypeInfo]], isMainContext: Boolean, config: Config): TypeInfoImpl = {
       cacheHit = false
       val tree = new GoTree(pkg)
-      new TypeInfoImpl(tree, dependentTypeInfo, isMainContext)(config: Config, executionContext)
+      new TypeInfoImpl(tree, dependentTypeInfo, isMainContext)(config: Config)
     }
 
     def getTypeInfoCached(pkg: PPackage, dependentTypeInfo: Map[AbstractImport, () => Either[Vector[VerifierError], ExternalTypeInfo]], isMainContext: Boolean, config: Config): TypeInfoImpl = {

diff --git a/src/test/scala/viper/gobra/GobraTests.scala b/src/test/scala/viper/gobra/GobraTests.scala
@@ -51,8 +51,8 @@ class GobraTests extends AbstractGobraTests with BeforeAndAfterAll {
   }
 
   override def runTests(testName: Option[String], args: Args): Status = {
-    val inputMap = inputMapping.toMap
     if (cacheParser) {
+      val inputMap = inputMapping.toMap
       val config = Config(packageInfoInputMap = inputMap, cacheParser = true)
       val parseManager = new ParseManager(config, executor)
       parseManager.parseAll(inputMap.keys.toVector)
@@ -72,16 +72,17 @@ class GobraTests extends AbstractGobraTests with BeforeAndAfterAll {
 
       override def run(input: AnnotatedTestInput): Seq[AbstractOutput] = {
 
+        val source = FromFileSource(input.file)
+        val packageInfoInputMap = if (cacheParser) inputMapping.toMap else Map(Source.getPackageInfo(source, Path.of("")) -> Vector(source))
         val config = Config(
           logLevel = Level.INFO,
           reporter = NoopReporter,
-          packageInfoInputMap = inputMapping.toMap,
+          packageInfoInputMap = packageInfoInputMap,
           checkConsistency = true,
           cacheParser = cacheParser,
           z3Exe = z3Exe
         )
 
-        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))
 

diff --git a/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala b/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala
@@ -7,28 +7,17 @@
 package viper.gobra.erasing
 
 import org.bitbucket.inkytonik.kiama.util.{Positions, StringSource}
-import org.scalatest.{Assertion, BeforeAndAfterAll, Inside, Succeeded}
+import org.scalatest.{Assertion, Inside, Succeeded}
 import org.scalatest.funsuite.AnyFunSuite
 import org.scalatest.matchers.should.Matchers
 import viper.gobra.ast.frontend._
 import viper.gobra.frontend.{Config, PackageInfo, Parser}
 import viper.gobra.frontend.info.Info
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.frontend.info.implementation.typing.ghost.separation.GhostLessPrinter
-import viper.gobra.util.{DefaultGobraExecutionContext, GobraExecutionContext}
 
-class GhostErasureUnitTests extends AnyFunSuite with Matchers with Inside with BeforeAndAfterAll {
+class GhostErasureUnitTests extends AnyFunSuite with Matchers with Inside {
   val frontend = new TestFrontend()
-  var executor: GobraExecutionContext = _
-
-  override def beforeAll(): Unit = {
-    executor = new DefaultGobraExecutionContext()
-  }
-
-  override def afterAll(): Unit = {
-    executor.terminateAndAssertInexistanceOfTimeout()
-  }
-
   test("Ghost Erasure: variable declaration should not have a trailing equal sign") {
     // var value int
     val decl = PVarDecl(Some(PIntType()), Vector(), Vector(PIdnDef("value")), Vector(false))
@@ -353,7 +342,7 @@ class GhostErasureUnitTests extends AnyFunSuite with Matchers with Inside with B
       )
       val tree = new Info.GoTree(pkg)
       val config = Config()
-      val info = new TypeInfoImpl(tree, Map.empty)(config, executor)
+      val info = new TypeInfoImpl(tree, Map.empty)(config)
       info.errors match {
         case Vector(msgs) => fail(s"Type-checking failed: $msgs")
         case _ =>

diff --git a/src/test/scala/viper/gobra/typing/ExprTypingUnitTests.scala b/src/test/scala/viper/gobra/typing/ExprTypingUnitTests.scala
@@ -8,27 +8,17 @@ package viper.gobra.typing
 
 import org.bitbucket.inkytonik.kiama.util.Positions
 import org.scalatest.funsuite.AnyFunSuite
-import org.scalatest.{BeforeAndAfterAll, Inside}
+import org.scalatest.Inside
 import org.scalatest.matchers.should.Matchers
 import viper.gobra.ast.frontend._
 import viper.gobra.frontend.{Config, PackageInfo}
 import viper.gobra.frontend.info.Info
 import viper.gobra.frontend.info.base.Type
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
-import viper.gobra.util.{DefaultGobraExecutionContext, GobraExecutionContext}
 import viper.gobra.util.TypeBounds.{DefaultInt, UnboundedInteger}
 
-class ExprTypingUnitTests extends AnyFunSuite with Matchers with Inside with BeforeAndAfterAll {
+class ExprTypingUnitTests extends AnyFunSuite with Matchers with Inside {
   val frontend = new TestFrontend()
-  var executor: GobraExecutionContext = _
-
-  override def beforeAll(): Unit = {
-    executor = new DefaultGobraExecutionContext()
-  }
-
-  override def afterAll(): Unit = {
-    executor.terminateAndAssertInexistanceOfTimeout()
-  }
 
   test("TypeChecker: should classify an integer literal as integer") {
     frontend.exprType(PIntLit(42))() should matchPattern {
@@ -3402,7 +3392,7 @@ class ExprTypingUnitTests extends AnyFunSuite with Matchers with Inside with Bef
       )
       val tree = new Info.GoTree(pkg)
       val config = Config()
-      new TypeInfoImpl(tree, Map.empty)(config, executor)
+      new TypeInfoImpl(tree, Map.empty)(config)
     }
 
     def exprType(expr : PExpression)(inArgs: Vector[(PParameter, Boolean)] = Vector()) : Type.Type =

diff --git a/src/test/scala/viper/gobra/typing/StmtTypingUnitTests.scala b/src/test/scala/viper/gobra/typing/StmtTypingUnitTests.scala
@@ -6,7 +6,7 @@
 
 package viper.gobra.typing
 
-import org.scalatest.{BeforeAndAfterAll, Inside}
+import org.scalatest.Inside
 import org.scalatest.matchers.should.Matchers
 import org.scalatest.funsuite.AnyFunSuite
 import viper.gobra.ast.frontend._
@@ -15,19 +15,9 @@ import org.bitbucket.inkytonik.kiama.util.Positions
 import viper.gobra.frontend.PackageInfo
 import viper.gobra.frontend.info.Info
 import viper.gobra.frontend.Config
-import viper.gobra.util.{DefaultGobraExecutionContext, GobraExecutionContext}
 
-class StmtTypingUnitTests extends AnyFunSuite with Matchers with Inside with BeforeAndAfterAll {
+class StmtTypingUnitTests extends AnyFunSuite with Matchers with Inside {
   val frontend = new TestFrontend()
-  var executor: GobraExecutionContext = _
-
-  override def beforeAll(): Unit = {
-    executor = new DefaultGobraExecutionContext()
-  }
-
-  override def afterAll(): Unit = {
-    executor.terminateAndAssertInexistanceOfTimeout()
-  }
 
   test("TypeChecker: should detect labeled continues outside of loops") {
     assert(!frontend.wellDefStmt(PContinue(Some(PLabelUse("l"))))().valid)
@@ -92,7 +82,7 @@ class StmtTypingUnitTests extends AnyFunSuite with Matchers with Inside with Bef
       )
       val tree = new Info.GoTree(pkg)
       val config = Config()
-      new TypeInfoImpl(tree, Map.empty)(config, executor)
+      new TypeInfoImpl(tree, Map.empty)(config)
     }
 
     def wellDefStmt(stmt : PStatement)(inArgs: Vector[(PParameter, Boolean)] = Vector()) =

diff --git a/src/test/scala/viper/gobra/typing/TypeTypingUnitTests.scala b/src/test/scala/viper/gobra/typing/TypeTypingUnitTests.scala
@@ -9,26 +9,16 @@ package viper.gobra.typing
 import org.bitbucket.inkytonik.kiama.util.Positions
 import org.scalatest.funsuite.AnyFunSuite
 import org.scalatest.matchers.should.Matchers
-import org.scalatest.{BeforeAndAfterAll, Inside}
+import org.scalatest.Inside
 import viper.gobra.ast.frontend._
 import viper.gobra.frontend.{Config, PackageInfo}
 import viper.gobra.frontend.info.Info
 import viper.gobra.frontend.info.base.Type
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
-import viper.gobra.util.{DefaultGobraExecutionContext, GobraExecutionContext}
 import viper.gobra.util.TypeBounds.DefaultInt
 
-class TypeTypingUnitTests extends AnyFunSuite with Matchers with Inside with BeforeAndAfterAll {
+class TypeTypingUnitTests extends AnyFunSuite with Matchers with Inside {
   val frontend = new TestFrontend()
-  var executor: GobraExecutionContext = _
-
-  override def beforeAll(): Unit = {
-    executor = new DefaultGobraExecutionContext()
-  }
-
-  override def afterAll(): Unit = {
-    executor.terminateAndAssertInexistanceOfTimeout()
-  }
 
   test("Typing: should correctly type an integer sequence type") {
     val t = PSequenceType(PIntType())
@@ -389,7 +379,7 @@ class TypeTypingUnitTests extends AnyFunSuite with Matchers with Inside with Bef
       )
       val tree = new Info.GoTree(pkg)
       val config = Config()
-      new TypeInfoImpl(tree, Map.empty)(config, executor)
+      new TypeInfoImpl(tree, Map.empty)(config)
     }
 
     def areComparable(t1 : PType, t2 : PType) : Boolean = {