From a6860646d045648203c6f1dafa425437725ea66b Mon Sep 17 00:00:00 2001 From: Alexander Stekelenburg Date: Wed, 25 Jun 2025 17:46:58 +0200 Subject: [PATCH 1/2] Add implementation of setTimeout for CVC5 --- src/main/scala/Config.scala | 23 ++++++-------------- src/main/scala/decider/CVC5ProverStdIO.scala | 18 ++++++++++++--- 2 files changed, 22 insertions(+), 19 deletions(-) diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala index b0fd1cfb6..95934e2c5 100644 --- a/src/main/scala/Config.scala +++ b/src/main/scala/Config.scala @@ -213,8 +213,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") { ) val assertTimeout: ScallopOption[Int] = opt[Int]("assertTimeout", - descr = ("Timeout (in ms) per SMT solver assertion (default: 0, i.e. no timeout). " - + s"Ignored when using the ${Cvc5ProverStdIO.name} prover."), + descr = ("Timeout (in ms) per SMT solver assertion (default: 0, i.e. no timeout). "), default = None, noshort = true ) @@ -225,8 +224,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") { + "check doesn't, at least not directly. However, failing checks might result in " + "performance degradation, e.g. when a dead program path is nevertheless explored, " + "and indirectly in verification failures due to incompletenesses, e.g. when " - + "the held permission amount is too coarsely underapproximated (default: 10). " - + s"Ignored when using the ${Cvc5ProverStdIO.name} prover."), + + "the held permission amount is too coarsely underapproximated (default: 10). "), default = Some(10), noshort = true ) @@ -239,17 +237,13 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") { private val rawProverSaturationTimeout = opt[Int]("proverSaturationTimeout", descr = ( "Timeout (in ms) used for the prover's state saturation calls (default: 100). " - + "A timeout of 0 disables all saturation checks." - + s"Note that for the ${Cvc5ProverStdIO.name} prover, state saturation calls can " - + "either be disabled (weights or base timeout of 0) or forced with no timeout " - + "(positive weight and base timeout)."), + + "A timeout of 0 disables all saturation checks."), default = Some(100), noshort = true ) val pushTimeout: ScallopOption[Int] = opt[Int]("pushTimeout", - descr = ( "Timeout (in ms) per push operation in the SMT solver. (default: 0, i.e. no timeout). " - + s"Ignored when using the ${Cvc5ProverStdIO.name} prover."), + descr = ( "Timeout (in ms) per push operation in the SMT solver. (default: 0, i.e. no timeout). "), default = Some(0), noshort = true ) @@ -302,10 +296,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") { + s" after inhale: ${defaultProverSaturationTimeoutWeights.afterInhale}\n" + s" before repeated prover queries: ${defaultProverSaturationTimeoutWeights.beforeRepetition}\n" + "Weights must be non-negative, a weight of 0 disables the corresponding saturation " - + "call and a minimal timeout of 10ms is enforced." - + s"Note that for the ${Cvc5ProverStdIO.name} prover, state saturation calls can " - + "either be disabled (weights or base timeout of 0) or forced with no timeout " - + "(positive weight and base timeout)."), + + "call and a minimal timeout of 10ms is enforced."), default = Some(defaultProverSaturationTimeoutWeights), noshort = true )(saturationTimeoutWeightsConverter) @@ -404,7 +395,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") { lazy val proverResourcesPerMillisecond: Int = { if (rawZ3ResourcesPerMillisecond.isSupplied) rawZ3ResourcesPerMillisecond() else rawProverResourcesPerMillisecond() - } + } val rawProverRandomizeSeeds: ScallopOption[Boolean] = opt[Boolean]("proverRandomizeSeeds", descr = "Set various random seeds of the prover to random values", @@ -795,7 +786,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") { ) val conditionalizePermissions: ScallopOption[Boolean] = opt[Boolean]("conditionalizePermissions", - descr = "Potentially reduces the number of symbolic execution paths, by conditionalising " + + descr = "Potentially reduces the number of symbolic execution paths, by conditionalising " + "permission expressions. E.g. rewrite \"b ==> acc(x.f, p)\" to \"acc(x.f, b ? p : none)\"." + "This is an experimental feature; report problems if you observe any.", default = Some(false), diff --git a/src/main/scala/decider/CVC5ProverStdIO.scala b/src/main/scala/decider/CVC5ProverStdIO.scala index cece2a4e0..02cacce3f 100644 --- a/src/main/scala/decider/CVC5ProverStdIO.scala +++ b/src/main/scala/decider/CVC5ProverStdIO.scala @@ -29,7 +29,7 @@ class Cvc5ProverStdIO(uniqueId: String, identifierFactory: IdentifierFactory, reporter: Reporter) extends ProverStdIO(uniqueId, termConverter, identifierFactory, reporter) { - + val name: String = Cvc5ProverStdIO.name val minVersion: Version = Cvc5ProverStdIO.minVersion val maxVersion: Option[Version] = Cvc5ProverStdIO.maxVersion @@ -39,8 +39,20 @@ class Cvc5ProverStdIO(uniqueId: String, val startUpArgs: Seq[String] = Cvc5ProverStdIO.startUpArgs val randomizeSeedsOptions: Seq[String] = Cvc5ProverStdIO.randomizeSeedsOptions - // cvc5 does not support per-check timeouts after instantiation. - protected def setTimeout(timeout: Option[Int]): Unit = {} + protected def setTimeout(timeout: Option[Int]): Unit = { + val effectiveTimeout = timeout.getOrElse(Verifier.config.proverTimeout) + + if (lastTimeout != effectiveTimeout) { + lastTimeout = effectiveTimeout + + if (Verifier.config.proverEnableResourceBounds) { + writeLine(s"(set-option :rlimit-per ${effectiveTimeout * Verifier.config.proverResourcesPerMillisecond})") + } else { + writeLine(s"(set-option :tlimit-per $effectiveTimeout)") + } + readSuccess() + } + } protected def getProverPath: Path = { Paths.get(Verifier.config.cvc5Exe) From 80666bec372fbc249351afecf230bbe1d15b3449 Mon Sep 17 00:00:00 2001 From: Alexander Stekelenburg Date: Fri, 27 Jun 2025 16:58:21 +0200 Subject: [PATCH 2/2] Change rlimit-per to reproducible-resource-limit for CVC5 --- src/main/scala/decider/CVC5ProverStdIO.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/decider/CVC5ProverStdIO.scala b/src/main/scala/decider/CVC5ProverStdIO.scala index 02cacce3f..d1acda569 100644 --- a/src/main/scala/decider/CVC5ProverStdIO.scala +++ b/src/main/scala/decider/CVC5ProverStdIO.scala @@ -46,7 +46,7 @@ class Cvc5ProverStdIO(uniqueId: String, lastTimeout = effectiveTimeout if (Verifier.config.proverEnableResourceBounds) { - writeLine(s"(set-option :rlimit-per ${effectiveTimeout * Verifier.config.proverResourcesPerMillisecond})") + writeLine(s"(set-option :reproducible-resource-limit ${effectiveTimeout * Verifier.config.proverResourcesPerMillisecond})") } else { writeLine(s"(set-option :tlimit-per $effectiveTimeout)") }