Unique specifier for types leading to using different fields in the backend

examples/concepts/unique/arrays.c

@@ -0,0 +1,15 @@
+/*@
+  context_everywhere x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i<n; Perm(&x0[i], write));
+  context_everywhere x1 != NULL ** \pointer_length(x1) == n ** (\forall* int i; 0<=i && i<n; Perm(&x1[i], 1\2));
+  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 f(int n, /*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1, /*@ unique<3> @*/ int* x2){
+  /*@
+    loop_invariant 0 <= j && j <= n;
+    loop_invariant (\forall int i; 0<=i && i<j; x0[i] == x1[i] + x2[i] );
+  @*/
+  for(int j=0; j<n; j++){
+    x0[j] = x1[j] + x2[j];
+  }
+}

examples/verifythis/2018/challenge2.pvl

@@ -23,7 +23,7 @@ class ColoredTiles {
          || (i < n - 2        && s[i+1] && s[i+2])
       );
 
-  pure boolean unique(seq<seq<boolean>> s)
+  pure boolean uniqueS(seq<seq<boolean>> s)
    = (\forall int i;0<=i && i<|s|;
        (\forall int j;0<=j && j<|s|; (s[i] == s[j]) ==> i == j));
 
@@ -63,7 +63,7 @@ class ColoredTiles {
     }
   }
 
-  requires unique(res);
+  requires uniqueS(res);
   requires 0 <= j;
   requires j < |res|;
   ensures (\forall int y;0 <= y && y < j;!(prefix + res[y] == prefix + res[j]));
@@ -78,9 +78,9 @@ class ColoredTiles {
     return;
   }
 
-  requires unique(ini);
+  requires uniqueS(ini);
   requires (\forall int y;0 <= y && y < |ini|;!(ini[y] == elm));
