diff options
Diffstat (limited to 'eng/fv/tool-setup.rst')
| -rwxr-xr-x | eng/fv/tool-setup.rst | 317 |
1 files changed, 317 insertions, 0 deletions
diff --git a/eng/fv/tool-setup.rst b/eng/fv/tool-setup.rst new file mode 100755 index 0000000..f8cf046 --- /dev/null +++ b/eng/fv/tool-setup.rst @@ -0,0 +1,317 @@ +.. 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 + |