[VCLLVM] LLVM to COL rewriter for LLVM specific nodes

col/src/main/java/vct/col/ast/Node.scala

@@ -919,7 +919,9 @@ final case class BipInternal[G]()(implicit val o: Origin = DiagnosticOrigin) ext
 final case class BipPortSynchronization[G](ports: Seq[Ref[G, BipPort[G]]], wires: Seq[BipGlueDataWire[G]])(val blame: Blame[BipSynchronizationFailure])(implicit val o: Origin) extends GlobalDeclaration[G] with BipPortSynchronizationImpl[G]
 final case class BipTransitionSynchronization[G](transitions: Seq[Ref[G, BipTransition[G]]], wires: Seq[BipGlueDataWire[G]])(val blame: Blame[BipSynchronizationFailure])(implicit val o: Origin) extends GlobalDeclaration[G] with BipTransitionSynchronizationImpl[G]
 
-final class LlvmFunctionContract[G](val value:String, val references:Seq[(String, Ref[G, Declaration[G]])])(implicit val o: Origin) extends NodeFamily[G] with LLVMFunctionContractImpl[G]
+final class LlvmFunctionContract[G](val value:String, val references:Seq[(String, Ref[G, Declaration[G]])])
+                                   (val blame: Blame[NontrivialUnsatisfiable])
+                                   (implicit val o: Origin) extends NodeFamily[G] with LLVMFunctionContractImpl[G]
 
 final class LlvmFunctionDefinition[G](val returnType: Type[G],
                                       val args: Seq[Variable[G]],

col/src/main/java/vct/col/ast/lang/LLVMFunctionDefinitionImpl.scala

@@ -1,7 +1,8 @@
 package vct.col.ast.lang
 
-import vct.col.ast.LlvmFunctionDefinition
-
-trait LLVMFunctionDefinitionImpl[G] { this: LlvmFunctionDefinition[G] =>
+import vct.col.ast.{Declaration, LlvmFunctionDefinition}
+import vct.col.ast.util.Declarator
 
+trait LLVMFunctionDefinitionImpl[G] extends Declarator[G] { this: LlvmFunctionDefinition[G] =>
+  override def declarations: Seq[Declaration[G]] = args
 }

col/src/main/java/vct/col/resolve/ctx/Referrable.scala

@@ -124,6 +124,7 @@ case object Referrable {
     case decl: VeyMontSeqProg[G] => RefSeqProg(decl)
     case decl: VeyMontThread[G] => RefVeyMontThread(decl)
     case decl: JavaBipGlueContainer[G] => RefJavaBipGlueContainer()
+    case decl: LlvmFunctionDefinition[G] => RefLlvmFunctionDefinition()
   })
 
   def originName(decl: Declaration[_]): String = decl.o match {
@@ -221,7 +222,7 @@ case class RefPVLConstructor[G](decl: PVLConstructor[G]) extends Referrable[G] w
 case class RefJavaBipStatePredicate[G](state: String, decl: JavaAnnotation[G]) extends Referrable[G] with JavaBipStatePredicateTarget[G]
 case class RefJavaBipGuard[G](decl: JavaMethod[G]) extends Referrable[G] with JavaNameTarget[G]
 case class RefJavaBipGlueContainer[G]() extends Referrable[G] // Bip glue jobs are not actually referrable
-
+case class RefLlvmFunctionDefinition[G]() extends Referrable[G]
 case class RefSeqProg[G](decl: VeyMontSeqProg[G]) extends Referrable[G]
 case class RefVeyMontThread[G](decl: VeyMontThread[G]) extends Referrable[G] with PVLNameTarget[G]
 

parsers/src/main/java/vct/parsers/ColLLVMParser.scala

@@ -19,11 +19,11 @@ case class ColLLVMParser(override val originProvider: OriginProvider, override v
   }
 
   override def parse[G](stream: CharStream): ParseResult[G] = {
-    throw Unreachable("LLVM IR files should be parsed from an not ANTLR CharStream, use VCLLVM instead!")
+    throw Unreachable("LLVM IR files shouldn't be parsed from an ANTLR CharStream, use VCLLVM instead!")
   }
 
   override def parse[G](readable: Readable): ParseResult[G] = {
-    val command = Seq("VCLLVM", "--sample-col") //TODO convert --sample-col to actual file at some point
+    val command = Seq("VCLLVM", readable.fileName)
     val process = new ProcessBuilder(command:_*).start()
     process.waitFor()
     if (process.exitValue() != 0) {

rewrite/src/main/java/vct/col/rewrite/lang/LangLLVMToCol.scala

@@ -0,0 +1,40 @@
+package vct.col.rewrite.lang
+
+import com.typesafe.scalalogging.LazyLogging
+import vct.col.ast._
+import vct.col.origin.Origin
+import vct.col.rewrite.{Generation, Rewritten}
+
+case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends LazyLogging {
+  type Post = Rewritten[Pre]
+  implicit val implicitRewriter: AbstractRewriter[Pre, Post] = rw
+
+
+  def rewriteFunctionDef(func: LlvmFunctionDefinition[Pre]): Unit = {
+    implicit val o: Origin = func.contract.o
+    // TODO replace stub contract
+    val stubContract = new ApplicableContract[Post](
+      requires = new UnitAccountedPredicate[Post](BooleanValue(value = true)),
+      ensures = new UnitAccountedPredicate[Post](BooleanValue(value = true)),
+      contextEverywhere = BooleanValue(value = true),
+      signals = Seq.empty,
+      givenArgs = Seq.empty,
+      yieldsArgs = Seq.empty,
+      decreases = None)(func.contract.blame)(func.contract.o)
+
+
+    rw.globalDeclarations.declare(
+      new Procedure[Post](
+        returnType = rw.dispatch(func.returnType),
+        args = rw.variables.collect {
+          func.args.foreach(rw.dispatch)
+        }._1,
+        outArgs = Nil,
+        typeArgs = Nil,
+        body = Some(rw.dispatch(func.body)),
+        contract = stubContract
+      )(func.blame)(func.o)
+    )
+  }
+
+}

rewrite/src/main/java/vct/col/rewrite/lang/LangSpecificToCol.scala

@@ -37,6 +37,7 @@ case class LangSpecificToCol[Pre <: Generation]() extends Rewriter[Pre] with Laz
   val c: LangCToCol[Pre] = LangCToCol(this)
   val pvl: LangPVLToCol[Pre] = LangPVLToCol(this)
   val silver: LangSilverToCol[Pre] = LangSilverToCol(this)
+  val llvm: LangLLVMToCol[Pre] = LangLLVMToCol(this)
 
   val currentThis: ScopedStack[Expr[Post]] = ScopedStack()
   val currentClass: ScopedStack[Class[Pre]] = ScopedStack()
@@ -66,6 +67,7 @@ case class LangSpecificToCol[Pre <: Generation]() extends Rewriter[Pre] with Laz
     case func: CFunctionDefinition[Pre] => c.rewriteFunctionDef(func)
     case decl: CGlobalDeclaration[Pre] => c.rewriteGlobalDecl(decl)
     case decl: CLocalDeclaration[Pre] => ???
+    case func: LlvmFunctionDefinition[Pre] => llvm.rewriteFunctionDef(func)
 
     case cls: Class[Pre] =>
       currentClass.having(cls) {