-  ensures unique(ini + seq<seq<boolean>> { elm });
+  ensures uniqueS(ini + seq<seq<boolean>> { elm });
   void lemma_unique_add_one(seq<seq<boolean>> ini, seq<boolean> elm)
   { 
     seq<seq<boolean>> res = ini + seq<seq<boolean>> { elm };
@@ -119,19 +119,19 @@ class ColoredTiles {
     assert (|res[1]| == count[1]);
     assert (|res[2]| == count[2]);
     assert (|res[3]| == count[3]);
-    assert unique(res[0]);
-    assert unique(res[1]);
-    assert unique(res[2]);
+    assert uniqueS(res[0]);
+    assert uniqueS(res[1]);
+    assert uniqueS(res[2]);
     assert !(res[3][0][0] == res[3][1][0]);
-    assert unique(res[3]);
+    assert uniqueS(res[3]);
 
     int n=4;
     loop_invariant n>=4 && n<=i;
     loop_invariant |res| == n;
     loop_invariant (\forall* int j;0<=j && j<i;Perm(count[j],write));
     loop_invariant (\forall int j;0<=j && j<n;|res[j]| == count[j]);
     loop_invariant (\forall int z=0..n, int y=0..|res[z]|; validSequence(res[z][y],z)); // all sequences valid
-    loop_invariant (\forall int z;0<=z && z<n;unique(res[z])); // all sequences unique
+    loop_invariant (\forall int z;0<=z && z<n;uniqueS(res[z])); // all sequences uniqueS
     while(n<i){
       seq<seq <boolean>> last = seq<seq <boolean>> {};
       count[n] = count[n-1];
@@ -144,10 +144,10 @@ class ColoredTiles {
       loop_invariant (\forall int y; 0<=y && y <j; validSequence(last[y],n));
       loop_invariant (\forall int z;0<=z && z <j;|last[z]|>0);
       loop_invariant (\forall int z;0<=z && z <j;last[z][0]==false);
-      loop_invariant (\forall int z;0<=z && z<|res|;unique(res[z]));
+      loop_invariant (\forall int z;0<=z && z<|res|;uniqueS(res[z]));
       loop_invariant (\let int predN = n - 1; (\forall int z;0<=z && z<j;(last[z] == seq <boolean> {false} + res[predN][z])));
       loop_invariant (\forall int z;0<=z && z<j;last[z][0]==false);
-      loop_invariant unique(last);
+      loop_invariant uniqueS(last);
       while (j < |res[n-1]|){
         lemma_uniqueness_implies_unequal(res[n - 1],j,seq <boolean> {false});
         assert (\let int predN = n - 1;
@@ -166,7 +166,7 @@ class ColoredTiles {
       loop_invariant (\forall int y;0<=y && y <|last|;validSequence(last[y],n));
       loop_invariant (\forall int y;0<=y && y <|startBlock|;startBlock[y]);
       loop_invariant (\forall int z;0<=z && z <|last|;has_false_in_prefix(last[z],k-1));
-      loop_invariant unique(last);
+      loop_invariant uniqueS(last);
       while(k < n){
         int j = 0;
         seq<seq <boolean>> nxtblock = seq<seq <boolean>> {};
@@ -182,7 +182,7 @@ class ColoredTiles {
         loop_invariant (\forall int y;0<=y && y <j;!has_false_in_prefix(nxtblock[y],k-1)); // li176
         loop_invariant (\forall int y;0<=y && y <j;has_false_in_prefix(nxtblock[y],k));  // li177
         loop_invariant (\forall int y;0<=y && y <j;nxtblock[y] == (startBlock+seq <boolean> {false}) + res[n-k-1][y]);
-        loop_invariant unique(nxtblock);
+        loop_invariant uniqueS(nxtblock);
         while (j < |res[n-k-1]|){
           seq<boolean> nxtelm = (startBlock + seq <boolean> {false}) + res[n-k-1][j];
           lemma_uniqueness_implies_unequal(res[n-k-1],j,startBlock + seq <boolean> {false});
@@ -211,7 +211,7 @@ class ColoredTiles {
     assert (\let int predI = i - 1;
         (\forall int y; 0<=y && y <|res[i-1]|;validSequence(res[predI][y],i-1)) // all sequences are valid
         );
-    assert unique(res[i-1]); // all sequences are unique
+    assert uniqueS(res[i-1]); // all sequences are uniqueS
     return count[i-1];
   }
 

res/universal/res/adt/const_pointer.pvl

@@ -0,0 +1,27 @@
+adt `const_pointer`<A> {
+  pure `const_pointer`<A> const_pointer_of(seq<A> b, int offset);
+  pure seq<A> const_pointer_block(`const_pointer`<A> p);
+  pure int const_pointer_offset(`const_pointer`<A> p);
+
+  // the block offset is valid wrt the length of the block
+  axiom (∀ `const_pointer`<A> p;
+    const_pointer_offset(p) >= 0 &&
+      const_pointer_offset(p) < |const_pointer_block(p)|);
+
+  // const_pointer_of is injective: a (block, offset) pair indicates a unique const_pointer value
+  axiom (∀seq<A> b, int offset;
+    {:const_pointer_block(const_pointer_of(b, offset)):} == b &&
+      {:const_pointer_offset(const_pointer_of(b, offset)):} == offset);
+}
+
+decreases;
+pure A const_ptr_deref<A>(`const_pointer`<A> p) =
+  `const_pointer`<A>.const_pointer_block(p)[`const_pointer`<A>.const_pointer_offset(p)];
+
+decreases;
+requires 0 <= `const_pointer`<A>.const_pointer_offset(p) + offset;
+requires `const_pointer`<A>.const_pointer_offset(p) + offset < |`const_pointer`<A>.const_pointer_block(p)|;
+pure `const_pointer`<A> const_ptr_add<A>(`const_pointer`<A> p, int offset) =
+  `const_pointer`<A>.const_pointer_of(
+     `const_pointer`<A>.const_pointer_block(p),
+     `const_pointer`<A>.const_pointer_offset(p) + offset);

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

@@ -129,14 +129,35 @@ 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]
+final case class TConst[G](inner: Type[G])(
+  implicit val o: Origin = DiagnosticOrigin
+) extends Type[G] with TConstImpl[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])(
+  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]
+final case class TConstPointer[G](pureElement: Type[G])(
+  implicit val o: Origin = DiagnosticOrigin
+) extends PointerType[G] with TConstPointerImpl[G]
 
 sealed trait CompositeType[G] extends Type[G] with CompositeTypeImpl[G]
 sealed trait SizedType[G] extends CompositeType[G] with SizedTypeImpl[G]
@@ -325,10 +346,16 @@ final case class SpecIgnoreEnd[G]()(implicit val o: Origin)
 
 sealed trait NormallyCompletingStatement[G]
     extends Statement[G] with NormallyCompletingStatementImpl[G]
+sealed trait AssignStmt[G]
+  extends NormallyCompletingStatement[G] with AssignStmtImpl[G]
 final case class Assign[G](target: Expr[G], value: Expr[G])(
     val blame: Blame[AssignFailed]
 )(implicit val o: Origin)
-    extends NormallyCompletingStatement[G] with AssignImpl[G]
+    extends AssignStmt[G] with AssignImpl[G]
+final case class AssignInitial[G](target: Expr[G], value: Expr[G])(
+  val blame: Blame[AssignFailed]
+)(implicit val o: Origin)
+  extends AssignStmt[G] with AssignInitialImpl[G]
 final case class Send[G](decl: SendDecl[G], delta: BigInt, res: Expr[G])(
     val blame: Blame[SendFailed]
 )(implicit val o: Origin)
@@ -924,6 +951,42 @@ final case class CoercionSequence[G](coercions: Seq[Coercion[G]])(
     implicit val o: Origin
 ) extends Coercion[G] with CoercionSequenceImpl[G]
 
+final case class CoerceBetweenUnique[G](sourceId: BigInt, targetId: BigInt, innerCoercion: Coercion[G])(
+  implicit val o: Origin
+) extends Coercion[G] with CoerceBetweenUniqueImpl[G]
+final case class CoerceToUnique[G](source: Type[G], targetId: BigInt)(
+  implicit val o: Origin
+) extends Coercion[G] with CoerceToUniqueImpl[G]
+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](source: Type[G], target: Type[G])(
+  implicit val o: Origin
+) extends Coercion[G] with CoerceToUniquePointerImpl[G]
+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](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]
+
+final case class CoerceFromConst[G](target: Type[G])(
+  implicit val o: Origin
+) extends Coercion[G] with CoerceFromConstImpl[G]
+
 final case class CoerceNothingSomething[G](target: Type[G])(
     implicit val o: Origin
 ) extends Coercion[G] with CoerceNothingSomethingImpl[G]
@@ -970,7 +1033,7 @@ final case class CoerceNullJavaClass[G](
     extends Coercion[G] with CoerceNullJavaClassImpl[G]
 final case class CoerceNullAnyClass[G]()(implicit val o: Origin)
     extends Coercion[G] with CoerceNullAnyClassImpl[G]
-final case class CoerceNullPointer[G](pointerElementType: Type[G])(
+final case class CoerceNullPointer[G](target: Type[G])(
     implicit val o: Origin
 ) extends Coercion[G] with CoerceNullPointerImpl[G]
 final case class CoerceNullEnum[G](targetEnum: Ref[G, Enum[G]])(
@@ -1820,10 +1883,20 @@ final case class NewArray[G](
     initialize: Boolean,
 )(val blame: Blame[ArraySizeError])(implicit val o: Origin)
     extends Expr[G] with NewArrayImpl[G]
-final case class NewPointerArray[G](element: Type[G], size: Expr[G])(
+sealed trait NewPointer[G] extends Expr[G] with NewPointerImpl[G]
+final case class NewPointerArray[G](element: Type[G], size: Expr[G], unique: Option[BigInt])(
     val blame: Blame[ArraySizeError]
 )(implicit val o: Origin)
-    extends Expr[G] with NewPointerArrayImpl[G]
+    extends NewPointer[G] with NewPointerArrayImpl[G]
+final case class NewConstPointerArray[G](element: Type[G], size: Expr[G])(
+  val blame: Blame[ArraySizeError]
+)(implicit val o: Origin)
+  extends NewPointer[G] with NewConstPointerArrayImpl[G]
+
+final case class UniquePointerCoercion[G](e: Expr[G], t: Type[G])(
+  implicit val o: Origin
+) extends Expr[G] with UniquePointerCoercionImpl[G]
+
 final case class FreePointer[G](pointer: Expr[G])(
     val blame: Blame[PointerFreeError]
 )(implicit val o: Origin)
@@ -2571,6 +2644,12 @@ final case class CVolatile[G]()(implicit val o: Origin)
     extends CTypeQualifier[G] with CVolatileImpl[G]
 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]
@@ -2764,6 +2843,8 @@ final case class CLiteralArray[G](exprs: Seq[Expr[G]])(implicit val o: Origin)
     extends CExpr[G] with CLiteralArrayImpl[G]
 
 sealed trait CType[G] extends Type[G] with CTypeImpl[G]
+sealed trait CPointerType[G] extends CType[G] with CPointerTypeImpl[G]
+
 final case class TCInt[G]()(implicit val o: Origin = DiagnosticOrigin)
     extends IntType[G] with CType[G] with TCIntImpl[G]
 final case class TCFloat[G](exponent: Int, mantissa: Int)(
@@ -2774,11 +2855,11 @@ final case class CPrimitiveType[G](specifiers: Seq[CDeclarationSpecifier[G]])(
 ) extends CType[G] with CPrimitiveTypeImpl[G]
 final case class CTPointer[G](innerType: Type[G])(
     implicit val o: Origin = DiagnosticOrigin
-) extends CType[G] with CTPointerImpl[G]
+) extends CPointerType[G] with CTPointerImpl[G]
 final case class CTArray[G](size: Option[Expr[G]], innerType: Type[G])(
     val blame: Blame[ArraySizeError]
 )(implicit val o: Origin = DiagnosticOrigin)
-    extends CType[G] with CTArrayImpl[G]
+    extends CPointerType[G] with CTArrayImpl[G]
 final case class CTStruct[G](ref: Ref[G, CGlobalDeclaration[G]])(
     implicit val o: Origin = DiagnosticOrigin
 ) extends CType[G] with CTStructImpl[G]

src/col/vct/col/ast/expr/heap/alloc/NewConstPointerArrayImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.expr.heap.alloc
+
+import vct.col.ast.{NewConstPointerArray, TConstPointer, Type}
+import vct.col.ast.ops.NewConstPointerArrayOps
+import vct.col.print._
+
+trait NewConstPointerArrayImpl[G] extends NewConstPointerArrayOps[G] { this: NewConstPointerArray[G] =>
+  override lazy val t: Type[G] = TConstPointer[G](element)
+}

src/col/vct/col/ast/expr/heap/alloc/NewPointerArrayImpl.scala

@@ -1,14 +1,11 @@
 package vct.col.ast.expr.heap.alloc
 
-import vct.col.ast.{NewPointerArray, TPointer, Type}
+import vct.col.ast.{NewPointerArray, TPointer, TUniquePointer, Type}
 import vct.col.print._
 import vct.col.ast.ops.NewPointerArrayOps
 
 trait NewPointerArrayImpl[G] extends NewPointerArrayOps[G] {
   this: NewPointerArray[G] =>
-  override lazy val t: Type[G] = TPointer(element)
-
-  override def precedence: Int = Precedence.POSTFIX
-  override def layout(implicit ctx: Ctx): Doc =
-    Text("new") <+> element <> "[" <> size <> "]"
+  override lazy val t: Type[G] = unique.map(TUniquePointer[G](element,_))
+    .getOrElse(TPointer[G](element))
 }

src/col/vct/col/ast/expr/heap/alloc/NewPointerImpl.scala

@@ -0,0 +1,16 @@
+package vct.col.ast.expr.heap.alloc
+
+import vct.col.ast.{Expr, NewPointer, Type}
+import vct.col.origin.{ArraySizeError, Blame}
+import vct.col.print._
+
+trait NewPointerImpl[G] {
+  this: NewPointer[G] =>
+  val blame: Blame[ArraySizeError]
+  val element: Type[G]
+  val size: Expr[G]
+
+  override def precedence: Int = Precedence.POSTFIX
+  override def layout(implicit ctx: Ctx): Doc =
+    Text("new") <+> element <> "[" <> size <> "]"
+}

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/expr/misc/UniquePointerCoercionImpl.scala

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