Add support for vectors and pointer coercions

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

@@ -428,6 +428,9 @@ final case class CoerceMapType[G](inner: Coercion[G], sourceBound: Type[G], targ
 final case class CoerceRatZFrac[G]()(implicit val o: Origin) extends Coercion[G] with CoerceRatZFracImpl[G]
 final case class CoerceZFracFrac[G]()(implicit val o: Origin) extends Coercion[G] with CoerceZFracFracImpl[G]
 
+final case class CoerceLLVMIntInt[G]()(implicit val o: Origin) extends Coercion[G] with CoerceLLVMIntIntImpl[G]
+final case class CoerceLLVMPointer[G](from: Option[Type[G]], to: Option[Type[G]])(implicit val o: Origin) extends Coercion[G] with CoerceLLVMPointerImpl[G]
+
 @family sealed trait Expr[G] extends NodeFamily[G] with ExprImpl[G]
 
 sealed trait Constant[G] extends Expr[G] with ConstantImpl[G]
@@ -1297,8 +1300,8 @@ final case class LLVMAllocA[G](allocationType: Type[G], numElements: Expr[G])
 final case class LLVMLoad[G](loadType: Type[G], pointer: Expr[G], ordering: LLVMMemoryOrdering[G])
                             (implicit val o: Origin) extends LLVMExpr[G] with LLVMLoadImpl[G]
 
-final case class LLVMStore[G](storeType: Type[G], pointer: Expr[G], ordering: LLVMMemoryOrdering[G])
-                             (implicit val o: Origin) extends LLVMExpr[G] with LLVMStoreImpl[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]
 
 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]
@@ -1328,20 +1331,23 @@ 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 LLVMFunctionPointerValue[G](value: Ref[G, LLVMFunctionDefinition[G]])(implicit val o: Origin) extends Constant[G] with LLVMExpr[G] with LLVMFunctionPointerValueImpl[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]
 final case class LLVMArrayValue[G](value: Seq[Expr[G]], arrayType: Type[G])(implicit val o: Origin) extends Constant[G] with LLVMExpr[G] with LLVMArrayValueImpl[G]
 final case class LLVMRawArrayValue[G](value: String, arrayType: Type[G])(implicit val o: Origin) extends Constant[G] with LLVMExpr[G] with LLVMRawArrayValueImpl[G]
+final case class LLVMVectorValue[G](value: Seq[Expr[G]], vectorType: Type[G])(implicit val o: Origin) extends Constant[G] with LLVMExpr[G] with LLVMVectorValueImpl[G]
+final case class LLVMRawVectorValue[G](value: String, vectorType: Type[G])(implicit val o: Origin) extends Constant[G] with LLVMExpr[G] with LLVMRawVectorValueImpl[G]
 final case class LLVMZeroedAggregateValue[G](aggregateType: Type[G])(implicit val o: Origin) extends Constant[G] with LLVMExpr[G] with LLVMZeroedAggregateValueImpl[G]
 
-final case class LLVMTInt[G](bitWidth: Int)(implicit val o: Origin = DiagnosticOrigin) extends Type[G] with LLVMTIntImpl[G]
+final case class LLVMTInt[G](bitWidth: Int)(implicit val o: Origin = DiagnosticOrigin) extends IntType[G] with LLVMTIntImpl[G]
 final case class LLVMTFunction[G]()(implicit val o: Origin = DiagnosticOrigin) extends Type[G] with LLVMTFunctionImpl[G]
 final case class LLVMTPointer[G](innerType: Option[Type[G]])(implicit val o: Origin = DiagnosticOrigin) extends Type[G] with LLVMTPointerImpl[G]
 final case class LLVMTMetadata[G]()(implicit val o: Origin = DiagnosticOrigin) extends Type[G] with LLVMTMetadataImpl[G]
 final case class LLVMTStruct[G](name: Option[String], packed: Boolean, elements: Seq[Type[G]])(implicit val o: Origin = DiagnosticOrigin) extends Type[G] with LLVMTStructImpl[G]
 final case class LLVMTArray[G](numElements: Long, elementType: Type[G])(implicit val o: Origin = DiagnosticOrigin) extends Type[G] with LLVMTArrayImpl[G]
