================
JSON File Format
================

The JSON file format accepted by GPUVerify has the following form::

  [ kernel_instantiation, ..., kernel_instantiation ]

where each ``kernel_instantiation`` is an object::

  {
    "language"         : "OpenCL",
    "endianness"       : string,
    "kernel_file"      : string,
    "local_size"       : [ number, ..., number ],
    "global_size"      : [ number, ..., number ],
    "global_offset"    : [ number, ..., number ],
    "compiler_flags"   : string,
    "entry_point"      : string,
    "kernel_arguments" : [ kernel_argument, ..., kernel_argument ],
    "host_api_calls"   : [ host_api_call, ..., host_api_call ]
  }

The value of ``language`` should always be the string ``OpenCL``.

The ``endianness`` can be set to ``big`` or ``little``.  This
specifies the endianness of the device on which the kernel was
captured.

The value of ``kernel_file`` is the name of an OpenCL source file
whose location is relative to the JSON file. The intended usage of
this latter value is to specify the file name of the file to which the
kernel is dumped upon interception.

If ``kernel_file`` has the value ``/some/path/foo.cl``, then if
preprocessing was applied after kernel interception the preprocessed
version of the file will be at ``/some/path/foo.pre.cl`` (where
``/some/path`` is the same as in ``kernel_file``).

The values of ``local_size``, ``global_size``, and ``global_offset``
are arrays of numbers satisfying the usual restrictions on the
``local_work_size``, ``global_work_size``, and ``global_offset``
arguments of ``clEnqueueNDRangeKernel``, respectively.

The ``compiler_flags`` value specifies the string passed to the kernel
compiler upon compilation of the kernel.

The value of ``entry_point`` specifies which kernel in the kernel
file needs to be verified.

The ``kernel_arguments`` field specifies properties of the concrete
argument values pass to the kernel during launch, where the nth
element of the array corresponds to the nth argument of the kernel.

The ``host_api_calls`` array specifies the source file locations of
relevant OpenCL host-side functions that were invoked leading up to
the original kernel launch.

The ``language``, ``kernel_file``, ``global_size``, and ``entry_point`` fields
are required.

The ``endianness``, ``local_size``, , ``global_offset``, ``kernel_arguments``
and ``host_api_calls`` are optional. Not specifiying ``local_size`` corresponds
to a ``NULL`` value being passed to ``clEnqueueNDRangeKernel`` (observe that
omitting ``local_size`` can significantly slow down verification with
GPUVerify). When ``global_offset`` is not specified, the offset is assumed to
be 0 in each dimension. When ``kernel_arguments`` is not specified the argument
values used during verification are assumed to be unconstrained.

Each ``kernel_argument`` is an object of one of the following four forms::

  {
    "type"  : "scalar",
    "value" : string
  }

::

  {
    "type" : "array",
    "size" : number,
    "address_space" : string,
    "flags" : [ string, ..., string ],
    "data" : string
  }

::

  {
    "type" : "image"
  }

::

  {
    "type" : "sampler"
  }

where the ``type`` field is the only required field.

In the case of scalars, the ``value`` field gives the argument value
passed to the kernel during launch. The value should be string
representing a hexadecimal value, e.g., ``"0xA208"``; the string
should always start with ``0x``.

In the case of arrays, the ``size`` field specifies the size of the
argument array passed to the kernel during launch. The value is a
number specifying the size of the array in bytes.  The
``address_space`` field must be one of ``global``, ``local`` and
``constant``, and specifies which memory space the array data resides
in.  The ``flags`` field provides the cl_mem_flags that were used to
create the buffer.  The ``data`` field names a binary file containing,
in bytes, the data the array was populated with on kernel launch.

If ``value`` or ``size`` is omitted their values are assumed
to be unconstrained during verification, otherwise the specific values are use.

Each ``host_api_call`` is of the following form::

  {
    "function_name"    : string,
    "compilation_unit" : string,
    "line_number"      : number
  }

All fields are required, with ``function_name`` and ``compilation_unit``
respectively specifying the name of the called function and the compilation
unit in which the call occurs. The ``line_number`` specifies the line number
within the compilation unit.