Syntax and parsing of unique specifier

Author: sakehl

examples/concepts/unique/arrays.c

@@ -0,0 +1,16 @@
+
+/*@
+  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<1> @*/ /*@ 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] );
+  @*/
+  for(int j=0; j<n; j++){
+    x0[j] = x1[j] + x2[j];
+  }
+}

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

@@ -2489,6 +2489,8 @@ 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]

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

@@ -0,0 +1,9 @@
+package vct.col.ast.lang.c
+
+import vct.col.ast.CUnique
+import vct.col.ast.ops.CUniqueOps
+import vct.col.print._
+
+trait CUniqueImpl[G] extends CUniqueOps[G] { this: CUnique[G] =>
+  override def layout(implicit ctx: Ctx): Doc = Doc.inlineSpec(Text("unique<") <> i.toString() <> ">")
+}

src/parsers/antlr4/SpecLexer.g4

@@ -58,6 +58,7 @@ VAL_STRING: 'string';
 VAL_PURE: 'pure';
 VAL_THREAD_LOCAL: 'thread_local';
 VAL_BIP_ANNOTATION: 'bip_annotation';
+VAL_UNIQUE: 'unique';
 
 VAL_WITH: 'with';
 VAL_THEN: 'then';

src/parsers/antlr4/SpecParser.g4

@@ -417,6 +417,7 @@ valImpureDef
 valModifier
  : ('pure' | 'inline' | 'thread_local' | 'bip_annotation')
  | langStatic # valStatic
+ | 'unique' '<' langConstInt '>' # valUnique
  ;
 
 valArgList

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

@@ -168,10 +168,13 @@ case class CToCol[G](
             else if (m.consume(m.inline))
               CInline[G]()
             else
+              m.consume(m.unique).map(CUnique[G](_)).getOrElse(
+
               fail(
                 m.nodes.head,
                 "This modifier cannot be attached to a declaration in C",
               )
+              )
           },
         )
     }
@@ -1183,6 +1186,7 @@ case class CToCol[G](
           case "thread_local" => collector.threadLocal += mod
         }
       case ValStatic(_) => collector.static += mod
+      case ValUnique(_, _, i, _) => collector.unique += ((mod, convert(i)))
     }
 
   def convertEmbedWith(

src/parsers/vct/parsers/transform/ToCol.scala

@@ -130,13 +130,22 @@ abstract class ToCol[G](
     val static: mutable.ArrayBuffer[ParserRuleContext] = mutable.ArrayBuffer()
     val bipAnnotation: mutable.ArrayBuffer[ParserRuleContext] = mutable
       .ArrayBuffer()
+    val unique: mutable.ArrayBuffer[(ParserRuleContext, BigInt)] = mutable
+      .ArrayBuffer()
 
     def consume(buffer: mutable.ArrayBuffer[ParserRuleContext]): Boolean = {
       val result = buffer.nonEmpty
       buffer.clear()
       result
     }
 
+    def consume(buffer: mutable.ArrayBuffer[(ParserRuleContext, BigInt)]): Option[BigInt] = {
+      buffer match {
+        case mutable.ArrayBuffer() => None
+        case (_, i) +: _ => buffer.clear(); Some(i)
+      }
+    }
+
     def nodes: Seq[ParserRuleContext] =
       Seq(pure, inline, threadLocal, static, bipAnnotation).flatten
   }

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

@@ -30,6 +30,12 @@ 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 =
@@ -860,22 +866,36 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
     var extern = false
     var innerType: Option[Type[Pre]] = None
     var arraySize: Option[Expr[Pre]] = None
+    var mainType: Option[Type[Pre]] = None
+
     var sizeBlame: Option[Blame[ArraySizeError]] = None
+    var pure = false
+    var inline = false
+    var unique: Option[BigInt] = None
+    var static = false
 
     specs.foreach {
       case GPULocal() => shared = true
       case GPUGlobal() => global = true
-      case CSpecificationType(CTPointer(t)) =>
+      case CSpecificationType(t@CTPointer(it)) =>
         arrayOrPointer = true
-        innerType = Some(t)
+        innerType = Some(it)
+        mainType = Some(t)
       case CSpecificationType(ctarr @ CTArray(size, t)) =>
         arraySize = size
         innerType = Some(t)
         sizeBlame = Some(
           ctarr.blame
         ) // we set the blame here, together with the size
         arrayOrPointer = true
+        mainType = Some(t)
+      case CSpecificationType(t) =>
+        mainType = Some(t)
       case CExtern() => extern = true
+      case CUnique(i) => unique = Some(i)
+      case CPure() => pure = true
+      case CInline() => inline = true
+      case CStatic() => static = true
       case _ =>
     }
 
@@ -894,7 +914,6 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
   }
 
   def addStaticShared(
-      decl: CDeclarator[Pre],
       cRef: CNameTarget[Pre],
       t: Type[Pre],
       o: Origin,
@@ -942,7 +961,6 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
           !prop.extern
         ) {
           addStaticShared(
-            init.decl,
             cRef,
             prop.innerType.get,
             varO,
@@ -958,7 +976,6 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
           !prop.extern
         ) {
           addStaticShared(
-            init.decl,
             cRef,
             prop.innerType.get,
             varO,

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

@@ -0,0 +1,9 @@
+package vct.test.integration.examples
+
+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){}"""
+}