From aadeda532c7db89eaba584489690a85614d43cd6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Thu, 14 Jul 2022 10:56:50 +0200 Subject: [PATCH] Add tests for carbon --- .../viper/gobra/GobraCarbonPackageTests.scala | 138 ++++++++++++++++++ ...scala => GobraCarbonRegressionTests.scala} | 8 +- ...s.scala => GobraSiliconPackageTests.scala} | 4 +- .../gobra/GobraSiliconRegressionTests.scala | 90 ++++++++++++ 4 files changed, 236 insertions(+), 4 deletions(-) create mode 100644 src/test/scala/viper/gobra/GobraCarbonPackageTests.scala rename src/test/scala/viper/gobra/{GobraTests.scala => GobraCarbonRegressionTests.scala} (94%) rename src/test/scala/viper/gobra/{GobraPackageTests.scala => GobraSiliconPackageTests.scala} (97%) create mode 100644 src/test/scala/viper/gobra/GobraSiliconRegressionTests.scala diff --git a/src/test/scala/viper/gobra/GobraCarbonPackageTests.scala b/src/test/scala/viper/gobra/GobraCarbonPackageTests.scala new file mode 100644 index 000000000..c54ed703c --- /dev/null +++ b/src/test/scala/viper/gobra/GobraCarbonPackageTests.scala @@ -0,0 +1,138 @@ +// 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-2020 ETH Zurich. + +package viper.gobra + +import ch.qos.logback.classic.Level +import org.bitbucket.inkytonik.kiama.util.Source +import org.rogach.scallop.exceptions.ValidationFailure +import org.rogach.scallop.throwError +import viper.gobra.backend.ViperBackends +import viper.gobra.frontend.Source.FromFileSource +import viper.gobra.frontend.{Config, PackageInfo, ScallopGobraConfig, Source} +import viper.gobra.reporting.VerifierResult.{Failure, Success} +import viper.gobra.reporting.{NoopReporter, ParserError} +import viper.silver.testing._ +import viper.silver.utility.TimingUtils + +import java.io.File +import java.nio.file.Path +import scala.concurrent.Await +import scala.concurrent.duration.Duration + +class GobraCarbonPackageTests extends GobraCarbonRegressionTests { + val samePackagePropertyName = "GOBRATESTS_SAME_PACKAGE_DIR" + val builtinPackagePropertyName = "GOBRATESTS_BUILTIN_PACKAGES_DIR" + val stubPackagesPropertyName = "GOBRATESTS_STUB_PACKAGES_DIR" + + val samePackageDir: String = System.getProperty(samePackagePropertyName, "same_package") + val builtinStubDir: String = System.getProperty(builtinPackagePropertyName, "builtin") + val stubPackagesDir: String = System.getProperty(stubPackagesPropertyName, "stubs") + + override val testDirectories: Seq[String] = Vector(samePackageDir, builtinStubDir, stubPackagesDir) + + override def buildTestInput(file: Path, prefix: String): DefaultAnnotatedTestInput = { + // get package clause of file and collect all other files belonging to this package: + val input = for { + pkgName <- getPackageClause(file.toFile) + currentDir = file.getParent.toFile + samePkgFiles = currentDir.listFiles + .filter(_.isFile) + .map(f => (f, getPackageClause(f))) + .filter { case (_, Some(clause)) if clause == pkgName => true } + .map { case (f, _) => f.toPath } + .sortBy(_.toString) + .toSeq + } yield DefaultTestInput(s"$prefix/$pkgName (${file.getFileName.toString})", prefix, samePkgFiles, Seq()) + GobraAnnotatedTestInput(input.get) + } + + override val gobraInstanceUnderTest: SystemUnderTest = + new SystemUnderTest with TimingUtils { + /** For filtering test annotations. Does not need to be unique. */ + override val projectInfo: ProjectInfo = new ProjectInfo(List("Gobra")) + + override def run(input: AnnotatedTestInput): Seq[AbstractOutput] = { + // test scallop parsing by giving package name and testing whether the same set of files is created + val currentDir = input.file.getParent + val parsedConfig = for { + pkgName <- getPackageClause(input.file.toFile) + config <- createConfig(Array( + "--logLevel", "INFO", + "--directory", currentDir.toFile.getPath, + "--projectRoot", currentDir.toFile.getPath, // otherwise, it assumes Gobra's root directory as the project root + "-I", currentDir.toFile.getPath + )) + } yield config + + val pkgInfo = Source.getPackageInfo(FromFileSource(input.files.head), currentDir) + + val config = Config( + logLevel = Level.INFO, + reporter = NoopReporter, + packageInfoInputMap = Map(pkgInfo -> input.files.toVector.map(FromFileSource(_))), + includeDirs = Vector(currentDir), + checkConsistency = true, + backend = ViperBackends.CarbonBackend, + z3Exe = z3Exe + ) + + val (result, elapsedMilis) = time(() => Await.result(gobraInstance.verify(pkgInfo, config)(executor), Duration.Inf)) + + info(s"Time required: $elapsedMilis ms") + + equalConfigs(parsedConfig.get, config) ++ (result match { + case Success => Vector.empty + case Failure(errors) => errors map GobraTestOuput + }) + } + } + + private lazy val pkgClauseRegex = """(?:\/\/.*|\/\*(?:.|\n)*\*\/|package(?:\s|\n)+([a-zA-Z_][a-zA-Z0-9_]*))""".r + + private def getPackageClause(file: File): Option[String] = { + val bufferedSource = scala.io.Source.fromFile(file) + val content = bufferedSource.mkString + bufferedSource.close() + // TODO is there a way to perform the regex lazily on the file's content? + pkgClauseRegex + .findAllMatchIn(content) + .collectFirst { case m if m.group(1) != null => m.group(1) } + } + + private def createConfig(args: Array[String]): Option[Config] = { + try { + // set throwError to true: Scallop will throw an exception instead of terminating the program in case an + // exception occurs (e.g. a validation failure) + throwError.value = true + + new ScallopGobraConfig(args.toSeq).config.toOption + } catch { + case _: ValidationFailure => None + case other: Throwable => throw other + } + } + + private def equalConfigs(config1: Config, config2: Config): Vector[GobraTestOuput] = { + def equalFiles(v1: Vector[Path], v2: Vector[Path]): Boolean = v1.sortBy(_.toString).equals(v2.sortBy(_.toString)) + + /** + * Checks that two given maps contain the same PPackageInfo source mapping + */ + def equalPkgInfoSourceMaps(v1: Map[PackageInfo, Vector[Source]], v2: Map[PackageInfo, Vector[Source]]): Boolean = { + val keys = (v1.keys ++ v2.keys).toSet + keys.forall(pkgInfo => + v1.contains(pkgInfo) && v2.contains(pkgInfo) && v1(pkgInfo).map(_.name).sorted.equals(v2(pkgInfo).map(_.name).sorted) + ) + } + + val equal = (equalPkgInfoSourceMaps(config1.packageInfoInputMap, config2.packageInfoInputMap) + && equalFiles(config1.includeDirs, config2.includeDirs) + && config1.logLevel == config2.logLevel) + if (equal) Vector() + else Vector(GobraTestOuput(ParserError("unexpected results for conversion of package clause to input files", None))) + } +} diff --git a/src/test/scala/viper/gobra/GobraTests.scala b/src/test/scala/viper/gobra/GobraCarbonRegressionTests.scala similarity index 94% rename from src/test/scala/viper/gobra/GobraTests.scala rename to src/test/scala/viper/gobra/GobraCarbonRegressionTests.scala index a719e5a26..f2bd4aad6 100644 --- a/src/test/scala/viper/gobra/GobraTests.scala +++ b/src/test/scala/viper/gobra/GobraCarbonRegressionTests.scala @@ -6,21 +6,22 @@ package viper.gobra -import java.nio.file.Path import ch.qos.logback.classic.Level import org.scalatest.BeforeAndAfterAll +import viper.gobra.backend.ViperBackends import viper.gobra.frontend.Source.FromFileSource import viper.gobra.frontend.{Config, PackageResolver, Source} import viper.gobra.reporting.VerifierResult.{Failure, Success} import viper.gobra.reporting.{NoopReporter, VerifierError} +import viper.gobra.util.{DefaultGobraExecutionContext, GobraExecutionContext} import viper.silver.testing.{AbstractOutput, AnnotatedTestInput, ProjectInfo, SystemUnderTest} import viper.silver.utility.TimingUtils -import viper.gobra.util.{DefaultGobraExecutionContext, GobraExecutionContext} +import java.nio.file.Path import scala.concurrent.Await import scala.concurrent.duration.Duration -class GobraTests extends AbstractGobraTests with BeforeAndAfterAll { +class GobraCarbonRegressionTests extends AbstractGobraTests with BeforeAndAfterAll { val regressionsPropertyName = "GOBRATESTS_REGRESSIONS_DIR" @@ -54,6 +55,7 @@ class GobraTests extends AbstractGobraTests with BeforeAndAfterAll { reporter = NoopReporter, packageInfoInputMap = Map(Source.getPackageInfo(source, Path.of("")) -> Vector(source)), checkConsistency = true, + backend = ViperBackends.CarbonBackend, z3Exe = z3Exe ) diff --git a/src/test/scala/viper/gobra/GobraPackageTests.scala b/src/test/scala/viper/gobra/GobraSiliconPackageTests.scala similarity index 97% rename from src/test/scala/viper/gobra/GobraPackageTests.scala rename to src/test/scala/viper/gobra/GobraSiliconPackageTests.scala index 8b170788d..9d71819b3 100644 --- a/src/test/scala/viper/gobra/GobraPackageTests.scala +++ b/src/test/scala/viper/gobra/GobraSiliconPackageTests.scala @@ -12,6 +12,7 @@ import ch.qos.logback.classic.Level import org.bitbucket.inkytonik.kiama.util.Source import org.rogach.scallop.exceptions.ValidationFailure import org.rogach.scallop.throwError +import viper.gobra.backend.ViperBackends import viper.gobra.frontend.Source.FromFileSource import viper.gobra.frontend.{Config, PackageInfo, ScallopGobraConfig, Source} import viper.gobra.reporting.{NoopReporter, ParserError} @@ -22,7 +23,7 @@ import viper.silver.utility.TimingUtils import scala.concurrent.Await import scala.concurrent.duration.Duration -class GobraPackageTests extends GobraTests { +class GobraSiliconPackageTests extends GobraSiliconRegressionTests { val samePackagePropertyName = "GOBRATESTS_SAME_PACKAGE_DIR" val builtinPackagePropertyName = "GOBRATESTS_BUILTIN_PACKAGES_DIR" val stubPackagesPropertyName = "GOBRATESTS_STUB_PACKAGES_DIR" @@ -75,6 +76,7 @@ class GobraPackageTests extends GobraTests { packageInfoInputMap = Map(pkgInfo -> input.files.toVector.map(FromFileSource(_))), includeDirs = Vector(currentDir), checkConsistency = true, + backend = ViperBackends.SiliconBackend, z3Exe = z3Exe ) diff --git a/src/test/scala/viper/gobra/GobraSiliconRegressionTests.scala b/src/test/scala/viper/gobra/GobraSiliconRegressionTests.scala new file mode 100644 index 000000000..0938e7cd8 --- /dev/null +++ b/src/test/scala/viper/gobra/GobraSiliconRegressionTests.scala @@ -0,0 +1,90 @@ +// 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-2020 ETH Zurich. + +package viper.gobra + +import java.nio.file.Path +import ch.qos.logback.classic.Level +import org.scalatest.BeforeAndAfterAll +import viper.gobra.backend.ViperBackends +import viper.gobra.frontend.Source.FromFileSource +import viper.gobra.frontend.{Config, PackageResolver, Source} +import viper.gobra.reporting.VerifierResult.{Failure, Success} +import viper.gobra.reporting.{NoopReporter, VerifierError} +import viper.silver.testing.{AbstractOutput, AnnotatedTestInput, ProjectInfo, SystemUnderTest} +import viper.silver.utility.TimingUtils +import viper.gobra.util.{DefaultGobraExecutionContext, GobraExecutionContext} + +import scala.concurrent.Await +import scala.concurrent.duration.Duration + +class GobraSiliconRegressionTests extends AbstractGobraTests with BeforeAndAfterAll { + + val regressionsPropertyName = "GOBRATESTS_REGRESSIONS_DIR" + + val regressionsDir: String = System.getProperty(regressionsPropertyName, "regressions") + val testDirectories: Seq[String] = Vector(regressionsDir) + override val defaultTestPattern: String = PackageResolver.inputFilePattern + + var gobraInstance: Gobra = _ + var executor: GobraExecutionContext = _ + + override def beforeAll(): Unit = { + executor = new DefaultGobraExecutionContext() + gobraInstance = new Gobra() + } + + override def afterAll(): Unit = { + executor.terminateAndAssertInexistanceOfTimeout() + gobraInstance = null + } + + val gobraInstanceUnderTest: SystemUnderTest = + new SystemUnderTest with TimingUtils { + /** For filtering test annotations. Does not need to be unique. */ + override val projectInfo: ProjectInfo = new ProjectInfo(List("Gobra")) + + 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)), + checkConsistency = true, + backend = ViperBackends.SiliconBackend, + z3Exe = z3Exe + ) + + val (result, elapsedMilis) = time(() => Await.result(gobraInstance.verify(config.packageInfoInputMap.keys.head, config)(executor), Duration.Inf)) + + info(s"Time required: $elapsedMilis ms") + + result match { + case Success => Vector.empty + case Failure(errors) => errors map GobraTestOuput + } + } + } + + + /** + * The systems to test each input on. + * + * This method is not modeled as a constant field deliberately, such that + * subclasses can instantiate a new [[viper.silver.testing.SystemUnderTest]] + * for each test input. + */ + override def systemsUnderTest: Seq[SystemUnderTest] = Vector(gobraInstanceUnderTest) + + case class GobraTestOuput(error: VerifierError) extends AbstractOutput { + /** Whether the output belongs to the given line in the given file. */ + override def isSameLine(file: Path, lineNr: Int): Boolean = error.position.exists(_.line == lineNr) + + /** A short and unique identifier for this output. */ + override def fullId: String = error.id + } +}