Ast opencl fixes

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

@@ -536,6 +536,7 @@ final case class Length[G](arr: Expr[G])(val blame: Blame[ArrayNull])(implicit v
 final case class Size[G](obj: Expr[G])(implicit val o: Origin) extends Expr[G] with SizeImpl[G]
 final case class PointerBlockLength[G](pointer: Expr[G])(val blame: Blame[PointerNull])(implicit val o: Origin) extends Expr[G] with PointerBlockLengthImpl[G]
 final case class PointerBlockOffset[G](pointer: Expr[G])(val blame: Blame[PointerNull])(implicit val o: Origin) extends Expr[G] with PointerBlockOffsetImpl[G]
+final case class SharedMemSize[G](pointer: Expr[G])(implicit val o: Origin) extends Expr[G] with SharedMemSizeImpl[G]
 
 final case class Cons[G](x: Expr[G], xs: Expr[G])(implicit val o: Origin) extends Expr[G] with ConsImpl[G]
 final case class Head[G](xs: Expr[G])(val blame: Blame[SeqBoundFailure])(implicit val o: Origin) extends Expr[G] with HeadImpl[G]
@@ -633,6 +634,8 @@ sealed trait CStorageClassSpecifier[G] extends CDeclarationSpecifier[G] with CSt
 final case class CTypedef[G]()(implicit val o: Origin) extends CStorageClassSpecifier[G] with CTypedefImpl[G]
 final case class CExtern[G]()(implicit val o: Origin) extends CStorageClassSpecifier[G] with CExternImpl[G]
 final case class CStatic[G]()(implicit val o: Origin) extends CStorageClassSpecifier[G] with CStaticImpl[G]
+final case class GPULocal[G]()(implicit val o: Origin) extends CStorageClassSpecifier[G] with GPULocalImpl[G]
+final case class GPUGlobal[G]()(implicit val o: Origin) extends CStorageClassSpecifier[G] with GPUGlobalImpl[G]
 
 sealed trait CTypeSpecifier[G] extends CDeclarationSpecifier[G] with CTypeSpecifierImpl[G]
 final case class CVoid[G]()(implicit val o: Origin) extends CTypeSpecifier[G] with CVoidImpl[G]

col/src/main/java/vct/col/ast/temporaryimplpackage/lang/GPUGlobalImpl.scala

@@ -0,0 +1,7 @@
+package vct.col.ast.temporaryimplpackage.lang
+
+import vct.col.ast.GPUGlobal
+
+trait GPUGlobalImpl[G] { this: GPUGlobal[G] =>
+
+}

col/src/main/java/vct/col/ast/temporaryimplpackage/lang/GPULocalImpl.scala

@@ -0,0 +1,7 @@
+package vct.col.ast.temporaryimplpackage.lang
+
+import vct.col.ast.GPULocal
+
+trait GPULocalImpl[G] {this: GPULocal[G] =>
+
+}

col/src/main/java/vct/col/ast/temporaryimplpackage/lang/SharedMemSizeImpl.scala

@@ -0,0 +1,7 @@
+package vct.col.ast.temporaryimplpackage.lang
+
+import vct.col.ast.{SharedMemSize, TInt, Type}
+
+trait SharedMemSizeImpl[G] { this: SharedMemSize[G] =>
+  override def t: Type[G] = TInt()
+}

col/src/main/java/vct/col/coerce/CoercingRewriter.scala

@@ -406,7 +406,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends Rewriter[Pre] with
 
     e match {
       case ApplyCoercion(_, _) =>
-        throw Unreachable("All instances of ApplyCoercion should be immediately rewritten by CoercingRewriter.disptach.")
+        throw Unreachable("All instances of ApplyCoercion should be immediately rewritten by CoercingRewriter.dispatch.")
 
       case ActionApply(action, args) =>
         ActionApply(action, coerceArgs(args, action.decl))
@@ -988,6 +988,11 @@ abstract class CoercingRewriter[Pre <: Generation]() extends Rewriter[Pre] with
         val (right, TSet(rightT)) = set(ys)
         val sharedElement = Types.leastCommonSuperType(leftT, rightT)
         SetUnion(coerce(left, TSet(sharedElement)), coerce(right, TSet(sharedElement)))
+      case SharedMemSize(xs) =>
+        firstOk(e, s"Expected operand to be a pointer or array, but got ${xs.t}.",
+          SharedMemSize(array(xs)._1),
+          SharedMemSize(pointer(xs)._1),
+        )
       case SilverBagSize(xs) =>
         SilverBagSize(bag(xs)._1)
       case SilverCurFieldPerm(obj, field) =>

col/src/main/java/vct/col/feature/FeatureRainbow.scala

@@ -457,6 +457,8 @@ class FeatureRainbow[G] {
     case node: CStructAccess[G] => return Nil
     case node: CStructDeref[G] => return Nil
     case node: GpgpuCudaKernelInvocation[G] => return Nil
+    case node: LocalThreadId[G] => return Nil
+    case node: GlobalThreadId[G] => return Nil
     case node: CPrimitiveType[G] => return Nil
     case node: JavaName[G] => return Nil
     case node: JavaImport[G] => return Nil

col/src/main/java/vct/col/origin/Origin.scala

@@ -260,6 +260,17 @@ case class ReadableOrigin(readable: Readable,
   override def toString: String = f"$startText - $endText"
 }
 
+case class InterpretedOriginVariable(name: String, original: Origin)
+  extends InputOrigin {
+  override def preferredName: String = name
+
+  override def context: String = original.context
+
+  override def inlineContext: String = original.inlineContext
+
+  override def shortPosition: String = original.shortPosition
+}
+
 case class InterpretedOrigin(interpreted: Readable,
                              startLineIdx: Int, endLineIdx: Int,
                              cols: Option[(Int, Int)],

col/src/main/java/vct/col/print/Printer.scala

@@ -633,9 +633,9 @@ case class Printer(out: Appendable,
     case MapDisjoint(left, right) =>
       (phrase("disjointMap(", left, ",", space, right, ")"), 100)
     case Forall(bindings, triggers, body) =>
-      (phrase("(", "\\forall", space, phrase(bindings.map(NodePhrase):_*), "; true; ", body, ")"), 120)
+      (phrase("(", "\\forall", space, commas(bindings.map(NodePhrase)), "; true; ", body, ")"), 120)
     case Exists(bindings, triggers, body) =>
-      (phrase("(", "\\exists", space, phrase(bindings.map(NodePhrase):_*), "; true; ", body, ")"), 120)
+      (phrase("(", "\\exists", space, commas(bindings.map(NodePhrase)), "; true; ", body, ")"), 120)
     case ValidArray(arr, len) =>
       (phrase("\\array(", arr, ",", space, len, ")"), 100)
     case ValidMatrix(mat, w, h) =>
@@ -655,13 +655,15 @@ case class Printer(out: Appendable,
     case JoinToken(thread) =>
       (phrase("running", "(", thread, ")"), 100)
     case Starall(bindings, triggers, body) =>
-      (phrase("(", "\\forall*", space, phrase(bindings.map(NodePhrase):_*), "; true; ", body, ")"), 120)
+      (phrase("(", "\\forall*", space, commas(bindings.map(NodePhrase)), "; true; ", body, ")"), 120)
     case Star(left, right) =>
       (phrase(assoc(40, left), space, "**", space, assoc(40, right)), 40)
     case Wand(left, right) =>
       (phrase(bind(30, left), space, "-*", space, assoc(30, right)), 30)
     case Scale(scale, res) =>
       (phrase("[", scale, "]", assoc(90, res)), 90)
+    case ScaleByParBlock(block, res) =>
+      (phrase("[", block.decl, "]", assoc(90, res)), 90)
     case Perm(loc, perm) =>
       (phrase("Perm(", loc, ",", space, perm, ")"), 100)
     case PointsTo(loc, perm, value) =>
@@ -849,6 +851,10 @@ case class Printer(out: Appendable,
       (phrase(assoc(100, arr), "[", index, "]"), 100)
     case PointerSubscript(pointer, index) =>
       (phrase(assoc(100, pointer), "[", index, "]"), 100)
+    case PointerBlockOffset(pointer) =>
+      (phrase("pointer_block(", pointer ,")"), 100)
+    case PointerBlockLength(pointer) =>
+      (phrase("block_length(", pointer ,")"), 100)
     case Cons(x, xs) =>
       (phrase(bind(87, x), space, "::", space, assoc(87, xs)), 87)
     case Head(xs) =>
@@ -970,7 +976,6 @@ case class Printer(out: Appendable,
       phrase(spaced(local.modifiers.map(NodePhrase)), space, local.t, space, javaDecls(local.decls))
     case defn: CFunctionDefinition[_] =>
       control(phrase(spaced(defn.specs.map(NodePhrase)), space, defn.declarator), defn.body)
-    case decl: CGlobalDeclaration[_] => decl
     case ns: JavaNamespace[_] =>
       phrase(
         if(ns.pkg.nonEmpty) statement("package", space, ns.pkg.get) else phrase(),
@@ -1208,6 +1213,13 @@ case class Printer(out: Appendable,
     case CSpecificationType(t) => say(t)
     case CTypeQualifierDeclarationSpecifier(typeQual) => say(typeQual)
     case CKernel() => say("__kernel")
+    case GPULocal() => say(syntax(
+      Cuda -> phrase("__shared__"),
+      OpenCL -> phrase("__local"),
+    ))
+    case GPUGlobal() => say(syntax(
+      OpenCL -> phrase("__global"),
+      ))
   }
 
   def printCTypeQualifier(node: CTypeQualifier[_]): Unit = node match {

col/src/main/java/vct/col/util/AstBuildHelpers.scala

@@ -316,10 +316,13 @@ object AstBuildHelpers {
     exprs.reduceOption(And(_, _)).getOrElse(tt)
 
   def unfoldPredicate[G](p: AccountedPredicate[G]): Seq[Expr[G]] = p match {
-    case UnitAccountedPredicate(pred) => Seq(pred)
+    case UnitAccountedPredicate(pred) => unfoldStar(pred)
     case SplitAccountedPredicate(left, right) => unfoldPredicate(left) ++ unfoldPredicate(right)
   }
 
+  def filterPredicate[G](p: AccountedPredicate[G], f: Expr[G] => Boolean): AccountedPredicate[G] =
+    foldPredicate(unfoldPredicate(p).filter(f))(p.o)
+
   def mapPredicate[G1, G2](p: AccountedPredicate[G1], f: Expr[G1] => Expr[G2]): AccountedPredicate[G2] = p match {
     case UnitAccountedPredicate(pred) => UnitAccountedPredicate(f(pred))(p.o)
     case SplitAccountedPredicate(left, right) => SplitAccountedPredicate(mapPredicate(left, f), mapPredicate(right, f))(p.o)
@@ -354,6 +357,12 @@ object AstBuildHelpers {
     case SplitAccountedPredicate(left, right) => Star(foldStar(left), foldStar(right))
   }
 
+  def foldPredicate[G](exprs: Seq[Expr[G]])(implicit o: Origin): AccountedPredicate[G] =
+    exprs
+      .map(e => UnitAccountedPredicate(e)(e.o))
+      .reduceOption[AccountedPredicate[G]](SplitAccountedPredicate(_, _))
+      .getOrElse(UnitAccountedPredicate(tt))
+
   def foldOr[G](exprs: Seq[Expr[G]])(implicit o: Origin): Expr[G] =
     exprs.reduceOption(Or(_, _)).getOrElse(ff)
 }

parsers/lib/antlr4/LangCParser.g4

@@ -259,6 +259,8 @@ storageClassSpecifier
     |   '_Thread_local'
     |   'auto'
     |   'register'
+    | gpgpuLocalMemory
+    | gpgpuGlobalMemory
     ;
 
 typeSpecifier

parsers/lib/antlr4/LangGPGPULexer.g4

@@ -5,6 +5,8 @@ GPGPU_LOCAL_BARRIER: '__vercors_local_barrier__';
 GPGPU_GLOBAL_BARRIER: '__vercors_global_barrier__';
 GPGPU_KERNEL: '__vercors_kernel__';
 GPGPU_ATOMIC: '__vercors_atomic__';
+GPGPU_GLOBAL_MEMORY: '__global';
+GPGPU_LOCAL_MEMORY: '__local';
 
 GPGPU_CUDA_OPEN_EXEC_CONFIG: '<<<';
 GPGPU_CUDA_CLOSE_EXEC_CONFIG: '>>>';

parsers/lib/antlr4/LangGPGPUParser.g4

@@ -16,4 +16,8 @@ gpgpuAtomicBlock
     : valEmbedWith? GPGPU_ATOMIC compoundStatement valEmbedThen?
     ;
 
-gpgpuKernelSpecifier: GPGPU_KERNEL;
+gpgpuKernelSpecifier: GPGPU_KERNEL;
+
+gpgpuLocalMemory: GPGPU_LOCAL_MEMORY;
+
+gpgpuGlobalMemory: GPGPU_GLOBAL_MEMORY;

parsers/lib/antlr4/SpecLexer.g4

@@ -135,6 +135,8 @@ POINTER: '\\pointer';
 POINTER_INDEX: '\\pointer_index';
 POINTER_BLOCK_LENGTH: '\\pointer_block_length';
 POINTER_BLOCK_OFFSET: '\\pointer_block_offset';
+POINTER_LENGTH: '\\pointer_length';
+SHARED_MEM_SIZE: '\\shared_mem_size';
 VALUES: '\\values';
 VCMP: '\\vcmp';
 VREP: '\\vrep';

parsers/lib/antlr4/SpecParser.g4

@@ -177,6 +177,7 @@ valPrimaryPermission
  | '\\pointer_index' '(' langExpr ',' langExpr ',' langExpr ')' # valPointerIndex
  | '\\pointer_block_length' '(' langExpr ')' # valPointerBlockLength
  | '\\pointer_block_offset' '(' langExpr ')' # valPointerBlockOffset
+ | '\\pointer_length' '(' langExpr ')' # valPointerLength
  ;
 
 valPrimaryBinder
@@ -253,6 +254,7 @@ valPrimary
  | '\\type' '(' langType ')' # valTypeValue
  | 'held' '(' langExpr ')' # valHeld
  | LANG_ID_ESCAPE # valIdEscape
+ | '\\shared_mem_size' '(' langExpr ')' # valSharedMemSize
  ;
 
 // Out spec: defined meaning: a language local

parsers/src/main/java/vct/parsers/ColCParser.scala

@@ -24,7 +24,8 @@ case class ColCParser(override val originProvider: OriginProvider,
                       cc: Path,
                       systemInclude: Path,
                       otherIncludes: Seq[Path],
-                      defines: Map[String, String]) extends Parser(originProvider, blameProvider) with LazyLogging {
+                      defines: Map[String, String],
+                      language: Language) extends Parser(originProvider, blameProvider) with LazyLogging {
   def interpret(localInclude: Seq[Path], input: String, output: String): Process = {
     var command = Seq(cc.toString, "-C", "-E")
 

src/main/java/vct/parsers/Language.scala → parsers/src/main/java/vct/parsers/Language.scala

@@ -3,7 +3,8 @@ package vct.parsers
 case object Language {
   def fromFilename(filename: String): Option[Language] =
     filename.split('.').last match {
-      case "cl" | "c" | "cu" => Some(C)
+      case "cl" | "c" => Some(C)
+      case "cu" => Some(CUDA)
       case "i" => Some(InterpretedC)
       case "java" => Some(Java)
       case "pvl" => Some(PVL)
@@ -12,6 +13,7 @@ case object Language {
     }
 
   case object C extends Language
+  case object CUDA extends Language
   case object InterpretedC extends Language
   case object Java extends Language
   case object PVL extends Language

parsers/src/main/java/vct/parsers/ParseResult.scala

@@ -4,11 +4,12 @@ import vct.col.ast.{GlobalDeclaration, VerificationContext}
 import vct.col.util.ExpectedError
 
 case object ParseResult {
-  def reduce[G](parses: Seq[ParseResult[G]]): ParseResult[G] =
+  def reduce[G](parses: Seq[(ParseResult[G], Option[Language])]): (ParseResult[G], Option[Language]) =
     parses.reduceOption((l, r) => (l, r) match {
-      case (ParseResult(declsLeft, expectedLeft), ParseResult(declsRight, expectedRight)) =>
-        ParseResult(declsLeft ++ declsRight, expectedLeft ++ expectedRight)
-    }).getOrElse(ParseResult(Nil, Nil))
+      case ((ParseResult(declsLeft, expectedLeft), l1), (ParseResult(declsRight, expectedRight), l2)) =>
+        val lan = if(l1 == l2) l1 else None
+        (ParseResult(declsLeft ++ declsRight, expectedLeft ++ expectedRight), lan)
+    }).getOrElse((ParseResult(Nil, Nil), None))
 }
 
 case class ParseResult[G](decls: Seq[GlobalDeclaration[G]], expectedErrors: Seq[ExpectedError])

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

@@ -82,6 +82,8 @@ case class CToCol[G](override val originProvider: OriginProvider, override val b
     case StorageClassSpecifier3(_) => ??(storageClass)
     case StorageClassSpecifier4(_) => ??(storageClass)
     case StorageClassSpecifier5(_) => ??(storageClass)
+    case StorageClassSpecifier6(_) => GPULocal()
+    case StorageClassSpecifier7(_) => GPUGlobal()
   }
 
   def convert(implicit typeSpec: TypeSpecifierContext): CTypeSpecifier[G] = typeSpec match {
@@ -956,6 +958,10 @@ case class CToCol[G](override val originProvider: OriginProvider, override val b
     case ValPointerIndex(_, _, ptr, _, idx, _, perm, _) => PermPointerIndex(convert(ptr), convert(idx), convert(perm))
     case ValPointerBlockLength(_, _, ptr, _) => PointerBlockLength(convert(ptr))(blame(e))
     case ValPointerBlockOffset(_, _, ptr, _) => PointerBlockOffset(convert(ptr))(blame(e))
+    case ValPointerLength(_, _, ptr, _) =>
+      val convertedPtr = convert(ptr)
+      val blameExpr = blame(e)
+      PointerBlockLength(convertedPtr)(blameExpr) - PointerBlockOffset(convertedPtr)(blameExpr)
   }
 
   def convert(implicit e: ValPrimaryBinderContext): Expr[G] = e match {
@@ -1033,6 +1039,7 @@ case class CToCol[G](override val originProvider: OriginProvider, override val b
     case ValTypeValue(_, _, t, _) => TypeValue(convert(t))
     case ValHeld(_, _, obj, _) => Held(convert(obj))
     case ValIdEscape(text) => local(e, text.substring(1, text.length-1))
+    case ValSharedMemSize(_, _, ptr, _) => SharedMemSize(convert(ptr))
   }
 
   def convert(implicit e: ValExprContext): Expr[G] = e match {