From 48260f5f24d6b82ac2aba8671f794da5864f8ae2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 22 Sep 2023 20:24:05 +0200 Subject: [PATCH 1/2] add --requireTriggers flag --- src/main/scala/viper/gobra/frontend/Config.scala | 16 +++++++++++++++- .../typing/ghost/GhostExprTyping.scala | 12 ++++++++---- 2 files changed, 23 insertions(+), 5 deletions(-) diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala index 794f86239..4cfc00913 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/src/main/scala/viper/gobra/frontend/Config.scala @@ -71,6 +71,8 @@ object ConfigDefaults { lazy val DefaultNoVerify: Boolean = false lazy val DefaultNoStreamErrors: Boolean = false lazy val DefaultParseAndTypeCheckMode: TaskManagerMode = TaskManagerMode.Parallel + // when enabled, all quantifiers without triggers are rejected + lazy val DefaultRequireTriggers: Boolean = false } // More-complete exhale modes @@ -134,6 +136,7 @@ case class Config( noVerify: Boolean = ConfigDefaults.DefaultNoVerify, noStreamErrors: Boolean = ConfigDefaults.DefaultNoStreamErrors, parseAndTypeCheckMode: TaskManagerMode = ConfigDefaults.DefaultParseAndTypeCheckMode, + requireTriggers: Boolean = ConfigDefaults.DefaultRequireTriggers, ) { def merge(other: Config): Config = { @@ -181,7 +184,8 @@ case class Config( enableLazyImports = enableLazyImports || other.enableLazyImports, noVerify = noVerify || other.noVerify, noStreamErrors = noStreamErrors || other.noStreamErrors, - parseAndTypeCheckMode = parseAndTypeCheckMode + parseAndTypeCheckMode = parseAndTypeCheckMode, + requireTriggers = requireTriggers || other.requireTriggers ) } @@ -234,6 +238,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector noVerify: Boolean = ConfigDefaults.DefaultNoVerify, noStreamErrors: Boolean = ConfigDefaults.DefaultNoStreamErrors, parseAndTypeCheckMode: TaskManagerMode = ConfigDefaults.DefaultParseAndTypeCheckMode, + requireTriggers: Boolean = ConfigDefaults.DefaultRequireTriggers, ) { def shouldParse: Boolean = true def shouldTypeCheck: Boolean = !shouldParseOnly @@ -290,6 +295,7 @@ trait RawConfig { noVerify = baseConfig.noVerify, noStreamErrors = baseConfig.noStreamErrors, parseAndTypeCheckMode = baseConfig.parseAndTypeCheckMode, + requireTriggers = baseConfig.requireTriggers, ) } @@ -665,6 +671,13 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals noshort = true, ) + val requireTriggers: ScallopOption[Boolean] = opt[Boolean]( + name = "requireTriggers", + descr = s"Enforces that all quantifiers have a user-provided trigger.", + default = Some(ConfigDefaults.DefaultRequireTriggers), + noshort = true, + ) + val noVerify: ScallopOption[Boolean] = opt[Boolean]( name = "noVerify", descr = s"Skip the verification step performed after encoding the Gobra program into Viper.", @@ -849,5 +862,6 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals noVerify = noVerify(), noStreamErrors = noStreamErrors(), parseAndTypeCheckMode = parseAndTypeCheckMode(), + requireTriggers = requireTriggers(), ) } diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala index 84fcf0155..6713908d8 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala @@ -46,17 +46,21 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl => // check that `thn` and `els` have a common type mergeableTypes.errors(exprType(thn), exprType(els))(expr) - case PForall(vars, triggers, body) => + case n@PForall(vars, triggers, body) => // check whether all triggers are valid and consistent validTriggers(vars, triggers) ++ // check that the quantifier `body` is either Boolean or an assertion - assignableToSpec(body) + assignableToSpec(body) ++ + // check that the user provided triggers when running with --requireTriggers + error(n, "found a quantifier without triggers.", config.requireTriggers && triggers.isEmpty) - case PExists(vars, triggers, body) => + case n@PExists(vars, triggers, body) => // check whether all triggers are valid and consistent validTriggers(vars, triggers) ++ // check that the quantifier `body` is Boolean - assignableToSpec(body) ++ assignableTo.errors(exprType(body), BooleanT)(expr) + assignableToSpec(body) ++ assignableTo.errors(exprType(body), BooleanT)(expr) ++ + // check that the user provided triggers when running with --requireTriggers + error(n, "found a quantifier without triggers.", config.requireTriggers && triggers.isEmpty) case n: PImplication => isExpr(n.left).out ++ isExpr(n.right).out ++ From af913313fa86970fea7af8629e2a0fd42cd6a0ca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Sun, 24 Sep 2023 10:58:20 +0200 Subject: [PATCH 2/2] change comment --- 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 4cfc00913..29d92a022 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/src/main/scala/viper/gobra/frontend/Config.scala @@ -71,7 +71,6 @@ object ConfigDefaults { lazy val DefaultNoVerify: Boolean = false lazy val DefaultNoStreamErrors: Boolean = false lazy val DefaultParseAndTypeCheckMode: TaskManagerMode = TaskManagerMode.Parallel - // when enabled, all quantifiers without triggers are rejected lazy val DefaultRequireTriggers: Boolean = false } @@ -136,6 +135,7 @@ case class Config( noVerify: Boolean = ConfigDefaults.DefaultNoVerify, noStreamErrors: Boolean = ConfigDefaults.DefaultNoStreamErrors, parseAndTypeCheckMode: TaskManagerMode = ConfigDefaults.DefaultParseAndTypeCheckMode, + // when enabled, all quantifiers without triggers are rejected requireTriggers: Boolean = ConfigDefaults.DefaultRequireTriggers, ) {