From 9a0d9117611550651446bf76f27ab3e924a3bd9f Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 10 Apr 2026 13:45:41 +0000 Subject: [PATCH 1/3] Add --assertTimeout CLI option and propagate it to Silicon backend Exposes Silicon's --assertTimeout option through Gobra's CLI, allowing users to set a per-assertion timeout in milliseconds. The option is Silicon-specific and guarded by validation to reject use with Carbon. https://claude.ai/code/session_01DNDg4ADj7NW35SQMt26uD2 --- .../viper/gobra/backend/ViperBackends.scala | 3 ++ .../scala/viper/gobra/frontend/Config.scala | 31 +++++++++++++++++++ 2 files changed, 34 insertions(+) diff --git a/src/main/scala/viper/gobra/backend/ViperBackends.scala b/src/main/scala/viper/gobra/backend/ViperBackends.scala index 420d64572..777728812 100644 --- a/src/main/scala/viper/gobra/backend/ViperBackends.scala +++ b/src/main/scala/viper/gobra/backend/ViperBackends.scala @@ -95,6 +95,9 @@ trait SiliconBasedBackend extends ViperBackend { options ++= Vector("--setAxiomatizationFile", axiomTmpPath.toString()) } + config.assertTimeout.foreach { timeout => + options ++= Vector(s"--assertTimeout=$timeout") + } options } diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala index 2562feedb..d59c26abd 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/src/main/scala/viper/gobra/frontend/Config.scala @@ -82,6 +82,7 @@ object ConfigDefaults { val DefaultMoreJoins: MoreJoins.Mode = MoreJoins.Disabled val DefaultRespectFunctionPrePermAmounts: Boolean = false val DefaultEnableExperimentalFriendClauses: Boolean = false + val DefaultAssertTimeout: Option[Int] = None } // More-complete exhale modes @@ -208,6 +209,7 @@ case class Config( moreJoins: MoreJoins.Mode = ConfigDefaults.DefaultMoreJoins, respectFunctionPrePermAmounts: Boolean = ConfigDefaults.DefaultRespectFunctionPrePermAmounts, enableExperimentalFriendClauses: Boolean = ConfigDefaults.DefaultEnableExperimentalFriendClauses, + assertTimeout: Option[Int] = ConfigDefaults.DefaultAssertTimeout, ) { def merge(other: Config): Config = { @@ -275,6 +277,10 @@ case class Config( moreJoins = MoreJoins.merge(moreJoins, other.moreJoins), respectFunctionPrePermAmounts = respectFunctionPrePermAmounts || other.respectFunctionPrePermAmounts, enableExperimentalFriendClauses = enableExperimentalFriendClauses || other.enableExperimentalFriendClauses, + assertTimeout = (assertTimeout, other.assertTimeout) match { + case (Some(a), Some(b)) => Some(math.min(a, b)) + case (a, b) => a.orElse(b) + }, ) } @@ -340,6 +346,7 @@ case class BaseConfig(gobraDirectory: Option[Path] = ConfigDefaults.DefaultGobra moreJoins: MoreJoins.Mode = ConfigDefaults.DefaultMoreJoins, respectFunctionPrePermAmounts: Boolean = ConfigDefaults.DefaultRespectFunctionPrePermAmounts, enableExperimentalFriendClauses: Boolean = ConfigDefaults.DefaultEnableExperimentalFriendClauses, + assertTimeout: Option[Int] = ConfigDefaults.DefaultAssertTimeout, ) { def shouldParse: Boolean = true def shouldTypeCheck: Boolean = !shouldParseOnly @@ -405,6 +412,7 @@ trait RawConfig { moreJoins = baseConfig.moreJoins, respectFunctionPrePermAmounts = baseConfig.respectFunctionPrePermAmounts, enableExperimentalFriendClauses = baseConfig.enableExperimentalFriendClauses, + assertTimeout = baseConfig.assertTimeout, ) } @@ -929,6 +937,13 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals noshort = true, ) + val assertTimeout: ScallopOption[Int] = opt[Int]( + name = "assertTimeout", + descr = "Sets a timeout (in milliseconds) for assert operations performed by Silicon. Does not have any effect on other backends.", + default = ConfigDefaults.DefaultAssertTimeout, + noshort = true, + ) + val enableExperimentalFriendClauses: ScallopOption[Boolean] = opt[Boolean]( name = "experimentalFriendClauses", descr = s"Enables the use of 'friendPkg' clauses (experimental).", @@ -1047,6 +1062,21 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals } } + addValidation { + if (!assertTimeout.isSupplied || isSiliconBasedBackend) { + Right(()) + } else { + Left("The flag --assertTimeout can only be used with Silicon or ViperServer with Silicon") + } + } + + addValidation { + assertTimeout.toOption match { + case Some(t) if t <= 0 => Left("--assertTimeout must be a positive integer (milliseconds)") + case _ => Right(()) + } + } + /** File Validation */ validateFilesExist(cutInput) @@ -1149,5 +1179,6 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals moreJoins = moreJoins(), respectFunctionPrePermAmounts = respectFunctionPrePermAmounts(), enableExperimentalFriendClauses = enableExperimentalFriendClauses(), + assertTimeout = assertTimeout.toOption, ) } From aba68c75cf852b878b4a892a85d7ba83860306dd Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 10 Apr 2026 14:08:13 +0000 Subject: [PATCH 2/3] Add regression test for --assertTimeout using a matching loop The test defines an abstract ghost pure function `magic` (uninterpreted) and a method that assumes a quantifier whose trigger creates a matching loop. With a 1-second assert timeout set via inline config, Silicon correctly reports the assertion as failed instead of looping forever. https://claude.ai/code/session_01DNDg4ADj7NW35SQMt26uD2 --- .../assert_timeout/dangerous_triggers.gobra | 21 +++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 src/test/resources/regressions/features/assert_timeout/dangerous_triggers.gobra diff --git a/src/test/resources/regressions/features/assert_timeout/dangerous_triggers.gobra b/src/test/resources/regressions/features/assert_timeout/dangerous_triggers.gobra new file mode 100644 index 000000000..a0e2d06bb --- /dev/null +++ b/src/test/resources/regressions/features/assert_timeout/dangerous_triggers.gobra @@ -0,0 +1,21 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +// ##(--assertTimeout 1000) + +package asserttimeout + +// magic is an abstract ghost pure function (uninterpreted) used only in specification +ghost pure func magic(i int) int + +func dangerousTriggers() { + // Our definition of `magic`, with a matching loop: + // instantiating the quantifier with i=magic(k) produces a new term magic(magic(k)), + // which triggers another instantiation, creating an infinite chain. + assume forall i int :: { magic(i) } magic(magic(i)) == magic(2*i) + i + + // The following assertion should fail: the matching loop prevents Silicon from + // proving this within the assert timeout. + //:: ExpectedOutput(assert_error:assertion_error) + assert magic(magic(10)) == magic(87987978) + 10 +} From 804fab42337821014443549e90ad5fd08191ae30 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 10 Apr 2026 16:17:49 +0200 Subject: [PATCH 3/3] Apply suggestion from @jcp19 --- .../features/assert_timeout/dangerous_triggers.gobra | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/test/resources/regressions/features/assert_timeout/dangerous_triggers.gobra b/src/test/resources/regressions/features/assert_timeout/dangerous_triggers.gobra index a0e2d06bb..af24e29d6 100644 --- a/src/test/resources/regressions/features/assert_timeout/dangerous_triggers.gobra +++ b/src/test/resources/regressions/features/assert_timeout/dangerous_triggers.gobra @@ -6,7 +6,9 @@ package asserttimeout // magic is an abstract ghost pure function (uninterpreted) used only in specification -ghost pure func magic(i int) int +ghost +decreases +pure func magic(i int) int func dangerousTriggers() { // Our definition of `magic`, with a matching loop: