path: root/eng/fv/refinement.rst

.. SPDX-License-Identifier: CC-BY-SA-4.0

.. Copyright (C) 2022 Trinity College Dublin

.. _Promela2CRefinement:

Promela to C Refinement
=======================

Promela models are more abstract than concrete C code.
A rigorous link, known as a :term:`refinement`, needs to be established
from Promela to C.
This is composed of two parts:
manual annotations in the Promela model to make its behavior easy
to identify and parse;
and a refinement defined as a YAML file that maps from
annotations to corresponding C code.
A single refinement YAML file is associated with each Promela model.

Model Annotations
-----------------

Promela ``printf`` statements are used in the models to output information that
is used by ``spin2test`` to generate test code. This information is used to
lookup keys in a YAML file that defines the mapping to C code. It uses a simple
format that makes it easy to parse and process, and is also designed to be
easily understood by a human reader. This is important because any V&V process
will require this information to be carefully assessed.

Annotation Syntax
^^^^^^^^^^^^^^^^^

Format, where :math:`N \geq 0`:

  ``@@@ <pid> <KEYWORD> <parameter1> ... <parameterN>``

The leading ``@@@`` is a marker that makes it easy to filter out this
information from other SPIN output.

Parameters take the following forms:

  ``<pid>``  Promela Process Id of ``proctype`` generating annotation

  ``<word>`` chunk of text containing no white space

  ``<name>`` Promela variable/structure/constant identifier

  ``<type>`` Promela type identifier

  ``<tid>``  OS Task/Thread/Process Id

  ``_``  unused argument (within containers)

Each ``<KEYWORD>`` is associated with specific forms of parameters:

.. code-block:: none

  LOG <word1> ... <wordN>
  NAME <name>
  INIT
  DEF <name> <value>
  DECL <type> <name> [<value>]
  DCLARRAY <type> <name> <value>
  TASK <name>
  SIGNAL <name> <value>
  WAIT   <name> <value>
  STATE tid <name>
  SCALAR (<name>|_) [<index>] <value>
  PTR <name> <value>
  STRUCT <name>
  SEQ <name>
  END <name>
  CALL <name> <value1> ... <valueN>


Annotation Lookup
-----------------

The way that code is generated depends on the keyword in the annotation.
In particular, the keyword determines how, or if,
the YAML refinement file is looked up.

  Direct Output - no lookup
  (``LOG``, ``DEF``)

  Keyword Refinement - lookup the ``<KEYWORD>``
  (``NAME``, ``INIT``, ``SIGNAL``, ``WAIT``)

  Name Refinement - lookup first parameter (considered as text)
  (``TASK``, ``DECL``, ``DCLARRAY``, ``PTR``, ``CALL``, ``SCALAR``)

The same name may appear in different contexts,
and the name can be extended with a suffix of the form
``_XXX`` to lookup less frequent uses:

  ``_DCL`` - A variable declaration

  ``_PTR`` - The pointer value itself

  ``_FSCALAR`` - A scalar that is a struct field

  ``_FPTR`` - A pointer that is a struct field

Generally, the keyword, or name is used to lookup ``mymodel-rfn.yml`` to get a
string result. This string typically has substitution placeholders, as used by
the Python ``format()`` method for strings. The other parameters in the
annotation are then textually substituted in, to produce a segment of test code.


Specifying Refinement
---------------------

Using the terminology of the :ref:`RTEMSTestFramework`
each Promela model is converted into a set of Test Cases,
one for each complete scenario produced by test generation.
There are a number of template files, tailored for each model,
that are used to assemble the test code sources,
along with code segments for each Promela process,
based on the annotations output for any given scenario.


The refinement mapping from annotations to code is defined in a YAML file that
describes a Python dictionary that maps a name to some C code, with placeholders
that are used to allow for substituting in actual test values.

The YAML file has entries of the following form:

.. code:: yaml

    entity: |
      C code line1{0}
      ...
      C code lineM{2}

The entity is a reference to an annotation concept, which can refer to key
declarations, values, variables, types, API calls or model events. There can be
zero or more arguments in the annotations, and any occurrence of braces
enclosing a number in the C code means that the corresponding annotation
argument string is substituted in (using the python string object `format()`
method).

The general pattern is working through all the annotations in order. The
code obtained by looking up the YAML file is collated into different
code-segments, one for each Promela process id (``<pid>``).