+final case class LLVMTVector[G](numElements: Long, elementType: Type[G])(implicit val o: Origin = DiagnosticOrigin) extends Type[G] with LLVMTVectorImpl[G]
 
 sealed trait PVLType[G] extends Type[G] with PVLTypeImpl[G]
 final case class PVLNamedType[G](name: String, typeArgs: Seq[Type[G]])(implicit val o: Origin = DiagnosticOrigin) extends PVLType[G] with PVLNamedTypeImpl[G] {

src/col/vct/col/ast/expr/op/BinExprImpl.scala

@@ -1,7 +1,7 @@
 package vct.col.ast.expr.op
 
 import vct.col.ast.`type`.typeclass.TFloats.getFloatMax
-import vct.col.ast.{BinExpr, Expr, IntType, TBool, TCInt, TInt, TProcess, TRational, TString, Type}
+import vct.col.ast.{BinExpr, Expr, IntType, TBool, TCInt, LLVMTInt, TInt, TProcess, TRational, TString, Type}
 import vct.col.typerules.{CoercionUtils, Types}
 import vct.result.VerificationError
 
@@ -18,6 +18,11 @@ trait BinExprImpl[G] { this: BinExpr[G] =>
     CoercionUtils.getCoercion(left.t, TCInt()).isDefined &&
       CoercionUtils.getCoercion(right.t, TCInt()).isDefined
 
+  def isLLVMIntOp: Boolean = (left.t, right.t) match {
+    case (LLVMTInt(_), LLVMTInt(_)) => true
+    case _ => false
+  }
+
   def isIntOp: Boolean =
     CoercionUtils.getCoercion(left.t, TInt()).isDefined &&
       CoercionUtils.getCoercion(right.t, TInt()).isDefined
@@ -37,15 +42,17 @@ trait BinExprImpl[G] { this: BinExpr[G] =>
   def isSeqOp: Boolean = CoercionUtils.getAnySeqCoercion(left.t).isDefined
   def isSetOp: Boolean = CoercionUtils.getAnySetCoercion(left.t).isDefined
 
-  def getIntType: IntType[G] = if(isCIntOp) TCInt() else TInt()
+  def getIntType: IntType[G] = if(isCIntOp) TCInt() else
+                               if(isLLVMIntOp) Types.leastCommonSuperType(left.t, right.t).asInstanceOf[LLVMTInt[G]] else TInt()
 
 
   def getNumericType: Type[G] = {
     if (isCIntOp) TCInt[G]() else
+    if (isLLVMIntOp) Types.leastCommonSuperType(left.t, right.t) else
     if(isIntOp) TInt[G]() else
       getFloatMax[G](left.t, right.t) getOrElse (
         if(isRationalOp) TRational[G]()
         else throw NumericBinError()
       )
   }
-}
+}

src/col/vct/col/ast/family/coercion/CoerceLLVMIntIntImpl.scala

@@ -0,0 +1,8 @@
+package vct.col.ast.family.coercion
+
+import vct.col.ast.{CoerceLLVMIntInt, TInt}
+import vct.col.ast.ops.CoerceLLVMIntIntOps
+
+trait CoerceLLVMIntIntImpl[G] extends CoerceLLVMIntIntOps[G] { this: CoerceLLVMIntInt[G] =>
+  override def target: TInt[G] = TInt()
+}

src/col/vct/col/ast/family/coercion/CoerceLLVMPointerImpl.scala

@@ -0,0 +1,8 @@
+package vct.col.ast.family.coercion
+
+import vct.col.ast.{CoerceLLVMPointer, LLVMTPointer}
+import vct.col.ast.ops.CoerceLLVMPointerOps
+
+trait CoerceLLVMPointerImpl[G] extends CoerceLLVMPointerOps[G] { this: CoerceLLVMPointer[G] =>
+  override def target: LLVMTPointer[G] = LLVMTPointer(to)
+}

src/col/vct/col/ast/family/coercion/CoercionImpl.scala

@@ -79,5 +79,8 @@ trait CoercionImpl[G] extends CoercionFamilyOps[G] { this: Coercion[G] =>
     case CoerceCFloatFloat(_, _) => true
     case CoerceDecreasePrecision(_, _) => false
     case CoerceCFloatCInt(_) => false
+
+    case CoerceLLVMIntInt() => true
+    case CoerceLLVMPointer(_, _) => true
   }
-}
+}

src/col/vct/col/ast/lang/llvm/LLVMFunctionPointerValueImpl.scala

@@ -1,4 +1,4 @@
-package vct.col.ast.unsorted
+package vct.col.ast.lang.llvm
 
 import vct.col.ast.{Type, LLVMTPointer, LLVMFunctionPointerValue}
 import vct.col.ast.ops.LLVMFunctionPointerValueOps

src/col/vct/col/ast/lang/llvm/LLVMGetElementPointerImpl.scala

@@ -1,10 +1,10 @@
 package vct.col.ast.unsorted
 
