WIP unique fields

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

@@ -140,6 +140,13 @@ final case class TConst[G](inner: Type[G])(
 final case class TUnique[G](inner: Type[G], unique: BigInt)(
   implicit val o: Origin = DiagnosticOrigin
 ) extends Type[G] with TUniqueImpl[G]
+final case class CTStructUnique[G](inner: Type[G], fieldRef: Ref[G, CStructMemberDeclarator[G]], unique: BigInt)(
+  implicit val o: Origin = DiagnosticOrigin
+) extends CType[G] with CTStructUniqueImpl[G]
+final case class TClassUnique[G](inner: Type[G], fieldRef: Ref[G, InstanceField[G]], unique: BigInt)(
+  implicit val o: Origin = DiagnosticOrigin
+) extends Type[G] with TClassUniqueImpl[G]
+
 
 sealed trait PointerType[G] extends Type[G] with PointerTypeImpl[G]
 final case class TPointer[G](element: Type[G])(
@@ -964,6 +971,14 @@ final case class CoerceBetweenUniquePointer[G](source: Type[G], target: Type[G])
   implicit val o: Origin
 ) extends Coercion[G] with CoerceBetweenUniquePointerImpl[G]
 
+final case class CoerceBetweenUniqueClass[G](source: Type[G], target: Type[G])(
+  implicit val o: Origin
+) extends Coercion[G] with CoerceBetweenUniqueClassImpl[G]
+final case class CoerceBetweenUniqueStruct[G](source: Type[G], target: Type[G])(
+  implicit val o: Origin
+) extends Coercion[G] with CoerceBetweenUniqueStructImpl[G]
+
+
 final case class CoerceToConst[G](source: Type[G])(
   implicit val o: Origin
 ) extends Coercion[G] with CoerceToConstImpl[G]
@@ -2631,6 +2646,10 @@ final case class CAtomic[G]()(implicit val o: Origin)
     extends CTypeQualifier[G] with CAtomicImpl[G]
 final case class CUnique[G](i: BigInt)(implicit val o: Origin)
   extends CTypeQualifier[G] with CUniqueImpl[G]
+final case class CUniquePointerField[G](name: String, i: BigInt)(implicit val o: Origin)
+  extends CTypeQualifier[G] with CUniquePointerFieldImpl[G] {
+  var ref: Option[RefCStructField[G]] = None
+}
 
 sealed trait CFunctionSpecifier[G]
     extends CDeclarationSpecifier[G] with CFunctionSpecifierImpl[G]

src/col/vct/col/ast/expr/heap/read/DerefImpl.scala

@@ -7,6 +7,9 @@ import vct.col.ast.{
   Expr,
   FieldLocation,
   TClass,
+  TClassUnique,
+  TPointer,
+  TUnique,
   Type,
   Value,
 }
@@ -17,8 +20,22 @@ import vct.col.ast.ops.DerefOps
 
 trait DerefImpl[G] extends ExprImpl[G] with DerefOps[G] {
   this: Deref[G] =>
-  override def t: Type[G] =
-    obj.t.asClass.map(_.instantiate(ref.decl.t)).getOrElse(ref.decl.t)
+  override def t: Type[G] = obj.t match {
+      case TClassUnique(inner, fieldRef, unique) if fieldRef.decl == ref.decl =>
+        addUniquePointer(inner, unique)
+      case t => getT(t)
+    }
+
+  def getT(classT: Type[G]): Type[G] = {
+    classT.asClass.map(_.instantiate(ref.decl.t)).getOrElse(ref.decl.t)
+  }
+
+  def addUniquePointer(inner: Type[G], unique: BigInt): Type[G] = {
+    getT(inner) match {
+      case TPointer(inner) => TPointer(TUnique(inner, unique))
+      case _ => ???
+    }
+  }
 
   override def check(context: CheckContext[G]): Seq[CheckError] =
     Check.inOrder(

src/col/vct/col/ast/unsorted/CTStructUniqueImpl.scala

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

src/col/vct/col/ast/unsorted/CUniquePointerFieldImpl.scala

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

src/col/vct/col/ast/unsorted/CoerceBetweenUniqueClassImpl.scala

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

src/col/vct/col/ast/unsorted/CoerceBetweenUniqueStructImpl.scala

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

src/col/vct/col/ast/unsorted/TClassUniqueImpl.scala

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

src/col/vct/col/resolve/ResolutionError.scala

@@ -17,6 +17,13 @@ case class MultipleForwardDeclarationContractError(
     )
 }
 
+case class NotSupportedStructUniqueField(use: Node[_])
+  extends ResolutionError {
+  override def text: String =
+    use.o.messageInContext(s"This use of unique_pointer_field is not supported")
+  override def code: String = "notSupportedStructUniqueField"
+}
+
 case class NoSuchNameError(kind: String, name: String, use: Node[_])
     extends ResolutionError {
   override def text: String =

src/col/vct/col/resolve/Resolve.scala

@@ -3,31 +3,16 @@ package vct.col.resolve
 import com.typesafe.scalalogging.LazyLogging
 import hre.data.BitString
 import hre.util.FuncTools
-import vct.col.ast._
+import vct.col.ast.{CUniquePointerField, _}
 import vct.col.ast.util.Declarator
 import vct.col.check.CheckError
 import vct.col.origin._
 import vct.col.resolve.ResolveReferences.scanScope
 import vct.col.ref.Ref
 import vct.col.resolve.ctx._
 import vct.col.resolve.lang.{C, CPP, Java, LLVM, PVL, Spec}
-import vct.col.resolve.Resolve.{
-  MalformedBipAnnotation,
-  SpecContractParser,
-  SpecExprParser,
-  getLit,
-  isBip,
-}
-import vct.col.resolve.lang.JavaAnnotationData.{
-  BipComponent,
-  BipData,
-  BipGuard,
-  BipInvariant,
-  BipPort,
-  BipPure,
-  BipStatePredicate,
-  BipTransition,
-}
+import vct.col.resolve.Resolve.{MalformedBipAnnotation, SpecContractParser, SpecExprParser, getLit, isBip}
+import vct.col.resolve.lang.JavaAnnotationData.{BipComponent, BipData, BipGuard, BipInvariant, BipPort, BipPure, BipStatePredicate, BipTransition}
 import vct.col.rewrite.InitialGeneration
 import vct.result.VerificationError.{Unreachable, UserError}
 
@@ -188,6 +173,16 @@ case object ResolveTypes {
       case _ => ctx
     }
 
+  def addUniquePointerFieldRef[G](specifiers: Seq[CDeclarationSpecifier[G]], ctx: TypeResolutionContext[G], blameNode: Node[G]): Unit = {
+    val pf: Seq[CUniquePointerField[G]] = specifiers.collect
+    { case CTypeQualifierDeclarationSpecifier(s: CUniquePointerField[G]) => s}
+    pf.foreach(f =>
+      f.ref = Some(C.getUniquePointerStructFieldRef(specifiers, ctx).getOrElse(
+        throw NotSupportedStructUniqueField(blameNode)
+      ))
+    )
+  }
+
   def resolveOne[G](node: Node[G], ctx: TypeResolutionContext[G]): Unit =
     node match {
       case javaClass @ JavaNamedType(genericNames) =>
@@ -206,6 +201,12 @@ case object ResolveTypes {
           C.findCStruct(name, ctx)
             .getOrElse(throw NoSuchNameError("struct", name, t))
         )
+      case d: CParam[G] => addUniquePointerFieldRef(d.specifiers, ctx, d)
+      case d: CStructMemberDeclarator[G] => addUniquePointerFieldRef(d.specs, ctx, d)
+      case d: CDeclaration[G] => addUniquePointerFieldRef(d.specs, ctx, d)
+      case d: CFunctionDefinition[G] => addUniquePointerFieldRef(d.specs, ctx, d)
+      case t: CPrimitiveType[G] => addUniquePointerFieldRef(t.specifiers, ctx, t)
+
       case t @ CPPTypedefName(nestedName, _) =>
         t.ref = Some(CPP.findCPPTypeName(nestedName, ctx).getOrElse(
           throw NoSuchNameError("class, struct, or namespace", nestedName, t)

src/col/vct/col/resolve/lang/C.scala

@@ -6,6 +6,7 @@ import vct.col.ast._
 import vct.col.ast.`type`.typeclass.TFloats.{C_ieee754_32bit, C_ieee754_64bit}
 import vct.col.ast.util.ExpressionEqualityCheck.isConstantInt
 import vct.col.origin._
+import vct.col.ref.Ref
 import vct.col.resolve._
 import vct.col.resolve.ctx._
 import vct.col.typerules.Types
@@ -71,6 +72,10 @@ case object C extends LazyLogging {
     q match {
       case CConst() => TConst(t)(q.o)
       case CUnique(i) => TUnique(t, i)(q.o)
+      case pf@CUniquePointerField(_, i) =>
+        val field: CStructMemberDeclarator[G] = pf.ref.get.decls
+        val fieldRef: Ref[G, CStructMemberDeclarator[G]] = field.ref
+        CTStructUnique(t, fieldRef, i)(q.o)
       case _ => throw CTypeNotSupported(Some(q))
     }
   }
@@ -166,18 +171,10 @@ case object C extends LazyLogging {
         case _ => throw CTypeNotSupported(context)
       }
 
-    val (typeSpecs, nonTypeSpecs) = specs.filter {
+    val (typeSpecs, qualifiers) = specs.filter {
       case _: CTypeSpecifier[G] | _: CTypeQualifierDeclarationSpecifier[G] => true ; case _ => false
     }.partition { case _: CTypeSpecifier[G] => true; case _ => false }
 
-    var unique: Option[BigInt] = None
-    var constant: Boolean = false
-    nonTypeSpecs.foreach({
-      case CTypeQualifierDeclarationSpecifier(CUnique(i)) if unique.isEmpty => unique = Some(i)
-      case CTypeQualifierDeclarationSpecifier(CConst()) => constant = true
-      case _ => throw CTypeNotSupported(context)
-    })
-
     val t: Type[G] =
       typeSpecs match {
         case Seq(CVoid()) => TVoid()
@@ -204,7 +201,7 @@ case object C extends LazyLogging {
       case Some(size) => CTVector(size, t)
     }
 
-    nonTypeSpecs.collect{ case CTypeQualifierDeclarationSpecifier(q) => q }
+    qualifiers.collect{ case CTypeQualifierDeclarationSpecifier(q) => q }
       .foldLeft(res)(qualify[G])
   }
 
@@ -294,12 +291,13 @@ case object C extends LazyLogging {
       case _ => None
     }
     case struct: CTStruct[G] => getCStructDeref(struct.ref.decl, name)
+    case struct: CTStructUnique[G] => findStruct(struct.inner, name)
   }
 
   def getCStructDeref[G](
       decl: CGlobalDeclaration[G],
       name: String,
-  ): Option[CDerefTarget[G]] =
+  ): Option[RefCStructField[G]] =
     decl.decl match {
       case CDeclaration(_, _, Seq(CStructDeclaration(_, decls)), Seq()) =>
         decls.flatMap(Referrable.from).collectFirst {
@@ -308,6 +306,28 @@ case object C extends LazyLogging {
       case _ => None
     }
 
+  def getUniquePointerStructFieldRef[G](
+      specs: Seq[CDeclarationSpecifier[G]],
+      ctx: TypeResolutionContext[G]
+  ): Option[RefCStructField[G]] = {
+    var pf: Option[CUniquePointerField[G]] = None
+    var struct: Option[CStructSpecifier[G]] = None
+    specs foreach {
+      case CTypeQualifierDeclarationSpecifier(s: CUniquePointerField[G]) =>
+        if(pf.isDefined) return None
+        pf = Some(s)
+      case s: CStructSpecifier[G] =>
+        if(struct.isDefined) return None
+        struct = Some(s)
+      case _ =>
+    }
+    if(pf.isEmpty || struct.isEmpty) return None
+
+    val structRef: RefCStruct[G] = C.findCStruct(struct.get.name, ctx)
+      .getOrElse(return None)
+    C.getCStructDeref(structRef.decl, pf.get.name)
+  }
+
   def openCLVectorAccessString[G](
       access: String,
       typeSize: BigInt,

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

@@ -278,6 +278,8 @@ abstract class CoercingRewriter[Pre <: Generation]()
       case CoerceFromUniquePointer(_, _) => e
       case CoerceToUniquePointer(_, _) => e
       case CoerceBetweenUniquePointer(_, _) => e
+      case CoerceBetweenUniqueStruct(_, _) => e
+      case CoerceBetweenUniqueClass(_, _) => e
 
       case CoerceSupports(_, _) => e
       case CoerceClassAnyClass(_, _) => e

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

@@ -194,6 +194,8 @@ case object CoercionUtils {
       case (TNull(), TArray(target)) => CoerceNullArray(target)
       case (TNull(), TClass(target, typeArgs)) =>
         CoerceNullClass(target, typeArgs)
+      case (TNull(), TClassUnique(TClass(target, typeArgs), _, _)) =>
+        CoerceNullClass(target, typeArgs)
       case (TNull(), JavaTClass(target, _)) => CoerceNullJavaClass(target)
       case (TNull(), TAnyClass()) => CoerceNullAnyClass()
       case (TNull(), target: PointerType[G]) => CoerceNullPointer(target)
@@ -291,10 +293,19 @@ case object CoercionUtils {
             supp.cls.decl == targetClass.decl
           } =>
         CoerceSupports(sourceClass, targetClass)
-
+      case (source @ TClass(_, _), target@TClassUnique(innerT @ TClass(_, _), _, _)) if innerT == source =>
+        CoerceBetweenUniqueClass(source, target)
+      case (source@TClassUnique(innerS @ TClass(_, _), _, _), target@ TClass(_, _)) if innerS == target =>
+        CoerceBetweenUniqueClass(source, target)
+      case (source@TClassUnique(innerS @ TClass(_, _), _, _), target@TClassUnique(innerT @ TClass(_, _), _, _))
+        if innerT == innerS =>
+        CoerceBetweenUniqueClass(source, target)
       case (source @ TClass(sourceClass, typeArgs), TAnyClass()) =>
         CoerceClassAnyClass(sourceClass, typeArgs)
 
+      case (source @ TClassUnique(TClass(sourceClass, typeArgs), _ ,_), TAnyClass()) =>
+        CoerceClassAnyClass(sourceClass, typeArgs)
+
       case (
             source @ JavaTClass(sourceClass, Nil),
             target @ JavaTClass(targetClass, Nil),
@@ -671,6 +682,7 @@ case object CoercionUtils {
       case t: TConst[G] =>
         getAnyClassCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)}
       case t: TClass[G] => Some((CoerceIdentity(source), t))
+      case t: TClassUnique[G] => getAnyClassCoercion(t.inner)
 
       case t: TUnion[G] =>
         val superType = Types.leastCommonSuperType(t.types)

src/parsers/antlr4/SpecLexer.g4

@@ -59,6 +59,7 @@ VAL_PURE: 'pure';
 VAL_THREAD_LOCAL: 'thread_local';
 VAL_BIP_ANNOTATION: 'bip_annotation';
 VAL_UNIQUE: 'unique';
+VAL_UNIQUE_POINTER_FIELD: 'unique_pointer_field';
 
 VAL_WITH: 'with';
 VAL_THEN: 'then';

src/parsers/antlr4/SpecParser.g4

@@ -421,6 +421,7 @@ valModifier
 
 valTypeQualifier
   : 'unique' '<' langConstInt '>' # valUnique
+  | 'unique_pointer_field' '<' langId ',' langConstInt '>' # valUniquePointerField
   ;
 
 valArgList

src/parsers/vct/parsers/transform/CToCol.scala

@@ -1188,15 +1188,16 @@ case class CToCol[G](
       case ValStatic(_) => collector.static += mod
     }
 
-  def convert(mod: ValEmbedTypeQualifierContext): CUnique[G] =
+  def convert(mod: ValEmbedTypeQualifierContext): CTypeQualifier[G] =
     mod match {
       case ValEmbedTypeQualifier0(_, mod, _) => convert(mod)
       case ValEmbedTypeQualifier1(mod) => convert(mod)
     }
 
-  def convert(implicit mod: ValTypeQualifierContext): CUnique[G] =
+  def convert(implicit mod: ValTypeQualifierContext): CTypeQualifier[G] =
     mod match {
       case ValUnique(_, _, uniqueId, _) => CUnique[G](convert(uniqueId))
+      case ValUniquePointerField(_, _, name, _, uniqueId, _) => CUniquePointerField[G](convert(name), convert(uniqueId))
     }
 
   def convertEmbedWith(