Merge pull request #483 from viperproject/meilers_timeout

Adding an overall timeout option
viperproject · Dec 7, 2023 · 6e4ce2f · 6e4ce2f
2 parents 2e12ccd + 5429a24
commit 6e4ce2f
Show file tree

Hide file tree

Showing 3 changed files with 48 additions and 21 deletions.
diff --git a/src/main/scala/viper/carbon/Carbon.scala b/src/main/scala/viper/carbon/Carbon.scala
@@ -116,5 +116,12 @@ class CarbonConfig(args: Seq[String]) extends SilFrontendConfig(args, "Carbon")
     noshort = true
   )
 
+  val timeout = opt[Int]("timeout",
+    descr = ("Time out after approx. n seconds. The timeout is for the whole verification in Boogie, "
+           + "not per method or proof obligation (default: 0, i.e. no timeout)."),
+    default = None,
+    noshort = true
+  )
+
   verify()
 }
diff --git a/src/main/scala/viper/carbon/CarbonVerifier.scala b/src/main/scala/viper/carbon/CarbonVerifier.scala
@@ -211,6 +211,8 @@ case class CarbonVerifier(override val reporter: Reporter,
       }
     }
 
+    var timeout: Option[Int] = None
+
     if(config != null)
     {
       config.boogieOut.toOption match {
@@ -222,9 +224,10 @@ case class CarbonVerifier(override val reporter: Reporter,
           stream.close()
         case None =>
       }
+      timeout = config.timeout.toOption
     }
 
-    invokeBoogie(_translated, options) match {
+    invokeBoogie(_translated, options, timeout) match {
       case (version,result) =>
         if (version!=null) { dependencies.foreach(_ match {
           case b:BoogieDependency => b.version = version

diff --git a/src/main/scala/viper/carbon/verifier/BoogieInterface.scala b/src/main/scala/viper/carbon/verifier/BoogieInterface.scala
@@ -79,7 +79,7 @@ trait BoogieInterface {
 
   var errormap: Map[Int, VerificationError] = Map()
   var models : collection.mutable.ListBuffer[String] = new collection.mutable.ListBuffer[String]
-  def invokeBoogie(program: Program, options: Seq[String]): (String,VerificationResult) = {
+  def invokeBoogie(program: Program, options: Seq[String], timeout: Option[Int]): (String,VerificationResult) = {
     // find all errors and assign everyone a unique id
     errormap = Map()
     program.visit {
@@ -88,22 +88,28 @@ trait BoogieInterface {
     }
 
     // invoke Boogie
-    val output = run(program.toString, defaultOptions ++ options)
-
-    // parse the output
-    parse(output) match {
-      case (version,Nil) =>
-        (version,Success)
-      case (version,errorIds) => {
-        val errors = (0 until errorIds.length).map(i => {
-          val id = errorIds(i)
-          val error = errormap.get(id).get
-          if (models.nonEmpty)
-            error.failureContexts = Seq(FailureContextImpl(Some(SimpleCounterexample(Model(models(i))))))
-          error
-        })
-        (version,Failure(errors))
-      }
+    val optOutput = run(program.toString, defaultOptions ++ options, timeout)
+    optOutput match {
+      case None =>
+        // Timeout
+        (null, Failure(Seq(TimeoutOccurred(timeout.get, "second(s)"))))
+      case Some(output) =>
+        // parse the output
+        parse(output) match {
+          case (version, Nil) =>
+            (version, Success)
+          case (version, errorIds) => {
+            val errors = (0 until errorIds.length).map(i => {
+              val id = errorIds(i)
+              val error = errormap.get(id).get
+              if (models.nonEmpty) {
+                error.failureContexts = Seq(FailureContextImpl(Some(SimpleCounterexample(Model(models(i))))))
+              }
+              error
+            })
+            (version, Failure(errors))
+          }
+        }
     }
   }
 
@@ -157,8 +163,9 @@ trait BoogieInterface {
 
   /**
     * Invoke Boogie.
+    * Returns None if there was a timeout, otherwise the Boogie output.
     */
-  private def run(input: String, options: Seq[String]) = {
+  private def run(input: String, options: Seq[String], timeout: Option[Int]) = {
     reporter report BackendSubProcessReport("carbon", boogiePath, BeforeInputSent, _boogieProcessPid)
 
     // When the filename is "stdin.bpl" Boogie reads the program from standard input.
@@ -193,8 +200,15 @@ trait BoogieInterface {
     proc.getOutputStream.write(input.getBytes);
     proc.getOutputStream.close()
 
+    var boogieTimeout = false
+
     try {
-      proc.waitFor()
+      timeout match {
+        case Some(t) if t > 0 =>
+          boogieTimeout = !proc.waitFor(t, java.util.concurrent.TimeUnit.SECONDS)
+        case _ =>
+          proc.waitFor()
+      }
     } finally {
       destroyProcessAndItsChildren(proc, boogiePath)
     }
@@ -212,7 +226,10 @@ trait BoogieInterface {
       val normalOutput = inputConsumer.result.get
       reporter report BackendSubProcessReport("carbon", boogiePath, OnExit, _boogieProcessPid)
 
-      errorOutput + normalOutput
+      if (boogieTimeout)
+        None
+      else
+        Some(errorOutput + normalOutput)
     } catch {
       case _: NoSuchElementException => sys.error("Could not retrieve output from Boogie")
     }