In addition to the explicit annotations generated by the Promela models, there
are two implicit annotations produced by the python refinement code. These
occur when the ``<pid>`` part of a given explicit annotation is different to the
one belonging to the immediately preceding annotation. This indicates a point in
a test generation scenario where one task is suspended and another resumes. This
generates internal annotations with keywords ``SUSPEND`` and ``WAKEUP`` which
should have entries in the refinement file to provide code to ensure that the
corresponding RTEMS tasks in the test behave accordingly.

The annotations can also be output as comments into the generated test-code, so
it is easy to check that parameters are correct, and the generated code is
correct.

If a lookup fails, a C comment line is output stating the lookup failed.
The translation continues in any case.

Lookup Example
^^^^^^^^^^^^^^

Consider the following annotation, from the Events Manager model:

  ``@@@ 1 CALL event_send 1 2 10 sendrc``

This uses Name refinement so a lookup  with ``event_send`` as the key
and gets back the following text:

.. code-block:: python3

  T_log( T_NORMAL, "Calling Send(%d,%d)", mapid( ctx, {1}), {2} );
  {3} = ( *ctx->send )( mapid( ctx, {1} ), {2} );
  T_log( T_NORMAL, "Returned 0x%x from Send", {3} );

Arguments ``1``, ``2``, ``10``, and ``sendrc``
are then substituted to get the code:

.. code-block:: c

  T_log( T_NORMAL, "Calling Send(%d,%d)", mapid( ctx, 2), 10 );
  sendrc = ( *ctx->send )( mapid( ctx, 2 ), 10 );
  T_log( T_NORMAL, "Returned 0x%x from Send", sendrc );

Given a Promela process id of ``1``, this code is put into  a code segment
for the corresponding RTEMS task.


Annotation Refinement Guide
---------------------------

This guide describes how each annotation is processed
by the test generation software.

LOG
^^^

``LOG <word1> ... <wordN>`` (Direct Output)
    Generate a call to ``T_log()`` with a message formed from the ``<word..>``
    parameters.
    This message will appear in the test output for certain verbosity settings.

NAME
^^^^

``NAME <name>`` (Keyword Refinement)
    Looks up ``NAME`` (currently ignoring ``<name>``) and returns the resulting
    text as is as part of the code. This code should define the name of the
    testcase, if needed.

INIT
^^^^

``INIT`` (Keyword Refinement)
    Lookup ``INIT`` and expect to obtain test initialisation code.

TASK
^^^^

``TASK <name>`` (Name Refinement)
    Lookup ``<name>`` and return corresponding C code.

SIGNAL
^^^^^^

``SIGNAL <value>`` (Keyword Refinement)
    Lookup `SIGNAL` and return code with `<value>` substituted in.

WAIT
^^^^

``WAIT <value>`` (Keyword Refinement)
    Lookup `WAIT` and return code with `<value>` substituted in.

DEF
^^^

``DEF <name> <value>`` (Direct Output)
    Output ``#define <name> <value>``.

DECL
^^^^

``DECL <type> <name> [<value>]`` (Name Refinement)
    Lookup ``<name>_DCL`` and substitute ``<name>`` in. If ``<value>`` is
    present, append ``=<value>``. Add a final semicolon. If the `<pid>` value
    is zero, prepend ``static``.

DCLARRAY
^^^^^^^^

``DCLARRAY <type> <name> <value>`` (Name Refinement)
    Lookup ``<name>_DCL`` and substitute ``<name>`` and ``<value>`` in. If the
    `<pid>` value is zero, prepend ``static``.

CALL
^^^^

``CALL <name> <value0> .. <valueN>`` (Name refinement, ``N`` < 6)
    Lookup ``<name>`` and substitute all ``<value..>`` in.

STATE
^^^^^

``STATE <tid> <name>`` (Name Refinement)
    Lookup ``<name>`` and substitute in ``<tid>``.

STRUCT
^^^^^^

``STRUCT <name>``
    Declares the output of the contents of variable ``<name>``
    that is itself a structure. The ``<name>`` is noted, as is the fact
    that a structured value is being processes.
    Should not occur if already be processing a structure or a sequence.

SEQ
^^^

``SEQ <name>``
    Declares the output of the contents of array variable ``<name>``.
    The ``<name>`` is noted, as is the fact that an array is being processed.
    Values are accumulated in a string now initialsed to empty.
    Should not occur if already processing a structure or a sequence.

PTR
^^^

