Add implementation of setTimeout for CVC5 (#933)

Author: superaxander

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),

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 :reproducible-resource-limit ${effectiveTimeout * Verifier.config.proverResourcesPerMillisecond})")
+      } else {
+        writeLine(s"(set-option :tlimit-per $effectiveTimeout)")
+      }
+      readSuccess()
+    }
+  }
 
   protected def getProverPath: Path = {
     Paths.get(Verifier.config.cvc5Exe)