Added full examples and fixed wrongly inferred data accessor types in…

… declarations

examples/concepts/sycl/accessors/AccessorGetRangeDimensionOutOfBounds.cpp

@@ -11,7 +11,7 @@ void test(int* a) {
 	myQueue.submit(
   	[&](sycl::handler& cgh) {
 
-      sycl::accessor<int, 2> a_accessor = sycl::accessor(aBuffer, cgh, sycl::read_only);
+      sycl::accessor<int, 2, sycl::access_mode::read> a_accessor = sycl::accessor(aBuffer, cgh, sycl::read_only);
 
       cgh.parallel_for(sycl::range<2>(2, 3),
         [=] (sycl::item<2> it) {

examples/concepts/sycl/accessors/AllAccessorDeclarations.cpp

@@ -0,0 +1,47 @@
+#include <sycl/sycl.hpp>
+
+/*@
+  requires \pointer(a, 12, write);
+  requires \pointer(b, 12, write);
+  requires \pointer(c, 12, write);
+  requires \pointer(d, 12, write);
+*/
+void test(int* a, int* b, int* c, int* d) {
+	sycl::queue myQueue;
+
+  sycl::buffer<int, 1> aBuffer = sycl::buffer(a, sycl::range<1>(12));
+  sycl::buffer<int, 2> bBuffer = sycl::buffer(b, sycl::range<2>(3, 4));
+  sycl::buffer<int, 3> cBuffer = sycl::buffer(c, sycl::range<3>(2, 3, 2));
+  sycl::buffer<int, 1> dBuffer = sycl::buffer(d, sycl::range<1>(12));
+
+	myQueue.submit(
+  	[&](sycl::handler& cgh) {
+
+      sycl::accessor<int, 1, sycl::access_mode::read> a_accessor = sycl::accessor(aBuffer, cgh, sycl::read_only);
+      sycl::accessor<int, 2> b_accessor = sycl::accessor(bBuffer, cgh, sycl::read_write);
+      sycl::accessor<int, 2, sycl::access_mode::read_write> bb_accessor = sycl::accessor<int, 2>(bBuffer, cgh, sycl::read_write);
+      sycl::accessor<int, 2, sycl::access_mode::read_write> bbb_accessor = sycl::accessor<int, 2, sycl::access_mode::read_write>(bBuffer, cgh, sycl::read_write);
+      sycl::accessor<int, 3, sycl::access_mode::read> c_accessor = sycl::accessor(cBuffer, cgh, sycl::read_only);
+      sycl::accessor<int, 3, sycl::access_mode::read> ccc_accessor = sycl::accessor<int, 3, sycl::access_mode::read>(cBuffer, cgh, sycl::read_only);
+      sycl::accessor<int, 1> d_accessor = sycl::accessor<int>(dBuffer, cgh, sycl::read_write);
+
+      cgh.parallel_for(sycl::range<1>(1),
+        /*@
+          context 1 < a_accessor.get_range().get(0);
+          context 1 < b_accessor.get_range().get(0);
+          context 2 < b_accessor.get_range().get(1);
+          context 1 < c_accessor.get_range().get(0);
+          context 2 < c_accessor.get_range().get(1);
+          context 1 < c_accessor.get_range().get(2);
+          context it.get_range(0) == 1;
+          context Perm(a_accessor[1], read);
+          context Perm(b_accessor[1][2], write);
+          context Perm(c_accessor[1][2][1], read);
+        */
+        [=] (sycl::item<1> it) {
+//          b_accessor[1][2] = c_accessor[1][2][1] + a_accessor[1];
+        }
+      );
+  	}
+  );
+}

examples/concepts/sycl/accessors/DoNotWriteOnReadAccessorWithDoubleAccessors.cpp

@@ -9,7 +9,7 @@ void test(int* a) {
 
     myQueue.submit(
       [&](sycl::handler& cgh) {
-        sycl::accessor<int, 1> a_accessor = sycl::accessor(aBuffer, cgh, sycl::read_only);
+        sycl::accessor<int, 1, sycl::access_mode::read> a_accessor = sycl::accessor(aBuffer, cgh, sycl::read_only);
         sycl::accessor<int, 1> aa_accessor = sycl::accessor(aBuffer, cgh, sycl::read_write);
 
         cgh.parallel_for(sycl::range<1>(12),

examples/concepts/sycl/accessors/MissingRangeRequirements.cpp

@@ -11,7 +11,7 @@ void test(int* a) {
 	myQueue.submit(
   	[&](sycl::handler& cgh) {
 
-      sycl::accessor<int, 3> a_accessor = sycl::accessor(aBuffer, cgh, sycl::read_only);
+      sycl::accessor<int, 3, sycl::access_mode::read> a_accessor = sycl::accessor(aBuffer, cgh, sycl::read_only);
 
       cgh.parallel_for(sycl::range<1>(1),
         /*@

examples/concepts/sycl/accessors/TwoReadKernels.cpp

@@ -12,15 +12,15 @@ void test(int* a) {
 
 	myQueue.submit(
   	[&](sycl::handler& cgh) {
-      sycl::accessor<int, 1> a_accessor = sycl::accessor(aBuffer, cgh, sycl::read_only);
+      sycl::accessor<int, 1, sycl::access_mode::read> a_accessor = sycl::accessor(aBuffer, cgh, sycl::read_only);
 
       cgh.parallel_for(sycl::range<1>(1), [=] (sycl::item<1> it) {});
   	}
   );
 
   myQueue.submit(
     [&](sycl::handler& cgh) {
-      sycl::accessor<int, 1> a_accessor = sycl::accessor(aBuffer, cgh, sycl::read_only);
+      sycl::accessor<int, 1, sycl::access_mode::read> a_accessor = sycl::accessor(aBuffer, cgh, sycl::read_only);
 
       cgh.parallel_for(sycl::range<1>(1), [=] (sycl::item<1> it) {});
     }

examples/concepts/sycl/accessors/TwoWriteKernels.cpp

@@ -8,7 +8,7 @@ void test(int* a) {
 
   sycl::buffer<int, 1> aBuffer = sycl::buffer<int, 1>(a, sycl::range<1>(12));
 
-  // Two kernels writing to the same buffer is not allowed
+  // Two kernels writing to the same buffer wait on each other
 
 	myQueue.submit(
   	[&](sycl::handler& cgh) {

examples/concepts/sycl/accessors/WriteToReadAccessor.cpp

@@ -11,7 +11,7 @@ void test(int* a) {
 	myQueue.submit(
   	[&](sycl::handler& cgh) {
 
-      sycl::accessor<int, 1> a_accessor = sycl::accessor(aBuffer, cgh, sycl::read_only);
+      sycl::accessor<int, 1, sycl::access_mode::read> a_accessor = sycl::accessor(aBuffer, cgh, sycl::read_only);
 
       cgh.parallel_for(sycl::range<1>(10),
         /*@

examples/concepts/sycl/fullExamples/MatrixTransposeWithF.cpp

@@ -0,0 +1,91 @@
+#include <sycl/sycl.hpp>
+
+// helper function to be used in verification statements
+/*@
+  requires id0 >= 0 && id0 < r0 && id1 >= 0 && id1 < r1;
+  requires r0 >= 0 && r1 >= 0;
+  ensures \result == id1 + (id0 * r1);
+  ensures \result >= 0 && \result < r0 * r1;
+  pure int linearize(int id0, int id1, int r0, int r1);
+*/
+
+//@ pure
+float f(float value);
+
+/*@
+  context row_size >= 0 && col_size > 0;
+  context (row_size * col_size) % col_size == 0;
+  context \pointer(matrix, row_size * col_size, write);
+  context \pointer(result, col_size * row_size, write);
+  ensures (\forall int r, int c; r >= 0 && r < row_size && c >= 0 && c < col_size;
+    result[linearize(c, r, col_size, row_size)] == f(matrix[linearize(r, c, row_size, col_size)])
+  );
+*/
+void transpose_with_f(float matrix[], int row_size, int col_size, float* result) {
+	sycl::queue myQueue;
+
+	float temp[row_size * col_size];
+
+  sycl::buffer<float, 2> matrix_buffer = sycl::buffer(matrix, sycl::range<2>(row_size, col_size));
+  sycl::buffer<float, 1> temp_buffer = sycl::buffer(temp, sycl::range<1>(row_size * col_size));
+
+  // Apply f to all elements of matrix and store in temp
+  myQueue.submit(
+    [&](sycl::handler& cgh) {
+      sycl::accessor<float, 2, sycl::access_mode::read> matrix_acc = sycl::accessor(matrix_buffer, cgh, sycl::read_only);
+      sycl::accessor<float, 1> temp_acc = sycl::accessor(temp_buffer, cgh, sycl::read_write);
+
+      cgh.parallel_for(sycl::range<2>(row_size, col_size),
+        /*@
+          context it.get_id(0) < matrix_acc.get_range().get(0);
+          context it.get_id(1) < matrix_acc.get_range().get(1);
+          context Perm(matrix_acc[it.get_id(0)][it.get_id(1)], read);
+          context it.get_linear_id() < temp_acc.get_range().get(0);
+          context Perm(temp_acc[it.get_linear_id()], write);
+          ensures temp_acc[it.get_linear_id()] == f(matrix_acc[it.get_id(0)][it.get_id(1)]);
+        */
+        [=] (sycl::item<2> it) {
+          temp_acc[it.get_linear_id()] = f(matrix_acc[it.get_id(0)][it.get_id(1)]);
+        }
+      );
+    }
+  );
+
+  bool done = false;
+  {
+    sycl::buffer<float, 2> result_buffer = sycl::buffer(result, sycl::range<2>(col_size, row_size));
+    // Transpose matrix and store in result
+    // Implicitly waits on previous kernel as that kernel writes to temp_buffer and this kernel needs read access to temp_buffer
+    sycl::event transpose_event = myQueue.submit(
+      [&](sycl::handler& cgh) {
+        sycl::accessor<float, 1, sycl::access_mode::read> temp_acc = sycl::accessor(temp_buffer, cgh, sycl::read_only);
+        sycl::accessor<float, 2> result_acc = sycl::accessor(result_buffer, cgh, sycl::read_write);
+
+
+        // result_acc.get_range().get(0) == col_size, cannot use col_size itself here
+        sycl::local_accessor<float, 1> temp_local_acc = sycl::local_accessor<float, 1>(sycl::range<1>(result_acc.get_range().get(0)), cgh);
+
+        cgh.parallel_for(sycl::nd_range<1>(sycl::range<1>(row_size * col_size), sycl::range<1>(col_size)),
+          /*@
+            context it.get_global_id(0) < temp_acc.get_range().get(0);
+            context Perm(temp_acc[it.get_global_id(0)], read);
+            context it.get_local_id(0) < result_acc.get_range().get(0);
+            context it.get_group(0) < result_acc.get_range().get(1);
+            context Perm(result_acc[it.get_local_id(0)][it.get_group(0)], write);
+            context Perm(temp_local_acc[it.get_local_linear_id()], write);
+            ensures result_acc[it.get_local_id(0)][it.get_group(0)] == temp_acc[it.get_global_id(0)];
+          */
+          [=] (sycl::nd_item<1> it) {
+            temp_local_acc[it.get_local_linear_id()] = temp_acc[it.get_global_id(0)];
+            result_acc[it.get_local_id(0)][it.get_group(0)] = temp_local_acc[it.get_local_linear_id()];
+          }
+        );
+      }
+    );
+    transpose_event.wait(); // Explicitly wait till f has been applied to all elements of matrix
+    done = true;
+  }
+  // result_buffer has been destroyed so result is accessible again
+  //@ assert row_size > 0 ==> result[linearize(0, 0, col_size, row_size)] == f(matrix[linearize(0, 0, row_size, col_size)]);
+}
+

examples/concepts/sycl/fullExamples/VectorAdd.cpp

@@ -0,0 +1,33 @@
+#include <sycl/sycl.hpp>
+
+/*@
+  context size >= 0;
+  context \pointer(a, size, write);
+  context \pointer(b, size, write);
+  context \pointer(c, size, write);
+  ensures (\forall int i; 0 <= i && i < size; c[i] == a[i] + b[i]);
+@*/
+void array_add(sycl::queue q, int size, int* a, int* b, int* c) {
+  sycl::buffer<int, 1> a_buf = sycl::buffer(a, sycl::range<1>(size));
+  sycl::buffer<int, 1> b_buf = sycl::buffer(b, sycl::range<1>(size));
+  sycl::buffer<int, 1> c_buf = sycl::buffer(c, sycl::range<1>(size));
+
+  sycl::event e = q.submit([&](sycl::handler& h) {
+    sycl::accessor<int, 1, sycl::access_mode::read> a_acc = sycl::accessor(a_buf, h, sycl::read_only);
+    sycl::accessor<int, 1, sycl::access_mode::read> b_acc = sycl::accessor(b_buf, h, sycl::read_only);
+    sycl::accessor<int, 1> c_acc = sycl::accessor(c_buf, h, sycl::read_write);
+
+    h.parallel_for(sycl::range<1>(size),
+      /*@
+        context it.get_id(0) < a_acc.get_range().get(0) ** Perm(a_acc[it.get_id(0)], read);
+        context it.get_id(0) < b_acc.get_range().get(0) ** Perm(b_acc[it.get_id(0)], read);
+        context it.get_id(0) < c_acc.get_range().get(0) ** Perm(c_acc[it.get_id(0)], write);
+        ensures c_acc[it.get_id(0)] == a_acc[it.get_id(0)] + b_acc[it.get_id(0)];
+      @*/
+      [=](sycl::item<1> it) {
+        int tid = it.get_id(0);
+        c_acc[tid] = a_acc[tid] + b_acc[tid];
+      }
+    );
+  });
+}

examples/concepts/sycl/kernels/NDRangeKernel.cpp

@@ -15,7 +15,7 @@ void test() {
 					int e = it.get_local_linear_id();
 					int f = it.get_local_range(0);
 
-					int g = it.get_group_id(0);
+					int g = it.get_group(0);
 					int h = it.get_group_linear_id();
 					int i = it.get_group_range(0);
 				}