From 91c10fe9b64b94d434295a880676454e80822a4f Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Tue, 21 Jan 2025 11:10:37 +0100 Subject: [PATCH 1/8] adds unit tests for all supported backends --- .../viper/gobra/backend/BackendVerifier.scala | 4 ++-- .../scala/viper/gobra/frontend/Config.scala | 22 +++++++++++++------ .../features/backends/carbon.gobra | 10 +++++++++ .../features/backends/silicon.gobra | 10 +++++++++ .../features/backends/vs-with-carbon.gobra | 10 +++++++++ .../features/backends/vs-with-silicon.gobra | 10 +++++++++ 6 files changed, 57 insertions(+), 9 deletions(-) create mode 100644 src/test/resources/regressions/features/backends/carbon.gobra create mode 100644 src/test/resources/regressions/features/backends/silicon.gobra create mode 100644 src/test/resources/regressions/features/backends/vs-with-carbon.gobra create mode 100644 src/test/resources/regressions/features/backends/vs-with-silicon.gobra diff --git a/src/main/scala/viper/gobra/backend/BackendVerifier.scala b/src/main/scala/viper/gobra/backend/BackendVerifier.scala index 873fd7179..40668aa39 100644 --- a/src/main/scala/viper/gobra/backend/BackendVerifier.scala +++ b/src/main/scala/viper/gobra/backend/BackendVerifier.scala @@ -41,14 +41,14 @@ object BackendVerifier { case _ => } - (config.backend, config.boogieExe) match { + (config.backendOrDefault, config.boogieExe) match { case (Carbon, Some(boogieExe)) => exePaths ++= Vector("--boogieExe", boogieExe) case _ => } val verificationResults: Future[VerificationResult] = { - val verifier = config.backend.create(exePaths, config) + val verifier = config.backendOrDefault.create(exePaths, config) val reporter = BacktranslatingReporter(config.reporter, task.backtrack, config) if (!config.shouldChop) { diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala index 0ba06416b..3e6e1d4f2 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/src/main/scala/viper/gobra/frontend/Config.scala @@ -129,7 +129,8 @@ case class Config( includeDirs: Vector[Path] = ConfigDefaults.DefaultIncludeDirs.map(_.toPath).toVector, projectRoot: Path = ConfigDefaults.DefaultProjectRoot.toPath, reporter: GobraReporter = ConfigDefaults.DefaultReporter, - backend: ViperBackend = ConfigDefaults.DefaultBackend, + // `None` indicates that no backend has been specified and instructs Gobra to use the default backend + backend: Option[ViperBackend] = None, isolate: Option[Vector[SourcePosition]] = None, choppingUpperBound: Int = ConfigDefaults.DefaultChoppingUpperBound, packageTimeout: Duration = ConfigDefaults.DefaultPackageTimeout, @@ -194,7 +195,12 @@ case class Config( projectRoot = projectRoot, includeDirs = (includeDirs ++ other.includeDirs).distinct, reporter = reporter, - backend = backend, + backend = (backend, other.backend) match { + case (l, None) => l + case (None, r) => r + case (l, r) if l == r => l + case (Some(l), Some(r)) => Violation.violation(s"Unable to merge differing backends from in-file configuration options, got $l and $r") + }, isolate = (isolate, other.isolate) match { case (None, r) => r case (l, None) => l @@ -241,6 +247,8 @@ case class Config( } else { TypeBounds(Int = TypeBounds.IntWith64Bit, UInt = TypeBounds.UIntWith64Bit) } + + lazy val backendOrDefault: ViperBackend = backend.getOrElse(ConfigDefaults.DefaultBackend) } object Config { @@ -259,7 +267,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector moduleName: String = ConfigDefaults.DefaultModuleName, includeDirs: Vector[Path] = ConfigDefaults.DefaultIncludeDirs.map(_.toPath).toVector, reporter: GobraReporter = ConfigDefaults.DefaultReporter, - backend: ViperBackend = ConfigDefaults.DefaultBackend, + backend: Option[ViperBackend] = None, // list of pairs of file and line numbers. Indicates which lines of files should be isolated. isolate: List[(Path, List[Int])] = ConfigDefaults.DefaultIsolate, choppingUpperBound: Int = ConfigDefaults.DefaultChoppingUpperBound, @@ -564,7 +572,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals choices = Seq("SILICON", "CARBON", "VSWITHSILICON", "VSWITHCARBON"), name = "backend", descr = "Specifies the used Viper backend. The default is SILICON.", - default = Some("SILICON"), + default = None, noshort = true ).map{ case "SILICON" => ViperBackends.SiliconBackend @@ -864,8 +872,8 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals conflicts(directory, List(inclPackages, exclPackages)) // must be lazy to guarantee that this value is computed only during the CLI options validation and not before. - lazy val isSiliconBasedBackend = backend.toOption match { - case Some(ViperBackends.SiliconBackend | _: ViperBackends.ViperServerWithSilicon) => true + lazy val isSiliconBasedBackend = backend.toOption.getOrElse(ConfigDefaults.DefaultBackend) match { + case ViperBackends.SiliconBackend | _: ViperBackends.ViperServerWithSilicon => true case _ => false } @@ -1014,7 +1022,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals printInternal = printInternal(), printVpr = printVpr(), streamErrs = !noStreamErrors()), - backend = backend(), + backend = backend.toOption, isolate = isolate, choppingUpperBound = chopUpperBound(), packageTimeout = packageTimeoutDuration, diff --git a/src/test/resources/regressions/features/backends/carbon.gobra b/src/test/resources/regressions/features/backends/carbon.gobra new file mode 100644 index 000000000..a0efc7ca6 --- /dev/null +++ b/src/test/resources/regressions/features/backends/carbon.gobra @@ -0,0 +1,10 @@ +package carbon + +// ##(--backend CARBON) + +// tests whether the carbon backend is operational + +func foo() { + //:: ExpectedOutput(assert_error:assertion_error) + assert false; +} diff --git a/src/test/resources/regressions/features/backends/silicon.gobra b/src/test/resources/regressions/features/backends/silicon.gobra new file mode 100644 index 000000000..7b942ad9f --- /dev/null +++ b/src/test/resources/regressions/features/backends/silicon.gobra @@ -0,0 +1,10 @@ +package silicon + +// ##(--backend SILICON) + +// tests whether the silicon backend is operational + +func foo() { + //:: ExpectedOutput(assert_error:assertion_error) + assert false; +} diff --git a/src/test/resources/regressions/features/backends/vs-with-carbon.gobra b/src/test/resources/regressions/features/backends/vs-with-carbon.gobra new file mode 100644 index 000000000..d67396873 --- /dev/null +++ b/src/test/resources/regressions/features/backends/vs-with-carbon.gobra @@ -0,0 +1,10 @@ +package vswithcarbon + +// ##(--backend VSWITHCARBON) + +// tests whether the carbon backend in connection with ViperServer is operational + +func foo() { + //:: ExpectedOutput(assert_error:assertion_error) + assert false; +} diff --git a/src/test/resources/regressions/features/backends/vs-with-silicon.gobra b/src/test/resources/regressions/features/backends/vs-with-silicon.gobra new file mode 100644 index 000000000..d7980c360 --- /dev/null +++ b/src/test/resources/regressions/features/backends/vs-with-silicon.gobra @@ -0,0 +1,10 @@ +package vswithsilicon + +// ##(--backend VSWITHSILICON) + +// tests whether the silicon backend in connection with ViperServer is operational + +func foo() { + //:: ExpectedOutput(assert_error:assertion_error) + assert false; +} From 8278e4cd436f25a878c1b723053677f014148f05 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Tue, 21 Jan 2025 11:28:47 +0100 Subject: [PATCH 2/8] fixes license headers --- src/test/resources/regressions/features/backends/carbon.gobra | 3 +++ src/test/resources/regressions/features/backends/silicon.gobra | 3 +++ .../regressions/features/backends/vs-with-carbon.gobra | 3 +++ .../regressions/features/backends/vs-with-silicon.gobra | 3 +++ 4 files changed, 12 insertions(+) diff --git a/src/test/resources/regressions/features/backends/carbon.gobra b/src/test/resources/regressions/features/backends/carbon.gobra index a0efc7ca6..b38457789 100644 --- a/src/test/resources/regressions/features/backends/carbon.gobra +++ b/src/test/resources/regressions/features/backends/carbon.gobra @@ -1,3 +1,6 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + package carbon // ##(--backend CARBON) diff --git a/src/test/resources/regressions/features/backends/silicon.gobra b/src/test/resources/regressions/features/backends/silicon.gobra index 7b942ad9f..935d9a27d 100644 --- a/src/test/resources/regressions/features/backends/silicon.gobra +++ b/src/test/resources/regressions/features/backends/silicon.gobra @@ -1,3 +1,6 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + package silicon // ##(--backend SILICON) diff --git a/src/test/resources/regressions/features/backends/vs-with-carbon.gobra b/src/test/resources/regressions/features/backends/vs-with-carbon.gobra index d67396873..42f25abba 100644 --- a/src/test/resources/regressions/features/backends/vs-with-carbon.gobra +++ b/src/test/resources/regressions/features/backends/vs-with-carbon.gobra @@ -1,3 +1,6 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + package vswithcarbon // ##(--backend VSWITHCARBON) diff --git a/src/test/resources/regressions/features/backends/vs-with-silicon.gobra b/src/test/resources/regressions/features/backends/vs-with-silicon.gobra index d7980c360..d088ffcdc 100644 --- a/src/test/resources/regressions/features/backends/vs-with-silicon.gobra +++ b/src/test/resources/regressions/features/backends/vs-with-silicon.gobra @@ -1,3 +1,6 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + package vswithsilicon // ##(--backend VSWITHSILICON) From bac2c5abd8a7798d3f7405cb2b70d869230c6fb0 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Tue, 21 Jan 2025 11:16:55 +0100 Subject: [PATCH 3/8] fixes ViperServer with Silicon backend --- src/main/scala/viper/gobra/backend/ViperBackends.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/gobra/backend/ViperBackends.scala b/src/main/scala/viper/gobra/backend/ViperBackends.scala index 526c0996b..2190d6ade 100644 --- a/src/main/scala/viper/gobra/backend/ViperBackends.scala +++ b/src/main/scala/viper/gobra/backend/ViperBackends.scala @@ -119,7 +119,7 @@ object ViperBackends { /** returns an existing ViperCoreServer instance or otherwise creates a new one */ protected def getOrCreateServer(config: Config)(executionContext: GobraExecutionContext): ViperCoreServer = { server.getOrElse({ - var serverConfig = List("--disablePlugins", "--logLevel", config.logLevel.levelStr) + var serverConfig = List("--logLevel", config.logLevel.levelStr) if(config.cacheFile.isDefined) { serverConfig = serverConfig.appendedAll(List("--cacheFile", config.cacheFile.get.toString)) } From 2e491e7e35a16c515543e2deda7a77329ac70438 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Tue, 21 Jan 2025 12:31:32 +0100 Subject: [PATCH 4/8] fixes uniqueness issue of Terminator actor in ViperServer --- viperserver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/viperserver b/viperserver index e0890869a..d6243bd70 160000 --- a/viperserver +++ b/viperserver @@ -1 +1 @@ -Subproject commit e0890869a8f3a53d8de3b8b0c1ee995398a04978 +Subproject commit d6243bd7078484cc74152081baa0f2534407c989 From f8404aa8308433e3c03d6bcdc3012174b1c0625d Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Tue, 21 Jan 2025 11:18:56 +0100 Subject: [PATCH 5/8] fixes Carbon backend --- src/main/scala/viper/gobra/backend/Carbon.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/gobra/backend/Carbon.scala b/src/main/scala/viper/gobra/backend/Carbon.scala index fec619be4..23ea5508a 100644 --- a/src/main/scala/viper/gobra/backend/Carbon.scala +++ b/src/main/scala/viper/gobra/backend/Carbon.scala @@ -24,7 +24,7 @@ class Carbon(commandLineArguments: Seq[String]) extends ViperVerifier { val carbonApi: carbon.CarbonFrontendAPI = new CarbonFrontendAPI(reporter) val startTime = System.currentTimeMillis() - carbonApi.initialize(commandLineArguments ++ Seq("--ignoreFile", "dummy.sil")) + carbonApi.initialize(commandLineArguments) val result = carbonApi.verify(program) carbonApi.stop() From c4472c1be787586e3c54fe2d9308be11b59f14c1 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Tue, 21 Jan 2025 11:27:16 +0100 Subject: [PATCH 6/8] fixes ViperServer with Carbon backend --- src/main/scala/viper/gobra/backend/ViperBackends.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/gobra/backend/ViperBackends.scala b/src/main/scala/viper/gobra/backend/ViperBackends.scala index 2190d6ade..e78c996ce 100644 --- a/src/main/scala/viper/gobra/backend/ViperBackends.scala +++ b/src/main/scala/viper/gobra/backend/ViperBackends.scala @@ -180,7 +180,7 @@ object ViperBackends { case class ViperServerWithCarbon(initialServer: Option[ViperCoreServer] = None) extends ViperServerBackend(initialServer) { override def getViperVerifierConfig(exePaths: Vector[String], config: Config): ViperVerifierConfig = { var options: Vector[String] = Vector.empty - options ++= Vector("--logLevel", "ERROR") + // options ++= Vector("--logLevel", "ERROR") if (config.respectFunctionPrePermAmounts) { options ++= Vector("--respectFunctionPrePermAmounts") } From 16b19370dead2878962513d2c9f06ebff124419f Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Tue, 21 Jan 2025 14:12:14 +0100 Subject: [PATCH 7/8] implements Joao's CR suggestions --- src/main/scala/viper/gobra/frontend/Config.scala | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala index 3e6e1d4f2..2f2e97f02 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/src/main/scala/viper/gobra/frontend/Config.scala @@ -248,7 +248,7 @@ case class Config( TypeBounds(Int = TypeBounds.IntWith64Bit, UInt = TypeBounds.UIntWith64Bit) } - lazy val backendOrDefault: ViperBackend = backend.getOrElse(ConfigDefaults.DefaultBackend) + val backendOrDefault: ViperBackend = backend.getOrElse(ConfigDefaults.DefaultBackend) } object Config { @@ -871,8 +871,8 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals conflicts(input, List(projectRoot, inclPackages, exclPackages)) conflicts(directory, List(inclPackages, exclPackages)) - // must be lazy to guarantee that this value is computed only during the CLI options validation and not before. - lazy val isSiliconBasedBackend = backend.toOption.getOrElse(ConfigDefaults.DefaultBackend) match { + // must be a function or lazy to guarantee that this value is computed only during the CLI options validation and not before. + private def isSiliconBasedBackend = backend.toOption.getOrElse(ConfigDefaults.DefaultBackend) match { case ViperBackends.SiliconBackend | _: ViperBackends.ViperServerWithSilicon => true case _ => false } From d3d0ad7622de3ecf1e72668c361de293ae0ae56e Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Tue, 21 Jan 2025 16:06:20 +0100 Subject: [PATCH 8/8] Updates ViperServer to latest commit on branch 'master' --- viperserver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/viperserver b/viperserver index d6243bd70..7fb656ba3 160000 --- a/viperserver +++ b/viperserver @@ -1 +1 @@ -Subproject commit d6243bd7078484cc74152081baa0f2534407c989 +Subproject commit 7fb656ba3f5cd910100291cdfc37ea23ff67bf42