Merge pull request #715 from utwente-fmt/enable-gpgpu-testing

Enable GPGPU examples for testing

col/src/main/java/vct/col/ast/type/TypeExpression.scala

@@ -38,6 +38,12 @@ case class TypeExpression(val operator:TypeOperator, val types:List[Type]) exten
   override def isNumeric: Boolean =
     if (isLeaky) firstType.isNumeric else false
 
+  override def isIntegerType: Boolean =
+    if (isLeaky) firstType.isIntegerType else false
+
+  override def isInteger: Boolean =
+    if (isLeaky) firstType.isInteger else false
+
   override def supertypeof(context: ProgramUnit, t: Type): Boolean =
     if (isLeaky) firstType.supertypeof(context, t) else false
 

examples/gpgpu/ASSSP.cu

@@ -1,4 +1,10 @@
 //:: case ASSSP
+
+/* Currently this file does not pass because of some renaming errors. Mohsen Safari might have a version in which
+ * data-race freedom is verified, and which was also used in his ASSSP paper. This file might be included in the future,
+ * and can then replace this file.
+ */
+
 /***********************************************************************************
 Created by Mohsen Safari.
 ************************************************************************************/

examples/gpgpu/ASSSPv3.cu

@@ -1,4 +1,5 @@
 //:: case ASSSPv3
+//:: tool silicon
 /***********************************************************************************
 Created by Mohsen Safari.
 ************************************************************************************/

examples/gpgpu/ASSSPv4.cu

@@ -1,4 +1,9 @@
 //:: case ASSSPv4
+
+/* Currently this file does not verify because CUDA features are needed that VerCors doesn't support yet. This file
+ * is included in the example folder to serve as an example of CUDA features we might want in the future.
+ */
+
 /***********************************************************************************
 Created by Mohsen Safari.
 ************************************************************************************/

examples/gpgpu/GPGPU-Example-updates.cu

@@ -1,5 +1,10 @@
 //:: case GPGPUExampleUpdates
 
+/* This is the realistic version of GPGPU-Example.cu, with the difference that this version uses actual CUDA functions,
+ * such as cudaMemcpy. Unfortunately this file cannot be verified yet as VerCors does not yet support these primitives.
+ * Therefore it is not included in the test suite.
+ */
+
 /***********************************************************************************
 Created by Mohsen Safari.
 ************************************************************************************/

examples/gpgpu/GPGPU-Example.cu

@@ -1,4 +1,11 @@
 //:: case GPGPUExample
+//:: tool silicon
+
+/* This is the verifiable version of GPGPU-Example-updates.cu, with the difference being that we use custom functions
+ * for modelling the GPU here (vercorsCudaMalloc, vercorsCudaFreeInt, etc.) instead of actual CUDA functions. This
+ * example is verified to be memory safe and has some functional properties.
+ */
+
 /***********************************************************************************
 Created by Mohsen Safari.
 ************************************************************************************/
@@ -22,7 +29,7 @@ __global__ void CUDAKernel(int* g_array1, int* g_array2, int N)
 {
   int tid = blockIdx.x * N + threadIdx.x;
   //@ assert tid == \gtid;
-  atomicMin(g_array1 + tid, g_array2[tid]) /*@ then { assert false && false; } */;
+  atomicMin(g_array1 + tid, g_array2[tid]);
 }
 
 //@ ensures \pointer(\result, N, write);

examples/gpgpu/cuda.cu

@@ -1,4 +1,5 @@
 //:: cases BasicCuda
+//:: tool silicon
 //:: verdict Pass
 
 #include <cuda.h>

examples/gpgpu/opencl.c

@@ -1,4 +1,5 @@
 //:: cases BasicOpenCL
+//:: tool silicon
 //:: verdict Pass
 
 #include <opencl.h>