From 7248b8f5af9370ea896ae1a1a941c3e07188cb6c Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Mon, 23 Feb 2026 21:46:50 +0800 Subject: [PATCH 1/3] catches I/O exceptions while writing input to Boogie --- .../scala/viper/carbon/verifier/BoogieInterface.scala | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/carbon/verifier/BoogieInterface.scala b/src/main/scala/viper/carbon/verifier/BoogieInterface.scala index 2f24baf8..ca1de5ae 100644 --- a/src/main/scala/viper/carbon/verifier/BoogieInterface.scala +++ b/src/main/scala/viper/carbon/verifier/BoogieInterface.scala @@ -13,6 +13,7 @@ import viper.silver.verifier.errors.Internal import viper.silver.verifier.reasons.InternalReason import viper.silver.verifier._ +import java.io import java.io._ import scala.jdk.CollectionConverters._ @@ -197,8 +198,12 @@ trait BoogieInterface { inputStreamThread.start() // Send the program to Boogie - proc.getOutputStream.write(input.getBytes); - proc.getOutputStream.close() + try { + proc.getOutputStream.write(input.getBytes) + proc.getOutputStream.close() + } catch { + case e: IOException => sys.error(s"Couldn't pass input to Boogie process: $e") + } var boogieTimeout = false From ce647e2a6b2d0da341435554c09a5a95bc59c861 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Mon, 23 Feb 2026 23:24:31 +0800 Subject: [PATCH 2/3] adds stderr logging in case writing to boogie process fails --- .../carbon/verifier/BoogieInterface.scala | 60 +++++++++++++++---- 1 file changed, 49 insertions(+), 11 deletions(-) diff --git a/src/main/scala/viper/carbon/verifier/BoogieInterface.scala b/src/main/scala/viper/carbon/verifier/BoogieInterface.scala index ca1de5ae..1f79873e 100644 --- a/src/main/scala/viper/carbon/verifier/BoogieInterface.scala +++ b/src/main/scala/viper/carbon/verifier/BoogieInterface.scala @@ -15,6 +15,7 @@ import viper.silver.verifier._ import java.io import java.io._ +import java.nio.charset.StandardCharsets import scala.jdk.CollectionConverters._ class BoogieDependency(_location: String) extends Dependency { @@ -25,16 +26,28 @@ class BoogieDependency(_location: String) extends Dependency { class InputStreamConsumer(val is: InputStream, actionBeforeConsumption: () => Unit) extends Runnable { var result : Option[String] = None - - private def convertStreamToString(is: InputStream) = { - val s = new java.util.Scanner(is).useDelimiter("\\A") - if (s.hasNext) s.next() else "" - } + private val buffer = new StringBuilder def run(): Unit = { actionBeforeConsumption() - result = Some(convertStreamToString(is)) - is.close() + val reader = new BufferedReader(new InputStreamReader(is, StandardCharsets.UTF_8)) + try { + var line = reader.readLine() + while (line != null) { + buffer.synchronized { + buffer.append(line).append('\n') + } + line = reader.readLine() + } + result = Some(snapshot) + } finally { + reader.close() + is.close() + } + } + + def snapshot: String = buffer.synchronized { + buffer.toString() } } @@ -164,7 +177,7 @@ trait BoogieInterface { /** * Invoke Boogie. - * Returns None if there was a timeout, otherwise the Boogie output. + * Returns None if there was a timeout or error, otherwise the Boogie output. */ private def run(input: String, options: Seq[String], timeout: Option[Int]) = { reporter report BackendSubProcessReport("carbon", boogiePath, BeforeInputSent, _boogieProcessPid) @@ -172,7 +185,12 @@ trait BoogieInterface { // When the filename is "stdin.bpl" Boogie reads the program from standard input. val cmd: Seq[String] = Seq(boogiePath) ++ options ++ Seq("stdin.bpl") val pb: ProcessBuilder = new ProcessBuilder(cmd.asJava) - val proc: Process = pb.start() + val proc: Process = try { + pb.start() + } catch { + case e: IOException => + sys.error(s"Couldn't start Boogie process. Command: ${cmd.mkString(" ")}. Error: $e") + } _boogieProcess = Some(proc) _boogieProcessPid = Some(proc.pid) @@ -197,12 +215,31 @@ trait BoogieInterface { errorStreamThread.start() inputStreamThread.start() + def captureEarlyContext(): String = { + val processState = + if (proc.isAlive) "alive" + else s"exited(${proc.exitValue()})" + errorStreamThread.join(200) + inputStreamThread.join(200) + val earlyStderr = errorConsumer.snapshot.trim + val earlyStdout = inputConsumer.snapshot.trim + val stderrSuffix = + if (earlyStderr.nonEmpty) s"\nBoogie stderr (early):\n$earlyStderr" + else "" + val stdoutSuffix = + if (earlyStdout.nonEmpty) s"\nBoogie stdout (early):\n$earlyStdout" + else "" + s"\nProcess state: $processState$stderrSuffix$stdoutSuffix" + } + // Send the program to Boogie try { proc.getOutputStream.write(input.getBytes) proc.getOutputStream.close() } catch { - case e: IOException => sys.error(s"Couldn't pass input to Boogie process: $e") + case e: IOException => + // The write usually fails because Boogie already terminated. + sys.error(s"Couldn't pass input to Boogie process: $e${captureEarlyContext()}") } var boogieTimeout = false @@ -236,7 +273,8 @@ trait BoogieInterface { else Some(errorOutput + normalOutput) } catch { - case _: NoSuchElementException => sys.error("Could not retrieve output from Boogie") + case e: NoSuchElementException => + sys.error(s"Could not retrieve output from Boogie: $e${captureEarlyContext()}") } } From aa16b9ad70a0f073abf9e712fb82c62675893201 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Tue, 24 Feb 2026 10:17:37 +0800 Subject: [PATCH 3/3] improves diff slightly --- src/main/scala/viper/carbon/verifier/BoogieInterface.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/carbon/verifier/BoogieInterface.scala b/src/main/scala/viper/carbon/verifier/BoogieInterface.scala index 1f79873e..d5909f34 100644 --- a/src/main/scala/viper/carbon/verifier/BoogieInterface.scala +++ b/src/main/scala/viper/carbon/verifier/BoogieInterface.scala @@ -216,11 +216,11 @@ trait BoogieInterface { inputStreamThread.start() def captureEarlyContext(): String = { + errorStreamThread.join(200) + inputStreamThread.join(200) val processState = if (proc.isAlive) "alive" else s"exited(${proc.exitValue()})" - errorStreamThread.join(200) - inputStreamThread.join(200) val earlyStderr = errorConsumer.snapshot.trim val earlyStdout = inputConsumer.snapshot.trim val stderrSuffix =