Merge pull request #1126 from utwente-fmt/sycl-examples-and-bugfixes

More sycl examples and bugfixes

examples/concepts/cpp/Arrays.cpp

@@ -18,4 +18,18 @@ int sumWithLast(int a[], int size, int b) {
 //@ ensures a[2] == 5;
 void writeToArray(int a[], int size) {
 	a[2] = 5;
+}
+
+//@ ensures \pointer(\result, 2, read);
+//@ ensures \result[0] == 10 && \result[1] == 6;
+int* createLocalArray() {
+  int a[] = {4,5,6};
+  //@ assert \pointer(a, 3, read) ** a[0] == 4 ** a[1] == 5 ** a[2] == 6;
+  int b[2] = {7,a[2]};
+  //@ assert \pointer(b, 2, write) ** b[0] == 7 ** b[1] == 6;
+  int c[3];
+  //@ assert \pointer(c, 3, write);
+  c[1] = 10;
+  b[0] = c[1];
+  return b;
 }

examples/concepts/cpp/Pointers.cpp

@@ -4,9 +4,13 @@
 //:: verdict Pass
 
 //@ context \pointer(ints, size, write);
+//@ context \pointer(p, size, write);
 void test(int ints[], int size, int* p) {
 	int* intsPtr = ints;
 	//@ assert intsPtr == ints;
 
+	int* pPtr = p;
+  //@ assert pPtr == p;
+
 	void* voidPtr = nullptr;
 }

examples/concepts/cpp/methods/ContextAndContextEverywhere.cpp

@@ -4,19 +4,16 @@
 //:: verdict Pass
 
 //@ context b != 0;
-// requires b != 0;
-// ensures b != 0;
 int div(int a, int b) {
+  //@ assert b != 0;
 	return a / b;
 }
 
 //@ context_everywhere number > 0;
-// requires number > 0;
-// ensures number > 0;
 int factorial(int number) {
 	int result = 1;
-	// loop_invariant number > 0;
 	for(int i = 2; i <= number; i++) {
+	  //@ assert number > 0;
 		result *= i;
 	}
 	return result;

examples/concepts/cpp/methods/Overloading.cpp

@@ -0,0 +1,19 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases Overloading
+//:: tools silicon
+//:: verdict Pass
+
+//@ ensures \result == 1;
+int method(int number);
+
+//@ ensures \result == 2;
+int method(float number);
+
+//@ ensures \result == 3;
+int method(int number, int number2);
+
+void test() {
+  //@ assert method(1) == 1;
+  //@ assert method(1.0f) == 2;
+  //@ assert method(1, 2) == 3;
+}

examples/concepts/sycl/buffers/BufferDeclarations.cpp

@@ -0,0 +1,12 @@
+#include <sycl/sycl.hpp>
+
+/*@
+  requires \pointer(a, 10, write);
+  requires \pointer(b, 10, write);
+  requires \pointer(c, 10, write);
+*/
+void test(bool a[], int* b, float c[]) {
+  sycl::buffer<bool, 1> aBuffer = sycl::buffer<bool>(a, sycl::range<1>(10));
+  sycl::buffer<int, 2> bBuffer = sycl::buffer<int, 2>(b, sycl::range<2>(2, 5));
+  sycl::buffer<float, 3> cBuffer = sycl::buffer(c, sycl::range<3>(2, 5, 1));
+}

examples/concepts/sycl/buffers/NegativeRange.cpp

@@ -0,0 +1,6 @@
+#include <sycl/sycl.hpp>
+
+//@ requires \pointer(a, 10, write);
+void test(bool* a) {
+  sycl::buffer<bool, 1> aBuffer = sycl::buffer(a, sycl::range<1>(-1));
+}

examples/concepts/sycl/buffers/NoBufferReassign.cpp

@@ -1,8 +1,6 @@
 #include <sycl/sycl.hpp>
 
-/*@
-  requires \pointer(a, 10, write);
-*/
+//@ requires \pointer(a, 10, write);
 void test(bool* a) {
   sycl::buffer<bool, 1> aBuffer = sycl::buffer(a, sycl::range<1>(10));
   aBuffer = sycl::buffer(a, sycl::range<1>(10)); // Reassigning of buffers is not supported

examples/concepts/sycl/buffers/NoWritePermission.cpp

@@ -0,0 +1,6 @@
+#include <sycl/sycl.hpp>
+
+//@ requires \pointer(a, 10, read);
+void test(bool* a) {
+  sycl::buffer<bool, 1> aBuffer = sycl::buffer(a, sycl::range<1>(10));
+}

examples/concepts/sycl/buffers/ReadDataInBufferScope.cpp

@@ -1,10 +1,7 @@
 #include <sycl/sycl.hpp>
 
-/*@ 
-  requires \pointer(a, 10, write);
-*/
+//@ requires \pointer(a, 10, write);
 void test(bool* a) {
   sycl::buffer<bool, 1> aBuffer = sycl::buffer(a, sycl::range<1>(10));
-
   bool x = a[5]; // Not allowed
 }

examples/concepts/sycl/buffers/ReleaseFromBuffer.cpp → examples/concepts/sycl/buffers/ReleaseDataFromBuffer.cpp

@@ -1,13 +1,9 @@
 #include <sycl/sycl.hpp>
 
-/*@ 
-  requires \pointer(a, 10, write);
-*/
+//@ requires \pointer(a, 10, write);
 void test(bool* a) {
   {
     sycl::buffer<bool, 1> aBuffer = sycl::buffer(a, sycl::range<1>(10));
-
-    int b = 20;
   }
   // Buffer should be destroyed now, so permissions should have been given back
   a[5] = true;

examples/concepts/sycl/buffers/TooSmallBuffer.cpp → examples/concepts/sycl/buffers/SmallerBuffer.cpp

@@ -1,8 +1,6 @@
 #include <sycl/sycl.hpp>
 
-/*@ 
-  requires \pointer(a, 10, write);
-*/
+//@ requires \pointer(a, 10, write);
 void test(bool* a) {
   sycl::buffer<bool, 1> aBuffer = sycl::buffer<bool, 1>(a, sycl::range<1>(9));
   a[9] = true;  // Should be allowed as buffer only claimed indices 0-8

examples/concepts/sycl/buffers/TooBigBuffer.cpp

@@ -1,8 +1,7 @@
 #include <sycl/sycl.hpp>
 
-/*@ 
-  requires \pointer(a, 10, write);
-*/
+//@ requires \pointer(a, 10, write);
 void test(bool* a) {
-  sycl::buffer<bool, 1> aBuffer = sycl::buffer(a, sycl::range<1>(11)); // Buffer to big, so should fail
+  // a is only guaranteed to have 10 elements, so cannot make buffer with 11
+  sycl::buffer<bool, 1> aBuffer = sycl::buffer(a, sycl::range<1>(11));
 }

examples/concepts/sycl/buffers/TwoBuffersForSameData.cpp

@@ -1,8 +1,6 @@
 #include <sycl/sycl.hpp>
 
-/*@ 
-  requires \pointer(a, 10, write);
-*/
+//@ requires \pointer(a, 10, write);
 void test(bool* a) {
   sycl::buffer<bool, 1> aBuffer = sycl::buffer(a, sycl::range<1>(10));
   sycl::buffer<bool, 1> aaBuffer = sycl::buffer(a, sycl::range<1>(10)); // Should fail as the previous buffer already claimed indices 0-9

examples/concepts/sycl/buffers/UnfoldingExclusiveHostDataAccessPredicate.cpp

@@ -1,8 +1,6 @@
 #include <sycl/sycl.hpp>
 
-/*@
-  requires \pointer(a, 10, write);
-*/
+//@ requires \pointer(a, 10, write);
 void test(bool* a) {
   sycl::buffer<bool, 1> aBuffer = sycl::buffer(a, sycl::range<1>(10));
 

examples/concepts/sycl/buffers/WriteDataInBufferScope.cpp

@@ -1,8 +1,6 @@
 #include <sycl/sycl.hpp>
 
-/*@ 
-  requires \pointer(a, 10, write);
-*/
+//@ requires \pointer(a, 10, write);
 void test(bool* a) {
   sycl::buffer<bool, 1> aBuffer = sycl::buffer(a, sycl::range<1>(10));
 

examples/concepts/sycl/buffers/WrongGenericArgumentForConstructorHostdataType.cpp

@@ -0,0 +1,6 @@
+#include <sycl/sycl.hpp>
+
+//@ requires \pointer(a, 10, write);
+void test(bool a[]) {
+  sycl::buffer<int>(a, sycl::range<1>(10));
+}

examples/concepts/sycl/buffers/WrongGenericArgumentForConstructorRangeType1.cpp

@@ -0,0 +1,6 @@
+#include <sycl/sycl.hpp>
+
+//@ requires \pointer(a, 10, write);
+void test(bool a[]) {
+  sycl::buffer<bool, 2>(a, sycl::range<1>(10));
+}

examples/concepts/sycl/buffers/WrongGenericArgumentForConstructorRangeType2.cpp

@@ -0,0 +1,7 @@
+#include <sycl/sycl.hpp>
+
+//@ requires \pointer(a, 10, write);
+void test(bool a[]) {
+  // generic arg <int> will be expanded to <int, 1>
+  sycl::buffer<int>(a, sycl::range<2>(10));
+}

examples/concepts/sycl/buffers/WrongGenericArgumentForHostdataType.cpp

@@ -0,0 +1,6 @@
+#include <sycl/sycl.hpp>
+
+//@ requires \pointer(a, 10, write);
+void test(bool a[]) {
+  sycl::buffer<int, 1> aBuffer = sycl::buffer(a, sycl::range<1>(10));
+}

examples/concepts/sycl/buffers/WrongGenericArgumentForRangeType.cpp

@@ -0,0 +1,6 @@
+#include <sycl/sycl.hpp>
+
+//@ requires \pointer(a, 10, write);
+void test(bool a[]) {
+  sycl::buffer<bool, 2> aBuffer = sycl::buffer(a, sycl::range<1>(10));
+}

examples/concepts/sycl/dataAccessors/AccessorDeclarations.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/AccessorGetRangeDimensionOutOfBounds.cpp → examples/concepts/sycl/dataAccessors/GetRangeDimensionOutOfBounds1.cpp

@@ -1,17 +1,14 @@
 #include <sycl/sycl.hpp>
 
-/*@
-  requires \pointer(a, 6, write);
-*/
+//@ requires \pointer(a, 6, write);
 void test(int* a) {
 	sycl::queue myQueue;
 
   sycl::buffer<int, 2> aBuffer = sycl::buffer(a, sycl::range<2>(2, 3));
 
 	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/dataAccessors/GetRangeDimensionOutOfBounds2.cpp

@@ -0,0 +1,21 @@
+#include <sycl/sycl.hpp>
+
+//@ requires \pointer(a, 6, write);
+void test(int* a) {
+	sycl::queue myQueue;
+
+  sycl::buffer<int, 2> aBuffer = sycl::buffer(a, sycl::range<2>(2, 3));
+
+	myQueue.submit(
+  	[&](sycl::handler& cgh) {
+
+      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) {
+          a_accessor.get_range().get(-1); // Dimension cannot be negative
+        }
+      );
+  	}
+  );
+}

examples/concepts/sycl/accessors/MissingRangeRequirements.cpp → examples/concepts/sycl/dataAccessors/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),
         /*@