From 6cf3297fffe0c02e38525aafdb4b14744a817512 Mon Sep 17 00:00:00 2001 From: Alexander Stekelenburg Date: Thu, 14 Mar 2024 11:06:29 +0100 Subject: [PATCH] Translate simple getelementptr and alloca instructions --- src/col/vct/col/ast/Node.scala | 11 ++- .../col/ast/lang/llvm/LLVMAllocAImpl.scala | 4 +- .../ast/lang/llvm/LLVMArrayValueImpl.scala | 2 +- .../lang/llvm/LLVMGetElementPointerImpl.scala | 2 +- .../lang/llvm/LLVMGlobalVariableImpl.scala | 2 +- .../ast/lang/llvm/LLVMIntegerValueImpl.scala | 2 +- .../vct/col/ast/lang/llvm/LLVMLoadImpl.scala | 2 +- .../ast/lang/llvm/LLVMMemoryAcquireImpl.scala | 2 +- .../llvm/LLVMMemoryAcquireReleaseImpl.scala | 2 +- .../lang/llvm/LLVMMemoryMonotonicImpl.scala | 2 +- .../lang/llvm/LLVMMemoryNotAtomicImpl.scala | 2 +- .../lang/llvm/LLVMMemoryOrderingImpl.scala | 2 +- .../ast/lang/llvm/LLVMMemoryReleaseImpl.scala | 2 +- ...LLVMMemorySequentiallyConsistentImpl.scala | 2 +- .../lang/llvm/LLVMMemoryUnorderedImpl.scala | 2 +- .../ast/lang/llvm/LLVMPointerValueImpl.scala | 11 ++- .../ast/lang/llvm/LLVMRawArrayValueImpl.scala | 2 +- .../lang/llvm/LLVMRawVectorValueImpl.scala | 2 +- .../ast/lang/llvm/LLVMSignExtendImpl.scala | 2 +- .../col/ast/lang/llvm/LLVMStatementImpl.scala | 7 ++ .../vct/col/ast/lang/llvm/LLVMStoreImpl.scala | 2 +- .../ast/lang/llvm/LLVMStructValueImpl.scala | 2 +- .../col/ast/lang/llvm/LLVMTArrayImpl.scala | 2 +- .../col/ast/lang/llvm/LLVMTFunctionImpl.scala | 2 +- .../vct/col/ast/lang/llvm/LLVMTIntImpl.scala | 2 +- .../col/ast/lang/llvm/LLVMTStructImpl.scala | 2 +- .../col/ast/lang/llvm/LLVMTVectorImpl.scala | 2 +- .../col/ast/lang/llvm/LLVMTruncateImpl.scala | 2 +- .../ast/lang/llvm/LLVMVectorValueImpl.scala | 2 +- .../ast/lang/llvm/LLVMZeroExtendImpl.scala | 2 +- .../llvm/LLVMZeroedAggregateValueImpl.scala | 2 +- .../vct/col/typerules/CoercingRewriter.scala | 6 +- src/col/vct/col/typerules/CoercionUtils.scala | 17 +++- .../Passes/Function/FunctionBodyTransformer.h | 9 +- src/llvm/include/Transform/Transform.h | 2 + .../Function/FunctionBodyTransformer.cpp | 19 ++-- .../Instruction/MemoryOpTransform.cpp | 7 +- src/llvm/lib/Transform/Transform.cpp | 7 ++ .../ResolveExpressionSideEffects.scala | 1 + .../vct/rewrite/lang/LangLLVMToCol.scala | 93 ++++++++++++++++++- .../vct/rewrite/lang/LangSpecificToCol.scala | 3 + 41 files changed, 196 insertions(+), 55 deletions(-) create mode 100644 src/col/vct/col/ast/lang/llvm/LLVMStatementImpl.scala diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index 72d31fd124..492f351984 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -1278,14 +1278,21 @@ final case class LLVMFunctionInvocation[G](ref: Ref[G, LLVMFunctionDefinition[G] final case class LLVMLoop[G](cond:Expr[G], contract:LLVMLoopContract[G], body:Statement[G]) (implicit val o: Origin) extends CompositeStatement[G] with LLVMLoopImpl[G] + @family sealed trait LLVMLoopContract[G] extends NodeFamily[G] with LLVMLoopContractImpl[G] + final case class LLVMLoopInvariant[G](value:String, references:Seq[(String, Ref[G, Declaration[G]])]) (val blame: Blame[LoopInvariantFailure]) (implicit val o: Origin) extends LLVMLoopContract[G] with LLVMLoopInvariantImpl[G] + +sealed trait LLVMStatement[G] extends Statement[G] with LLVMStatementImpl[G] + sealed trait LLVMExpr[G] extends Expr[G] with LLVMExprImpl[G] + final case class LLVMLocal[G](name: String)(val blame: Blame[DerefInsufficientPermission])(implicit val o: Origin) extends LLVMExpr[G] with LLVMLocalImpl[G] { var ref: Option[Ref[G, Variable[G]]] = None } + final case class LLVMAmbiguousFunctionInvocation[G](name: String, args: Seq[Expr[G]], givenMap: Seq[(Ref[G, Variable[G]], Expr[G])], @@ -1301,7 +1308,7 @@ final case class LLVMLoad[G](loadType: Type[G], pointer: Expr[G], ordering: LLVM (implicit val o: Origin) extends LLVMExpr[G] with LLVMLoadImpl[G] final case class LLVMStore[G](value: Expr[G], pointer: Expr[G], ordering: LLVMMemoryOrdering[G]) - (implicit val o: Origin) extends Statement[G] with LLVMStoreImpl[G] + (implicit val o: Origin) extends LLVMStatement[G] with LLVMStoreImpl[G] final case class LLVMGetElementPointer[G](structureType: Type[G], resultType: Type[G], pointer: Expr[G], indices: Seq[Expr[G]]) (implicit val o: Origin) extends LLVMExpr[G] with LLVMGetElementPointerImpl[G] @@ -1331,7 +1338,7 @@ final case class LLVMMemorySequentiallyConsistent[G]()(implicit val o:Origin) ex final case class LLVMIntegerValue[G](value: BigInt, integerType: Type[G])(implicit val o: Origin) extends ConstantInt[G] with LLVMExpr[G] with LLVMIntegerValueImpl[G] -final case class LLVMPointerValue[G](value: Ref[G, LLVMGlobalVariable[G]])(implicit val o: Origin) extends Constant[G] with LLVMExpr[G] with LLVMPointerValueImpl[G] +final case class LLVMPointerValue[G](value: Ref[G, Declaration[G]])(implicit val o: Origin) extends Constant[G] with LLVMExpr[G] with LLVMPointerValueImpl[G] // TODO: The LLVMFunctionPointerValue references a GlobalDeclaration instead of an LLVMFunctionDefinition because there is no other COL node we can use as a function pointer literal final case class LLVMFunctionPointerValue[G](value: Ref[G, GlobalDeclaration[G]])(implicit val o: Origin) extends Constant[G] with LLVMExpr[G] with LLVMFunctionPointerValueImpl[G] final case class LLVMStructValue[G](value: Seq[Expr[G]], structType: Type[G])(implicit val o: Origin) extends Constant[G] with LLVMExpr[G] with LLVMStructValueImpl[G] diff --git a/src/col/vct/col/ast/lang/llvm/LLVMAllocAImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMAllocAImpl.scala index 760533ca67..0b7ca28484 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMAllocAImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMAllocAImpl.scala @@ -1,8 +1,8 @@ package vct.col.ast.lang.llvm import vct.col.ast.ops.LLVMAllocAOps -import vct.col.ast.{LLVMAllocA, Type} +import vct.col.ast.{LLVMAllocA, Type, LLVMTPointer} trait LLVMAllocAImpl[G] extends LLVMAllocAOps[G] { this: LLVMAllocA[G] => - override val t: Type[G] = this.allocationType + override val t: Type[G] = LLVMTPointer(Some(this.allocationType)) } diff --git a/src/col/vct/col/ast/lang/llvm/LLVMArrayValueImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMArrayValueImpl.scala index 045e874eae..594a73df49 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMArrayValueImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMArrayValueImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.{Type, LLVMArrayValue} import vct.col.ast.ops.LLVMArrayValueOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMGetElementPointerImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMGetElementPointerImpl.scala index db235c727a..6442aa3654 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMGetElementPointerImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMGetElementPointerImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.{LLVMGetElementPointer, LLVMTPointer, Type} import vct.col.ast.ops.LLVMGetElementPointerOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMGlobalVariableImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMGlobalVariableImpl.scala index 30b77a7302..dc5dfd6275 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMGlobalVariableImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMGlobalVariableImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.LLVMGlobalVariable import vct.col.ast.ops.LLVMGlobalVariableOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMIntegerValueImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMIntegerValueImpl.scala index de19524d71..8713ca04a0 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMIntegerValueImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMIntegerValueImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.{Type, LLVMIntegerValue} import vct.col.ast.ops.LLVMIntegerValueOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMLoadImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMLoadImpl.scala index 18fc1f5b76..f82e50112a 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMLoadImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMLoadImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.{LLVMLoad, Type} import vct.col.ast.ops.LLVMLoadOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMMemoryAcquireImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMMemoryAcquireImpl.scala index df738623a8..aec8f004f3 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMMemoryAcquireImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMMemoryAcquireImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.LLVMMemoryAcquire import vct.col.ast.ops.LLVMMemoryAcquireOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMMemoryAcquireReleaseImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMMemoryAcquireReleaseImpl.scala index 786e2b442c..6080f98594 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMMemoryAcquireReleaseImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMMemoryAcquireReleaseImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.LLVMMemoryAcquireRelease import vct.col.ast.ops.LLVMMemoryAcquireReleaseOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMMemoryMonotonicImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMMemoryMonotonicImpl.scala index 51414e62e4..88a93ec4d6 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMMemoryMonotonicImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMMemoryMonotonicImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.LLVMMemoryMonotonic import vct.col.ast.ops.LLVMMemoryMonotonicOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMMemoryNotAtomicImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMMemoryNotAtomicImpl.scala index 1038b551ef..7ac6a77eb4 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMMemoryNotAtomicImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMMemoryNotAtomicImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.LLVMMemoryNotAtomic import vct.col.ast.ops.LLVMMemoryNotAtomicOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMMemoryOrderingImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMMemoryOrderingImpl.scala index 8730936c44..515f9be83f 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMMemoryOrderingImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMMemoryOrderingImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.LLVMMemoryOrdering import vct.col.ast.ops.LLVMMemoryOrderingFamilyOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMMemoryReleaseImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMMemoryReleaseImpl.scala index db4f5a44e4..6baf5533f7 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMMemoryReleaseImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMMemoryReleaseImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.LLVMMemoryRelease import vct.col.ast.ops.LLVMMemoryReleaseOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMMemorySequentiallyConsistentImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMMemorySequentiallyConsistentImpl.scala index 12c7e4c655..22381c5262 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMMemorySequentiallyConsistentImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMMemorySequentiallyConsistentImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.LLVMMemorySequentiallyConsistent import vct.col.ast.ops.LLVMMemorySequentiallyConsistentOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMMemoryUnorderedImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMMemoryUnorderedImpl.scala index 855d3c9ee5..b778c4295c 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMMemoryUnorderedImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMMemoryUnorderedImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.LLVMMemoryUnordered import vct.col.ast.ops.LLVMMemoryUnorderedOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMPointerValueImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMPointerValueImpl.scala index 8d1dc6f168..415d58f05b 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMPointerValueImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMPointerValueImpl.scala @@ -1,10 +1,15 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm -import vct.col.ast.{Type, LLVMPointerValue, LLVMTPointer} +import vct.col.ast.{LLVMGlobalVariable, LLVMPointerValue, LLVMTPointer, Type, HeapVariable} import vct.col.ast.ops.LLVMPointerValueOps import vct.col.print._ trait LLVMPointerValueImpl[G] extends LLVMPointerValueOps[G] { this: LLVMPointerValue[G] => - override lazy val t: Type[G] = LLVMTPointer(Some(value.decl.variableType)) + override lazy val t: Type[G] = { + value.decl match { + case LLVMGlobalVariable(variableType, _, _) => LLVMTPointer(Some(variableType)) + case v: HeapVariable[G] => LLVMTPointer(Some(v.t)) + } + } // override def layout(implicit ctx: Ctx): Doc = ??? } diff --git a/src/col/vct/col/ast/lang/llvm/LLVMRawArrayValueImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMRawArrayValueImpl.scala index e1bf1c9306..b310ce588c 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMRawArrayValueImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMRawArrayValueImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.{Type, LLVMRawArrayValue} import vct.col.ast.ops.LLVMRawArrayValueOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMRawVectorValueImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMRawVectorValueImpl.scala index c12d66a013..72a82ad346 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMRawVectorValueImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMRawVectorValueImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.{Type, LLVMRawVectorValue} import vct.col.ast.ops.LLVMRawVectorValueOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMSignExtendImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMSignExtendImpl.scala index 016f44d6d9..9294bb2466 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMSignExtendImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMSignExtendImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.{LLVMSignExtend, Type} import vct.col.ast.ops.LLVMSignExtendOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMStatementImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMStatementImpl.scala new file mode 100644 index 0000000000..5f8d9a1d4c --- /dev/null +++ b/src/col/vct/col/ast/lang/llvm/LLVMStatementImpl.scala @@ -0,0 +1,7 @@ +package vct.col.ast.lang.llvm + + +import vct.col.ast.LLVMStatement +trait LLVMStatementImpl[G] { this: LLVMStatement[G] => + +} diff --git a/src/col/vct/col/ast/lang/llvm/LLVMStoreImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMStoreImpl.scala index c661ed452a..3e803bdcfa 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMStoreImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMStoreImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.LLVMStore import vct.col.ast.ops.LLVMStoreOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMStructValueImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMStructValueImpl.scala index 5d19914140..77d18d9135 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMStructValueImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMStructValueImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.{LLVMStructValue, Type} import vct.col.ast.ops.LLVMStructValueOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMTArrayImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMTArrayImpl.scala index db50ecd024..471b355f84 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMTArrayImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMTArrayImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.LLVMTArray import vct.col.ast.ops.LLVMTArrayOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMTFunctionImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMTFunctionImpl.scala index 85b5951f9f..2776838c27 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMTFunctionImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMTFunctionImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.LLVMTFunction import vct.col.ast.ops.LLVMTFunctionOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMTIntImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMTIntImpl.scala index 580c5c414d..4f13f92ade 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMTIntImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMTIntImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.LLVMTInt import vct.col.ast.ops.LLVMTIntOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMTStructImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMTStructImpl.scala index b5634ecc98..d782fdd91b 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMTStructImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMTStructImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.LLVMTStruct import vct.col.ast.ops.LLVMTStructOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMTVectorImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMTVectorImpl.scala index 5c0617be93..2a1a85b661 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMTVectorImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMTVectorImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.LLVMTVector import vct.col.ast.ops.LLVMTVectorOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMTruncateImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMTruncateImpl.scala index 610e9780b9..0eef4cff6b 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMTruncateImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMTruncateImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.{LLVMTruncate, Type} import vct.col.ast.ops.LLVMTruncateOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMVectorValueImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMVectorValueImpl.scala index 8012c0ded0..a9db55c0b9 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMVectorValueImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMVectorValueImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.{Type, LLVMVectorValue} import vct.col.print._ diff --git a/src/col/vct/col/ast/lang/llvm/LLVMZeroExtendImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMZeroExtendImpl.scala index 9bcdc0fc55..686f7fc7e1 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMZeroExtendImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMZeroExtendImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.{LLVMZeroExtend, Type} import vct.col.ast.ops.LLVMZeroExtendOps diff --git a/src/col/vct/col/ast/lang/llvm/LLVMZeroedAggregateValueImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMZeroedAggregateValueImpl.scala index 8161633046..053cf691ed 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMZeroedAggregateValueImpl.scala +++ b/src/col/vct/col/ast/lang/llvm/LLVMZeroedAggregateValueImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.lang.llvm import vct.col.ast.{Type, LLVMZeroedAggregateValue} import vct.col.ast.ops.LLVMZeroedAggregateValueOps diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala index 83316253d6..0a88d521f7 100644 --- a/src/col/vct/col/typerules/CoercingRewriter.scala +++ b/src/col/vct/col/typerules/CoercingRewriter.scala @@ -1463,8 +1463,8 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite case glue: JavaBipGlue[Pre] => glue case LLVMLocal(name) => e case LLVMAllocA(allocationType, numElements) => e - case LLVMLoad(loadType, p, ordering) => LLVMLoad(loadType, p, ordering) - case LLVMGetElementPointer(structureType, resultType, pointer, indices) => e + case LLVMLoad(loadType, p, ordering) => LLVMLoad(loadType, llvmPointer(p, loadType)._1, ordering) + case LLVMGetElementPointer(structureType, resultType, pointer, indices) => LLVMGetElementPointer(structureType, resultType, llvmPointer(pointer, structureType)._1, indices) case LLVMSignExtend(inputType, outputType, value) => e case LLVMZeroExtend(inputType, outputType, value) => e case LLVMTruncate(inputType, outputType, value) => e @@ -1528,7 +1528,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite case l @ Lock(obj) => Lock(cls(obj))(l.blame) case Loop(init, cond, update, contract, body) => Loop(init, bool(cond), update, contract, body) case LLVMLoop(cond, contract, body) => LLVMLoop(bool(cond), contract, body) - case LLVMStore(value, p, ordering) => LLVMStore(value, p, ordering) + case LLVMStore(value, p, ordering) => LLVMStore(value, llvmPointer(p, value.t)._1, ordering) case ModelDo(model, perm, after, action, impl) => ModelDo(model, rat(perm), after, action, impl) case n @ Notify(obj) => Notify(cls(obj))(n.blame) case at @ ParAtomic(inv, content) => ParAtomic(inv, content)(at.blame) diff --git a/src/col/vct/col/typerules/CoercionUtils.scala b/src/col/vct/col/typerules/CoercionUtils.scala index 7d17879d19..3b3e4d22d2 100644 --- a/src/col/vct/col/typerules/CoercionUtils.scala +++ b/src/col/vct/col/typerules/CoercionUtils.scala @@ -6,6 +6,8 @@ import vct.col.origin.{DiagnosticOrigin, Origin} import vct.col.resolve.lang.{C, CPP} import vct.col.resolve.lang.CPP.getBaseTypeFromSpecs +import scala.annotation.tailrec + case object CoercionUtils { private implicit val o: Origin = DiagnosticOrigin @@ -200,6 +202,8 @@ case object CoercionUtils { case (LLVMTPointer(Some(leftInner)), LLVMTPointer(Some(rightInner))) => getAnyCoercion(leftInner, rightInner).getOrElse(return None) + + // Something with TVar? // Unsafe coercions @@ -299,11 +303,20 @@ case object CoercionUtils { case _ => None } + @tailrec + def firstElementIsType[G](aggregate: Type[G], innerType: Type[G]): Boolean = aggregate match { + case aggregate if getAnyCoercion(aggregate, innerType).isDefined => true + case LLVMTStruct(_, _, elements) => firstElementIsType(elements.head, innerType) + case LLVMTArray(numElements, elementType) => numElements > 0 && firstElementIsType(elementType, innerType) + case LLVMTVector(_, _) => false // TODO: Should this be possible? + case _ => false + } + def getAnyLLVMPointerCoercion[G](source: Type[G], innerType: Type[G]): Option[(Coercion[G], LLVMTPointer[G])] = source match { case LLVMTPointer(None) => Some((CoerceLLVMPointer(None, Some(innerType)), LLVMTPointer[G](Some(innerType)))) - case LLVMTPointer(Some(t)) if t == innerType => - Some((CoerceLLVMPointer(Some(t), Some(innerType)), LLVMTPointer[G](Some(innerType)))) + case LLVMTPointer(Some(t)) if firstElementIsType(t, innerType) => + Some(CoerceLLVMPointer(Some(t), Some(innerType)), LLVMTPointer[G](Some(innerType))) case _: TNull[G] => Some((CoerceLLVMPointer(None, Some(innerType)), LLVMTPointer[G](Some(innerType)))) case _ => None diff --git a/src/llvm/include/Passes/Function/FunctionBodyTransformer.h b/src/llvm/include/Passes/Function/FunctionBodyTransformer.h index 4c300bb368..83120722b7 100644 --- a/src/llvm/include/Passes/Function/FunctionBodyTransformer.h +++ b/src/llvm/include/Passes/Function/FunctionBodyTransformer.h @@ -70,7 +70,8 @@ class FunctionCursor { * @param llvmInstruction * @return the created variable declaration */ - col::Variable &declareVariable(Instruction &llvmInstruction); + col::Variable &declareVariable(Instruction &llvmInstruction, + Type *llvmPointerType = nullptr); /** * Functionality is twofold: @@ -82,8 +83,10 @@ class FunctionCursor { * @param colBlock * @return The created col assignment */ - col::Assign &createAssignmentAndDeclaration(Instruction &llvmInstruction, - col::Block &colBlock); + col::Assign & + createAssignmentAndDeclaration(Instruction &llvmInstruction, + col::Block &colBlock, + Type *llvmPointerType = nullptr); /** * Creates an assignment in the provided colBlock referencing the provided diff --git a/src/llvm/include/Transform/Transform.h b/src/llvm/include/Transform/Transform.h index ea10017d36..4506aa4a97 100644 --- a/src/llvm/include/Transform/Transform.h +++ b/src/llvm/include/Transform/Transform.h @@ -12,6 +12,8 @@ namespace llvm2col { namespace col = vct::col::ast; // type transformers +void transformAndSetPointerType(llvm::Type &llvmType, col::Type &colType); + void transformAndSetType(llvm::Type &llvmType, col::Type &colType); /** diff --git a/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp b/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp index 506687ef8d..215d9ae74e 100644 --- a/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp +++ b/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp @@ -103,13 +103,19 @@ FDResult &FunctionCursor::getFDResult(Function &otherLLVMFunction) { return FAM.getResult(otherLLVMFunction); } -col::Variable &FunctionCursor::declareVariable(Instruction &llvmInstruction) { +col::Variable &FunctionCursor::declareVariable(Instruction &llvmInstruction, + Type *llvmPointerType) { // create declaration in buffer col::Variable *varDecl = functionScope.add_locals(); // set type of declaration try { - llvm2col::transformAndSetType(*llvmInstruction.getType(), - *varDecl->mutable_t()); + if (llvmPointerType == nullptr) { + llvm2col::transformAndSetType(*llvmInstruction.getType(), + *varDecl->mutable_t()); + } else { + llvm2col::transformAndSetPointerType(*llvmPointerType, + *varDecl->mutable_t()); + } } catch (pallas::UnsupportedTypeException &e) { std::stringstream errorStream; errorStream << e.what() << " in variable declaration."; @@ -125,10 +131,9 @@ col::Variable &FunctionCursor::declareVariable(Instruction &llvmInstruction) { return *varDecl; } -col::Assign & -FunctionCursor::createAssignmentAndDeclaration(Instruction &llvmInstruction, - col::Block &colBlock) { - col::Variable &varDecl = declareVariable(llvmInstruction); +col::Assign &FunctionCursor::createAssignmentAndDeclaration( + Instruction &llvmInstruction, col::Block &colBlock, Type *llvmPointerType) { + col::Variable &varDecl = declareVariable(llvmInstruction, llvmPointerType); return createAssignment(llvmInstruction, colBlock, varDecl); } diff --git a/src/llvm/lib/Transform/Instruction/MemoryOpTransform.cpp b/src/llvm/lib/Transform/Instruction/MemoryOpTransform.cpp index 005f3b143f..a1f4916574 100644 --- a/src/llvm/lib/Transform/Instruction/MemoryOpTransform.cpp +++ b/src/llvm/lib/Transform/Instruction/MemoryOpTransform.cpp @@ -36,13 +36,14 @@ void llvm2col::transformMemoryOp(llvm::Instruction &llvmInstruction, void llvm2col::transformAllocA(llvm::AllocaInst &allocAInstruction, col::Block &colBlock, pallas::FunctionCursor &funcCursor) { - col::Assign &assignment = - funcCursor.createAssignmentAndDeclaration(allocAInstruction, colBlock); + col::Assign &assignment = funcCursor.createAssignmentAndDeclaration( + allocAInstruction, colBlock, + /* pointer type*/ allocAInstruction.getAllocatedType()); col::Expr *allocAExpr = assignment.mutable_value(); col::LlvmAllocA *allocA = allocAExpr->mutable_llvm_alloc_a(); allocA->set_allocated_origin( llvm2col::generateSingleStatementOrigin(allocAInstruction)); - llvm2col::transformAndSetType(*allocAInstruction.getType(), + llvm2col::transformAndSetType(*allocAInstruction.getAllocatedType(), *allocA->mutable_allocation_type()); llvm2col::transformAndSetExpr(funcCursor, allocAInstruction, *allocAInstruction.getArraySize(), diff --git a/src/llvm/lib/Transform/Transform.cpp b/src/llvm/lib/Transform/Transform.cpp index 27329d87e4..06b95c9861 100644 --- a/src/llvm/lib/Transform/Transform.cpp +++ b/src/llvm/lib/Transform/Transform.cpp @@ -15,6 +15,13 @@ const std::string SOURCE_LOC = "Transform::Transform"; namespace col = vct::col::ast; +void llvm2col::transformAndSetPointerType(llvm::Type &llvmType, + col::Type &colType) { + col::LlvmtPointer *pointerType = colType.mutable_llvmt_pointer(); + pointerType->set_allocated_origin(generateTypeOrigin(llvmType)); + llvm2col::transformAndSetType(llvmType, *pointerType->mutable_inner_type()); +} + void llvm2col::transformAndSetType(llvm::Type &llvmType, col::Type &colType) { switch (llvmType.getTypeID()) { case llvm::Type::IntegerTyID: diff --git a/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala b/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala index 7b2b0441df..a59198e0a9 100644 --- a/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala +++ b/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala @@ -353,6 +353,7 @@ case class ResolveExpressionSideEffects[Pre <: Generation]() extends Rewriter[Pr case _: CStatement[Pre] => throw ExtraNode case _: CPPStatement[Pre] => throw ExtraNode case _: JavaStatement[Pre] => throw ExtraNode + case _: LLVMStatement[Pre] => throw ExtraNode } } diff --git a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala index ba44d21ecd..e20274dc4f 100644 --- a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala @@ -3,12 +3,12 @@ package vct.rewrite.lang import com.typesafe.scalalogging.LazyLogging import vct.col.ast._ import vct.col.origin.Origin -import vct.col.ref.{LazyRef, Ref} +import vct.col.ref.{DirectRef, LazyRef, Ref} import vct.col.resolve.ctx.RefLLVMFunctionDefinition import vct.col.rewrite.{Generation, Rewritten} +import vct.col.util.AstBuildHelpers.tt import vct.col.util.{CurrentProgramContext, SuccessionMap} -import vct.result.VerificationError.SystemError -import vct.rewrite.lang.LangLLVMToCol.UnexpectedLLVMNode +import vct.result.VerificationError.{SystemError, UserError} case object LangLLVMToCol { case class UnexpectedLLVMNode(node: Node[_]) extends SystemError { @@ -18,14 +18,25 @@ case object LangLLVMToCol { .getOrElse(node.o) .messageInContext("VerCors assumes this node does not occur here in llvm input.") } + + case class NonConstantStructIndex(origin: Origin) extends UserError { + override def code: String = "nonConstantStructIndex" + + override def text: String = + origin.messageInContext(s"This struct indexing operation (getelementptr) uses a non-constant struct index which we do not support.") + } } case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends LazyLogging { + import LangLLVMToCol._ type Post = Rewritten[Pre] implicit val implicitRewriter: AbstractRewriter[Pre, Post] = rw private val llvmFunctionMap: SuccessionMap[LLVMFunctionDefinition[Pre], Procedure[Post]] = SuccessionMap() private val specFunctionMap: SuccessionMap[LLVMSpecFunction[Pre], Function[Post]] = SuccessionMap() + private val globalVariableMap: SuccessionMap[LLVMGlobalVariable[Pre], HeapVariable[Post]] = SuccessionMap() + private val structMap: SuccessionMap[LLVMTStruct[Pre], Class[Post]] = SuccessionMap() + private val structFieldMap: SuccessionMap[(LLVMTStruct[Pre], Int), InstanceField[Post]] = SuccessionMap() def rewriteLocal(local: LLVMLocal[Pre]): Expr[Post] = { @@ -122,6 +133,82 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends ) } + def rewriteStruct(t: LLVMTStruct[Pre]): Unit = { + val LLVMTStruct(name, packed, elements) = t + val newStruct = new Class[Post](rw.classDeclarations.collect { + elements.zipWithIndex.foreach { case (fieldType, idx) => + structFieldMap((t, idx)) = + new InstanceField(rw.dispatch(fieldType), flags = Nil)(fieldType.o) + rw.classDeclarations.declare(structFieldMap((t, idx))) + } + }._1, Seq(), tt[Post])(t.o) + + rw.globalDeclarations.declare(newStruct) + structMap(t) = newStruct + } + + def rewriteGlobalVariable(decl: LLVMGlobalVariable[Pre]): Unit = { + // TODO: Handle the initializer + // TODO: Include array and vector bounds somehow + decl.variableType match { + case struct: LLVMTStruct[Pre] => { + rewriteStruct(struct) + globalVariableMap.update(decl, rw.globalDeclarations.declare(new HeapVariable[Post](new TClass[Post](new DirectRef[Post, Class[Post]](structMap(struct)))(struct.o))(decl.o))) + } + case array: LLVMTArray[Pre] => { + globalVariableMap.update(decl, rw.globalDeclarations.declare(new HeapVariable[Post](new TArray[Post](rw.dispatch(array.elementType))(array.o))(decl.o))) + } + case vector: LLVMTVector[Pre] => { + globalVariableMap.update(decl, rw.globalDeclarations.declare(new HeapVariable[Post](new TArray[Post](rw.dispatch(vector.elementType))(vector.o))(decl.o))) + } + case _ => { + ??? + } + } + } + + def rewritePointerChain(pointer: Expr[Post], t: Type[Pre], indices: Seq[Expr[Pre]])(implicit o: Origin): Expr[Post] = { + if (indices.isEmpty) { + return pointer + } + t match { + case struct: LLVMTStruct[Pre] => { + indices.head match { + // TODO: This doesn't quite work because struct types are not uniqued + case value: LLVMIntegerValue[Pre] => + rewritePointerChain(Deref[Post](pointer, structFieldMap.ref((struct, value.value.intValue)))(o), struct.elements(value.value.intValue), indices.tail) + case _ => throw NonConstantStructIndex(o) + } + } + case array: LLVMTArray[Pre] => ??? + case vector: LLVMTVector[Pre] => ??? + } + } + + def rewriteGetElementPointer(gep: LLVMGetElementPointer[Pre]): Expr[Post] = { + implicit val o: Origin = gep.o + val t = gep.structureType + t match { + case struct: LLVMTStruct[Pre] => { + // TODO: We don't support variables in GEP yet and this just assumes all the indices are integer constants + // TODO: Use an actual Blame + + // Acquire the actual struct through a PointerAdd + // TODO: Can we somehow wrap the rw.dispatch(gep.pointer) to add the known type structureType? + val structPointer = DerefPointer(PointerAdd(rw.dispatch(gep.pointer), rw.dispatch(gep.indices.head))(o))(o) + + rewritePointerChain(structPointer, struct, gep.indices.tail) + } + case array: LLVMTArray[Pre] => ??? + case vector: LLVMTVector[Pre] => ??? + } + // Deref might not be the correct thing to use here since technically the pointer is only dereferenced in the load or store instruction + } + + def rewritePointerValue(pointer: LLVMPointerValue[Pre]): Expr[Post] = { + new LLVMPointerValue[Post](globalVariableMap.ref(pointer.value.decl.asInstanceOf[LLVMGlobalVariable[Pre]]))(pointer.o) + } + def result(ref: RefLLVMFunctionDefinition[Pre])(implicit o: Origin): Expr[Post] = Result[Post](llvmFunctionMap.ref(ref.decl)) diff --git a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala index 3746d2800d..44cdf4c158 100644 --- a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala @@ -123,6 +123,7 @@ case class LangSpecificToCol[Pre <: Generation](veymontGeneratePermissions: Bool case func: LLVMFunctionDefinition[Pre] => llvm.rewriteFunctionDef(func) case global: LLVMGlobalSpecification[Pre] => llvm.rewriteGlobal(global) + case global: LLVMGlobalVariable[Pre] => llvm.rewriteGlobalVariable(global) case cls: Class[Pre] => currentClass.having(cls) { @@ -267,6 +268,8 @@ case class LangSpecificToCol[Pre <: Generation](veymontGeneratePermissions: Bool case inv: LLVMAmbiguousFunctionInvocation[Pre] => llvm.rewriteAmbiguousFunctionInvocation(inv) case local: LLVMLocal[Pre] => llvm.rewriteLocal(local) case pointer: LLVMFunctionPointerValue[Pre] => llvm.rewriteFunctionPointer(pointer) + case pointer: LLVMPointerValue[Pre] => llvm.rewritePointerValue(pointer) + case gep: LLVMGetElementPointer[Pre] => llvm.rewriteGetElementPointer(gep) case other => rewriteDefault(other) }