Using Option type instead to mark timeout

Author: marcoeilers

src/main/scala/viper/carbon/verifier/BoogieInterface.scala

@@ -64,8 +64,6 @@ trait BoogieInterface {
     "/proverOpt:O:smt.qi.max_multi_patterns=1000",
     s"/proverOpt:PROVER_PATH=$z3Path")
 
-  val timeoutErrorName = "TIMEOUT"
-
   /** The (resolved) path where Boogie is supposed to be located. */
   def boogiePath: String
 
@@ -79,7 +77,7 @@ trait BoogieInterface {
   // Hence, for now we have to trust Boogie to manage its own sub-processes.
   // private var _z3ProcessStream: Option[LazyList[ProcessHandle]] = None
 
-  var errormap: Map[Int, AbstractError] = Map()
+  var errormap: Map[Int, VerificationError] = Map()
   var models : collection.mutable.ListBuffer[String] = new collection.mutable.ListBuffer[String]
   def invokeBoogie(program: Program, options: Seq[String], timeout: Option[Int]): (String,VerificationResult) = {
     // find all errors and assign everyone a unique id
@@ -90,33 +88,35 @@ trait BoogieInterface {
     }
 
     // invoke Boogie
-    val output = run(program.toString, defaultOptions ++ options, timeout)
-    // parse the output
-    parse(output, timeout) 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 match {
-              case e: AbstractVerificationError =>
-                e.failureContexts = Seq(FailureContextImpl(Some(SimpleCounterexample(Model(models(i))))))
-              case _ =>
-            }
+    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))
           }
-          error
-        })
-        (version,Failure(errors))
-      }
+        }
     }
   }
 
   /**
     * Parse the output of Boogie. Returns a pair of the detected version number and a sequence of error identifiers.
     */
-  private def parse(output: String, timeout: Option[Int]): (String,Seq[Int]) = {
+  private def parse(output: String): (String,Seq[Int]) = {
     val LogoPattern = "Boogie program verifier version ([0-9.]+),.*".r
     val SummaryPattern = "Boogie program verifier finished with ([0-9]+) verified, ([0-9]+) error.*".r
     val ErrorPattern = "  .+ \\[([0-9]+)\\]".r
@@ -131,13 +131,6 @@ trait BoogieInterface {
       errormap += (otherErrId -> internalError)
     }
 
-    def reportTimeout() = {
-      otherErrId -= 1
-      errors += otherErrId
-      val timeoutError = TimeoutOccurred(timeout.get, "second(s)")
-      errormap += (otherErrId -> timeoutError)
-    }
-
     var parsingModel : Option[StringBuilder] = None
     var stateInitialBlock = false
     for (l <- output.linesIterator) {
@@ -161,7 +154,6 @@ trait BoogieInterface {
         case SummaryPattern(v, e) =>
           if(e.toInt != errors.size) unexpected(s"Found ${errors.size} errors, but there should be $e. The output was: $output")
         case "" => // ignore empty lines
-        case `timeoutErrorName` if timeout.isDefined => reportTimeout()
         case _ =>
           unexpected(s"Found an unparsable output from Boogie: $l")
       }
@@ -171,6 +163,7 @@ trait BoogieInterface {
 
   /**
     * Invoke Boogie.
+    * Returns None if there was a timeout, otherwise the Boogie output.
     */
   private def run(input: String, options: Seq[String], timeout: Option[Int]) = {
     reporter report BackendSubProcessReport("carbon", boogiePath, BeforeInputSent, _boogieProcessPid)
@@ -233,7 +226,10 @@ trait BoogieInterface {
       val normalOutput = inputConsumer.result.get
       reporter report BackendSubProcessReport("carbon", boogiePath, OnExit, _boogieProcessPid)
 
-      errorOutput + normalOutput + (if (boogieTimeout) timeoutErrorName else "")
+      if (boogieTimeout)
+        None
+      else
+        Some(errorOutput + normalOutput)
     } catch {
       case _: NoSuchElementException => sys.error("Could not retrieve output from Boogie")
     }