Added qualifers (const, unique), const pointers, decrease fix

examples/concepts/unique/arrays.c

@@ -1,11 +1,10 @@
-
 /*@
   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 main(int n, /*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1, /*@ unique<2> @*/ int* x2){
+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] );

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

@@ -133,6 +133,12 @@ final case class TType[G](t: Type[G])(implicit val o: Origin = DiagnosticOrigin)
 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]
 
 sealed trait PointerType[G] extends Type[G] with PointerTypeImpl[G]
 final case class TPointer[G](element: Type[G])(
@@ -141,6 +147,9 @@ final case class TPointer[G](element: Type[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]
@@ -329,10 +338,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)
@@ -928,6 +943,24 @@ 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 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]
@@ -974,7 +1007,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]])(
@@ -1822,10 +1855,18 @@ 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 ToUnique[G](inner: Expr[G])(implicit val o: Origin) extends Expr[G] with ToUniqueImpl[G]
+
 final case class FreePointer[G](pointer: Expr[G])(
     val blame: Blame[PointerFreeError]
 )(implicit val o: Origin)
@@ -2494,8 +2535,6 @@ final case class CPure[G]()(implicit val o: Origin)
     extends CSpecificationModifier[G] with CPureImpl[G]
 final case class CInline[G]()(implicit val o: Origin)
     extends CSpecificationModifier[G] with CInlineImpl[G]
-final case class CUnique[G](i: BigInt)(implicit val o: Origin)
-  extends CSpecificationModifier[G] with CUniqueImpl[G]
 
 sealed trait CStorageClassSpecifier[G]
     extends CDeclarationSpecifier[G] with CStorageClassSpecifierImpl[G]
@@ -2575,6 +2614,8 @@ 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]
 
 sealed trait CFunctionSpecifier[G]
     extends CDeclarationSpecifier[G] with CFunctionSpecifierImpl[G]
