Improved Boogie Process Error Reporting

[ArquintL]

Feel free to merge this PR after the Viper release.

This PR simply provides more error reporting in case the Boogie process does not work as expected.
These changes were motivated by Gobra due to the following scenario: I wanted to upgrade the JVM version we use within the Docker image that Gobra produces as part of its CI. While doing so, I noticed that all our Carbon-based testcases failed and the only error I got was "java.io.IOException: Broken pipe". After applying this PR's changes, I additionally got "Boogie stderr (early):\n No usable version of libssl was found" which was immensely useful to eventually resolve the issue within our Docker image

[marcoeilers]

LGTM, thanks!

[Copilot]

Pull request overview

This PR improves diagnostics around Boogie subprocess failures by capturing and surfacing early stdout/stderr and process state when Boogie cannot be started, terminates early, or output retrieval fails—addressing cases where previous failures were hard to debug (e.g., “Broken pipe” without actionable stderr).

Changes:

• Reworked Boogie stdout/stderr consumption to support incremental “early” snapshots for richer error messages.
• Added contextual error reporting when starting Boogie fails, when writing to stdin fails, and when output retrieval fails.
• Updated documentation to reflect the intended behavior of run (though it currently mismatches implementation).

Suppressed comments (4)

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

• InputStreamConsumer.run does not guarantee the input stream is closed if actionBeforeConsumption() throws, and it redundantly closes both the BufferedReader and the underlying InputStream (the reader close already closes the stream). Restructure the method so the reader is always closed in a single finally.

  def run(): Unit = {
    actionBeforeConsumption()
    val reader = new BufferedReader(new InputStreamReader(is, StandardCharsets.UTF_8))
    try {
      var line = reader.readLine()

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

• The Scaladoc says run returns None on "timeout or error", but on I/O/process errors it throws via sys.error(...) instead of returning None. This mismatch is confusing for callers (and invokeBoogie treats None as a timeout). Update the comment to match the actual behavior.

  /**
    * Invoke Boogie.
    * Returns None if there was a timeout or error, otherwise the Boogie output.
    */

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

• captureEarlyContext() calls Thread.join(...) without handling InterruptedException. If the thread is interrupted while building the error message, it can mask the original failure (e.g., broken pipe) and lose the early stdout/stderr context. Catch the interruption and restore the interrupt flag.

    def captureEarlyContext(): String = {
      errorStreamThread.join(200)
      inputStreamThread.join(200)
      val processState =
        if (proc.isAlive) "alive"

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

• The input is written using the platform default charset (input.getBytes), but the subprocess output is decoded explicitly as UTF-8. Use UTF-8 consistently when sending the Boogie program to avoid corruption on non-UTF-8 platforms or when the input contains non-ASCII characters.

      proc.getOutputStream.write(input.getBytes)

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.