Added support for SYCL's accessors and declarators.

[Ellen-Wittingen]

Added support for SYCL's accessors and declarators, so now data on the host can be copied to kernels and written back to the host when the kernels are done. An example of the supported usage of accessors and declarators can be seen below (taken from examples/concepts/sycl/accessors/GetKernelResult.cpp):

#include <sycl/sycl.hpp>

/*@ 
  requires \pointer(a, 10, write);
*/
void main(int* a) {
	sycl::queue myQueue;

  {
    sycl::buffer<int, 1> aBuffer = sycl::buffer(a, sycl::range<1>(10));

    myQueue.submit(
      [&](sycl::handler& cgh) {
        
        sycl::accessor<int, 1> a_accessor = sycl::accessor(aBuffer, cgh, sycl::read_write);

        cgh.parallel_for(sycl::range<1>(10),
          /*@
            context it.get_id(0) < a_accessor.get_range().get(0);
            context Perm(a_accessor[it.get_id(0)], write);
            ensures a_accessor[it.get_id(0)] == 10;
          */
          [=] (sycl::item<1> it) {
            a_accessor[it.get_id(0)] = 10;
          }
        );
      }
    );
  } // Leaving scope, so automatically wait on all running kernels to finish and write data back to the buffers

  //@ assert (\forall int i; i >= 0 && i < 10; a[i] == 10);

}

[pieter-bos]

I've not merged this yet because you are failing this test: https://github.com/utwente-fmt/vercors/actions/runs/6768903759/job/18394515499?pr=1100

[Ellen-Wittingen]

I've not merged this yet because you are failing this test: https://github.com/utwente-fmt/vercors/actions/runs/6768903759/job/18394515499?pr=1100

You mean this?

ExampleCoverage:
Not tested: examples/concepts/sycl/accessors/AllAccessModes.cpp
Not tested: examples/concepts/sycl/accessors/GetKernelResult.cpp
- should cover all examples in the examples directory *** FAILED ***
The test suite does not have a test entry that processes the above files. (ExampleCoverage.scala:70)

These two tests are commented out in SYCLTest, because they need a flag to pass, see my comment here

I see two options to solve this:

• Add the tests, but write them to expect an error for now vercors should error withCode 'CODE' example "concepts/sycl/accessors/AllAccessModes.cpp" and add a comment about the issue above these tests.
• Removing these tests from the examples directory.

These tests are quite important, as they test some core functionality of SYCL's data accessors. I also expect to add more example files for the next research questions which will probably have the same issue. So I think I would prefer the first option, what do you think?

[pieter-bos]

Right, sorry. Let's go for the first solution right now, I'll think about adding flags to test fixtures.

[Ellen-Wittingen]

I added the tests. I did have to add the line case Left(err: BlameUnreachable) if code.equals("unreachable:schematic") && err.message.equals("schematic") => to VercorsSpec to allow the tests to "pass"