@@ -2768,6 +2809,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)(
@@ -2778,11 +2821,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/family/coercion/CoerceBetweenUniqueImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.family.coercion
+
+import vct.col.ast.{CoerceBetweenUnique, TUnique}
+import vct.col.ast.ops.CoerceBetweenUniqueOps
+import vct.col.print._
+
+trait CoerceBetweenUniqueImpl[G] extends CoerceBetweenUniqueOps[G] { this: CoerceBetweenUnique[G] =>
+  override def target = TUnique(innerCoercion.target, targetId)
+}

src/col/vct/col/ast/unsorted/CoerceDecreasePrecisionImpl.scala → src/col/vct/col/ast/family/coercion/CoerceDecreasePrecisionImpl.scala

@@ -1,10 +1,9 @@
-package vct.col.ast.unsorted
+package vct.col.ast.family.coercion
 
 import vct.col.ast.CoerceDecreasePrecision
 import vct.col.ast.ops.CoerceDecreasePrecisionOps
 import vct.col.print._
 
 trait CoerceDecreasePrecisionImpl[G] extends CoerceDecreasePrecisionOps[G] {
   this: CoerceDecreasePrecision[G] =>
-  // override def layout(implicit ctx: Ctx): Doc = ???
 }

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

@@ -0,0 +1,9 @@
+package vct.col.ast.family.coercion
+
+import vct.col.ast.{CoerceFromConst, TConst, Type}
+import vct.col.ast.ops.CoerceFromConstOps
+import vct.col.print._
+
+trait CoerceFromConstImpl[G] extends CoerceFromConstOps[G] { this: CoerceFromConst[G] =>
+  val source: Type[G] = TConst[G](target)
+}

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

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

src/col/vct/col/ast/unsorted/CoerceIncreasePrecisionImpl.scala → src/col/vct/col/ast/family/coercion/CoerceIncreasePrecisionImpl.scala

@@ -1,10 +1,9 @@
-package vct.col.ast.unsorted
+package vct.col.ast.family.coercion
 
 import vct.col.ast.CoerceIncreasePrecision
 import vct.col.ast.ops.CoerceIncreasePrecisionOps
 import vct.col.print._
 
 trait CoerceIncreasePrecisionImpl[G] extends CoerceIncreasePrecisionOps[G] {
   this: CoerceIncreasePrecision[G] =>
-  // override def layout(implicit ctx: Ctx): Doc = ???
 }

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

@@ -1,9 +1,8 @@
 package vct.col.ast.family.coercion
 
-import vct.col.ast.{CoerceNullPointer, TPointer}
+import vct.col.ast.{CoerceNullPointer}
 import vct.col.ast.ops.CoerceNullPointerOps
 
 trait CoerceNullPointerImpl[G] extends CoerceNullPointerOps[G] {
   this: CoerceNullPointer[G] =>
-  override def target: TPointer[G] = TPointer(pointerElementType)
 }

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

@@ -0,0 +1,9 @@
+package vct.col.ast.family.coercion
+
+import vct.col.ast.{CoerceToConst, TConst, Type}
+import vct.col.ast.ops.CoerceToConstOps
+import vct.col.print._
+
+trait CoerceToConstImpl[G] extends CoerceToConstOps[G] { this: CoerceToConst[G] =>
+  val target: Type[G] = TConst[G](source)
+}

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

@@ -0,0 +1,9 @@
+package vct.col.ast.family.coercion
+
+import vct.col.ast.{CoerceToUnique, TUnique}
+import vct.col.ast.ops.CoerceToUniqueOps
+import vct.col.print._
+
+trait CoerceToUniqueImpl[G] extends CoerceToUniqueOps[G] { this: CoerceToUnique[G] =>
+  override def target = TUnique(source, targetId)
+}

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

@@ -67,6 +67,11 @@ trait CoercionImpl[G] extends CoercionFamilyOps[G] {
       case CoerceCVectorVector(_, _) => true
       case CoerceResourceResourceVal() => true
       case CoerceResourceValResource() => true
+      case CoerceFromConst(_) => true
+      case CoerceToConst(_) => true
+      case CoerceFromUnique(_, _) => true
+      case CoerceToUnique(_, _) => true
+      case CoerceBetweenUnique(_, _, inner) => inner.isPromoting
       case CoerceMapOption(inner, _, _) => inner.isPromoting
       case CoerceMapTuple(inner, _, _) => inner.forall(_.isPromoting)
       case CoerceMapEither(inner, _, _) =>

src/col/vct/col/ast/lang/c/CPointerDeclaratorImpl.scala

@@ -7,5 +7,5 @@ import vct.col.print.{Ctx, Doc}
 trait CPointerDeclaratorImpl[G] extends CPointerDeclaratorOps[G] {
   this: CPointerDeclarator[G] =>
   override def layout(implicit ctx: Ctx): Doc =
-    inner.show <> Doc.fold(pointers)(_ <> _)
+    Doc.fold(pointers)(_ <> _) <> inner.show
 }

src/col/vct/col/ast/lang/c/CPointerTypeImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.lang.c
+
+import vct.col.ast.{CPointerType, Type}
+
+trait CPointerTypeImpl[G] {
+  this: CPointerType[G] =>
+
+  val innerType: Type[G]
+}

src/col/vct/col/ast/statement/terminal/AssignImpl.scala

@@ -1,36 +1,8 @@
 package vct.col.ast.statement.terminal
 
-import vct.col.ast.{Assign, EndpointName, Local}
-import vct.col.check.{CheckContext, CheckError, SeqProgEndpointAssign}
-import vct.col.print._
+import vct.col.ast.Assign
 import vct.col.ast.ops.AssignOps
+import vct.col.print._
 
-trait AssignImpl[G]
-    extends NormallyCompletingStatementImpl[G] with AssignOps[G] {
-  this: Assign[G] =>
-  override def check(context: CheckContext[G]): Seq[CheckError] =
-    super.check(context) ++
-      (target match {
-        case Local(ref) =>
-          context.checkInWriteScope(context.roScopeReason, this, ref)
-        case EndpointName(_) if context.currentChoreography.isDefined =>
-          Seq(SeqProgEndpointAssign(this))
-        case _ => Nil
-      })
-
-  def layoutAsExpr(implicit ctx: Ctx): Doc =
-    Group(
-      target.show <+>
-        (if (ctx.syntax == Ctx.Silver)
-           ":="
-         else
-           "=") <>> value
-    )
-
-  override def layout(implicit ctx: Ctx): Doc =
-    layoutAsExpr <>
-      (if (ctx.syntax == Ctx.Silver)
-         Empty
-       else
-         Text(";"))
+trait AssignImpl[G] extends AssignOps[G] { this: Assign[G] =>
 }

src/col/vct/col/ast/statement/terminal/AssignInitialImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.statement.terminal
+
+import vct.col.ast.AssignInitial
+import vct.col.ast.ops.AssignInitialOps
+import vct.col.print._
+
+trait AssignInitialImpl[G] extends AssignInitialOps[G] { this: AssignInitial[G] =>
+
+}