simpler pointer coercions

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

@@ -954,13 +954,13 @@ final case class CoerceFromUnique[G](target: Type[G], sourceId: BigInt)(
   implicit val o: Origin
 ) extends Coercion[G] with CoerceFromUniqueImpl[G]
 
-final case class CoerceToUniquePointer[G](inner: Type[G], targetId: BigInt)(
+final case class CoerceToUniquePointer[G](source: Type[G], target: Type[G])(
   implicit val o: Origin
 ) extends Coercion[G] with CoerceToUniquePointerImpl[G]
-final case class CoerceFromUniquePointer[G](target: Type[G], sourceId: BigInt)(
+final case class CoerceFromUniquePointer[G](source: Type[G], target: Type[G])(
   implicit val o: Origin
 ) extends Coercion[G] with CoerceFromUniquePointerImpl[G]
-final case class CoerceBetweenUniquePointer[G](target: Type[G], sourceId: BigInt, targetId: BigInt)(
+final case class CoerceBetweenUniquePointer[G](source: Type[G], target: Type[G])(
   implicit val o: Origin
 ) extends Coercion[G] with CoerceBetweenUniquePointerImpl[G]
 

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

@@ -5,5 +5,5 @@ import vct.col.ast.ops.CoerceBetweenUniquePointerOps
 import vct.col.print._
 
 trait CoerceBetweenUniquePointerImpl[G] extends CoerceBetweenUniquePointerOps[G] { this: CoerceBetweenUniquePointer[G] =>
-  // override def layout(implicit ctx: Ctx): Doc = ???
+
 }

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

@@ -5,5 +5,5 @@ import vct.col.ast.ops.CoerceFromUniquePointerOps
 import vct.col.print._
 
 trait CoerceFromUniquePointerImpl[G] extends CoerceFromUniquePointerOps[G] { this: CoerceFromUniquePointer[G] =>
-  // override def layout(implicit ctx: Ctx): Doc = ???
+
 }

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

@@ -5,6 +5,5 @@ import vct.col.ast.ops.CoerceToUniquePointerOps
 import vct.col.print._
 
 trait CoerceToUniquePointerImpl[G] extends CoerceToUniquePointerOps[G] { this: CoerceToUniquePointer[G] =>
-  // override def layout(implicit ctx: Ctx): Doc = ???
-  override def target: Type[G] = TUniquePointer(inner, targetId)
+
 }

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

@@ -276,7 +276,7 @@ abstract class CoercingRewriter[Pre <: Generation]()
 
       case CoerceFromUniquePointer(_, _) => e
       case CoerceToUniquePointer(_, _) => e
-      case CoerceBetweenUniquePointer(_, _, _) => e
+      case CoerceBetweenUniquePointer(_, _) => e
 
       case CoerceSupports(_, _) => e
       case CoerceClassAnyClass(_, _) => e

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

@@ -13,6 +13,19 @@ case object CoercionUtils {
   def getCoercion[G](source: Type[G], target: Type[G]): Option[Coercion[G]] =
     getAnyCoercion(source, target).filter(_.isCPromoting)
 
+  def getPointerCoercion[G](source: Type[G], target: Type[G], innerSource: Type[G], innerTarget: Type[G]) : Option[Coercion[G]] = {
+    Some((innerSource, innerTarget) match {
+      case (i,l) if i == l => CoerceIdentity(source)
+      case (TUnique(l, lId), TUnique(r, rId)) =>
+        if(l == r) CoerceBetweenUniquePointer(source, target) else return None
+      case (TUnique(l, lId), r) =>
+        if(l == r) CoerceFromUniquePointer(source, target) else return None
+      case (TUnique(l, lId), r) =>
+        if(l == r) CoerceToUniquePointer(source, target) else return None
+      case _ => return None
+    })
+  }
+
   def getAnyCoercion[G](
       source: Type[G],
       target: Type[G],
@@ -183,37 +196,20 @@ case object CoercionUtils {
       case (source @ TOpenCLVector(lSize, innerType), TVector(rSize, element))
           if element == innerType && lSize == rSize =>
         CoerceCVectorVector(rSize, element)
-      case (
-            CTPointer(innerType),
-            TPointer(element),
-          ) => // if element == innerType =>
-        getAnyCoercion(element, innerType).getOrElse(return None)
-      case (
-            TPointer(element),
-            CTPointer(innerType),
-          ) => // if element == innerType =>
-        getAnyCoercion(element, innerType).getOrElse(return None)
-      case (
-        TPointer(innerType),
-        t@TPointer(TUnique(element, unique)),
-        ) if element == innerType =>
-        ??? //CoerceToUnique()
-      case (
-        TPointer(TUnique(element, unique)),
-        t@TPointer(innerType)
-        ) if element == innerType =>
-        CoerceFromUniquePointer(t, unique)
-      case (
-        TPointer(TUnique(elementS, uniqueS)),
-        t@TPointer(TUnique(elementT, uniqueT))
-        ) if elementS == elementT =>
-        CoerceBetweenUniquePointer(t, uniqueS, uniqueT)
-      case (CTArray(_, innerType), CTPointer(element)) =>
+      case (s@CTPointer(innerLeft), t@CTPointer(innerRight)) =>
+        getPointerCoercion(s, t, innerLeft, innerRight).getOrElse(return None)
+      case (s@TPointer(innerLeft), t@TPointer(innerRight)) =>
+        getPointerCoercion(s, t, innerLeft, innerRight).getOrElse(return None)
+      case (s@CTPointer(innerLeft), t@TPointer(innerRight)) =>
+        getPointerCoercion(s, t, innerLeft, innerRight).getOrElse(return None)
+      case (s@TPointer(innerLeft), t@CTPointer(innerRight)) =>
+        getPointerCoercion(s, t, innerLeft, innerRight).getOrElse(return None)
+      case (CTArray(_, innerType), t@CTPointer(element)) =>
         if (element == innerType) { CoerceCArrayPointer(innerType) }
         else {
           CoercionSequence(Seq(
             CoerceCArrayPointer(element),
-            getAnyCoercion(element, innerType).getOrElse(return None),
+            getPointerCoercion(CTPointer(innerType), t, innerType, element).getOrElse(return None)
           ))
         }
       case (TFraction(), TZFraction()) => CoerceFracZFrac()

src/rewrite/vct/rewrite/TypeQualifierCoercion.scala

@@ -20,12 +20,18 @@ case class DisallowedQualifiedType(target: Node[_]) extends UserError {
     target.o.messageInContext("This qualified type is not allowed.")
 }
 
-case class DisallowedQualifiedCoercion(calledOrigin: Origin) extends UserError {
-  override def code: String = "disallowedQualifiedCoercion"
+case class DisallowedQualifiedMethodCoercion(calledOrigin: Origin) extends UserError {
+  override def code: String = "disallowedQualifiedMethodCoercion"
   override def text: String =
     calledOrigin.messageInContext("The coercion of args with qualifiers for this method call is not allowed.")
 }
 
+case class DisallowedQualifiedCoercion(calledOrigin: Origin, source: Type[_], target: Type [_]) extends UserError {
+  override def code: String = "disallowedQualifiedCoercion"
+  override def text: String =
+    calledOrigin.messageInContext(s"The coercion of $source to $target is not allowed.")
+}
+
 case object TypeQualifierCoercion extends RewriterBuilder {
   override def key: String = "TypeQualifierCoercion"
   override def desc: String =
@@ -43,12 +49,6 @@ case class TypeQualifierCoercion[Pre <: Generation]()
 
   def getCopyType(t: Type[Pre]): Option[Type[Post]] = methodCopyTypes.topOption.flatMap(m => m.get(t))
 
-  def uniquePointerType(t: Type[Pre], unique: BigInt) = t match {
-    case TPointer(TUnique(it, _)) => TPointer(TUnique(it, unique))
-    case TPointer(it) => TPointer(TUnique(it, unique))
-    case _ => ???
-  }
-
   override def applyCoercion(e: => Expr[Post], coercion: Coercion[Pre])(
     implicit o: Origin
   ): Expr[Post] = {
@@ -58,8 +58,9 @@ case class TypeQualifierCoercion[Pre <: Generation]()
       case CoerceToUnique(_, _) =>
       case CoerceFromUnique(_, _) =>
       case CoerceBetweenUnique(_, _, _) =>
-      case CoerceFromUniquePointer(target, sourceId) => ???
-      case CoerceBetweenUniquePointer(t, sourceId, targetId) => ???
+      case CoerceToUniquePointer(s, t) => throw DisallowedQualifiedCoercion(e.o, s, t)
+      case CoerceFromUniquePointer(s, t) => throw DisallowedQualifiedCoercion(e.o, s, t)
+      case CoerceBetweenUniquePointer(s, t) => throw DisallowedQualifiedCoercion(e.o, s, t)
       case _ =>
     }
     super.applyCoercion(e, coercion)
@@ -114,8 +115,11 @@ case class TypeQualifierCoercion[Pre <: Generation]()
 
   def containsUniqueCoerce(xs: Seq[Expr[Pre]]) : Seq[(UniqueCoercion, BigInt)] =
     xs.zipWithIndex.collect {
-      case (ApplyCoercion(_, CoerceFromUniquePointer(target, sourceId)), i) =>
-        val source = uniquePointerType(target, sourceId)
+      case (ApplyCoercion(_, CoerceFromUniquePointer(source, target)), i) =>
+        (UniqueCoercion(source, target), i)
+      case (ApplyCoercion(_, CoerceBetweenUniquePointer(source, target)), i) =>
+        (UniqueCoercion(source, target), i)
+      case (ApplyCoercion(_, CoerceToUniquePointer(source, target)), i) =>
         (UniqueCoercion(source, target), i)
     }
 
@@ -124,7 +128,7 @@ case class TypeQualifierCoercion[Pre <: Generation]()
       _.originalParamT)(
       c => dispatch(c.givenArgT))(
       // For any duplicates, we exit if they do not resolve to the same type
-      (l, r) => if(l == r) l else throw DisallowedQualifiedCoercion(calledOrigin))
+      (l, r) => if(l == r) l else throw DisallowedQualifiedMethodCoercion(calledOrigin))
   }
 
   def checkArgs(args: Seq[Variable[Pre]], coercedTypes: Set[Type[Pre]], coercedArgs: Set[BigInt], calledOrigin: Origin): Unit = {
@@ -135,7 +139,7 @@ case class TypeQualifierCoercion[Pre <: Generation]()
           ( a.collectFirst { case ApplyCoercion(_, CoerceFromUniquePointer(_, _)) => () }.isDefined ||
             coercedTypes.contains(a.t) || a.t.collectFirst { case t: Type[Pre] if coercedTypes.contains(t) => () }.isDefined)
         ) {
-          throw DisallowedQualifiedCoercion(calledOrigin)
+          throw DisallowedQualifiedMethodCoercion(calledOrigin)
         }
     })
   }
@@ -144,10 +148,10 @@ case class TypeQualifierCoercion[Pre <: Generation]()
   def checkBody(body: Node[Pre], callee: Declaration[Pre], seenMethods: mutable.Set[Declaration[Pre]], calledOrigin: Origin): Unit = {
     body.collect {
       case inv: AnyMethodInvocation[Pre] if !seenMethods.contains(inv.ref.decl) =>
-          if(inv.ref.decl == callee) throw DisallowedQualifiedCoercion(calledOrigin)
+          if(inv.ref.decl == callee) throw DisallowedQualifiedMethodCoercion(calledOrigin)
           inv.ref.decl.body.map(checkBody(_, callee, seenMethods.addOne(inv.ref.decl), calledOrigin))
       case inv: AnyFunctionInvocation[Pre] if !seenMethods.contains(inv.ref.decl) =>
-        if(inv.ref.decl == callee) throw DisallowedQualifiedCoercion(calledOrigin)
+        if(inv.ref.decl == callee) throw DisallowedQualifiedMethodCoercion(calledOrigin)
         inv.ref.decl.body.map(checkBody(_, callee, seenMethods.addOne(inv.ref.decl), calledOrigin))
     }
   }
@@ -173,7 +177,7 @@ case class TypeQualifierCoercion[Pre <: Generation]()
     })
     // check return type (also 2)
     returnType.collectFirst{
-      case t: Type[Pre] if coercedTypes.contains(t) => throw DisallowedQualifiedCoercion(calledOrigin) }
+      case t: Type[Pre] if coercedTypes.contains(t) => throw DisallowedQualifiedMethodCoercion(calledOrigin) }
     if(!checkedCallees.contains(original)) {
       // If the body of this functions calls the callee, we end up with recursion we do not want
       body.foreach(b => checkBody(b, callee.top, mutable.Set(original), calledOrigin)) // Checks 3
@@ -218,9 +222,9 @@ case class TypeQualifierCoercion[Pre <: Generation]()
       case inv@FunctionInvocation(f, args, typeArgs, givenMap, yields) =>
         val allArgs: Seq[Args] = Seq(addArgs(f.decl.args, args))
         if(argsNoCoercions(allArgs)) return inv.rewriteDefault()
-        if(callee.top == inv.ref.decl) throw DisallowedQualifiedCoercion(inv.o)
+        if(callee.top == inv.ref.decl) throw DisallowedQualifiedMethodCoercion(inv.o)
         // Yields and givens are not supported
-        if(givenMap.nonEmpty || yields.nonEmpty) throw DisallowedQualifiedCoercion(inv.o)
+        if(givenMap.nonEmpty || yields.nonEmpty) throw DisallowedQualifiedMethodCoercion(inv.o)
 
         val map = getCoercionMapAndCheck(allArgs, f.decl.returnType, inv.o, f.decl.body, f.decl)
         // Make sure we only create one copy per coercion mapping
@@ -232,9 +236,9 @@ case class TypeQualifierCoercion[Pre <: Generation]()
         val allArgs: Seq[Args] = Seq(addArgs(f.decl.args, args),
           addArgs(f.decl.outArgs, outArgs))
         if(argsNoCoercions(allArgs)) return inv.rewriteDefault()
-        if(callee.top == inv.ref.decl) throw DisallowedQualifiedCoercion(inv.o)
+        if(callee.top == inv.ref.decl) throw DisallowedQualifiedMethodCoercion(inv.o)
         // Yields and givens are not supported
-        if(givenMap.nonEmpty || yields.nonEmpty) throw DisallowedQualifiedCoercion(inv.o)
+        if(givenMap.nonEmpty || yields.nonEmpty) throw DisallowedQualifiedMethodCoercion(inv.o)
 
         val map = getCoercionMapAndCheck(allArgs, f.decl.returnType, inv.o, f.decl.body, f.decl)
         val newProc: Procedure[Post] =

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

@@ -14,19 +14,19 @@ class QualifierSpec extends VercorsSpec {
   void f(){/*@ unique<1> @*/ int* x0 = (/*@ unique<1> @*/ int*) malloc(sizeof(int)*2); /*@ unique<1> @*/ int* x1; x1 = x0;}"""
   vercors should verify using silicon in "uniques pointer of unique pointer" c """void f(){/*@ unique<1> @*/ int * /*@ unique<2> @*/ * x0;}"""
 
-  vercors should error withCode "resolutionError:type" in "malloc different uniques" c
+  vercors should error withCode "disallowedQualifiedCoercion" in "malloc different uniques" c
     """#include <stdlib.h>
   void f(){/*@ unique<1> @*/ int* x0; x0 = (/*@ unique<2> @*/ int*) malloc(sizeof(int)*2); /*@ unique<1> @*/ int* x1; x1 = x0;}"""
 
   vercors should error withCode "resolutionError:type" in "diff uniques pointer of unique pointer - 1" c """void f(){/*@ unique<1> @*/ int * /*@ unique<2> @*/ * x0; /*@ unique<3> @*/ int * /*@ unique<4> @*/ * x1; x0 = x1;}"""
-  vercors should error withCode "resolutionError:type" in "diff uniques pointer of unique pointer - 2" c """void f(){/*@ unique<1> @*/ int * /*@ unique<2> @*/ * x0; /*@ unique<1> @*/ int * /*@ unique<4> @*/ * x1; x0 = x1;}"""
+  vercors should error withCode "disallowedQualifiedCoercion" in "diff uniques pointer of unique pointer - 2" c """void f(){/*@ unique<1> @*/ int * /*@ unique<2> @*/ * x0; /*@ unique<1> @*/ int * /*@ unique<4> @*/ * x1; x0 = x1;}"""
   vercors should error withCode "resolutionError:type" in "diff uniques pointer of unique pointer - 3" c """void f(){/*@ unique<1> @*/ int * /*@ unique<2> @*/ * x0; /*@ unique<3> @*/ int * /*@ unique<2> @*/ * x1; x0 = x1;}"""
 
   vercors should error withCode "cTypeNotSupported" in "multiple uniques" c """void f(/*@ unique<1> @*/ /*@ unique<2> @*/ int* x0){}"""
-  vercors should error withCode "resolutionError:type" in "different uniques param - 1" c """void f(/*@ unique<1> @*/ int* x0){ int* x1 = x0;}"""
-  vercors should error withCode "resolutionError:type" in "different uniques param - 2" c """void f(/*@ unique<1> @*/ int* x0){ /*@ unique<2> @*/ int* x1 = x0;}"""
-  vercors should error withCode "resolutionError:type" in "different uniques local" c """void f(){/*@ unique<1> @*/ int x0[2] = {1,2}; /*@ unique<2> @*/ int* x1; x1 = x0;}"""
-  vercors should error withCode "resolutionError:type" in "multiple uniques parameter" c """void f(/*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1){x1 = x0;}"""
+  vercors should error withCode "disallowedQualifiedCoercion" in "different uniques param - 1" c """void f(/*@ unique<1> @*/ int* x0){ int* x1 = x0;}"""
+  vercors should error withCode "disallowedQualifiedCoercion" in "different uniques param - 2" c """void f(/*@ unique<1> @*/ int* x0){ /*@ unique<2> @*/ int* x1 = x0;}"""
+  vercors should error withCode "disallowedQualifiedCoercion" in "different uniques local" c """void f(){/*@ unique<1> @*/ int x0[2] = {1,2}; /*@ unique<2> @*/ int* x1; x1 = x0;}"""
+  vercors should error withCode "disallowedQualifiedCoercion" in "multiple uniques parameter" c """void f(/*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1){x1 = x0;}"""
 
   vercors should verify using silicon in "Assign to init const" c """void f(){const int x = 2; /*@ assert x == 2; @*/}"""
   vercors should error withCode "disallowedConstAssignment" in "Assign to local const" c """void f(){const int x; x = 0;}"""
@@ -44,10 +44,8 @@ class QualifierSpec extends VercorsSpec {
   vercors should verify using silicon in "Assign element of const pointer" c
     """/*@ context x!=NULL ** \pointer_length(x) == 1 ** Perm(&x[0], write); ensures x[0] == 1;@*/
   void f(int * const x){x[0] = 1;}"""
-}
 
-class QualifierSpecWIP2 extends VercorsSpec {
-  vercors should verify using silicon in "Call non-unique function" c """/*@
+  vercors should verify using silicon in "Call non-unique procedure" c """/*@
   context n > 0;
   context x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i<n; Perm(&x0[i], 1\2));
   context x1 != NULL ** \pointer_length(x1) == n ** (\forall* int i; 0<=i && i<n; Perm(&x1[i], 1\2));
@@ -64,38 +62,26 @@ class QualifierSpecWIP2 extends VercorsSpec {
   int h(int* x){
     return x[0];
   }"""
-}
 
-class QualifierSpecWIP extends VercorsSpec {
-  vercors should verify using silicon in "Call non-unique function" c """/*@
-  context n > 0;
-  context x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i<n; Perm(&x0[i], 1\2));
-  context x1 != NULL ** \pointer_length(x1) == n ** (\forall* int i; 0<=i && i<n; Perm(&x1[i], 1\2));
-  ensures \result == x0[0] + x1[0];
-  @*/
-  int f(int n, /*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1){
-    return h(x0) + h(x1);
-  }
-
-  /*@
-    context x != NULL ** \pointer_length(x) > 0 ** Perm(&x[0], 1\2);
-    ensures \result == x[0];
-  @*/
-  int h(int* x){
-    return x[0];
-  }"""
-
-  vercors should error withCode "???" in "Recursive call wrong uniques" c """/*@
+  vercors should error withCode "disallowedQualifiedMethodCoercion" in "Recursive procedure call wrong uniques" c """/*@
   context n > 0;
   context x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i<n; Perm(&x0[i], 1\2));
   context x1 != NULL ** \pointer_length(x1) == n ** (\forall* int i; 0<=i && i<n; Perm(&x1[i], 1\2));
 @*/
 int f(int n, /*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1){
   if(n == 1){
-    return h(x0) + h(x1);
+    return x0[0] + x1[0];
   }
   else {
     return f(n-1, x1, x0);
   }
 }"""
+}
+
+class QualifierSpecWIP2 extends VercorsSpec {
+
+}
+
+class QualifierSpecWIP extends VercorsSpec {
+
 }