Basics and targets

Dependencies

Sentry build system is based on Meson, but also needs some external python tooling. The external dependencies are checked by meson in order to detect if they are properly installed. If not, the build system will inform the user that there is a missing dep in the build environment.

The Sentry dependencies are the following:

• meson: the effective Sentry build system. This is a python module. that can be installed with pip.

• ninja: build system used as backend by meson. Can be replaced with another if needed. This is a python module.

• kconfiglib: This is the Kconfig configuration parser and manager that respect the kconfig syntax that has been intially defined by the Linux kernel and which is documented here.

• device-tree-compiler: This is the device tree compiler tool, that compile device tree sources into device tree blobs. This tool is a part of the kernel.org projects and is packaged in all GNU/Linux distros.

• dtschema: This is python toolset to manipulate and validate device trees. This is a python module that can be installed with pip.

• sphinx: Used in order to generate this very documentation. This is a python module.

• sphinx_rtd_theme: Theme used for Sentry documentation. This is a python module.

• exhale: Python tool that convert Doxygen XML output into sphinx ReST content automatically. It is used to generate the complete source documentations with sphinx output.

• sphinx-simplepdf: sphinx extention to generate the documentation in its PDF format. This is a python module.

• weasyprint: widechar compatible python module that help in generating pdf files. Dependency of the sphinx-simplepdf module. This is a python module.

• svd2json: Tool that convert SVD files into json dictionary in order to allow header generation in meson build system directly from SVD files. This is a python module.

• dts-utils: Tool that convert device tree file into a dictionary with some helpers that can be used to generate header files. This is used by jinja to forge autogenerated headers from the project device tree. This is a python module.

• jinja-cli: This is the jinja implementation that allows to generate template in any language using an efficient templating language with various builtins, intially designed for web services and now used widespread. This is a python module.

• rustup: This is the Rust ecosystem bootsraper that allows toolchain deployment. When installed, the Sentry build system automatically fetch the correct toolchain version for the configured target if needed. Rustup can be found on Rustup website.

• C cross-toolchain: This is the C toolchain to be used for the cross-compilation. Like the Rust toolchain downloaded, it will be used at compile time, and it is checked by the build system to be sure that it is able to cross-compile correctly the Sentry C standard required (C11). For example, ARM toolchains can be found on ARM website.

• native C/C++ toolchain: This is used for unit-testing, in order to compile and execute unit tests. Unit tests are using the gtest/gmock framework. The build system checks if the gtest framework is installed and fallback to a local download if needed. This toolchain can be found as a part of all GNU/Linux distributions.

The meson build system automatically check that all python modules are installed on the build system, but in order to simplify the setup phase, a requirements.txt file has been added to the kernel root source path.

As a consequence, before building the project, one needs to install meson, and then all python dependencies are described in requirements.txt.

pip3 install -r requirements.txt

Warning

For non-python dependencies, the user needs to check and install himself the build dependencies in the way he wants.

About Sentry sources hierarchy

The Sentry kernel sources is divided in three main blocks:

• The Sentry kernel itself, hosted in the kernel/ subdir

• The Sentry UAPI, hosted in the uapi/ subdir

• The Sentry idle task, hosted in the idle/ subdir

Sentry kernel core

Built by default: true

Output: kernel/sentry-kernel.elf

The Sentry kernel core is written in both C and Rust and is built by default. It is possible to deactivate the kernel build with the following option:

-Dwith_kernel=false

The sentry kernel is composed of separated elements that are built as libraries, alowing easy testing, correctness checking and portability.

To achieve that, the Sentry kernel is decomposed of the following libraries:

• libsentry_arch: This library hold all the architecture relative implementation. This library API is defined in the <sentry/arch> subdirectory of the kernel include path.

• libsentry_bsp: This library hold all the device drivers implementation. This library API is defined in the <bsp> subdirectory of the kernel include path.

• libsentry_sched: This library hold schedulers implementation. Its API is hold in the <sentry/sched.h> header file.

• libsentry_managers: This library hold the portable, high level implementation of The kernel features, denoted managers. This library API is defined in the <sentry/managers> kernel include path.

• libsentry_zlib: This library hold portable-C, generic base tooling to be used kernel-wide. This library API is defined in the <sentry/zlib> subdirectory of the kernel include path.

• libsentry_syscalls: This library hold the Sentry, portable, kernel syscall gate (not including supervisor call handler, that is a part of libsentry_arch). This library API is defined in the single header <sentry/syscalls.h> of the kernel include path.

Sentry UAPI

Built by default: true

Output: uapi/libuapi.a

This is the Sentry UAPI userspace library. This library is fully written in Rust, but export its headers in C to allow both C and Rust implementation.

It is possible to deactivate the libuapi build with the following option:

-Dwith_uapi=false

Sentry Idle task

Built by default: true

Output: idle/idle.elf

This is the Sentry Idle task, used as fallback when no user task is eligible. This task request a low power enter mode, while not forbidden by another task.

It is possible to deactivate the libuapi build with the following option:

