From 1eeff3afd16208d91bd0057a6fab35901564a01e Mon Sep 17 00:00:00 2001 From: Dspil Date: Fri, 1 Dec 2023 15:28:06 +0100 Subject: [PATCH 1/7] disable nlir --- .../viper/gobra/backend/ViperBackends.scala | 3 +++ .../scala/viper/gobra/frontend/Config.scala | 21 +++++++++++++++++++ 2 files changed, 24 insertions(+) diff --git a/src/main/scala/viper/gobra/backend/ViperBackends.scala b/src/main/scala/viper/gobra/backend/ViperBackends.scala index 7746255ec..e498fa501 100644 --- 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 index 29d92a022..b4162d576 100644 --- 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(), From 5a57ea0bcafd17e8659d7ceb513f33b5bdefd97d Mon Sep 17 00:00:00 2001 From: Dspil Date: Fri, 1 Dec 2023 15:40:59 +0100 Subject: [PATCH 2/7] disable NLIR --- .../viper/gobra/backend/ViperBackends.scala | 2 +- .../scala/viper/gobra/frontend/Config.scala | 19 ++++++++++++------- 2 files changed, 13 insertions(+), 8 deletions(-) diff --git a/src/main/scala/viper/gobra/backend/ViperBackends.scala b/src/main/scala/viper/gobra/backend/ViperBackends.scala index e498fa501..a9ad9eb6c 100644 --- a/src/main/scala/viper/gobra/backend/ViperBackends.scala +++ b/src/main/scala/viper/gobra/backend/ViperBackends.scala @@ -31,7 +31,7 @@ object ViperBackends { if (config.z3APIMode) { options = options ++ Vector(s"--prover=${Z3ProverAPI.name}") } - if (config.disableNLRI) { + if (config.disableNLIR) { options = options ++ Vector(s"--disableNLRI") } 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 b4162d576..47835fb31 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/src/main/scala/viper/gobra/frontend/Config.scala @@ -66,6 +66,7 @@ object ConfigDefaults { lazy val DefaultParallelizeBranches: Boolean = false lazy val DefaultConditionalizePermissions: Boolean = false lazy val DefaultZ3APIMode: Boolean = false + lazy val DefaultDisableNLIR: Boolean = false lazy val DefaultMCEMode: MCE.Mode = MCE.Enabled lazy val DefaultEnableLazyImports: Boolean = false lazy val DefaultNoVerify: Boolean = false @@ -130,6 +131,7 @@ case class Config( parallelizeBranches: Boolean = ConfigDefaults.DefaultParallelizeBranches, conditionalizePermissions: Boolean = ConfigDefaults.DefaultConditionalizePermissions, z3APIMode: Boolean = ConfigDefaults.DefaultZ3APIMode, + disableNLIR: Boolean = ConfigDefaults.DefaultDisableNLIR, mceMode: MCE.Mode = ConfigDefaults.DefaultMCEMode, enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports, noVerify: Boolean = ConfigDefaults.DefaultNoVerify, @@ -180,6 +182,7 @@ case class Config( parallelizeBranches = parallelizeBranches, conditionalizePermissions = conditionalizePermissions, z3APIMode = z3APIMode || other.z3APIMode, + disableNLIR = disableNLIR || other.disableNLIR, mceMode = mceMode, enableLazyImports = enableLazyImports || other.enableLazyImports, noVerify = noVerify || other.noVerify, @@ -233,6 +236,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector parallelizeBranches: Boolean = ConfigDefaults.DefaultParallelizeBranches, conditionalizePermissions: Boolean = ConfigDefaults.DefaultConditionalizePermissions, z3APIMode: Boolean = ConfigDefaults.DefaultZ3APIMode, + disableNLIR: Boolean = ConfigDefaults.DefaultDisableNLIR, mceMode: MCE.Mode = ConfigDefaults.DefaultMCEMode, enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports, noVerify: Boolean = ConfigDefaults.DefaultNoVerify, @@ -290,6 +294,7 @@ trait RawConfig { parallelizeBranches = baseConfig.parallelizeBranches, conditionalizePermissions = baseConfig.conditionalizePermissions, z3APIMode = baseConfig.z3APIMode, + disableNLIR = baseConfig.disableNLIR, mceMode = baseConfig.mceMode, enableLazyImports = baseConfig.enableLazyImports, noVerify = baseConfig.noVerify, @@ -562,13 +567,6 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals 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 @@ -654,6 +652,13 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals noshort = true, ) + val disableNLIR: ScallopOption[Boolean] = opt[Boolean]( + name = "disableNLIR", + descr = "Disable non-linear integer arithmetics. Non compatible using Z3 via API or Carbon", + default = Some(ConfigDefaults.DefaultDisableNLIR), + noshort = true, + ) + val mceMode: ScallopOption[MCE.Mode] = { val on = "on" val off = "off" From fbb0f64c48c0eb0f52b3be0a014de5304f4446cd Mon Sep 17 00:00:00 2001 From: Dspil Date: Fri, 1 Dec 2023 23:03:17 +0100 Subject: [PATCH 3/7] cure dyslexia --- .../viper/gobra/backend/ViperBackends.scala | 4 ++-- .../scala/viper/gobra/frontend/Config.scala | 22 +++++++++---------- 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 a9ad9eb6c..e4b0308f8 100644 --- a/src/main/scala/viper/gobra/backend/ViperBackends.scala +++ b/src/main/scala/viper/gobra/backend/ViperBackends.scala @@ -31,8 +31,8 @@ object ViperBackends { if (config.z3APIMode) { options = options ++ Vector(s"--prover=${Z3ProverAPI.name}") } - if (config.disableNLIR) { - options = options ++ Vector(s"--disableNLRI") + if (config.disableNL) { + options = options ++ Vector(s"--disableNL") } val mceSiliconOpt = config.mceMode match { case MCE.Disabled => "0" diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala index 47835fb31..66d6bb307 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/src/main/scala/viper/gobra/frontend/Config.scala @@ -66,7 +66,7 @@ object ConfigDefaults { lazy val DefaultParallelizeBranches: Boolean = false lazy val DefaultConditionalizePermissions: Boolean = false lazy val DefaultZ3APIMode: Boolean = false - lazy val DefaultDisableNLIR: Boolean = false + lazy val DefaultDisableNL: Boolean = false lazy val DefaultMCEMode: MCE.Mode = MCE.Enabled lazy val DefaultEnableLazyImports: Boolean = false lazy val DefaultNoVerify: Boolean = false @@ -131,7 +131,7 @@ case class Config( parallelizeBranches: Boolean = ConfigDefaults.DefaultParallelizeBranches, conditionalizePermissions: Boolean = ConfigDefaults.DefaultConditionalizePermissions, z3APIMode: Boolean = ConfigDefaults.DefaultZ3APIMode, - disableNLIR: Boolean = ConfigDefaults.DefaultDisableNLIR, + disableNL: Boolean = ConfigDefaults.DefaultDisableNL, mceMode: MCE.Mode = ConfigDefaults.DefaultMCEMode, enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports, noVerify: Boolean = ConfigDefaults.DefaultNoVerify, @@ -182,7 +182,7 @@ case class Config( parallelizeBranches = parallelizeBranches, conditionalizePermissions = conditionalizePermissions, z3APIMode = z3APIMode || other.z3APIMode, - disableNLIR = disableNLIR || other.disableNLIR, + disableNL = disableNL || other.disableNL, mceMode = mceMode, enableLazyImports = enableLazyImports || other.enableLazyImports, noVerify = noVerify || other.noVerify, @@ -236,7 +236,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector parallelizeBranches: Boolean = ConfigDefaults.DefaultParallelizeBranches, conditionalizePermissions: Boolean = ConfigDefaults.DefaultConditionalizePermissions, z3APIMode: Boolean = ConfigDefaults.DefaultZ3APIMode, - disableNLIR: Boolean = ConfigDefaults.DefaultDisableNLIR, + disableNL: Boolean = ConfigDefaults.DefaultDisableNL, mceMode: MCE.Mode = ConfigDefaults.DefaultMCEMode, enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports, noVerify: Boolean = ConfigDefaults.DefaultNoVerify, @@ -294,7 +294,7 @@ trait RawConfig { parallelizeBranches = baseConfig.parallelizeBranches, conditionalizePermissions = baseConfig.conditionalizePermissions, z3APIMode = baseConfig.z3APIMode, - disableNLIR = baseConfig.disableNLIR, + disableNL = baseConfig.disableNL, mceMode = baseConfig.mceMode, enableLazyImports = baseConfig.enableLazyImports, noVerify = baseConfig.noVerify, @@ -652,10 +652,10 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals noshort = true, ) - val disableNLIR: ScallopOption[Boolean] = opt[Boolean]( - name = "disableNLIR", + val disableNL: ScallopOption[Boolean] = opt[Boolean]( + name = "disableNL", descr = "Disable non-linear integer arithmetics. Non compatible using Z3 via API or Carbon", - default = Some(ConfigDefaults.DefaultDisableNLIR), + default = Some(ConfigDefaults.DefaultDisableNL), noshort = true, ) @@ -784,9 +784,9 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals } addValidation { - if (disableNLIR.toOption.contains(true)) { + if (disableNL.toOption.contains(true)) { if (z3APIMode.toOption.contains(true) || !isSiliconBasedBackend) { - Left("--disableNLIR is not compatible with Z3 via API or Carbon") + Left("--disableNL is not compatible with Z3 via API or Carbon") } else { Right(()) } @@ -882,7 +882,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals parallelizeBranches = parallelizeBranches(), conditionalizePermissions = conditionalizePermissions(), z3APIMode = z3APIMode(), - disableNLIR = disableNLIR(), + disableNL = disableNL(), mceMode = mceMode(), enableLazyImports = enableLazyImports(), noVerify = noVerify(), From 27ec565024eab2f9842c67432b9821ab601bb591 Mon Sep 17 00:00:00 2001 From: Dspil Date: Fri, 1 Dec 2023 23:08:04 +0100 Subject: [PATCH 4/7] test --- .../resources/regressions/examples/disableNL.gobra | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 src/test/resources/regressions/examples/disableNL.gobra diff --git a/src/test/resources/regressions/examples/disableNL.gobra b/src/test/resources/regressions/examples/disableNL.gobra new file mode 100644 index 000000000..8a7f103e5 --- /dev/null +++ b/src/test/resources/regressions/examples/disableNL.gobra @@ -0,0 +1,11 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package pkg + +requires 0 <= x && x <= 10 +requires 0 <= y && y <= 10 +ensures 0 <= res && res <= 100 // would fail with --disableNL +func f(x, y int) (res int) { + return x * y +} From d96588dd757ac02f6353bfb7e731354900b511af Mon Sep 17 00:00:00 2001 From: Dionysios Spiliopoulos <32896454+Dspil@users.noreply.github.com> Date: Sat, 2 Dec 2023 15:05:58 +0100 Subject: [PATCH 5/7] Update src/main/scala/viper/gobra/frontend/Config.scala MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: João Pereira --- src/main/scala/viper/gobra/frontend/Config.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala index 66d6bb307..5ef9f40f0 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/src/main/scala/viper/gobra/frontend/Config.scala @@ -654,7 +654,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals val disableNL: ScallopOption[Boolean] = opt[Boolean]( name = "disableNL", - descr = "Disable non-linear integer arithmetics. Non compatible using Z3 via API or Carbon", + descr = "Disable non-linear integer arithmetics. Non compatible with using Z3 via API or Carbon", default = Some(ConfigDefaults.DefaultDisableNL), noshort = true, ) From 86ada0d54d864e37fffbf44c297d0ed429b83da4 Mon Sep 17 00:00:00 2001 From: Dionysios Spiliopoulos <32896454+Dspil@users.noreply.github.com> Date: Sat, 2 Dec 2023 17:57:45 +0100 Subject: [PATCH 6/7] Update src/main/scala/viper/gobra/frontend/Config.scala MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: João Pereira --- src/main/scala/viper/gobra/frontend/Config.scala | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala index 5ef9f40f0..c4904c2fa 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/src/main/scala/viper/gobra/frontend/Config.scala @@ -784,14 +784,10 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals } addValidation { - if (disableNL.toOption.contains(true)) { - if (z3APIMode.toOption.contains(true) || !isSiliconBasedBackend) { - Left("--disableNL is not compatible with Z3 via API or Carbon") - } else { - Right(()) - } + if (!disableNL.toOption.contains(true) || (!z3APIMode.toOption.contains(true) && isSiliconBasedBackend)) { + Right(()) } else { - Right(()) + Left("--disableNL is not compatible with Z3 via API or Carbon") } } From b39bf9e118c1a018d6e37f477f7f72adf307f55e Mon Sep 17 00:00:00 2001 From: Dspil Date: Tue, 5 Dec 2023 11:50:50 +0100 Subject: [PATCH 7/7] z3 api and tests --- src/main/scala/viper/gobra/frontend/Config.scala | 6 +++--- .../resources/regressions/examples/disableNL.gobra | 4 +++- .../regressions/examples/disableNL_success.gobra | 11 +++++++++++ 3 files changed, 17 insertions(+), 4 deletions(-) create mode 100644 src/test/resources/regressions/examples/disableNL_success.gobra diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala index c4904c2fa..42ae527e9 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/src/main/scala/viper/gobra/frontend/Config.scala @@ -654,7 +654,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals val disableNL: ScallopOption[Boolean] = opt[Boolean]( name = "disableNL", - descr = "Disable non-linear integer arithmetics. Non compatible with using Z3 via API or Carbon", + descr = "Disable non-linear integer arithmetics. Non compatible with Carbon", default = Some(ConfigDefaults.DefaultDisableNL), noshort = true, ) @@ -784,10 +784,10 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals } addValidation { - if (!disableNL.toOption.contains(true) || (!z3APIMode.toOption.contains(true) && isSiliconBasedBackend)) { + if (!disableNL.toOption.contains(true) || isSiliconBasedBackend) { Right(()) } else { - Left("--disableNL is not compatible with Z3 via API or Carbon") + Left("--disableNL is not compatible with Carbon") } } diff --git a/src/test/resources/regressions/examples/disableNL.gobra b/src/test/resources/regressions/examples/disableNL.gobra index 8a7f103e5..53e144e85 100644 --- a/src/test/resources/regressions/examples/disableNL.gobra +++ b/src/test/resources/regressions/examples/disableNL.gobra @@ -1,11 +1,13 @@ // Any copyright is dedicated to the Public Domain. // http://creativecommons.org/publicdomain/zero/1.0/ +// ##(--disableNL) package pkg requires 0 <= x && x <= 10 requires 0 <= y && y <= 10 -ensures 0 <= res && res <= 100 // would fail with --disableNL +//:: ExpectedOutput(postcondition_error:assertion_error) +ensures 0 <= res && res <= 100 func f(x, y int) (res int) { return x * y } diff --git a/src/test/resources/regressions/examples/disableNL_success.gobra b/src/test/resources/regressions/examples/disableNL_success.gobra new file mode 100644 index 000000000..f2ca41718 --- /dev/null +++ b/src/test/resources/regressions/examples/disableNL_success.gobra @@ -0,0 +1,11 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package pkg + +requires 0 <= x && x <= 10 +requires 0 <= y && y <= 10 +ensures 0 <= res && res <= 100 +func f(x, y int) (res int) { + return x * y +}