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
viperproject · Sep 12, 2023 · 21bd69f · 21bd69f
1 parent d2acefb
commit 21bd69f
Show file tree

Hide file tree

Showing 3 changed files with 43 additions and 11 deletions.
diff --git 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
@@ -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
@@ -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(),