path: root/eng/fv/tool-setup.rst

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

.. Copyright (C) 2022 Trinity College Dublin

.. _FormalToolSetup:

Formal Tools Setup
==================

The required formal tools consist of
the model checking software (Promela/SPIN),
and the test generation software (spin2test/testbuilder).

Installing Tools
----------------

Installing Promela/SPIN
^^^^^^^^^^^^^^^^^^^^^^^

Follow the installation instructions for Promela/Spin
at https://spinroot.com/spin/Man/README.html.

There are references there to the Spin Distribution which is now on
Github (https://github.com/nimble-code/Spin).

Installing Test Generation Tools
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

The test generation tools are found in ``formal/promela/src``, written in
Python3, and installed using a virtual environment.
To build the tools, enter ``formal/promela/src`` and issue the
commands:

.. code:: shell

  make env
  . env/bin/activate
  make py

The test generation tools need to be used from within this Python virtual
environment. Use the ``deactivate`` command to exit from it.

Test generation is managed at the top level by the script ``testbuilder.py``
located in the top-level of ``formal/promela/src``.
To avoid using (long) absolute pathnames,
it helps to define an suitable alias
*(e.g.)*:

.. code-block:: shell

  alias tbuild='python3 /..../formal/promela/src/testbuilder.py'

This alias is used subsequently in this documentation.

To check for a successful tool build, invoke the command without any
arguments, which should result in an extended help message being displayed:

.. code-block:: shell

  (env) prompt % tbuild
  USAGE:
  help - more details about usage and commands below
  all modelname - runs clean, spin, gentests, copy, compile and run
  clean modelname - remove spin, test files
  archive modelname - archives spin, test files
  zero  - remove all tesfiles from RTEMS
  spin modelname - generate spin files
  gentests modelname - generate test files
  copy modelname - copy test files and configuration to RTEMS
  compile - compiles RTEMS tests
  run - runs RTEMS tests

The tool is not yet ready for use, as it needs to be configured.

Tool Configuration
------------------

Tool configuration involves setting up a new testsuite in RTEMS, and providing
information to ``tbuild`` that tells it where to find key locations, and some
command-line arguments for some of the tools.
A template file ``testbuilder-template.yml`` is included,
and contains the following entries:

.. code-block:: python

  # This should be specialised for your setup, as testbuilder.yml,
  # located in the same directory as testbuilder.py
  # All pathnames should be absolute

  spin2test: <spin2test_directory>/spin2test.py
  rtems: <path-to-main-rtems-directory>  # rtems.git, or ..../modules/rtems/
  rsb: <rsb-build_directory>/rtems/6/bin/
  simulator: <path-to>/sparc-rtems6-sis
  testyamldir: <rtems>/spec/build/testsuites/validation/ # directory containing <modelname>.yml
  testcode: <rtems>/testsuites/validation/
  testexedir:  <rtems>/build/.../testsuites/validation/ # directory containing ts-<modelname>.exe
  testsuite: model-0
  simulatorargs: -leon3 -r s -m 2  # run command executes "<simulator> <simargs> <testexedir>/ts-<testsuite>.exe"
  spinallscenarios: -DTEST_GEN -run -E -c0 -e # trail generation "spin <spinallscenarios> <model>.pml"

This template should be copied/renamed to ``testbuilder.yml``
and each entry updated as follows:

* spin2test:
    This should be the absolute path to ``spin2test.py``
    in the Promela sources directory.

    ``/.../formal/promela/src/spin2test.py``

* rtems:
    This should be the absolute path to your RTEMS source directory,
    with the terminating ``/``.
    From ``rtems-central`` this would be:

    ``/.../rtems-central/modules/rtems/``

    For a separate ``rtems`` installation
    it would be where ``rtems.git`` was cloned.

    We refer to this path below as ``<rtems>``.

* rsb:
    This should be the absolute path
    to your RTEMS source-builder binaries directory,
    with the terminating ``/``.
    From ``rtems-central`` this would be (assuming RTEMS 6):

    ``/.../rtems-central/modules/rsb/6/bin/``

* simulator:
    This should be the absolute path to the RTEMS Tester
    (See Host Tools in the RTEMS User Manual)

    It defaults at present to the ``sis`` simulator

    ``/.../rtems-central/modules/rsb/6/bin/sparc-rtems6-sis``

* testsuite:
    This is the name for the testsuite :

    Default value: ``model-0``

* testyamldir:
    This should be the absolute path to where validation tests are *specified*:

    ``<rtems>/spec/build/testsuites/validation/``

* testcode:
    This should be the absolute path to where validation test sources
    are found:

    ``<rtems>/testsuites/validation/``

* testexedir:
    This should be the absolute path to where
    the model-based validation test executable
    will be found:

    ``<rtems>/build/.../testsuites/validation/``

    This will contain ``ts-<testsuite>.exe`` (e.g. ``ts-model-0.exe``)

* simulatorargs:
    These are the command line arguments for the RTEMS Tester.
    It defaults at present to those for the ``sis`` simulator.

    ``-<bsp> -r s -m <cpus>``

    The first argument should be the BSP used when building RTEMS sources.
    BSPs ``leon3``, ``gr712rc`` and ``gr740`` have been used.
    The argument to the ``-m`` flag is the number of cores.
    Possible values are: 1, 2 and 4 (BSP dependent)

    Default: ``-leon3 -r s -m 2``

* spinallscenarios:
    These are command line arguments for SPIN,
    that ensure that all counter-examples are generated.

    Default: ``-DTEST_GEN -run -E -c0 -e`` (recommended)

Testsuite Setup
^^^^^^^^^^^^^^^

The C test code generated by these tools is installed into the main ``rtems``
repository  at ``testsuites/validation`` in the exact same way as other RTEMS
test code.
This means that whenever ``waf`` is used at the top level to build and/or run
tests, that the formally generated code is automatically included.
This requires adding and modifying some *Specification Items*
(See Software Requirements Engineering section in this document).

To create a testsuite called ``model-0`` (say), do the following, in the
``spec/build/testsuites/validation`` directory:

* Edit ``grp.yml`` and add the following two lines into the `links` entry:

  .. code-block:: YAML

    - role: build-dependency
      uid: model-0

* Copy ``validation-0.yml`` (say) to ``model-0.yml``, and change the following
  entries as shown:

  .. code-block:: YAML

    enabled-by: RTEMS_SMP
    source:
    - testsuites/validation/ts-model-0.c
    target: testsuites/validation/ts-model-0.exe

Then, go to the ``testsuites/validation`` directory, and copy
``ts-validation-0.c`` to ``ts-model-0.c``, and edit as follows:

  * Change all occurrences of ``Validation0`` in comments to ``Model0``.

  * Change ``rtems_test_name`` to ``Model0``.

Running Test Generation
-----------------------

The testbuilder takes a command as its first command-line argument. Some of
these commands require the model-name as a second argument:

  Usage:   ``tbuild <command> [<modelname>]``

The commands provided are:

``clean <model>``
  Removes generated files.

``spin <model>``
  Runs SPIN to find all scenarios. The scenarios are found in numbered files
  called ``<model>N.spn``.

``gentests <model>``
  Convert SPIN scenarios to test sources. Each ``<model>N.spn`` produces a numbered
  test source file.

``copy <model>``
  Copies the generated test files to the relevant test source directory, and
  updates the relevant test configuration files.

``archive <model>``
  Copies generated spn, trail, source, and test log files to an archive
  sub-directory of the model directory.

``compile``
  Rebuilds the test executable.

``run``
  Runs tests in a simulator.

``all <model>``
  Does clean, spin, gentests, copy, compile, and run.

``zero``
  Removes all generated test filenames from the test configuration files, but
  does NOT remove the test sources from the test source directory.

In order to generate test files the following input files are required:
    ``<model>.pml``,
    ``<model>-rfn.yml``,
    ``<model>-pre.h``,
    ``<model>-post.h``, and
    ``<model>-run.h``.
In addition there may be other files
whose names have <model> embedded in them. These are included in what is
transfered to the test source directory by the copy command.

The simplest way to check test generation is setup properly is to visit one of
the models, found under ``formal/promela/models`` and execute the following
command:

.. code-block:: shell

   tbuild all mymodel

This should end by generating a file `model-0-test.log`. The output is
identical to that generated by the regular RTEMS tests, using the
*Software Test Framework* described elsewhere in this document.

Output for the Event Manager model, highly redacted:

.. code-block::

  SIS - SPARC/RISCV instruction simulator 2.29,  copyright Jiri Gaisler 2020
  Bug-reports to jiri@gaisler.se

  GR740/LEON4 emulation enabled, 4 cpus online, delta 50 clocks

  Loaded ts-model-0.exe, entry 0x00000000

  *** BEGIN OF TEST Model0 ***
  *** TEST VERSION: 6.0.0.03337dab21e961585d323a9974c8eea6106c803d
  *** TEST STATE: EXPECTED_PASS
  *** TEST BUILD: RTEMS_SMP
  *** TEST TOOLS: 10.3.1 20210409 (RTEMS 6, RSB 889cf95db0122bd1a6b21598569620c40ff2069d, Newlib eb03ac1)
  A:Model0
  S:Platform:RTEMS
  ...
  B:RtemsModelSystemEventsMgr8
  ...
  L:@@@ 3 CALL event_send 1 2 10 sendrc
  L:Calling Send(167837697,10)
  L:Returned 0x0 from Send
  ...
  E:RtemsModelEventsMgr0:N:21:F:0:D:0.005648
  Z:Model0:C:18:N:430:F:0:D:0.130464
  Y:ReportHash:SHA256:5EeLdWsRd25IE-ZsS6pduLDsrD_qzB59dMU-Mg2-BDA=

  *** END OF TEST Model0 ***

  cpu 0 in error mode (tt = 0x80)
    6927700  0000d580:  91d02000   ta  0x0