From 21bd69f423832468686ea0b484445046188f2ff4 Mon Sep 17 00:00:00 2001 From: Dionysios Spiliopoulos <32896454+Dspil@users.noreply.github.com> Date: Tue, 12 Sep 2023 11:52:32 +0200 Subject: [PATCH] Add flag to use Z3 via API (#666) * added z3ApiMode flag * Api -> API * changed space to = * catch ugly exception when z3 java api not in path * Joao's feedback --- .../scala/viper/gobra/backend/Silicon.scala | 28 +++++++++++-------- .../viper/gobra/backend/ViperBackends.scala | 4 +++ .../scala/viper/gobra/frontend/Config.scala | 22 +++++++++++++++ 3 files changed, 43 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..5440be1c0 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,25 @@ 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 => System.err.println("Couldn't find Z3 java API. No libz3java in java.library.path") + new Failure(Seq.empty) + case e: Throwable => + throw e + } } } } diff --git a/src/main/scala/viper/gobra/backend/ViperBackends.scala b/src/main/scala/viper/gobra/backend/ViperBackends.scala index ed4ca4f49..7746255ec 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..794f86239 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(),