-import vct.col.ast.{LLVMGetElementPointer, Type}
+import vct.col.ast.{LLVMGetElementPointer, LLVMTPointer, Type}
 import vct.col.ast.ops.LLVMGetElementPointerOps
 import vct.col.print._
 
 trait LLVMGetElementPointerImpl[G] extends LLVMGetElementPointerOps[G] { this: LLVMGetElementPointer[G] =>
-  override def t: Type[G] = resultType
+  override def t: Type[G] = LLVMTPointer(Some(resultType))
   // override def layout(implicit ctx: Ctx): Doc = ???
 }

src/col/vct/col/ast/lang/llvm/LLVMRawVectorValueImpl.scala

@@ -0,0 +1,10 @@
+package vct.col.ast.unsorted
+
+import vct.col.ast.{Type, LLVMRawVectorValue}
+import vct.col.ast.ops.LLVMRawVectorValueOps
+import vct.col.print._
+
+trait LLVMRawVectorValueImpl[G] extends LLVMRawVectorValueOps[G] { this: LLVMRawVectorValue[G] =>
+  override def t: Type[G] = vectorType
+  // override def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/llvm/LLVMStoreImpl.scala

@@ -1,8 +1,7 @@
 package vct.col.ast.unsorted
 
-import vct.col.ast.{LLVMStore, Type}
+import vct.col.ast.LLVMStore
 import vct.col.ast.ops.LLVMStoreOps
 
 trait LLVMStoreImpl[G] extends LLVMStoreOps[G] { this: LLVMStore[G] =>
-  override val t: Type[G] = this.storeType
 }

src/col/vct/col/ast/lang/llvm/LLVMTVectorImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.unsorted
+
+import vct.col.ast.LLVMTVector
+import vct.col.ast.ops.LLVMTVectorOps
+import vct.col.print._
+
+trait LLVMTVectorImpl[G] extends LLVMTVectorOps[G] { this: LLVMTVector[G] =>
+  // override def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/llvm/LLVMVectorValueImpl.scala

@@ -0,0 +1,10 @@
+package vct.col.ast.unsorted
+
+import vct.col.ast.{Type, LLVMVectorValue}
+import vct.col.print._
+import vct.col.ast.ops.LLVMVectorValueOps
+
+trait LLVMVectorValueImpl[G] extends LLVMVectorValueOps[G] { this: LLVMVectorValue[G] =>
+  override def t: Type[G] = vectorType
+  // override def layout(implicit ctx: Ctx): Doc = ???
+}

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

@@ -78,6 +78,7 @@ sealed trait Referrable[G] {
     case RefJavaBipGuard(decl) => Referrable.originName(decl)
     case RefLLVMFunctionDefinition(decl) => Referrable.originName(decl)
     case RefLLVMGlobalSpecification(decl) => Referrable.originName(decl)
+    case RefLLVMGlobalVariable(decl) => Referrable.originName(decl)
     case RefLLVMSpecFunction(decl) => Referrable.originName(decl)
     case RefBipComponent(decl) => Referrable.originName(decl)
     case RefBipGlue(decl) => ""
@@ -174,6 +175,7 @@ case object Referrable {
     case decl: LLVMFunctionDefinition[G] => RefLLVMFunctionDefinition(decl)
     case decl: LLVMGlobalSpecification[G] => RefLLVMGlobalSpecification(decl)
     case decl: LLVMSpecFunction[G] => RefLLVMSpecFunction(decl)
+    case decl: LLVMGlobalVariable[G] => RefLLVMGlobalVariable(decl)
     case decl: ProverType[G] => RefProverType(decl)
     case decl: ProverFunction[G] => RefProverFunction(decl)
     case decl: JavaBipGlueContainer[G] => RefJavaBipGlueContainer()
@@ -311,6 +313,7 @@ case class RefJavaBipGuard[G](decl: JavaMethod[G]) extends Referrable[G] with Ja
 case class RefJavaBipGlueContainer[G]() extends Referrable[G] // Bip glue jobs are not actually referrable
 case class RefLLVMFunctionDefinition[G](decl: LLVMFunctionDefinition[G]) extends Referrable[G] with LLVMInvocationTarget[G] with ResultTarget[G]
 case class RefLLVMGlobalSpecification[G](decl: LLVMGlobalSpecification[G]) extends Referrable[G]
+case class RefLLVMGlobalVariable[G](decl: LLVMGlobalVariable[G]) extends Referrable[G]
 case class RefBipComponent[G](decl: BipComponent[G]) extends Referrable[G]
 case class RefBipGlue[G](decl: BipGlue[G]) extends Referrable[G]
 case class RefBipGuard[G](decl: BipGuard[G]) extends Referrable[G]

src/col/vct/col/typerules/CoercingRewriter.scala

@@ -211,6 +211,9 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite
       case CoerceCIntCFloat(_) => e
       case CoerceCIntInt() => e
       case CoerceCFloatFloat(_, _) => e
+
+      case CoerceLLVMIntInt() => e
+      case CoerceLLVMPointer(_, _) => e
     }
   }
 
@@ -371,6 +374,11 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite
       case Some((coercion, t)) => (ApplyCoercion(e, coercion)(coercionOrigin(e)), t)
       case None => throw IncoercibleText(e, s"pointer")
     }
+  def llvmPointer(e: Expr[Pre], innerType: Type[Pre]): (Expr[Pre], LLVMTPointer[Pre]) =
+    CoercionUtils.getAnyLLVMPointerCoercion(e.t, innerType) match {
+      case Some((coercion, t)) => (ApplyCoercion(e, coercion)(coercionOrigin(e)), t)
+      case None => throw IncoercibleText(e, s"llvm pointer of $innerType")
+    }
   def matrix(e: Expr[Pre]): (Expr[Pre], TMatrix[Pre]) =
     CoercionUtils.getAnyMatrixCoercion(e.t) match {
       case Some((coercion, t)) => (ApplyCoercion(e, coercion)(coercionOrigin(e)), t)
@@ -1454,6 +1462,21 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite
       case localIncoming: BipLocalIncomingData[Pre] => localIncoming
       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 LLVMSignExtend(inputType, outputType, value) => e
+      case LLVMZeroExtend(inputType, outputType, value) => e
+      case LLVMTruncate(inputType, outputType, value) => e
+      case LLVMIntegerValue(value, integerType) => e
+      case LLVMPointerValue(value) => e
+      case LLVMFunctionPointerValue(value) => e
+      case LLVMStructValue(value, structType) => e
+      case LLVMArrayValue(value, arrayType) => e
+      case LLVMRawArrayValue(value, arrayType) => e
+      case LLVMVectorValue(value, vectorType) => e
+      case LLVMRawVectorValue(value, vectorType) => e
+      case LLVMZeroedAggregateValue(aggregateType) => e
     }
   }
 
