First version working for function parameters

Author: sakehl

examples/concepts/unique/arrays.c

@@ -5,7 +5,7 @@
   context_everywhere x2 != NULL ** \pointer_length(x2) == n ** (\forall* int i; 0<=i && i<n; Perm(&x2[i], 1\2));
   ensures (\forall int i; 0<=i && i<n; x0[i] == x1[i] + x2[i] );
 @*/
-int main(int n, /*@ unique<1> @*/ int* x0, /*@ unique<1> @*/ /*@ unique<2> @*/ int* x1, /*@ unique<2> @*/ int* x2){
+int main(int n, /*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1, /*@ unique<2> @*/ int* x2){
   /*@
     loop_invariant 0 <= j && j <= n;
     loop_invariant (\forall int i; 0<=i && i<j; x0[i] == x1[i] + x2[i] );

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

@@ -128,15 +128,20 @@ final case class TUnion[G](types: Seq[Type[G]])(
 final case class TArray[G](element: Type[G])(
     implicit val o: Origin = DiagnosticOrigin
 ) extends Type[G] with TArrayImpl[G]
-final case class TPointer[G](element: Type[G])(
-    implicit val o: Origin = DiagnosticOrigin
-) extends Type[G] with TPointerImpl[G]
 final case class TType[G](t: Type[G])(implicit val o: Origin = DiagnosticOrigin)
     extends Type[G] with TTypeImpl[G]
 final case class TVar[G](ref: Ref[G, Variable[G]])(
     implicit val o: Origin = DiagnosticOrigin
 ) extends Type[G] with TVarImpl[G]
 
+sealed trait PointerType[G] extends Type[G] with PointerTypeImpl[G]
+final case class TPointer[G](element: Type[G])(
+  implicit val o: Origin = DiagnosticOrigin
+) extends PointerType[G] with TPointerImpl[G]
+final case class TUniquePointer[G](element: Type[G], id: BigInt)(
+  implicit val o: Origin = DiagnosticOrigin
+) extends PointerType[G] with TUniquePointerImpl[G]
+
 sealed trait CompositeType[G] extends Type[G] with CompositeTypeImpl[G]
 sealed trait SizedType[G] extends CompositeType[G] with SizedTypeImpl[G]
 final case class TSeq[G](element: Type[G])(

src/col/vct/col/ast/type/PointerTypeImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.`type`
+
+import vct.col.ast.{PointerType, Type}
+
+trait PointerTypeImpl[G] {
+  this: PointerType[G] =>
+
+  val element: Type[G]
+}

src/col/vct/col/ast/type/TUniquePointerImpl.scala

@@ -0,0 +1,16 @@
+package vct.col.ast.`type`
+
+import vct.col.ast.TUniquePointer
+import vct.col.ast.ops.TUniquePointerOps
+import vct.col.print._
+
+trait TUniquePointerImpl[G] extends TUniquePointerOps[G] {
+  this: TUniquePointer[G] =>
+  override def layoutSplitDeclarator(implicit ctx: Ctx): (Doc, Doc) = {
+    val (spec, decl) = element.layoutSplitDeclarator
+    (spec, decl <> "*")
+  }
+
+  override def layout(implicit ctx: Ctx): Doc =
+    Group(Text("unique_pointer") <> open <> element <> "," <> id.toString <> close)
+}

src/col/vct/col/ast/type/typeclass/TypeImpl.scala

@@ -21,7 +21,7 @@ trait TypeImpl[G] extends TypeFamilyOps[G] {
   def asVector: Option[TVector[G]] =
     CoercionUtils.getAnyVectorCoercion(this).map(_._2)
   def asBag: Option[TBag[G]] = CoercionUtils.getAnyBagCoercion(this).map(_._2)
-  def asPointer: Option[TPointer[G]] =
+  def asPointer: Option[PointerType[G]] =
     CoercionUtils.getAnyPointerCoercion(this).map(_._2)
   def asArray: Option[TArray[G]] =
     CoercionUtils.getAnyArrayCoercion(this).map(_._2)

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

@@ -538,7 +538,7 @@ abstract class CoercingRewriter[Pre <: Generation]()
         (ApplyCoercion(e, coercion)(coercionOrigin(e)), t)
       case None => throw IncoercibleText(e, s"two-dimensional array")
     }
-  def pointer(e: Expr[Pre]): (Expr[Pre], TPointer[Pre]) =
+  def pointer(e: Expr[Pre]): (Expr[Pre], PointerType[Pre]) =
     CoercionUtils.getAnyPointerCoercion(e.t) match {
       case Some((coercion, t)) =>
         (ApplyCoercion(e, coercion)(coercionOrigin(e)), t)
@@ -2145,14 +2145,7 @@ abstract class CoercingRewriter[Pre <: Generation]()
     implicit val o: Origin = stat.o
     stat match {
       case a @ Assert(assn) => Assert(res(assn))(a.blame)
-      case a @ Assign(target, value) =>
-        try {
-          Assign(target, coerce(value, target.t, canCDemote = true))(a.blame)
-        } catch {
-          case err: Incoercible =>
-            println(err.text)
-            throw err
-        }
+      case a @ Assign(target, value) => Assign(target, coerce(value, target.t, canCDemote = true))(a.blame)
       case Assume(assn) => Assume(bool(assn))
       case Block(statements) => Block(statements)
       case Branch(branches) =>

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

@@ -122,6 +122,7 @@ case object CoercionUtils {
       case (TNull(), JavaTClass(target, _)) => CoerceNullJavaClass(target)
       case (TNull(), TAnyClass()) => CoerceNullAnyClass()
       case (TNull(), TPointer(target)) => CoerceNullPointer(target)
+      case (TNull(), TUniquePointer(target, id)) => CoerceNullPointer(target)
       case (TNull(), CTPointer(target)) => CoerceNullPointer(target)
       case (TNull(), TEnum(target)) => CoerceNullEnum(target)
 
@@ -425,10 +426,11 @@ case object CoercionUtils {
 
   def getAnyPointerCoercion[G](
       source: Type[G]
-  ): Option[(Coercion[G], TPointer[G])] =
+  ): Option[(Coercion[G], PointerType[G])] =
     source match {
       case t: CPrimitiveType[G] => chainCCoercion(t, getAnyPointerCoercion)
       case t: TPointer[G] => Some((CoerceIdentity(source), t))
+      case t: TUniquePointer[G] => Some((CoerceIdentity(source), t))
       case t: CTPointer[G] =>
         Some((CoerceIdentity(source), TPointer(t.innerType)))
       case t: CTArray[G] =>

src/rewrite/vct/rewrite/adt/ImportPointer.scala

@@ -10,8 +10,8 @@ import vct.col.util.AstBuildHelpers.{ExprBuildHelpers, const}
 import scala.collection.mutable
 
 case object ImportPointer extends ImportADTBuilder("pointer") {
-  private def PointerField(t: Type[_]): Origin =
-    Origin(Seq(PreferredName(Seq(typeText(t))), LabelContext("pointer field")))
+  private def PointerField(t: Type[_], uniqueId: Option[BigInt]): Origin =
+    Origin(Seq(PreferredName(Seq(typeText(t) + uniqueId.map(_.toString).getOrElse(""))), LabelContext("pointer field")))
 
   case class PointerNullOptNone(inner: Blame[PointerNull], expr: Expr[_])
       extends Blame[OptionNone] {
@@ -75,14 +75,18 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter)
   private lazy val pointerDeref = find[Function[Post]](pointerFile, "ptr_deref")
   private lazy val pointerAdd = find[Function[Post]](pointerFile, "ptr_add")
 
-  val pointerField: mutable.Map[Type[Post], SilverField[Post]] = mutable.Map()
+  val pointerField: mutable.Map[(Type[Post], Option[BigInt]), SilverField[Post]] = mutable.Map()
 
   private def getPointerField(ptr: Expr[Pre]): Ref[Post, SilverField[Post]] = {
-    val tElement = dispatch(ptr.t.asPointer.get.element)
+    val (tElementPre: Type[Pre], uniqueID) = ptr.t.asPointer.get match {
+      case TUniquePointer(e, i) => (e, Some(i))
+      case TPointer(e) => (e, None)
+    }
+    val tElement = dispatch(tElementPre)
     pointerField.getOrElseUpdate(
-      tElement, {
+      (tElement, uniqueID), {
         globalDeclarations
-          .declare(new SilverField(tElement)(PointerField(tElement)))
+          .declare(new SilverField(tElement)(PointerField(tElement, uniqueID)))
       },
     ).ref
   }
@@ -98,6 +102,7 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter)
   override def postCoerce(t: Type[Pre]): Type[Post] =
     t match {
       case TPointer(_) => TOption(TAxiomatic(pointerAdt.ref, Nil))
+      case TUniquePointer(_, _) => TOption(TAxiomatic(pointerAdt.ref, Nil))
       case other => rewriteDefault(other)
     }
 

src/rewrite/vct/rewrite/lang/LangCToCol.scala

@@ -30,12 +30,6 @@ case object LangCToCol {
       example.o.messageInContext("Global variables in C are not supported.")
   }
 
-  case class CDeclarationSpecifierNotSupported(spec: CDeclarationSpecifier[_]) extends UserError {
-    override def code: String = "notSupportedTypeDecl"
-    override def text: String =
-      spec.o.messageInContext("This decleration specifier is not supported.")
-  }
-
   case class MultipleSharedMemoryDeclaration(decl: Node[_]) extends UserError {
     override def code: String = "multipleSharedMemoryDeclaration"
     override def text: String =
@@ -60,7 +54,7 @@ case object LangCToCol {
       )
   }
 
-  case class WrongCType(decl: CLocalDeclaration[_]) extends UserError {
+  case class WrongCType(decl: Declaration[_]) extends UserError {
     override def code: String = "wrongCType"
     override def text: String =
       decl.o
@@ -445,7 +439,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
     implicit val o: Origin = cParam.o
     val varO = o.sourceName(C.getDeclaratorInfo(cParam.declarator).name)
     val cRef = RefCParam(cParam)
-    val tp = new TypeProperties(cParam.specifiers, cParam.declarator)
+    val tp = new TypeProperties(cParam.specifiers, cParam)
 
     kernelSpecifier match {
       case OpenCLKernel() =>
@@ -486,10 +480,11 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
       case GPULocal() => throw WrongGPUType(cParam)
       case GPUGlobal() => throw WrongGPUType(cParam)
     }
-    val specType =
-      cParam.specifiers.collectFirst { case t: CSpecificationType[Pre] =>
-        rw.dispatch(t.t)
-      }.get
+    val prop = new TypeProperties(cParam.specifiers, cParam)
+    if(!prop.validCParam) throw WrongCType(cParam)
+    val specType = if(prop.unique.isEmpty)
+      rw.dispatch(prop.mainType.get) else
+      TUniquePointer(rw.dispatch(prop.innerType.get), prop.unique.get)(cParam.o)
 
     cParam.drop()
     val v =
@@ -635,6 +630,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
     t match {
       case TArray(element) => element
       case TPointer(element) => element
+      case TUniquePointer(element, _) => element
       case _ => throw Unreachable("Already checked on pointer or array type")
     }
 
@@ -857,8 +853,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
   }
 
   class TypeProperties(
-      specs: Seq[CDeclarationSpecifier[Pre]],
-      decl: CDeclarator[Pre],
+      specs: Seq[CDeclarationSpecifier[Pre]], decl: Declaration[Pre]
   ) {
     var arrayOrPointer = false
     var global = false
@@ -892,15 +887,22 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
       case CSpecificationType(t) =>
         mainType = Some(t)
       case CExtern() => extern = true
+      case CUnique(i) if unique.isDefined => throw WrongCType(decl)
       case CUnique(i) => unique = Some(i)
       case CPure() => pure = true
       case CInline() => inline = true
       case CStatic() => static = true
-      case _ =>
+      // We want to make sure we process everything
+      case _ => ???
     }
 
     def isShared: Boolean = shared && !global
     def isGlobal: Boolean = !shared && global
+    def validNonGpu: Boolean = !global && !shared &&
+      (unique.isEmpty || (unique.isDefined && arrayOrPointer)) && mainType.isDefined
+    def validReturn: Boolean = validNonGpu && !static
+    def validCParam: Boolean = !pure && !inline && validNonGpu && !static
+    def validCLocal = validCParam
   }
 
   def addDynamicShared(
@@ -940,7 +942,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
     if (decl.decl.inits.size != 1)
       throw MultipleSharedMemoryDeclaration(decl)
 
-    val prop = new TypeProperties(decl.decl.specs, decl.decl.inits.head.decl)
+    val prop = new TypeProperties(decl.decl.specs, decl)
     if (!prop.shared)
       return false
     val init: CInit[Pre] = decl.decl.inits.head
@@ -1266,9 +1268,11 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
 
   def isPointer(t: Type[Pre]): Boolean = getPointer(t).isDefined
 
-  def getPointer(t: Type[Pre]): Option[TPointer[Pre]] =
+  def getPointer(t: Type[Pre]): Option[Type[Pre]] =
     getBaseType(t) match {
       case t @ TPointer(_) => Some(t)
+      case t @ TUniquePointer(_, _) => Some(t)
+      case t @ CTPointer(_) => Some(t)
       case _ => None
     }
 

test/main/vct/test/integration/examples/UniqueFieldsSpec.scala

@@ -5,5 +5,8 @@ import vct.test.integration.helper.VercorsSpec
 class UniqueFieldsSpec extends VercorsSpec {
   vercors should verify using silicon example "concepts/unique/arrays.c"
 
-  vercors should error withCode "???" in """int main(/*@ unique<1> @*/ /*@ unique<2> @*/ int* x0){}"""
+  vercors should error withCode "wrongCType" in "multiple uniques" c """int main(/*@ unique<1> @*/ /*@ unique<2> @*/ int* x0){}"""
+  vercors should error withCode "resolutionError:type" in "different uniques local" c """int main(/*@ unique<1> @*/ int* x0){ int* x1 = x0;}"""
+  vercors should error withCode "resolutionError:type" in "multiple uniques parameter" c """int main(/*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1){x1 = x0;}"""
+  vercors should verify using silicon in "same uniques parameter" c """int main(/*@ unique<1> @*/ int* x0, /*@ unique<1> @*/ int* x1){x1 = x0;}"""
 }