From 45b7df44387d007cc4d5a6c855a7cd53fac5c70a Mon Sep 17 00:00:00 2001 From: Dspil Date: Fri, 28 Jul 2023 13:12:47 +0200 Subject: [PATCH 1/5] added z3ApiMode flag --- .../viper/gobra/backend/ViperBackends.scala | 4 ++++ .../scala/viper/gobra/frontend/Config.scala | 22 +++++++++++++++++++ 2 files changed, 26 insertions(+) diff --git a/src/main/scala/viper/gobra/backend/ViperBackends.scala b/src/main/scala/viper/gobra/backend/ViperBackends.scala index ed4ca4f49..e1c647228 100644 --- a/src/main/scala/viper/gobra/backend/ViperBackends.scala +++ b/src/main/scala/viper/gobra/backend/ViperBackends.scala @@ -10,6 +10,7 @@ import viper.gobra.frontend.{Config, MCE} import viper.gobra.util.GobraExecutionContext import viper.server.ViperConfig import viper.server.core.ViperCoreServer +import viper.silicon.decider.Z3ProverAPI import viper.server.vsi.DefaultVerificationServerStart trait ViperBackend { @@ -27,6 +28,9 @@ object ViperBackends { if (config.conditionalizePermissions) { options ++= Vector("--conditionalizePermissions") } + if (config.z3ApiMode) { + options = options ++ Vector(s"--prover ${Z3ProverAPI.name}") + } val mceSiliconOpt = config.mceMode match { case MCE.Disabled => "0" case MCE.Enabled => "1" diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala index 2c26a944e..a0b40c251 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/src/main/scala/viper/gobra/frontend/Config.scala @@ -65,6 +65,7 @@ object ConfigDefaults { lazy val DefaultAssumeInjectivityOnInhale: Boolean = true lazy val DefaultParallelizeBranches: Boolean = false lazy val DefaultConditionalizePermissions: Boolean = false + lazy val DefaultZ3ApiMode: Boolean = false lazy val DefaultMCEMode: MCE.Mode = MCE.Enabled lazy val DefaultEnableLazyImports: Boolean = false lazy val DefaultNoVerify: Boolean = false @@ -127,6 +128,7 @@ case class Config( // branches will be verified in parallel parallelizeBranches: Boolean = ConfigDefaults.DefaultParallelizeBranches, conditionalizePermissions: Boolean = ConfigDefaults.DefaultConditionalizePermissions, + z3ApiMode: Boolean = ConfigDefaults.DefaultZ3ApiMode, mceMode: MCE.Mode = ConfigDefaults.DefaultMCEMode, enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports, noVerify: Boolean = ConfigDefaults.DefaultNoVerify, @@ -174,6 +176,7 @@ case class Config( assumeInjectivityOnInhale = assumeInjectivityOnInhale || other.assumeInjectivityOnInhale, parallelizeBranches = parallelizeBranches, conditionalizePermissions = conditionalizePermissions, + z3ApiMode = z3ApiMode || other.z3ApiMode, mceMode = mceMode, enableLazyImports = enableLazyImports || other.enableLazyImports, noVerify = noVerify || other.noVerify, @@ -225,6 +228,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector assumeInjectivityOnInhale: Boolean = ConfigDefaults.DefaultAssumeInjectivityOnInhale, parallelizeBranches: Boolean = ConfigDefaults.DefaultParallelizeBranches, conditionalizePermissions: Boolean = ConfigDefaults.DefaultConditionalizePermissions, + z3ApiMode: Boolean = ConfigDefaults.DefaultZ3ApiMode, mceMode: MCE.Mode = ConfigDefaults.DefaultMCEMode, enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports, noVerify: Boolean = ConfigDefaults.DefaultNoVerify, @@ -280,6 +284,7 @@ trait RawConfig { assumeInjectivityOnInhale = baseConfig.assumeInjectivityOnInhale, parallelizeBranches = baseConfig.parallelizeBranches, conditionalizePermissions = baseConfig.conditionalizePermissions, + z3ApiMode = baseConfig.z3ApiMode, mceMode = baseConfig.mceMode, enableLazyImports = baseConfig.enableLazyImports, noVerify = baseConfig.noVerify, @@ -628,6 +633,13 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals short = 'c', ) + val z3ApiMode: ScallopOption[Boolean] = opt[Boolean]( + name = "z3ApiMode", + descr = "When the backend is either SILICON or VSWITHSILICON, silicon will use Z3 via API.", + default = Some(ConfigDefaults.DefaultZ3ApiMode), + noshort = true, + ) + val mceMode: ScallopOption[MCE.Mode] = { val on = "on" val off = "off" @@ -726,6 +738,15 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals } } + addValidation { + val z3ApiModeOn = z3ApiMode.toOption.contains(true) + if (z3ApiModeOn && !isSiliconBasedBackend) { + Left("The selected backend does not support --z3ApiMode.") + } else { + Right(()) + } + } + // `mceMode` can only be provided when using a silicon-based backend addValidation { val mceModeSupplied = mceMode.isSupplied @@ -822,6 +843,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals assumeInjectivityOnInhale = assumeInjectivityOnInhale(), parallelizeBranches = parallelizeBranches(), conditionalizePermissions = conditionalizePermissions(), + z3ApiMode = z3ApiMode(), mceMode = mceMode(), enableLazyImports = enableLazyImports(), noVerify = noVerify(), From 884458405f10e5280f6dbd9e8d726f257e9448f0 Mon Sep 17 00:00:00 2001 From: Dspil Date: Fri, 28 Jul 2023 13:15:03 +0200 Subject: [PATCH 2/5] Api -> API --- .../viper/gobra/backend/ViperBackends.scala | 2 +- .../scala/viper/gobra/frontend/Config.scala | 24 +++++++++---------- 2 files changed, 13 insertions(+), 13 deletions(-) diff --git a/src/main/scala/viper/gobra/backend/ViperBackends.scala b/src/main/scala/viper/gobra/backend/ViperBackends.scala index e1c647228..8bb7a4e19 100644 --- a/src/main/scala/viper/gobra/backend/ViperBackends.scala +++ b/src/main/scala/viper/gobra/backend/ViperBackends.scala @@ -28,7 +28,7 @@ object ViperBackends { if (config.conditionalizePermissions) { options ++= Vector("--conditionalizePermissions") } - if (config.z3ApiMode) { + if (config.z3APIMode) { options = options ++ Vector(s"--prover ${Z3ProverAPI.name}") } val mceSiliconOpt = config.mceMode match { diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala index a0b40c251..794f86239 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/src/main/scala/viper/gobra/frontend/Config.scala @@ -65,7 +65,7 @@ object ConfigDefaults { lazy val DefaultAssumeInjectivityOnInhale: Boolean = true lazy val DefaultParallelizeBranches: Boolean = false lazy val DefaultConditionalizePermissions: Boolean = false - lazy val DefaultZ3ApiMode: Boolean = false + lazy val DefaultZ3APIMode: Boolean = false lazy val DefaultMCEMode: MCE.Mode = MCE.Enabled lazy val DefaultEnableLazyImports: Boolean = false lazy val DefaultNoVerify: Boolean = false @@ -128,7 +128,7 @@ case class Config( // branches will be verified in parallel parallelizeBranches: Boolean = ConfigDefaults.DefaultParallelizeBranches, conditionalizePermissions: Boolean = ConfigDefaults.DefaultConditionalizePermissions, - z3ApiMode: Boolean = ConfigDefaults.DefaultZ3ApiMode, + z3APIMode: Boolean = ConfigDefaults.DefaultZ3APIMode, mceMode: MCE.Mode = ConfigDefaults.DefaultMCEMode, enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports, noVerify: Boolean = ConfigDefaults.DefaultNoVerify, @@ -176,7 +176,7 @@ case class Config( assumeInjectivityOnInhale = assumeInjectivityOnInhale || other.assumeInjectivityOnInhale, parallelizeBranches = parallelizeBranches, conditionalizePermissions = conditionalizePermissions, - z3ApiMode = z3ApiMode || other.z3ApiMode, + z3APIMode = z3APIMode || other.z3APIMode, mceMode = mceMode, enableLazyImports = enableLazyImports || other.enableLazyImports, noVerify = noVerify || other.noVerify, @@ -228,7 +228,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector assumeInjectivityOnInhale: Boolean = ConfigDefaults.DefaultAssumeInjectivityOnInhale, parallelizeBranches: Boolean = ConfigDefaults.DefaultParallelizeBranches, conditionalizePermissions: Boolean = ConfigDefaults.DefaultConditionalizePermissions, - z3ApiMode: Boolean = ConfigDefaults.DefaultZ3ApiMode, + z3APIMode: Boolean = ConfigDefaults.DefaultZ3APIMode, mceMode: MCE.Mode = ConfigDefaults.DefaultMCEMode, enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports, noVerify: Boolean = ConfigDefaults.DefaultNoVerify, @@ -284,7 +284,7 @@ trait RawConfig { assumeInjectivityOnInhale = baseConfig.assumeInjectivityOnInhale, parallelizeBranches = baseConfig.parallelizeBranches, conditionalizePermissions = baseConfig.conditionalizePermissions, - z3ApiMode = baseConfig.z3ApiMode, + z3APIMode = baseConfig.z3APIMode, mceMode = baseConfig.mceMode, enableLazyImports = baseConfig.enableLazyImports, noVerify = baseConfig.noVerify, @@ -633,10 +633,10 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals short = 'c', ) - val z3ApiMode: ScallopOption[Boolean] = opt[Boolean]( - name = "z3ApiMode", + val z3APIMode: ScallopOption[Boolean] = opt[Boolean]( + name = "z3APIMode", descr = "When the backend is either SILICON or VSWITHSILICON, silicon will use Z3 via API.", - default = Some(ConfigDefaults.DefaultZ3ApiMode), + default = Some(ConfigDefaults.DefaultZ3APIMode), noshort = true, ) @@ -739,9 +739,9 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals } addValidation { - val z3ApiModeOn = z3ApiMode.toOption.contains(true) - if (z3ApiModeOn && !isSiliconBasedBackend) { - Left("The selected backend does not support --z3ApiMode.") + val z3APIModeOn = z3APIMode.toOption.contains(true) + if (z3APIModeOn && !isSiliconBasedBackend) { + Left("The selected backend does not support --z3APIMode.") } else { Right(()) } @@ -843,7 +843,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals assumeInjectivityOnInhale = assumeInjectivityOnInhale(), parallelizeBranches = parallelizeBranches(), conditionalizePermissions = conditionalizePermissions(), - z3ApiMode = z3ApiMode(), + z3APIMode = z3APIMode(), mceMode = mceMode(), enableLazyImports = enableLazyImports(), noVerify = noVerify(), From 25e635e22bd27bb298c22161bddd8874842d54d4 Mon Sep 17 00:00:00 2001 From: Dspil Date: Fri, 28 Jul 2023 15:43:05 +0200 Subject: [PATCH 3/5] changed space to = --- 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 8bb7a4e19..7746255ec 100644 --- a/src/main/scala/viper/gobra/backend/ViperBackends.scala +++ b/src/main/scala/viper/gobra/backend/ViperBackends.scala @@ -29,7 +29,7 @@ object ViperBackends { options ++= Vector("--conditionalizePermissions") } if (config.z3APIMode) { - options = options ++ Vector(s"--prover ${Z3ProverAPI.name}") + options = options ++ Vector(s"--prover=${Z3ProverAPI.name}") } val mceSiliconOpt = config.mceMode match { case MCE.Disabled => "0" From fda5d54950938d37c6c04a464ed534bc50389de3 Mon Sep 17 00:00:00 2001 From: Dspil Date: Fri, 8 Sep 2023 15:28:14 +0200 Subject: [PATCH 4/5] catch ugly exception when z3 java api not in path --- .../scala/viper/gobra/backend/Silicon.scala | 30 ++++++++++++------- 1 file changed, 19 insertions(+), 11 deletions(-) diff --git a/src/main/scala/viper/gobra/backend/Silicon.scala b/src/main/scala/viper/gobra/backend/Silicon.scala index a8cb1c33a..196d1e10c 100644 --- a/src/main/scala/viper/gobra/backend/Silicon.scala +++ b/src/main/scala/viper/gobra/backend/Silicon.scala @@ -11,7 +11,6 @@ import viper.silicon import viper.silver.ast.Program import viper.silver.reporter._ import viper.silver.verifier.{Failure, Success, VerificationResult} - import scala.concurrent.Future class Silicon(commandLineArguments: Seq[String]) extends ViperVerifier { @@ -23,18 +22,27 @@ class Silicon(commandLineArguments: Seq[String]) extends ViperVerifier { val backend: silicon.Silicon = silicon.Silicon.fromPartialCommandLineArguments(commandLineArguments, reporter) val startTime = System.currentTimeMillis() - backend.start() - val result = backend.verify(program) - backend.stop() + try { + backend.start() + val result = backend.verify(program) + backend.stop() - result match { - case Success => - reporter report OverallSuccessMessage(backend.name, System.currentTimeMillis() - startTime) - case f@Failure(_) => - reporter report OverallFailureMessage(backend.name, System.currentTimeMillis() - startTime, f) - } + result match { + case Success => + reporter report OverallSuccessMessage(backend.name, System.currentTimeMillis() - startTime) + case f@Failure(_) => + reporter report OverallFailureMessage(backend.name, System.currentTimeMillis() - startTime, f) + } - result + result + } catch { + case _: java.lang.UnsatisfiedLinkError => println("Couldn't find Z3 java API. No libz3java in java.library.path") + new Failure(Seq.empty) + case e: Throwable => + println("Couldn't verify package due to internal error:") + println(e.getMessage()) + new Failure(Seq.empty) + } } } } From 09ec7ebbf0661c8a7a4ed36dd9530a8f8ad9f72c Mon Sep 17 00:00:00 2001 From: Dspil Date: Tue, 12 Sep 2023 10:59:17 +0200 Subject: [PATCH 5/5] Joao's feedback --- src/main/scala/viper/gobra/backend/Silicon.scala | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/main/scala/viper/gobra/backend/Silicon.scala b/src/main/scala/viper/gobra/backend/Silicon.scala index 196d1e10c..5440be1c0 100644 --- a/src/main/scala/viper/gobra/backend/Silicon.scala +++ b/src/main/scala/viper/gobra/backend/Silicon.scala @@ -36,12 +36,10 @@ class Silicon(commandLineArguments: Seq[String]) extends ViperVerifier { result } catch { - case _: java.lang.UnsatisfiedLinkError => println("Couldn't find Z3 java API. No libz3java in java.library.path") + case _: java.lang.UnsatisfiedLinkError => System.err.println("Couldn't find Z3 java API. No libz3java in java.library.path") new Failure(Seq.empty) case e: Throwable => - println("Couldn't verify package due to internal error:") - println(e.getMessage()) - new Failure(Seq.empty) + throw e } } }