@@ -1505,6 +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 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)
@@ -1702,6 +1726,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite
       case function: LLVMSpecFunction[Pre] =>
         new LLVMSpecFunction[Pre](function.name, function.returnType, function.args, function.typeArgs, function.body.map(coerce(_, function.returnType)), function.contract, function.inline, function.threadLocal)(function.blame)
       case glob: LLVMGlobalSpecification[Pre] => glob
+      case glob: LLVMGlobalVariable[Pre] => glob
       case endpoint: PVLEndpoint[Pre] => endpoint
       case seqProg: PVLSeqProg[Pre] => seqProg
       case seqRun: PVLSeqRun[Pre] => seqRun

src/col/vct/col/typerules/CoercionUtils.scala

@@ -67,6 +67,7 @@ case object CoercionUtils {
       case (TNull(), TAnyClass()) => CoerceNullAnyClass()
       case (TNull(), TPointer(target)) => CoerceNullPointer(target)
       case (TNull(), CTPointer(target)) => CoerceNullPointer(target)
+      case (TNull(), LLVMTPointer(target)) => CoerceLLVMPointer(None, target)
       case (TNull(), TEnum(target)) => CoerceNullEnum(target)
 
       case (CTArray(_, innerType), TArray(element)) if element == innerType =>
@@ -107,6 +108,7 @@ case object CoercionUtils {
         val coercedCFloat = TCFloat[G](exponentR, mantissaR)
         CoercionSequence(Seq(CoerceDecreasePrecision(source, coercedCFloat), CoerceCFloatFloat(coercedCFloat, target)))
       case (TCInt(), TInt()) => CoerceCIntInt()
+      case (LLVMTInt(_), TInt()) => CoerceLLVMIntInt()
 
       case (TBoundedInt(gte, lt), TFraction()) if gte >= 1 && lt <= 2 => CoerceBoundIntFrac()
       case (source @ TBoundedInt(gte, lt), TZFraction()) if gte >= 0 && lt <= 2 => CoerceBoundIntZFrac(source)
@@ -189,6 +191,14 @@ case object CoercionUtils {
           case None => return None
         }
 
+      case (LLVMTPointer(Some(innerType)), LLVMTPointer(None)) =>
+        CoerceLLVMPointer(Some(innerType), None)
+      case (LLVMTPointer(None), LLVMTPointer(Some(innerType))) =>
+        CoerceLLVMPointer(None, Some(innerType))
+      case (LLVMTPointer(Some(LLVMTArray(numElements, elementType))), LLVMTPointer(Some(innerType)))  if numElements > 0 =>
+        getAnyCoercion(elementType, innerType).getOrElse(return None)
+      case (LLVMTPointer(Some(leftInner)), LLVMTPointer(Some(rightInner))) =>
+        getAnyCoercion(leftInner, rightInner).getOrElse(return None)
 
       // Something with TVar?
 
@@ -281,12 +291,24 @@ case object CoercionUtils {
     case t: CTArray[G] => Some((CoerceCArrayPointer(t.innerType), TPointer(t.innerType)))
     case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyPointerCoercion)
     case t: CPPTArray[G] => Some((CoerceCPPArrayPointer(t.innerType), TPointer(t.innerType)))
+    case LLVMTPointer(None) => Some((CoerceIdentity(source), TPointer[G](TAnyValue())))
+    case LLVMTPointer(Some(innerType)) => Some((CoerceIdentity(source), TPointer(innerType)))
     case _: TNull[G] =>
       val t = TPointer[G](TAnyValue())
       Some((CoerceNullPointer(t), t))
     case _ => None
   }
 
+  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 _: TNull[G] =>
+        Some((CoerceLLVMPointer(None, Some(innerType)), LLVMTPointer[G](Some(innerType))))
+      case _ => None
+  }
+
   def getAnyCArrayCoercion[G](source: Type[G]): Option[(Coercion[G], CTArray[G])] = source match {
     case t: CPrimitiveType[G] => chainCCoercion(t, getAnyCArrayCoercion)
     case t: CTArray[G] => Some((CoerceIdentity(source), t))
@@ -425,4 +447,4 @@ case object CoercionUtils {
     case t: TSmtlibSeq[G] => Some((CoerceIdentity(source), t))
     case _ => None
   }
-}
+}