``PTR <name> <value>`` (Name Refinement)
    If not inside a ``STRUCT``, lookup ``<name>_PTR``. Two lines of code should
    be returned. If the ``<value>`` is zero, use the first line, otherwise use
    the second with ``<value>`` substituted in. This is required to handle NULL
    pointers.

    If inside a ``STRUCT``, lookup ``<name>_FPTR``. Two lines of code should
    be returned. If the ``<value>`` is zero, use the first line, otherwise use
    the second with ``<value>`` substituted in. This is required to handle NULL
    pointers.

SCALAR
^^^^^^

There are quite a few variations here.

``SCALAR _ <value>``
    Should only be used inside a ``SEQ``. A space and ``<value>`` is appended
    to the string being accumulated by this ``SEQ``.

``SCALAR <name> <value>`` (Name Refinement)
    If not inside a ``STRUCT``, lookup ``<name>``, and substitute ``<value>``
    into the resulting code.

    If inside a ``STRUCT``, lookup ``<name>_FSCALAR`` and substitute the saved
    ``STRUCT`` name and ``<value>`` into the resulting code.

    This should not be used inside a ``SEQ``.

``SCALAR <name> <index> <value>`` (Name Refinement)
    If not inside a ``STRUCT``, lookup ``<name>``, and substitute ``<index>``
    and ``<value>`` into the resulting code.

    If inside a ``STRUCT``, lookup ``<name>_FSCALAR`` and substitute the saved
    ``STRUCT`` name and ``<value>`` into the resulting code.

    This should not be used inside a ``SEQ``.

END
^^^

``END <name>``
    If inside a ``STRUCT``, terminates processing a
    structured variable.

    If inside a ``SEQ``, lookup ``<name>_SEQ``. For each line of code obtained,
    substitute in the saved sequence string.
    Terminates processing a sequence/array variable.

    This should not be encountered outside of a ``STRUCT`` or ``SEQ``.

SUSPEND and WAKEUP
^^^^^^^^^^^^^^^^^^

A change of Promela process id from ``oldid`` to ``newid`` has been found.
Increment a counter that tracks the number of such changes.

``SUSPEND``  (Keyword Refinement)

    Lookup ``SUSPEND`` and substitute in the counter value, ``oldid`` and
    ``newid``.

``WAKEUP``  (Keyword Refinement)

    Lookup ``WAKEUP`` and substitute in the counter value, ``newid`` and
    ``oldid``.

Annotation Ordering
-------------------

While most annotations occur in an order determined by any given test scenario,
there are some annotations that need to be issued first. These are, in order:
``NAME``, ``DEF``, ``DECL`` and ``DCLARRAY``, and finally, ``INIT``.


Test Code Assembly
------------------

The code snippets produced by refining annotations are not enough.
We also need boilerplate code to setup, coordinate and teardown the tests,
as well as providing useful C support functions.

For a model called `mymodel` the following files are required:

* ``mymodel.pml`` - the Promela model
* ``mymodel-rfn.yml`` - the model refinement to C test code
* ``tc-mymodel.c`` - the testcase setup C file
* ``tr-mymodel.h`` - the test-runner header file
* ``tr-mymodel.c`` - the test-runner setup C file

The following files are templates used to assemble
a single test-runner C file
for each scenario generated by the Promela model:

* ``mymodel-pre.h`` - preamble material at the start
* ``mymodel-run.h`` - test runner material
* ``mymodel-post.h`` - postamble material at the end.

The process is entirely automated:

.. code-block:: shell

  tbuild all mymodel

The steps of the process are as follows:

Scenario Generation
^^^^^^^^^^^^^^^^^^^

When SPIN is invoked to find all scenarios,
it will produce a number (N) of counterexample files
with a ``.trail`` extension.
These files hold numeric data that refer to SPIN internals.

.. code-block:: none

  mymodel.pml1.trail
  ...
  mymodel.pmlN.trail

SPIN is then used to take each trail file and produce a human-readable
text file, using the same format as the SPIN simulation output.
SPIN numbers files from 1 up,
whereas the RTEMS convention is to number things,
including filenames, from zero.
SPIN is used to produce readable output in text files with a ``.spn`` extension,
with 1 subtracted from the trail file number.
This results in the following files:

.. code-block:: shell

  mymodel-0.spn
  ...
  mymodel-{N-1}.spn

Test Code Generation
^^^^^^^^^^^^^^^^^^^^

Each SPIN output file ``mymodel-I.spn``
is converted to a C test runner file ``tr-mymodel-I.c``
by concatenating the following components:

