From 8d24c0149cd9ef20835ca086fe7ef459e6b7dab8 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Thu, 29 Jun 2023 17:02:23 +0200 Subject: [PATCH] fixes compilation issue and undos parser caching for unit tests --- .../scala/viper/gobra/frontend/info/Info.scala | 6 +++--- src/test/scala/viper/gobra/GobraTests.scala | 7 ++++--- .../gobra/erasing/GhostErasureUnitTests.scala | 17 +++-------------- .../gobra/typing/ExprTypingUnitTests.scala | 16 +++------------- .../gobra/typing/StmtTypingUnitTests.scala | 16 +++------------- .../gobra/typing/TypeTypingUnitTests.scala | 16 +++------------- 6 files changed, 19 insertions(+), 59 deletions(-) diff --git a/src/main/scala/viper/gobra/frontend/info/Info.scala b/src/main/scala/viper/gobra/frontend/info/Info.scala index e474c1504..558e38a5d 100644 --- 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 index 97632dd79..71b0b33ff 100644 --- 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 index 5801caaa0..dd203575a 100644 --- a/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala +++ b/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala @@ -7,7 +7,7 @@ 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._ @@ -15,20 +15,9 @@ 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 index 1e0f7b4e8..ed9020f20 100644 --- 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 index f4dc6562b..dc3a3fbc7 100644 --- 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 index 4be78c86c..a248c2a15 100644 --- 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 = {