-Dwith_idle=false

Sentry Autotest task

Built by default: N/A

Output: autotest/autotest.elf

This is the Sentry utotest task, used in order to execute runtime autotest suite on the target device. This task is build only when the Sentry kernel configuration is in autotest mode (i.e. using the CONFIG_BUILD_TARGET_AUTOTEST build target in the config file or through the menuconfig interface). This task is not build in any of the other build targets (debug or release).

Cross-compilation concept

As the cross-toolchain installation and configuration is not a build-system related content but a build-host related information, the meson build systems is using cross-files to define the current build host toolchain configuration that need to be used for the project.

A typical cross-file defines all the toolchain binaries to use and would look like the following:

[constants]
cross_triple = 'arm-none-eabi'
cross_toolchain = '/opt/arm-none-eabi/'
cross_compile = cross_toolchain + 'bin/' + cross_triple + '-'

[host_machine]
system = 'baremetal'
cpu_family = 'arm'
cpu = 'cortex-m4'
endian = 'little'
exe_wrapper = 'qemu-arm-static'

[binaries]
c = cross_compile + 'gcc'
cpp = cross_compile + 'g++'
ar = cross_compile + 'gcc-ar'
ranlib = cross_compile + 'gcc-ranlib'
strip = cross_compile + 'strip'
objcopy = cross_compile + 'objcopy'
clang = 'clang'
rust_ld = cross_compile + 'gcc'
rust = ['rustc', '--target', 'thumbv7m-none-eabi']

Note

A repository hosting various cross-files, denoted meson-cross-files, exists in the Camelot organisation. Although, anyone can write its own toolchain for its own host, like, for e.g. on Windows build environment:

[constants]
cross_triple = 'arm-none-eabi'
sysroot = 'c:/program files (x86)/arm gnu toolchain arm-none-eabi/12.2 rel1/arm-none-eabi'

[host_machine]
system = 'baremetal'
cpu_family = 'arm'
endian = 'little'
cpu = 'cortex-m4'

[binaries]
c = cross_triple + '-gcc'
cpp = cross_triple + '-g++'
ar = cross_triple + '-gcc-ar'
ranlib = cross_triple + '-gcc-ranlib'
strip = cross_triple + '-strip'
objcopy = cross_triple + '-objcopy'
clang = 'clang'
rust_ld = cross_triple + '-gcc'
rust = ['rustc', '--target', 'thumbv7m-none-eabi']

[properties]
bindgen_clang_arguments = [ '--sysroot=' + sysroot, '--target=' + cross_triple ]

Bootstraping Sentry build

A common good practice is do not inject environment variable for build configuration. For this purpose, meson does not allow using relative path in toolchain definition. Toolchain path _must_ be absolute.

One needs to deliver to the meson build system the kernel configuration based on Kconfig. The configuration is forged at project level, using, among others, the Sentry kernel Kconfig entry.

Although, the global project config file generation is under the project responsability, and the Sentry kernel build system consider that this file is built when starting. This is a requirement in order to keep the configuration phase, under Kconfig responsablity, separated from the build phase of each project component, including the Sentry kernel itself. As the configuration phase is handled at project level, the project configuration(s) must be kept somewhere and passed to the kernel build system at setup time.

Modifying the configuration can be done at project level, upgrading or creating new defconfig files, so that the Sentry kernel setup phase can get back the newly created configuration. This part is out of this documentation though and is explained in the project generator documentation.

Here are all the Sentry kernel custom command line options:

• config: string: declare a project defconfig file that can be used by the Kernel as input

• with_docs: boolean: activate doc build targets

• with_proof: boolean: activate formal proof build and exec targets

• with_tests: boolean: activate gtest unit test framework build and exec

All options can be passed using the widely used -Doption=value argument passing. See meson build system manual to see all possible options that can be transmitted.

Building Sentry

Sentry build is decomposed into two main components:

• libsentry.a, a static containing all the Sentry components but the entrypoint and the ldscript. This lib is composed of:

  • libsysgate, a static library of the Rust implementation of the syscalls

  • Sentry static C sources

  • Sentry generated sources (from SVD and DTS files)

  • Sentry generated headers (from SVD and DTS files)

  libsentry sources list varies depending on the passed configuration, as all arch-dependant and SoC-dependant sources (such as drivers) are dynamically selected by the build system based on the current project configuration, namely the current SoC name, familly, subfamilly, and the current selected features-set (e.g. debug or release).

• sentry-kernel.elf, kernel executable, including libsentry, the entrypoint, linked using the Sentry ldscript

When setuping the project, the build system shows the current Sentry project configuration state:

$ meson setup -Dkconfig:config=configs/stm32f429i_disc1_defconfig -Dwith_doc=true --cross-file /workspace/arm-none-eabi-gcc.ini builddir
The Meson build system
Version: 1.2.2
Source dir: /workspace/sentry-kernel/sentry-kernel
Build dir: /workspace/sentry-kernel/builddir
Build type: cross build
Project name: sentry-kernel
Project version: undefined
C compiler for the host machine: /opt/arm-none-eabi/bin/arm-none-eabi-gcc (gcc 12.2.1 "arm-none-eabi-gcc (Arm GNU Toolchain 12.2.Rel1 (Build arm-12.24)) 12.2.1 20221205")
C linker for the host machine: /opt/arm-none-eabi/bin/arm-none-eabi-gcc ld.bfd 12.2
C++ compiler for the host machine: /opt/arm-none-eabi/bin/arm-none-eabi-g++ (gcc 12.2.1 "arm-none-eabi-g++ (Arm GNU Toolchain 12.2.Rel1 (Build arm-12.24)) 12.2.1 20221205")
C++ linker for the host machine: /opt/arm-none-eabi/bin/arm-none-eabi-g++ ld.bfd 12.2
C compiler for the build machine: cc (gcc 11.4.0 "cc (Ubuntu 11.4.0-1ubuntu1~22.04) 11.4.0")
C linker for the build machine: cc ld.bfd 2.38
C++ compiler for the build machine: c++ (gcc 11.4.0 "c++ (Ubuntu 11.4.0-1ubuntu1~22.04) 11.4.0")
C++ linker for the build machine: c++ ld.bfd 2.38
Build machine cpu family: x86_64
Build machine cpu: x86_64
Host machine cpu family: arm
Host machine cpu: cortex-m4
Target machine cpu family: arm
Target machine cpu: cortex-m4
Program objcopy found: YES
Program python3 (dunamai) found: YES (/bin/python3) modules: dunamai
[...]
Message: build targetting SoC STM32F429
../meson.build:200: WARNING: !!! This is NOT a release build ! DO NOT USE IT IN PRODUCTION !!!
Build targets in project: 33

sentry-kernel undefined

Configuration
    soc           : stm32f429
    dts           : dts/sentry_stm32f429i_disc1.dts

Subprojects
    cmsis         : YES
    devicetree    : YES
    kconfig       : YES
    meson-svd     : YES

User defined options
    Cross files   : /workspace/arm-none-eabi-gcc.ini
    with_doc      : true
    kconfig:config: configs/stm32f429i_disc1_defconfig

Building the Sentry kernel is as easy as calling Ninja:

ninja -C builddir all

Testing Sentry

Sentry kernel unit testing is using the gtest framework. All unit tests are executed as x86_64 userspace code, meaning that all Sentry code blocks that are executed under test are compiled and executed as x86_64 code.

Calling only a given est suite is then supported through:

meson test -C builddir --suite <suite>

Executing the test suite generates test report. SonarQube XML test report can be generated for SonarQube input.

A typical test execution is the following:

meson test -C builddir
[...]
[61/62] Running all tests.
1/5 sentry-kernel:ut-utils / io               OK              0.03s
2/5 sentry-kernel:ut-utils / bits             OK              0.02s
3/5 sentry-kernel:ut-bsp / exti               OK              0.01s
4/5 sentry-kernel:ut-managers / printk        OK              0.01s
5/5 sentry-kernel:ut-managers / task          OK              0.01s

Ok:                 5
Expected Fail:      0
Fail:               0
Unexpected Pass:    0
Skipped:            0
Timeout:            0

Note

More about the way unit testing Sentry is designed in described in a dedicated chapter.

Prooving Sentry

Sentry kernel is using Frama-C framework in order to include noRTE and functional correctness into the Kernel. For correctness analysis, Sentry is using:

• EVA (Evaluated Value Analysis) and RTE (Run Time Error) plugins to determine any potential RTE for all possible inputs

• WP (Weakest Precondition) plugin to validate subprogram contracts based on ACSL specifications of their behavior

Calling Frama-C analysus is done using proof dedicated est suite denoted proof, while the with_proof option is set to true.

meson test -C builddir --suite proof

Executing the test frama-C analysisgenerates a lot of reports, measurement, analysis in the kernel/proof build subdirectory.

A typical test execution is the following:

meson test -C builddir --suite proof
[1/1] Generating kernel/proof/framac.dep with a custom command
1/10 frama-C-parsing                              OK               20.04s
2/10 frama-c-eva-entrypoint                       OK              170.30s
3/10 frama-C-eva-handler-systick                  OK               66.74s
4/10 frama-c-eva-handler-svc                      OK              212.47s
5/10 frama-c-eva-zlib                             OK                1.25s
6/10 frama-c-eva-entrypoint-redalarm              OK                0.03s
7/10 frama-C-eva-handler-systick-redalarm         OK                0.04s
8/10 frama-c-eva-handler-svc-redalarm             EXPECTEDFAIL      0.03s   exit status 10
9/10 frama-c-eva-zlib-redalarm                    OK                0.03s
10/10 frama-c-wp-bsp-rcc                           OK               57.52s

Ok:                 9
Expected Fail:      1
Fail:               0
Unexpected Pass:    0
Skipped:            0
Timeout:            0

Note

More about the way unit testing Sentry is designed in described in a dedicated chapter.