Support for SYCL's basic and nd-range kernels

[Ellen-Wittingen]

This pull request adds support for SYCL's basic and nd-range kernels.

It supports the creation of new kernels with SYCL's submit method:

#include <sycl/sycl.hpp>

void main() {
  sycl::queue myQueue;

  sycl::event myEvent = myQueue.submit(
    [&](sycl::handler& cgh) {
      cgh.parallel_for(sycl::nd_range<2>(sycl::range<3>(6,4), sycl::range<2>(2,2)),
        /*@
          requires 1 + 2 == 3;
          ensures 3 * 5 == 15;
        */
        [=] (sycl::nd_item<2> it) {
          int a = 10;
        }
      );
    }
  );
  int a = 5;
  myEvent.wait();
}

Internally this block of code transformed into a class with a run method with a parallel block inside it, which holds the lambda function and contract written in the parallel_for parameters. Then sycl::event myEvent is assigned to an instance of the newly created class and is forked. This creates the following AST (after the language-specific rewrite pass):

...
class SYCL_EVENT_CLASS {
    requires 2 > 0;
    requires 6 >= 0;
    requires 6 % 2 == 0;
    requires 2 > 0;
    requires 4 >= 0;
    requires 4 % 2 == 0;
    requires [2 - 0][2 - 0][4 / 2 - 0][6 / 2 - 0](1 + 2 == 3);
    ensures [2 - 0][2 - 0][4 / 2 - 0][6 / 2 - 0](3 * 5 == 15);
    run {
        par SYCL_ND_RANGE_KERNEL(
            int GROUP_ID_0 = 0 .. 6 / 2,
            int GROUP_ID_1 = 0 .. 4 / 2,
            int LOCAL_ID_0 = 0 .. 2,
            int LOCAL_ID_1 = 0 .. 2
        )
        requires 1 + 2 == 3;
        ensures 3 * 5 == 15; {
            int a;
            a = 10;
        }
    }
}
void main() {
    ref myQueue;
    SYCL_EVENT_CLASS sycl_event_ref;
    sycl_event_ref = new SYCL_EVENT_CLASS();
    fork sycl_event_ref;
    int a;
    a = 5;
    join sycl_event_ref;
}

In SYCL, the host code does not wait on the submitted kernel to end before continuing. Therefore, the class containing the generated parellel block is forked. And when myEvent.wait() is called, which makes the host wait on the kernel code to end, the class instance is joined.

The methods of SYCL's item and nd_item which return the current (linear) thread id and range make use of the methods and their contracts inside the sycl.hpp header file.

Examples / tests for SYCL's kernels can be found in examples/concepts/sycl/kernels/ and test/main/vct/test/integration/examples/SYCLSpec.scala.

Lambda functions are only allowed in SYCL methods, if they are used anywhere else in C++ VerCors will throw an error.

To check if the kernel ranges are good, pre-conditions are added above the run method to check them (for example, for nd_ranges the global range should be divisible by the local range).

The comments on the previous pull request have also been addressed. The implementation of namespaces has changed, as I realized I only needed to be able to resolve methods inside them: now in the parsing stage the methods nested inside one or more namespaces get the names of the namespaces added in front of their name. This means that in the resolution stage, the methods can just be found by checking for a matching name, instead of the nested search it was before.