disable nlir

viperproject · Dec 1, 2023 · 1eeff3a · 1eeff3a
1 parent 9f38d64
commit 1eeff3a
Show file tree

Hide file tree

Showing 2 changed files with 24 additions and 0 deletions.
diff --git a/src/main/scala/viper/gobra/backend/ViperBackends.scala b/src/main/scala/viper/gobra/backend/ViperBackends.scala
@@ -31,6 +31,9 @@ object ViperBackends {
       if (config.z3APIMode) {
         options = options ++ Vector(s"--prover=${Z3ProverAPI.name}")
       }
+      if (config.disableNLRI) {
+        options = options ++ Vector(s"--disableNLRI")
+      }
       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
@@ -561,6 +561,14 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     default = None,
     noshort = true
   )
+
+  val disableNLIR: ScallopOption[Boolean] = opt[Boolean](
+    name = "disableNLIR",
+    descr = "Disable non-linear integer arithmetics. Non compatible using Z3 via API or Carbon",
+    noshort = true,
+    default = Some(false)
+  )
+
   lazy val packageTimeoutDuration: Duration = packageTimeout.toOption match {
     case Some(d) => Duration(d)
     case _ => Duration.Inf
@@ -770,6 +778,18 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     }
   }
 
+  addValidation {
+    if (disableNLIR.toOption.contains(true)) {
+      if (z3APIMode.toOption.contains(true) || !isSiliconBasedBackend) {
+        Left("--disableNLIR is not compatible with Z3 via API or Carbon")
+      } else {
+        Right(())
+      }
+    } else {
+      Right(())
+    }
+  }
+
 
   /** File Validation */
   validateFilesExist(cutInput)
@@ -857,6 +877,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     parallelizeBranches = parallelizeBranches(),
     conditionalizePermissions = conditionalizePermissions(),
     z3APIMode = z3APIMode(),
+    disableNLIR = disableNLIR(),
     mceMode = mceMode(),
     enableLazyImports = enableLazyImports(),
     noVerify = noVerify(),