Rewriting the SYCL encoding

examples/concepts/sycl/dataAccessors/AccessorInNDRange.cpp

@@ -1,7 +1,7 @@
 #include <sycl/sycl.hpp>
 
 /*@
-  requires \pointer(a, 10, write);
+  context \pointer(a, 10, write);
 */
 void test(int* a) {
 	sycl::queue myQueue;
@@ -28,6 +28,8 @@ void test(int* a) {
     );
   } // Leaving scope, which destroys aBuffer, which waits on the kernel to terminate as it uses aBuffer
 
+  //@ assert (\forall int i; 0 <= i && i < 10 ==> a[i] == a[sycl::linearize2(i/5, i%5, 2,5)]);
+
   //@ assert (\forall int i; i >= 0 && i < 10; a[i] == 10);
 
 }

examples/concepts/sycl/dataAccessors/MissingRangeRequirements.cpp

@@ -1,5 +1,9 @@
 #include <sycl/sycl.hpp>
+/*
 
+    This example is obsolete. Due to fixes in the scoping, the missing annotation here is not needed anymore.
+    I call it, "missing by design"
+*/
 /*@
   requires \pointer(a, 12, write);
 */
@@ -17,6 +21,8 @@ void test(int* a) {
         /*@
           requires 1 < a_accessor.get_range().get(0);
           requires 2 < a_accessor.get_range().get(1);
+          requires (\forall* int x = 0 .. a_accessor.get_range().get(0), int y = 0 .. a_accessor.get_range().get(1), int z = 0 .. a_accessor.get_range().get(2);
+            Perm(a_accessor[x][y][z], read));
         */
         [=] (sycl::item<1> it) { // Bound requirement for the 3rd index is missing, so cannot verify
           int a = a_accessor[1][2][1];

res/universal/res/cpp/sycl/sycl.hpp

@@ -1,5 +1,14 @@
 namespace sycl {
 
+  namespace h {
+    /*@
+      ensures (a>0 && b>0) ==> \result > 0;
+      ensures \result == a*b;
+      pure int mul(int a, int b) = a*b;
+
+    */
+  }
+
 	namespace event {
   	void wait();
   }
@@ -27,7 +36,7 @@ namespace sycl {
     requires id0 >= 0 && id0 < r0 && id1 >= 0 && id1 < r1;
     requires r0 > 0 && r1 > 0;
     ensures \result == sycl::linearize2formula(id0, id1, r1);
-    ensures \result >= 0 && \result < r0 * r1;
+    ensures \result >= 0 && \result < sycl::h::mul(r0,r1);
     ensures (\forall int ida0, int ida1;
       ida0 >= 0 && ida0 < r0 &&
       ida1 >= 0 && ida1 < r1 &&
@@ -36,7 +45,7 @@ namespace sycl {
     );
     pure int linearize2(int id0, int id1, int r0, int r1);
 
-    pure int linearize2formula(int id0, int id1, int r1) = id1 + (id0 * r1);
+    pure int linearize2formula(int id0, int id1, int r1) = id1 + sycl::h::mul(id0, r1);
 
     requires id0 >= 0 && id0 < r0 && id1 >= 0 && id1 < r1 && id2 >= 0 && id2 < r2;
     requires r0 > 0 && r1 > 0 && r2 > 0;

src/col/vct/col/ast/lang/sycl/SYCLTBufferImpl.scala

@@ -117,6 +117,7 @@ trait SYCLTBufferImpl[G] extends SYCLTBufferOps[G] {
       new Variable[G](TPointer(this.typ))(o.where(name = "hostData"))
     val sizeVar = new Variable[G](TCInt())(o.where(name = "size"))
     val indexVar = new Variable[G](TCInt())(o.where(name = "i"))
+    val indexVar2 = new Variable[G](TCInt())(o.where(name = "i"))
     val copyHostdataToBufferBlame = PanicBlame(
       "The generated method 'copy_hostData_to_buffer' should not throw any errors."
     )
@@ -150,6 +151,29 @@ trait SYCLTBufferImpl[G] extends SYCLTBufferOps[G] {
                 WritePerm(),
                 copyHostdataToBufferBlame,
               ),
+              Forall(
+                bindings = Seq(indexVar2),
+                triggers = Seq(
+                  Seq(ArraySubscript(result, Local[G](indexVar2.ref))(
+                    copyHostdataToBufferBlame
+                  ))
+                ),
+                body =
+                  (Local[G](indexVar2.ref) >= c_const(0) &&
+                    Local[G](indexVar2.ref) < Local[G](sizeVar.ref)) ==> Eq(
+                    PointerSubscript(
+                      Local[G](hostDataVar.ref),
+                      Local[G](indexVar2.ref),
+                    )(copyHostdataToBufferBlame),
+                    Old[G](
+                      PointerSubscript(
+                        Local[G](hostDataVar.ref),
+                        Local[G](indexVar2.ref),
+                      )(copyHostdataToBufferBlame),
+                      None
+                    )(copyHostdataToBufferBlame)
+                  ),
+              ),
               Forall(
                 bindings = Seq(indexVar),
                 triggers = Seq(

src/col/vct/col/resolve/lang/CPP.scala

@@ -188,7 +188,6 @@ case object CPP {
         getBaseTypeFromSpecs(returnedSpecs)
       case x => x
     }
-
   }
 
   def paramsFromDeclarator[G](declarator: CPPDeclarator[G]): Seq[CPPParam[G]] =

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

@@ -34,9 +34,7 @@ case object CoercionUtils {
       case (TResource(), TResourceVal()) => CoerceResourceResourceVal()
       case (TResourceVal(), TResource()) => CoerceResourceValResource()
       case (TBool(), TResource()) => CoerceBoolResource()
-      case (TBool(), TResourceVal()) =>
-        CoercionSequence(Seq(CoerceBoolResource(), CoerceResourceResourceVal()))
-
+      case (TBool(), TResourceVal()) => CoercionSequence(Seq(CoerceBoolResource(), CoerceResourceResourceVal()))
       case (_, TAnyValue()) => CoerceSomethingAnyValue(source)
 
       case (source @ TOption(innerSource), target @ TOption(innerTarget)) =>

src/parsers/antlr4/SpecLexer.g4

@@ -34,6 +34,9 @@ NEVER: EOF '=';
 // Must be able to contain identifiers from any frontend, so it's fine to over-approximate valid identifiers a bit.
 LANG_ID_ESCAPE: '`' ~[`]+ '`';
 
+VAL_PrependOp : '+:';
+VAL_AppendOp : ':+';
+
 VAL_RESOURCE: 'resource';
 VAL_PROCESS: 'process';
 VAL_FRAC: 'frac';

src/parsers/antlr4/SpecParser.g4

@@ -100,8 +100,8 @@ valImpOp: '-*' | '==>';
 valAndOp: '**';
 valInOp: '\\in';
 valMulOp: '\\';
-valPrependOp : '::';
-valAppendOp : '++'; // postfix issues? maybe disable in spec - no side effects?
+valPrependOp : '+:';
+valAppendOp : ':+'; // postfix issues? maybe disable in spec - no side effects?
 valPostfix
  : '[' '..' langExpr ']'
  | '[' langExpr '..' langExpr? ']'