This document specifies which procedures and techinques are used troughout the Xen codebase to prevent or minimize the impact of certain classes of run-time errors that can occurr in the execution of a C program, due to the very minimal built-in checks that are present in the language.
The presence of such documentation is requested by MISRA C:2012 Directive 4.1, whose headline states: "Run-time failures shall be minimized".
The ECLAIR checker for MISRA C:2012 Directive 4.1 requires the documentation to be supplied using the following format:
Documentation for MISRA C:2012 Dir 4.1: <category> <description>
The matched categories are the ones listed below (e.g., overflow and unexpected wrapping). The content of the description is not checked and can span multiple lines.
Pervasive use of assertions and extensive test suite.
The only wrapping that is present in the code concerns unsigned integers and they are all expected.
Pervasive use of assertions and extensive test suite.
The division or remainder operations in the project code ensure that their second argument is never zero.
Code executed in interrupt handlers uses spinlocks or disables interrupts at the right locations to avoid unsequenced side effects.
The amount of dynamically allocated objects is limited at runtime in static configurations. We make sure to initialize dynamically allocated objects before reading them, and we utilize static analysis tools to help check for that.
Dynamically allocated storage is used in a controlled manner, to prevent the access to uninitialized allocated storage.
The toolchain puts every string literal and const object into a read-only section of memory. The hardware exception raised when a write is attempted on such a memory section is correctly handled.
Volatile access is limited to registers that are always accessed through macros or inline functions, or by limited code chunks that are only used to access a register.
Although dynamically allocated storage is used in the project, in safety configurations its usage is very limited at runtime (it is "almost" only used at boot time). Coverity is regularly used to scan the code to detect non-freed allocated objects.
Pointers to automatic variables are never returned, nor stored in wider-scoped objects. No function does the same on any pointer received as a parameter.
The program does not use per-thread variables.
All possibly null pointers are checked before access.
Usage of pointers is limited. Pointers passed as parameters are always checked for validity.
Pointers are never used to access arrays without checking for the array size first.
Pointer conversion that may result in unaligned pointers are never used.
Pointer conversions that may result in mistyped accesses to objects are never used.
This behaviour can arise, for instance, from:
The project has adopted various compiler flags and MISRA rules to lessen the likelihood of this event.
Pointer arithmetic is never used without checking object boundaries.
Pointers to different objects are never compared (except for pointers that are actually linker symbols, but those cases are deviated with a justification).
The code never uses memcpy() to copy overlapping objects. The instances of assignments involving overlapping objects are very limited and motivated.
Many parameters to functions are checked for validity; there is ongoing work to make this true for all parameters.
Many functions that may produce an error, do return a suitable status code that is checked at each call site. There is ongoing work to make this true for all such functions.
All parameters of all functions in the extenal ABI are checked before being used.
Data that can be accessed concurrently from multiple threads and code executed by interrupt handlers is protected using spinlocks and other forms of locking, as appropriate.
The extensive checks in the code ensure that any violation of a compile-time invariant will be detected prior to release builds, and violation of run-time invariants is extensively tested. In release builds the number of invariants is greatly reduced.
This project does not involve any external communication.