src/col/vct/col/typerules/Types.scala

@@ -79,6 +79,8 @@ object Types {
     case (TBoundedInt(leftGte, leftLt), TBoundedInt(rightGte, rightLt)) =>
       TBoundedInt(leftGte.min(rightGte), leftLt.max(rightLt))
 
+    case (LLVMTInt(leftWidth), LLVMTInt(rightWidth)) => LLVMTInt(leftWidth.max(rightWidth))
+
     // Unrelated types below rational are simply a rational
     case (left, right) if TRational().superTypeOf(left) && TRational().superTypeOf(right) =>
       TRational()
@@ -89,4 +91,4 @@ object Types {
     case (_, _) =>
       TAny()
   }
-}
+}

src/llvm/include/Origin/OriginProvider.h

@@ -53,6 +53,8 @@ col::Origin *generateVoidOperandOrigin(llvm::Instruction &llvmInstruction);
 
 col::Origin *generateTypeOrigin(llvm::Type &llvmType);
 
+col::Origin *generateMemoryOrderingOrigin(llvm::AtomicOrdering &llvmOrdering);
+
 std::string extractShortPosition(const col::Origin &origin);
 
 col::Origin *deepenOperandOrigin(const col::Origin &origin,

src/llvm/include/Origin/PreferredNameDeriver.h

@@ -2,6 +2,7 @@
 #define PALLAS_PREFERREDNAMEDERIVER_H
 
 #include <llvm/IR/Value.h>
+#include <llvm/Support/AtomicOrdering.h>
 /**
  * Generators for VerCors origin objects preferredName fields for various LLVM
  * Value types.
@@ -14,6 +15,9 @@ std::string deriveOperandPreferredName(llvm::Value &llvmOperand);
 
 std::string deriveTypePreferredName(llvm::Type &llvmType);
 
+std::string
+deriveMemoryOrderingPreferredName(llvm::AtomicOrdering &llvmOrdering);
+
 std::string deriveArgumentPreferredName(llvm::Argument &llvmArgument);
 } // namespace llvm2col
 #endif // PALLAS_PREFERREDNAMEDERIVER_H

src/llvm/include/Passes/Function/FunctionBodyTransformer.h

@@ -97,7 +97,7 @@ class FunctionCursor {
     col::Assign &createAssignment(Instruction &llvmInstruction,
                                   col::Block &colBlock, col::Variable &varDecl);
 
-    col::Variable &getVariableMapEntry(llvm::Value &llvmValue);
+    col::Variable &getVariableMapEntry(llvm::Value &llvmValue, bool inPhiNode);
 
     /**
      * In many cases during transformation, it is not possible to derive whether