``mymodel-pre.h``
    This is a fairly standard first part of an RTEMS test C file.
    It is used unchanged.

refined test segments
  The annotations in ``mymodel-I.spn`` are converted, in order,
  into test code snippets using the refinement file ``mymodel-rfn.yml``.
  Snippets are gathered into distinct code segments based on the Promela
  process number reported in each annotation.
  Each code segment is used to construct a C function called
  ``TestSegmentP()``, where ``P`` is the relevant process number.

``mymodel-post.h``
    This is static code that declares the top-level RTEMS Tasks
    used in the test.
    These are where the code segments above get invoked.

``mymodel-run.h``
   This defines top-level C functions that implement a given test runner. The top-level function has a name like ``RtemsMyModel_Run``
   This is not valid C as it needs to produce a name parameterized by
   the relevant scenario number. It contains Python string format substitution
   placeholders that allow the relevant number to be added to end of the
   function name. So the above run function actually appears in this file as ``RtemsMyModel_Run{0}``, so ``I`` will be substituted in for ``{0}`` to result in the name ``RtemsMyModel_RunI``.
   In particular, it invokes ``TestSegment0()`` which contains code
   generated from Promela process 0, which is the main model function.
   This declares test variables, and initializes them.

These will generate test-runner test files as follows:

.. code-block:: none

  tr-mymodel-0.c
  ...
  tr-mymodel-{N-1}.c

In addition, the test case file ``tc-mymodel.c`` needs to have entries added
manually of the form below, for ``I`` in the range 0 to N-1.:

.. code-block:: c

  T_TEST_CASE( RtemsMyModelI )
  {
    RtemsMyModel_RunI(
      ...
    );
  }

These define the individual test cases in the model, each corresponding to precisely one SPIN scenario.

Test Code Deployment
^^^^^^^^^^^^^^^^^^^^

All files starting with ``tc-`` or ``tr-`` are copied to the
relevant testsuite directory.
At present, this is ``testsuites/validation`` at the top level in
the ``rtems`` repository.
All the names of the above files with a ``.c`` extension are added
into a YAML file that
defines the Promela generated-test sources.
At present, this
is ``spec/build/testsuites/validation/model-0.yml``
at the top-level in the ``rtems`` repository.
They appear in the YAML file under the ``source`` key:

.. code-block:: yaml

  source:
  - testsuites/validation/tc-mymodel.c
  - testsuites/validation/tr-mymodel-0.c
  ...
  - testsuites/validation/tr-mymodel-{N-1}.c
  - testsuites/validation/ts-model-0.c

Performing Tests
^^^^^^^^^^^^^^^^

At this point build RTEMS as normal. e.g., with ``waf``,
and the tests will get built.
The executable will be found in the designated build directory,
*(e.g.):*

 ``rtems/build/sparc/gr740/testsuites/validation/ts-model-0.exe``

 This can be run using the RTEMS Tester
 (RTEMS User Manual, Host Tools, RTEMS Tester and Run).


 Both building the code and running on the tester is also automated
 (see :ref:`FormalToolSetup`).

Traceability
------------

Traceability between requirements, specifications, designs, code, and tests,
is a key part of any qualification/certification effort. The test generation
methodology developed here supports this in two ways, when refining an
annotation:

1.  If the annotation is for a declaration of some sort, the annotation itself
    is added as a comment to the output code, just before the refined declaration.

    .. code-block:: c

      // @@@ 0 NAME Chain_AutoGen
      // @@@ 0 DEF MAX_SIZE 8
      #define MAX_SIZE 8
      // @@@ 0 DCLARRAY Node memory MAX_SIZE
      static item memory[MAX_SIZE];
      // @@@ 0 DECL unsigned nptr NULL
      static item * nptr = NULL;
      // @@@ 0 DECL Control chain
      static rtems_chain_control chain;

2.  If the annotation is for a test of some sort, a call to ``T_log()`` is
    generated with the annotation as its text, just before the test code.

    .. code-block:: c

      T_log(T_NORMAL,"@@@ 0 INIT");
      rtems_chain_initialize_empty( &chain );
      T_log(T_NORMAL,"@@@ 0 SEQ chain");
      T_log(T_NORMAL,"@@@ 0 END chain");
      show_chain( &chain, ctx->buffer );
      T_eq_str( ctx->buffer, " 0" );

In addition to traceability, these also help when debugging models, refinement
files, and the resulting test code.