Implement unreachable check and send files to opt using pipe

src/col/vct/col/serialize/SerializeOrigin.scala

@@ -32,7 +32,12 @@ object SerializeOrigin extends LazyLogging {
         val path = Path.of(context.directory, context.filename)
         val readable = fileMap.getOrElseUpdate(
           path, {
-            if (path.toFile.exists()) {
+            if (context.filename == "<stdin>") {
+              logger.warn(
+                "The file was compiled from standard input, origin information will be missing"
+              )
+              null
+            } else if (path.toFile.exists()) {
               if (
                 context.checksum.isDefined && context.checksumKind.isDefined
               ) {

src/parsers/vct/parsers/parser/ColLLVMParser.scala

@@ -11,10 +11,10 @@ import vct.col.origin.{ExpectedError, Origin}
 import vct.col.ref.Ref
 import vct.parsers.transform.{BlameProvider, LLVMContractToCol, OriginProvider}
 import vct.result.VerificationError.{SystemError, Unreachable, UserError}
-import vct.parsers.{Parser, ParseResult}
+import vct.parsers.{ParseResult, Parser}
 import vct.parsers.debug.DebugOptions
 
-import java.io.{IOException, Reader}
+import java.io.{IOException, OutputStreamWriter, Reader}
 import java.nio.file.Path
 import java.nio.charset.StandardCharsets
 import java.nio.file.Path
@@ -25,21 +25,18 @@ case class ColLLVMParser(
     blameProvider: BlameProvider,
     pallas: Path,
 ) extends Parser with LazyLogging {
-  private case class LLVMParseError(
-      fileName: String,
-      errorCode: Int,
-      error: String,
-  ) extends UserError {
+  private case class LLVMParseError(errorCode: Int, error: String)
+      extends UserError {
     override def code: String = "LLVMParseError"
 
     override def text: String =
       messageContext(
-        s"[ERROR] Parsing file $fileName failed with exit code $errorCode:\n$error"
+        s"[ERROR] Parsing failed with exit code $errorCode:\n$error"
       )
   }
 
-  override def parse[G](
-      readable: Readable,
+  override def parseReader[G](
+      reader: Reader,
       baseOrigin: Origin = Origin(Nil),
   ): ParseResult[G] = {
     if (pallas == null) {
@@ -51,17 +48,28 @@ case class ColLLVMParser(
       "opt-17",
       s"--load-pass-plugin=$pallas",
       "--passes=module(pallas-declare-variables,pallas-collect-module-spec),function(pallas-declare-function,pallas-assign-pure,pallas-declare-function-contract,pallas-transform-function-body),module(pallas-print-protobuf)",
-      readable.fileName,
       "--disable-output",
     )
 
     val process = new ProcessBuilder(command: _*).start()
 
+    new Thread(
+      () => {
+        Using(new OutputStreamWriter(
+          process.getOutputStream,
+          StandardCharsets.UTF_8,
+        )) { writer =>
+          val written = reader.transferTo(writer)
+          logger.debug(s"Wrote $written bytes to opt")
+        }.get
+      },
+      "[VerCors] opt stdout writer",
+    ).start()
+
     val protoProgram =
       Using(process.getInputStream) { is => Program.parseFrom(is) }
         .recoverWith { case _: IOException =>
           Failure(LLVMParseError(
-            readable.fileName,
             process.exitValue(),
             new String(
               process.getErrorStream.readAllBytes(),
@@ -73,7 +81,6 @@ case class ColLLVMParser(
     process.waitFor()
     if (process.exitValue() != 0) {
       throw LLVMParseError(
-        readable.fileName,
         process.exitValue(),
         new String(
           process.getErrorStream.readAllBytes(),
@@ -89,9 +96,4 @@ case class ColLLVMParser(
       .deserializeProgram[G](protoProgram, _ => blameProvider.apply())
     ParseResult(COLProgram.declarations, Seq.empty)
   }
-
-  override def parseReader[G](
-      reader: Reader,
-      baseOrigin: Origin,
-  ): ParseResult[G] = throw new UnsupportedOperationException()
 }

src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala

@@ -2,7 +2,15 @@ package vct.rewrite.lang
 
 import com.typesafe.scalalogging.LazyLogging
 import vct.col.ast._
-import vct.col.origin.{DiagnosticOrigin, Origin, PanicBlame, TypeName}
+import vct.col.origin.{
+  AssertFailed,
+  Blame,
+  DiagnosticOrigin,
+  Origin,
+  PanicBlame,
+  TypeName,
+  UnreachableReachedError,
+}
 import vct.col.ref.{DirectRef, LazyRef, Ref}
 import vct.col.resolve.ctx.RefLLVMFunctionDefinition
 import vct.col.rewrite.{Generation, Rewritten}
@@ -61,6 +69,13 @@ case object LangLLVMToCol {
         s"Unsupported truncation from '${trunc.inputType}' to '${trunc.outputType}'"
       )
   }
+
+  private final case class UnreachableReached(
+      unreachable: LLVMBranchUnreachable[_]
+  ) extends Blame[AssertFailed] {
+    override def blame(error: AssertFailed): Unit =
+      unreachable.blame.blame(UnreachableReachedError(unreachable))
+  }
 }
 
 case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
@@ -762,6 +777,13 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
     CastFloat(rw.dispatch(fpext.value), rw.dispatch(fpext.t))
   }
 
+  def rewriteUnreachable(
+      unreachable: LLVMBranchUnreachable[Pre]
+  ): Statement[Post] = {
+    implicit val o: Origin = unreachable.o
+    Assert[Post](ff)(UnreachableReached(unreachable))
+  }
+
   private def getInferredType(e: Expr[Pre]): Type[Pre] =
     e match {
       case Local(Ref(v)) => localVariableInferredType.getOrElse(v, e.t)

src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala

@@ -275,6 +275,8 @@ case class LangSpecificToCol[Pre <: Generation](
       case store: LLVMStore[Pre] => llvm.rewriteStore(store)
       case alloc: LLVMAllocA[Pre] => llvm.rewriteAllocA(alloc)
       case block: LLVMBasicBlock[Pre] => llvm.rewriteBasicBlock(block)
+      case unreachable: LLVMBranchUnreachable[Pre] =>
+        llvm.rewriteUnreachable(unreachable)
       case other => other.rewriteDefault()
     }
 

test/main/vct/test/integration/examples/LLVMSpec.scala

@@ -12,4 +12,18 @@ class LLVMSpec extends VercorsSpec {
   vercors should verify using silicon example "concepts/llvm/cubed.c"
   vercors should verify using silicon flags("--contract-import-file", "examples/concepts/llvm/cubed-contracts.pvl") example "concepts/llvm/cubed.ll"
   vercors should verify using silicon flags("--contract-import-file", "examples/concepts/llvm/void-contracts.pvl") example "concepts/llvm/void.ll"
+  vercors should fail withCode "unreachable" using silicon in "reaching an 'unreachable' statement" llvm
+  """
+  define void @foo() {
+    unreachable
+  }
+  """
+  vercors should verify using silicon in "an unreachable 'unreachable' statement" llvm
+    """
+  define void @foo() {
+    br i1 0, label %1, label %2
+    1: unreachable
+    2: ret void
+  }
+  """
 }

test/main/vct/test/integration/helper/VercorsSpec.scala

@@ -223,6 +223,7 @@ abstract class VercorsSpec extends AnyFlatSpec {
     def java(data: String)(implicit pos: source.Position): Unit = literal("java", data)
     def c(data: String)(implicit pos: source.Position): Unit = literal("c", data)
     def cpp(data: String)(implicit pos: source.Position): Unit = literal("cpp", data)
+    def llvm(data: String)(implicit pos: source.Position): Unit = literal("ll", data)
   }
 
   val vercors: VercorsWord = new VercorsWord