From 065e9771a312c96c16544844a1f5233b59492e4d Mon Sep 17 00:00:00 2001 From: Alexander Stekelenburg Date: Mon, 11 Nov 2024 16:12:02 +0100 Subject: [PATCH] Implement unreachable check and send files to opt using pipe --- .../vct/col/serialize/SerializeOrigin.scala | 7 +++- .../vct/parsers/parser/ColLLVMParser.scala | 38 ++++++++++--------- .../vct/rewrite/lang/LangLLVMToCol.scala | 24 +++++++++++- .../vct/rewrite/lang/LangSpecificToCol.scala | 2 + .../test/integration/examples/LLVMSpec.scala | 14 +++++++ .../test/integration/helper/VercorsSpec.scala | 1 + 6 files changed, 66 insertions(+), 20 deletions(-) diff --git a/src/col/vct/col/serialize/SerializeOrigin.scala b/src/col/vct/col/serialize/SerializeOrigin.scala index f27b08cd5..027e88bc1 100644 --- a/src/col/vct/col/serialize/SerializeOrigin.scala +++ b/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 == "") { + 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 ) { diff --git a/src/parsers/vct/parsers/parser/ColLLVMParser.scala b/src/parsers/vct/parsers/parser/ColLLVMParser.scala index 7a307ced4..b5bd13777 100644 --- a/src/parsers/vct/parsers/parser/ColLLVMParser.scala +++ b/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() } diff --git a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala index 297aba67f..555cb75da 100644 --- a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala +++ b/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) diff --git a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala index ff483425c..c1af3d68b 100644 --- a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala +++ b/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() } diff --git a/test/main/vct/test/integration/examples/LLVMSpec.scala b/test/main/vct/test/integration/examples/LLVMSpec.scala index b4bba0a97..799f21485 100644 --- a/test/main/vct/test/integration/examples/LLVMSpec.scala +++ b/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 + } + """ } diff --git a/test/main/vct/test/integration/helper/VercorsSpec.scala b/test/main/vct/test/integration/helper/VercorsSpec.scala index 62b1a9667..cd11cdabb 100644 --- a/test/main/vct/test/integration/helper/VercorsSpec.scala +++ b/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