[XEN PATCH 0/3] docs/misra: add documentation skeleton to address MISRA C:2012 Dir 4.1

[XEN PATCH 0/3] docs/misra: add documentation skeleton to address MISRA C:2012 Dir 4.1

[Nicola Vetrini]

The headline of Directive 4.1 states: "Run-time failures shall be minimized".
Thus, it requires the project to supply documentation that pertains the measures
and techinques used to prevent run-time failures from happening. For ease of
reading, the documentation is in RST format, but since ECLAIR needs a source file
to check that the needed subsections and their format is the one expected, the
Makefiles for the docs/ are amended to generate such a file.

The format and categories of the subsections in the .rst file can be
customized based on feedback from the community: the one provided is just a
basic skeleton that should be tailored to the project.

This series is based on the following RFC:
https://lore.kernel.org/xen-devel/cover.1692636338.git.nicola.vetrini@bugseng.com/

Nicola Vetrini (3):
  docs/misra: add documentation skeleton for MISRA C:2012 Dir 4.1
  docs: make the docs for MISRA C:2012 Dir 4.1 visible to ECLAIR
  automation/eclair: build docs/misra to address MISRA C:2012 Dir 4.1

 automation/eclair_analysis/build.sh   |  11 +-
 automation/eclair_analysis/prepare.sh |   5 +-
 docs/Makefile                         |   7 +-
 docs/misra/C-runtime-failures.rst     | 239 ++++++++++++++++++++++++++
 docs/misra/Makefile                   |  17 ++
 docs/misra/rules.rst                  |   7 +-
 6 files changed, 279 insertions(+), 7 deletions(-)
 create mode 100644 docs/misra/C-runtime-failures.rst
 create mode 100644 docs/misra/Makefile

--
2.34.1

[XEN PATCH 1/3] docs/misra: add documentation skeleton for MISRA C:2012 Dir 4.1

[Nicola Vetrini]

The aforementioned directive requires the project to supply documentation
on the measures taken towards the minimization of run-time failures.

The actual content of the documentation is yet to be written.

The 'rules.rst' file is updated accordingly to mention the newly
added documentation.

Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
---
 docs/misra/C-runtime-failures.rst | 239 ++++++++++++++++++++++++++++++
 docs/misra/rules.rst              |   7 +-
 2 files changed, 245 insertions(+), 1 deletion(-)
 create mode 100644 docs/misra/C-runtime-failures.rst

diff --git a/docs/misra/C-runtime-failures.rst b/docs/misra/C-runtime-failures.rst
new file mode 100644
index 000000000000..0d8d5adce231
--- /dev/null
+++ b/docs/misra/C-runtime-failures.rst
@@ -0,0 +1,239 @@
+===================================================================
+Measures taken towards the minimization of Run-time failures in Xen
+===================================================================
+
+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".
+
+
+Documentation for MISRA C:2012 Dir 4.1: overflow
+________________________________________________
+
+To be written.
+Example: Pervasive use of assertions and extensive test suite.
+
+
+Documentation for MISRA C:2012 Dir 4.1: unexpected wrapping
+___________________________________________________________
+
+To be written.
+Example: The only wrapping the is present in the code concerns
+unsigned integers and they are all expected.
+
+
+Documentation for MISRA C:2012 Dir 4.1: invalid shift
+_____________________________________________________
+
+To be written.
+Example: Pervasive use of assertions and extensive test suite.
+
+
+Documentation for MISRA C:2012 Dir 4.1: division/remainder by zero
+__________________________________________________________________
+
+To be written.
+Example:
+There division or remainder operations in the project code ensure that
+their second argument is never zero.
+
+
+Documentation for MISRA C:2012 Dir 4.1: unsequenced side effects
+________________________________________________________________
+
+To be written.
+Example:
+No function in this project is meant to be executed from interrupt handlers
+or in multi-threading environments.
+
+
+Documentation for MISRA C:2012 Dir 4.1: read from uninitialized automatic object
+________________________________________________________________________________
+
+To be written.
+Example:
+Automatic variables are used to store temporary parameters and they
+are always initialized to either a default value or a proper value
+before usage.
+
+
+Documentation for MISRA C:2012 Dir 4.1: read from uninitialized allocated object
+________________________________________________________________________________
+
+To be written.
+Example:
+The code does not use dynamically allocated storage.
+
+
+Documentation for MISRA C:2012 Dir 4.1: write to string literal or const object
+_______________________________________________________________________________
+
+To be written.
+Example:
+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.
+
+
+Documentation for MISRA C:2012 Dir 4.1: non-volatile access to volatile object
+______________________________________________________________________________
+
+To be written.
+Example:
+Volatile access is limited to registers that are always accessed
+through macros or inline functions.
+
+
+Documentation for MISRA C:2012 Dir 4.1: access to dead allocated object
+_______________________________________________________________________
+
+To be written.
+Example:
+The code does not use dynamically allocated storage.
+
+
+Documentation for MISRA C:2012 Dir 4.1: access to dead automatic object
+_______________________________________________________________________
+
+To be written.
+Example:
+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.
+
+
+Documentation for MISRA C:2012 Dir 4.1: access to dead thread object
+____________________________________________________________________
+
+To be written.
+Example:
+The program does not use per-thread variables.
+
+
+Documentation for MISRA C:2012 Dir 4.1: access using null pointer
+_________________________________________________________________
+
+To be written.
+Example:
+All possibly null pointers are checked before access.
+
+
+Documentation for MISRA C:2012 Dir 4.1: access using invalid pointer
+____________________________________________________________________
+
+To be written.
+Example:
+Usage of pointers is limited.  Pointers passed as parameters are
+always checked for validity.
+
+
+Documentation for MISRA C:2012 Dir 4.1: access using out-of-bounds pointer
+__________________________________________________________________________
+
+To be written.
+Example:
+Pointers are never uses to access arrays: indices are always used
+instead.
+
+
+Documentation for MISRA C:2012 Dir 4.1: access using unaligned pointer
+______________________________________________________________________
+
+To be written.
+Example:
+Pointer conversion that may result in unaligned pointers are never used.
+
+
+Documentation for MISRA C:2012 Dir 4.1: mistyped access to object
+_________________________________________________________________
+
+To be written.
+Example:
+Pointer conversions that may result in mistyped accesses to objects
+are never used.
+
+
+Documentation for MISRA C:2012 Dir 4.1: mistyped access to function
+___________________________________________________________________
+
+To be written.
+Example:
+The code never uses function pointers.
+
+
+Documentation for MISRA C:2012 Dir 4.1: invalid pointer arithmetic
+__________________________________________________________________
+
+To be written.
+Example:
+Pointer arithmetic is never used.
+
+
+Documentation for MISRA C:2012 Dir 4.1: invalid pointer comparison
+__________________________________________________________________
+
+To be written.
+Example:
+Arrays are always accessed using indices instead of pointers.  Pointers
+are only compared to NULL.
+
+
+Documentation for MISRA C:2012 Dir 4.1: overlapping copy
+________________________________________________________
+
+To be written.
+Example:
+The code never uses memcpy() and does not perform assignment of
+overlapping objects (which is doable only via pointers).
+
+
+Documentation for MISRA C:2012 Dir 4.1: invalid arguments to function
+_____________________________________________________________________
+
+To be written.
+Example:
+All parameters to functions are checked for validity.
+
+
+Documentation for MISRA C:2012 Dir 4.1: returned function error
+_______________________________________________________________
+
+To be written.
+Example:
+All functions that may produce an error, do returns a suitable status code
+that is checked at each call site.
+
+
+Documentation for MISRA C:2012 Dir 4.1: tainted input
+_____________________________________________________
+
+To be written.
+Example:
+All parameters of all functions in the API are checked before being used.
+
+
+Documentation for MISRA C:2012 Dir 4.1: data race
+_________________________________________________
+
+To be written.
+Example:
+No function in this code is meant to be executed from interrupt handlers or
+in a multi-threading environment.
+
+
+Documentation for MISRA C:2012 Dir 4.1: invariant violation
+___________________________________________________________
+
+To be written.
+
+
+Documentation for MISRA C:2012 Dir 4.1: communication error
+___________________________________________________________
+
+To be written.
+Example:
+This project does not involve any external communication.
diff --git a/docs/misra/rules.rst b/docs/misra/rules.rst
index 34916e266aa5..84bb57c8e908 100644
--- a/docs/misra/rules.rst
+++ b/docs/misra/rules.rst
@@ -47,7 +47,12 @@ maintainers if you want to suggest a change.
    * - `Dir 2.1 <https://gitlab.com/MISRA/MISRA-C/MISRA-C-2012/Example-Suite/-/blob/master/D_02_01.c>`_
      - Required
      - All source files shall compile without any compilation errors
-     -
+
+   * - `Dir 4.1 <https://gitlab.com/MISRA/MISRA-C/MISRA-C-2012/Example-Suite/-/blob/master/D_04_01.c>`_
+     - Required
+     - Run-time failures shall be minimized
+     - The strategies adopted by Xen to prevent certain classes of runtime
+       failures will be documented by `C-runtime-failures.rst <docs/misra/C-runtime-failures.rst>`_
 
    * - `Dir 4.7 <https://gitlab.com/MISRA/MISRA-C/MISRA-C-2012/Example-Suite/-/blob/master/D_04_07.c>`_
      - Required
-- 
2.34.1

[XEN PATCH 2/3] docs: make the docs for MISRA C:2012 Dir 4.1 visible to ECLAIR

[Nicola Vetrini]

To be able to check for the existence of the necessary subsections in
the documentation for MISRA C:2012 Dir 4.1, ECLAIR needs to have a source
file that is built.

This file is generated from 'C-runtime-failures.rst' in docs/misra
and the configuration is updated accordingly.

Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
---
Changes from RFC:
- Dropped unused/useless code
- Revised the sed command
- Revised the clean target
---
 docs/Makefile       |  7 ++++++-
 docs/misra/Makefile | 17 +++++++++++++++++
 2 files changed, 23 insertions(+), 1 deletion(-)
 create mode 100644 docs/misra/Makefile

diff --git a/docs/Makefile b/docs/Makefile
index 966a104490ac..ff991a0c3ca2 100644
--- a/docs/Makefile
+++ b/docs/Makefile
@@ -43,7 +43,7 @@ DOC_PDF  := $(patsubst %.pandoc,pdf/%.pdf,$(PANDOCSRC-y)) \
 all: build
 
 .PHONY: build
-build: html txt pdf man-pages figs
+build: html txt pdf man-pages figs misra
 
 .PHONY: sphinx-html
 sphinx-html:
@@ -66,9 +66,14 @@ endif
 .PHONY: pdf
 pdf: $(DOC_PDF)
 
+.PHONY: misra
+misra:
+	$(MAKE) -C misra
+
 .PHONY: clean
 clean: clean-man-pages
 	$(MAKE) -C figs clean
+	$(MAKE) -C misra clean
 	rm -rf .word_count *.aux *.dvi *.bbl *.blg *.glo *.idx *~
 	rm -rf *.ilg *.log *.ind *.toc *.bak *.tmp core
 	rm -rf html txt pdf sphinx/html
diff --git a/docs/misra/Makefile b/docs/misra/Makefile
new file mode 100644
index 000000000000..8ea0505c8a20
--- /dev/null
+++ b/docs/misra/Makefile
@@ -0,0 +1,17 @@
+TARGETS := C-runtime-failures.o
+
+all: $(TARGETS)
+
+# sed is used in place of cat to prevent occurrences of '*/'
+# in the .rst from breaking the compilation
+$(TARGETS:.o=.c): %.c: %.rst
+	echo "/*\n" > $@.tmp
+	sed -e 's|\*/|*//*|g' $< >> $@.tmp
+	echo "\n*/" >> $@.tmp
+	mv $@.tmp $@
+
+%.o: %.c
+	$(CC) -c $< -o $@
+
+clean:
+	rm -f C-runtime-failures.c *.o *.tmp
-- 
2.34.1

[XEN PATCH 3/3] automation/eclair: build docs/misra to address MISRA C:2012 Dir 4.1

[Nicola Vetrini]

The documentation pertaining Directive 4.1 is contained in docs/misra.
The build script driving the analysis is amended to allow ECLAIR to
analyze such file.

Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
---
 automation/eclair_analysis/build.sh   | 11 ++++++++---
 automation/eclair_analysis/prepare.sh |  5 +++--
 2 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/automation/eclair_analysis/build.sh b/automation/eclair_analysis/build.sh
index ec087dd822fa..556ed698bf8b 100755
--- a/automation/eclair_analysis/build.sh
+++ b/automation/eclair_analysis/build.sh
@@ -34,11 +34,16 @@ else
 fi
 
 (
-  cd xen
-
   make "-j${PROCESSORS}" "-l${PROCESSORS}.0"    \
        "CROSS_COMPILE=${CROSS_COMPILE}"         \
        "CC=${CROSS_COMPILE}gcc-12"              \
        "CXX=${CROSS_COMPILE}g++-12"             \
-       "XEN_TARGET_ARCH=${XEN_TARGET_ARCH}"
+       "XEN_TARGET_ARCH=${XEN_TARGET_ARCH}"     \
+       -C docs misra
+  make "-j${PROCESSORS}" "-l${PROCESSORS}.0"    \
+       "CROSS_COMPILE=${CROSS_COMPILE}"         \
+       "CC=${CROSS_COMPILE}gcc-12"              \
+       "CXX=${CROSS_COMPILE}g++-12"             \
+       "XEN_TARGET_ARCH=${XEN_TARGET_ARCH}"     \
+			 -C xen
 )
diff --git a/automation/eclair_analysis/prepare.sh b/automation/eclair_analysis/prepare.sh
index 275a1a3f517c..452e309b658b 100755
--- a/automation/eclair_analysis/prepare.sh
+++ b/automation/eclair_analysis/prepare.sh
@@ -35,8 +35,9 @@ else
 fi
 
 (
-    cd xen
-    cp "${CONFIG_FILE}" .config
+    ./configure
+    cp "${CONFIG_FILE}" xen/.config
     make clean
+    cd xen
     make -f ${script_dir}/Makefile.prepare prepare
 )
-- 
2.34.1

Re: [XEN PATCH 1/3] docs/misra: add documentation skeleton for MISRA C:2012 Dir 4.1

[Stefano Stabellini]

On Fri, 1 Sep 2023, Nicola Vetrini wrote:
> The aforementioned directive requires the project to supply documentation
> on the measures taken towards the minimization of run-time failures.
> 
> The actual content of the documentation is yet to be written.
> 
> The 'rules.rst' file is updated accordingly to mention the newly
> added documentation.
> 
> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
> ---
>  docs/misra/C-runtime-failures.rst | 239 ++++++++++++++++++++++++++++++
>  docs/misra/rules.rst              |   7 +-
>  2 files changed, 245 insertions(+), 1 deletion(-)
>  create mode 100644 docs/misra/C-runtime-failures.rst
> 
> diff --git a/docs/misra/C-runtime-failures.rst b/docs/misra/C-runtime-failures.rst
> new file mode 100644
> index 000000000000..0d8d5adce231
> --- /dev/null
> +++ b/docs/misra/C-runtime-failures.rst
> @@ -0,0 +1,239 @@
> +===================================================================
> +Measures taken towards the minimization of Run-time failures in Xen
> +===================================================================
> +
> +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".
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: overflow
> +________________________________________________
> +
> +To be written.
> +Example: Pervasive use of assertions and extensive test suite.

Can we just say:
Pervasive use of assertions and extensive test suite.

Without "Example:" and without "To be written". It is clear that more
information is needed but we don't need to repeat it every time.



> +Documentation for MISRA C:2012 Dir 4.1: unexpected wrapping
> +___________________________________________________________
> +
> +To be written.
> +Example: The only wrapping the is present in the code concerns
> +unsigned integers and they are all expected.

Same here, and also below (I won't repeat it every time)


> +Documentation for MISRA C:2012 Dir 4.1: invalid shift
> +_____________________________________________________
> +
> +To be written.
> +Example: Pervasive use of assertions and extensive test suite.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: division/remainder by zero
> +__________________________________________________________________
> +
> +To be written.
> +Example:
> +There division or remainder operations in the project code ensure that
> +their second argument is never zero.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: unsequenced side effects
> +________________________________________________________________
> +
> +To be written.
> +Example:
> +No function in this project is meant to be executed from interrupt handlers
> +or in multi-threading environments.

This would not be true. We have code that is executed in interrupt
handlers, but we take care to use spinlocks and/or disable interrupts at
the right locations to avoid unsequenced side effects



> +Documentation for MISRA C:2012 Dir 4.1: read from uninitialized automatic object
> +________________________________________________________________________________
> +
> +To be written.
> +Example:
> +Automatic variables are used to store temporary parameters and they
> +are always initialized to either a default value or a proper value
> +before usage.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: read from uninitialized allocated object
> +________________________________________________________________________________
> +
> +To be written.
> +Example:
> +The code does not use dynamically allocated storage.

We do use dynamically allocated storage with xzalloc but xzalloc
initializes the object to zero


> +Documentation for MISRA C:2012 Dir 4.1: write to string literal or const object
> +_______________________________________________________________________________
> +
> +To be written.
> +Example:
> +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.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: non-volatile access to volatile object
> +______________________________________________________________________________
> +
> +To be written.
> +Example:
> +Volatile access is limited to registers that are always accessed
> +through macros or inline functions.

Or very specific limited code chucks that are only used to access a
register


> +Documentation for MISRA C:2012 Dir 4.1: access to dead allocated object
> +_______________________________________________________________________
> +
> +To be written.
> +Example:
> +The code does not use dynamically allocated storage.

We do use dynamically allocated storage, but in a safety configuration
is used only in very limited ways at runtime (it is "almost" only used
at boot time). We use Coverity regularly to scan the code which I
believe can detect non-freed allocated objects.


> +Documentation for MISRA C:2012 Dir 4.1: access to dead automatic object
> +_______________________________________________________________________
> +
> +To be written.
> +Example:
> +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.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: access to dead thread object
> +____________________________________________________________________
> +
> +To be written.
> +Example:
> +The program does not use per-thread variables.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: access using null pointer
> +_________________________________________________________________
> +
> +To be written.
> +Example:
> +All possibly null pointers are checked before access.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: access using invalid pointer
> +____________________________________________________________________
> +
> +To be written.
> +Example:
> +Usage of pointers is limited.  Pointers passed as parameters are
> +always checked for validity.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: access using out-of-bounds pointer
> +__________________________________________________________________________
> +
> +To be written.
> +Example:
> +Pointers are never uses to access arrays: indices are always used
> +instead.

I am not certain this is true. I would say instead "Pointers are never
used to access arrays without checking for the array size first"


> +Documentation for MISRA C:2012 Dir 4.1: access using unaligned pointer
> +______________________________________________________________________
> +
> +To be written.
> +Example:
> +Pointer conversion that may result in unaligned pointers are never used.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: mistyped access to object
> +_________________________________________________________________
> +
> +To be written.
> +Example:
> +Pointer conversions that may result in mistyped accesses to objects
> +are never used.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: mistyped access to function
> +___________________________________________________________________
> +
> +To be written.
> +Example:
> +The code never uses function pointers.

We do use function pointers. What does it mean "mistyped access to
function"? Also wouldn't this class of type error be detected by
gcc/eclair/cppcheck/coverity?


> +Documentation for MISRA C:2012 Dir 4.1: invalid pointer arithmetic
> +__________________________________________________________________
> +
> +To be written.
> +Example:
> +Pointer arithmetic is never used.

I think it might be used sometimes. I would say: "Pointer arithmetic is
never used without checking object boundaries"


> +Documentation for MISRA C:2012 Dir 4.1: invalid pointer comparison
> +__________________________________________________________________
> +
> +To be written.
> +Example:
> +Arrays are always accessed using indices instead of pointers.  Pointers
> +are only compared to NULL.

I would say instead that pointers to different objects are never
compared (expect for pointers that are not really pointers but actually
linker symbols but they are deviated)


> +Documentation for MISRA C:2012 Dir 4.1: overlapping copy
> +________________________________________________________
> +
> +To be written.
> +Example:
> +The code never uses memcpy() and does not perform assignment of
> +overlapping objects (which is doable only via pointers).

We do use memcpy but we never use it to copy overlapping objects.


> +Documentation for MISRA C:2012 Dir 4.1: invalid arguments to function
> +_____________________________________________________________________
> +
> +To be written.
> +Example:
> +All parameters to functions are checked for validity.

this..

> +Documentation for MISRA C:2012 Dir 4.1: returned function error
> +_______________________________________________________________
> +
> +To be written.
> +Example:
> +All functions that may produce an error, do returns a suitable status code
> +that is checked at each call site.

.. and this are aspirational, in the sense that we wish they were true
in all cases but they are not today. Is that OK to write it anyway as an
explanation?


> +
> +Documentation for MISRA C:2012 Dir 4.1: tainted input
> +_____________________________________________________
> +
> +To be written.
> +Example:
> +All parameters of all functions in the API are checked before being used.

I would clarify saying "external ABI" instead of API


> +Documentation for MISRA C:2012 Dir 4.1: data race
> +_________________________________________________
> +
> +To be written.
> +Example:
> +No function in this code is meant to be executed from interrupt handlers or
> +in a multi-threading environment.

We do have multiple "threads" and code executed from interrupt handlers.
I would say instead that we protect data using spinlocks and other forms
of locks appropriately.


> +Documentation for MISRA C:2012 Dir 4.1: invariant violation
> +___________________________________________________________
> +
> +To be written.

What's an invariant violation?


> +Documentation for MISRA C:2012 Dir 4.1: communication error
> +___________________________________________________________
> +
> +To be written.
> +Example:
> +This project does not involve any external communication.
> diff --git a/docs/misra/rules.rst b/docs/misra/rules.rst
> index 34916e266aa5..84bb57c8e908 100644
> --- a/docs/misra/rules.rst
> +++ b/docs/misra/rules.rst
> @@ -47,7 +47,12 @@ maintainers if you want to suggest a change.
>     * - `Dir 2.1 <https://gitlab.com/MISRA/MISRA-C/MISRA-C-2012/Example-Suite/-/blob/master/D_02_01.c>`_
>       - Required
>       - All source files shall compile without any compilation errors
> -     -
> +
> +   * - `Dir 4.1 <https://gitlab.com/MISRA/MISRA-C/MISRA-C-2012/Example-Suite/-/blob/master/D_04_01.c>`_
> +     - Required
> +     - Run-time failures shall be minimized
> +     - The strategies adopted by Xen to prevent certain classes of runtime
> +       failures will be documented by `C-runtime-failures.rst <docs/misra/C-runtime-failures.rst>`_

I would say "is documented" because we don't want to go back and change
rules.rst if/when we update C-runtime-failures.rst

Also (nit) you can wrap around at 80 chars to make it easier to read as
it will still be displayed the same way by gitlab and other RST
renderers



>     * - `Dir 4.7 <https://gitlab.com/MISRA/MISRA-C/MISRA-C-2012/Example-Suite/-/blob/master/D_04_07.c>`_
>       - Required

Re: [XEN PATCH 2/3] docs: make the docs for MISRA C:2012 Dir 4.1 visible to ECLAIR

[Stefano Stabellini]

On Fri, 1 Sep 2023, Nicola Vetrini wrote:
> To be able to check for the existence of the necessary subsections in
> the documentation for MISRA C:2012 Dir 4.1, ECLAIR needs to have a source
> file that is built.
> 
> This file is generated from 'C-runtime-failures.rst' in docs/misra
> and the configuration is updated accordingly.
> 
> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
> ---
> Changes from RFC:
> - Dropped unused/useless code
> - Revised the sed command
> - Revised the clean target
> ---
>  docs/Makefile       |  7 ++++++-
>  docs/misra/Makefile | 17 +++++++++++++++++
>  2 files changed, 23 insertions(+), 1 deletion(-)
>  create mode 100644 docs/misra/Makefile
> 
> diff --git a/docs/Makefile b/docs/Makefile
> index 966a104490ac..ff991a0c3ca2 100644
> --- a/docs/Makefile
> +++ b/docs/Makefile
> @@ -43,7 +43,7 @@ DOC_PDF  := $(patsubst %.pandoc,pdf/%.pdf,$(PANDOCSRC-y)) \
>  all: build
>  
>  .PHONY: build
> -build: html txt pdf man-pages figs
> +build: html txt pdf man-pages figs misra
>  
>  .PHONY: sphinx-html
>  sphinx-html:
> @@ -66,9 +66,14 @@ endif
>  .PHONY: pdf
>  pdf: $(DOC_PDF)
>  
> +.PHONY: misra
> +misra:
> +	$(MAKE) -C misra
> +
>  .PHONY: clean
>  clean: clean-man-pages
>  	$(MAKE) -C figs clean
> +	$(MAKE) -C misra clean
>  	rm -rf .word_count *.aux *.dvi *.bbl *.blg *.glo *.idx *~
>  	rm -rf *.ilg *.log *.ind *.toc *.bak *.tmp core
>  	rm -rf html txt pdf sphinx/html
> diff --git a/docs/misra/Makefile b/docs/misra/Makefile
> new file mode 100644
> index 000000000000..8ea0505c8a20
> --- /dev/null
> +++ b/docs/misra/Makefile
> @@ -0,0 +1,17 @@
> +TARGETS := C-runtime-failures.o
> +
> +all: $(TARGETS)
> +
> +# sed is used in place of cat to prevent occurrences of '*/'
> +# in the .rst from breaking the compilation

Please expand this comment with what you are doing in this makefile and
specifically what kind of .c file you are generating and why.

Everything else looks good.


> +$(TARGETS:.o=.c): %.c: %.rst
> +	echo "/*\n" > $@.tmp
> +	sed -e 's|\*/|*//*|g' $< >> $@.tmp
> +	echo "\n*/" >> $@.tmp
> +	mv $@.tmp $@
> +
> +%.o: %.c
> +	$(CC) -c $< -o $@
> +
> +clean:
> +	rm -f C-runtime-failures.c *.o *.tmp
> -- 
> 2.34.1
> 

Re: [XEN PATCH 3/3] automation/eclair: build docs/misra to address MISRA C:2012 Dir 4.1

[Stefano Stabellini]

On Fri, 1 Sep 2023, Nicola Vetrini wrote:
> The documentation pertaining Directive 4.1 is contained in docs/misra.
> The build script driving the analysis is amended to allow ECLAIR to
> analyze such file.
> 
> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
> ---
>  automation/eclair_analysis/build.sh   | 11 ++++++++---
>  automation/eclair_analysis/prepare.sh |  5 +++--
>  2 files changed, 11 insertions(+), 5 deletions(-)
> 
> diff --git a/automation/eclair_analysis/build.sh b/automation/eclair_analysis/build.sh
> index ec087dd822fa..556ed698bf8b 100755
> --- a/automation/eclair_analysis/build.sh
> +++ b/automation/eclair_analysis/build.sh
> @@ -34,11 +34,16 @@ else
>  fi
>  
>  (
> -  cd xen
> -
>    make "-j${PROCESSORS}" "-l${PROCESSORS}.0"    \
>         "CROSS_COMPILE=${CROSS_COMPILE}"         \
>         "CC=${CROSS_COMPILE}gcc-12"              \
>         "CXX=${CROSS_COMPILE}g++-12"             \
> -       "XEN_TARGET_ARCH=${XEN_TARGET_ARCH}"
> +       "XEN_TARGET_ARCH=${XEN_TARGET_ARCH}"     \
> +       -C docs misra

I don't think you need all these options to generate docs and misra.
Probably it would be sufficient just make -C docs misra

However given that they are not harmful:

Reviewed-by: Stefano Stabellini <sstabellini@kernel.org>


> +  make "-j${PROCESSORS}" "-l${PROCESSORS}.0"    \
> +       "CROSS_COMPILE=${CROSS_COMPILE}"         \
> +       "CC=${CROSS_COMPILE}gcc-12"              \
> +       "CXX=${CROSS_COMPILE}g++-12"             \
> +       "XEN_TARGET_ARCH=${XEN_TARGET_ARCH}"     \
> +			 -C xen
>  )
> diff --git a/automation/eclair_analysis/prepare.sh b/automation/eclair_analysis/prepare.sh
> index 275a1a3f517c..452e309b658b 100755
> --- a/automation/eclair_analysis/prepare.sh
> +++ b/automation/eclair_analysis/prepare.sh
> @@ -35,8 +35,9 @@ else
>  fi
>  
>  (
> -    cd xen
> -    cp "${CONFIG_FILE}" .config
> +    ./configure
> +    cp "${CONFIG_FILE}" xen/.config
>      make clean
> +    cd xen
>      make -f ${script_dir}/Makefile.prepare prepare
>  )
> -- 
> 2.34.1
> 

Re: [XEN PATCH 1/3] docs/misra: add documentation skeleton for MISRA C:2012 Dir 4.1

[Jan Beulich]

On 08.09.2023 02:20, Stefano Stabellini wrote:
> On Fri, 1 Sep 2023, Nicola Vetrini wrote:
>> +Documentation for MISRA C:2012 Dir 4.1: read from uninitialized allocated object
>> +________________________________________________________________________________
>> +
>> +To be written.
>> +Example:
>> +The code does not use dynamically allocated storage.
> 
> We do use dynamically allocated storage with xzalloc but xzalloc
> initializes the object to zero

Just at the example of this: I'm not sure in how far the examples given
were actually meant to (remotely) apply to our code base. As to your
reply - there's also xmalloc() which doesn't, and the page allocator,
and other more specialized ones.

Jan

Re: [XEN PATCH 2/3] docs: make the docs for MISRA C:2012 Dir 4.1 visible to ECLAIR

[Nicola Vetrini]

On 08/09/2023 02:23, Stefano Stabellini wrote:
> On Fri, 1 Sep 2023, Nicola Vetrini wrote:
>> To be able to check for the existence of the necessary subsections in
>> the documentation for MISRA C:2012 Dir 4.1, ECLAIR needs to have a 
>> source
>> file that is built.
>> 
>> This file is generated from 'C-runtime-failures.rst' in docs/misra
>> and the configuration is updated accordingly.
>> 
>> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
>> ---
>> Changes from RFC:
>> - Dropped unused/useless code
>> - Revised the sed command
>> - Revised the clean target
>> ---
>>  docs/Makefile       |  7 ++++++-
>>  docs/misra/Makefile | 17 +++++++++++++++++
>>  2 files changed, 23 insertions(+), 1 deletion(-)
>>  create mode 100644 docs/misra/Makefile
>> 
>> diff --git a/docs/Makefile b/docs/Makefile
>> index 966a104490ac..ff991a0c3ca2 100644
>> --- a/docs/Makefile
>> +++ b/docs/Makefile
>> @@ -43,7 +43,7 @@ DOC_PDF  := $(patsubst 
>> %.pandoc,pdf/%.pdf,$(PANDOCSRC-y)) \
>>  all: build
>> 
>>  .PHONY: build
>> -build: html txt pdf man-pages figs
>> +build: html txt pdf man-pages figs misra
>> 
>>  .PHONY: sphinx-html
>>  sphinx-html:
>> @@ -66,9 +66,14 @@ endif
>>  .PHONY: pdf
>>  pdf: $(DOC_PDF)
>> 
>> +.PHONY: misra
>> +misra:
>> +	$(MAKE) -C misra
>> +
>>  .PHONY: clean
>>  clean: clean-man-pages
>>  	$(MAKE) -C figs clean
>> +	$(MAKE) -C misra clean
>>  	rm -rf .word_count *.aux *.dvi *.bbl *.blg *.glo *.idx *~
>>  	rm -rf *.ilg *.log *.ind *.toc *.bak *.tmp core
>>  	rm -rf html txt pdf sphinx/html
>> diff --git a/docs/misra/Makefile b/docs/misra/Makefile
>> new file mode 100644
>> index 000000000000..8ea0505c8a20
>> --- /dev/null
>> +++ b/docs/misra/Makefile
>> @@ -0,0 +1,17 @@
>> +TARGETS := C-runtime-failures.o
>> +
>> +all: $(TARGETS)
>> +
>> +# sed is used in place of cat to prevent occurrences of '*/'
>> +# in the .rst from breaking the compilation
> 
> Please expand this comment with what you are doing in this makefile and
> specifically what kind of .c file you are generating and why.
> 
> Everything else looks good.
> 

Ok

-- 
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)

Re: [XEN PATCH 3/3] automation/eclair: build docs/misra to address MISRA C:2012 Dir 4.1

[Nicola Vetrini]

On 08/09/2023 02:25, Stefano Stabellini wrote:
> On Fri, 1 Sep 2023, Nicola Vetrini wrote:
>> The documentation pertaining Directive 4.1 is contained in docs/misra.
>> The build script driving the analysis is amended to allow ECLAIR to
>> analyze such file.
>> 
>> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
>> ---
>>  automation/eclair_analysis/build.sh   | 11 ++++++++---
>>  automation/eclair_analysis/prepare.sh |  5 +++--
>>  2 files changed, 11 insertions(+), 5 deletions(-)
>> 
>> diff --git a/automation/eclair_analysis/build.sh 
>> b/automation/eclair_analysis/build.sh
>> index ec087dd822fa..556ed698bf8b 100755
>> --- a/automation/eclair_analysis/build.sh
>> +++ b/automation/eclair_analysis/build.sh
>> @@ -34,11 +34,16 @@ else
>>  fi
>> 
>>  (
>> -  cd xen
>> -
>>    make "-j${PROCESSORS}" "-l${PROCESSORS}.0"    \
>>         "CROSS_COMPILE=${CROSS_COMPILE}"         \
>>         "CC=${CROSS_COMPILE}gcc-12"              \
>>         "CXX=${CROSS_COMPILE}g++-12"             \
>> -       "XEN_TARGET_ARCH=${XEN_TARGET_ARCH}"
>> +       "XEN_TARGET_ARCH=${XEN_TARGET_ARCH}"     \
>> +       -C docs misra
> 
> I don't think you need all these options to generate docs and misra.
> Probably it would be sufficient just make -C docs misra
> 
> However given that they are not harmful:
> 
> Reviewed-by: Stefano Stabellini <sstabellini@kernel.org>
> 
> 

Ok, I'll try it out for the next version, otherwise I'll revert to this 
invocation.

-- 
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)

Re: [XEN PATCH 1/3] docs/misra: add documentation skeleton for MISRA C:2012 Dir 4.1

[Nicola Vetrini]

On 08/09/2023 08:33, Jan Beulich wrote:
> On 08.09.2023 02:20, Stefano Stabellini wrote:
>> On Fri, 1 Sep 2023, Nicola Vetrini wrote:
>>> +Documentation for MISRA C:2012 Dir 4.1: read from uninitialized 
>>> allocated object
>>> +________________________________________________________________________________
>>> +
>>> +To be written.
>>> +Example:
>>> +The code does not use dynamically allocated storage.
>> 
>> We do use dynamically allocated storage with xzalloc but xzalloc
>> initializes the object to zero
> 
> Just at the example of this: I'm not sure in how far the examples given
> were actually meant to (remotely) apply to our code base. As to your
> reply - there's also xmalloc() which doesn't, and the page allocator,
> and other more specialized ones.
> 

You're right in saying that these examples are not tied to Xen 
specifically, these categories
of runtime failures are just the default ones present in ECLAIR. Both 
the matched text and
the categories can be amended, if the community deems it valuable.

-- 
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)

Re: [XEN PATCH 1/3] docs/misra: add documentation skeleton for MISRA C:2012 Dir 4.1

[Nicola Vetrini]

>> diff --git a/docs/misra/rules.rst b/docs/misra/rules.rst
>> index 34916e266aa5..84bb57c8e908 100644
>> --- a/docs/misra/rules.rst
>> +++ b/docs/misra/rules.rst
>> @@ -47,7 +47,12 @@ maintainers if you want to suggest a change.
>>     * - `Dir 2.1 
>> <https://gitlab.com/MISRA/MISRA-C/MISRA-C-2012/Example-Suite/-/blob/master/D_02_01.c>`_
>>       - Required
>>       - All source files shall compile without any compilation errors
>> -     -
>> +
>> +   * - `Dir 4.1 
>> <https://gitlab.com/MISRA/MISRA-C/MISRA-C-2012/Example-Suite/-/blob/master/D_04_01.c>`_
>> +     - Required
>> +     - Run-time failures shall be minimized
>> +     - The strategies adopted by Xen to prevent certain classes of 
>> runtime
>> +       failures will be documented by `C-runtime-failures.rst 
>> <docs/misra/C-runtime-failures.rst>`_
> 
> I would say "is documented" because we don't want to go back and change
> rules.rst if/when we update C-runtime-failures.rst
> 
> Also (nit) you can wrap around at 80 chars to make it easier to read as
> it will still be displayed the same way by gitlab and other RST
> renderers
> 
> 
> 
>>     * - `Dir 4.7 
>> <https://gitlab.com/MISRA/MISRA-C/MISRA-C-2012/Example-Suite/-/blob/master/D_04_07.c>`_
>>       - Required

Ok

-- 
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)

Re: [XEN PATCH 2/3] docs: make the docs for MISRA C:2012 Dir 4.1 visible to ECLAIR

[Anthony PERARD]

On Fri, Sep 01, 2023 at 11:06:39AM +0200, Nicola Vetrini wrote:
> diff --git a/docs/misra/Makefile b/docs/misra/Makefile
> new file mode 100644
> index 000000000000..8ea0505c8a20
> --- /dev/null
> +++ b/docs/misra/Makefile
> @@ -0,0 +1,17 @@
> +TARGETS := C-runtime-failures.o
> +
> +all: $(TARGETS)
> +
> +# sed is used in place of cat to prevent occurrences of '*/'
> +# in the .rst from breaking the compilation
> +$(TARGETS:.o=.c): %.c: %.rst
> +	echo "/*\n" > $@.tmp

This doesn't really works as you expect. Depending on the shell used or
the echo binary used, the "\n" would write a <new-line> or justs "\n".
Bash just write "\n" for example, while dash does write a <new-line>.
But, you can use `printf` instead:
    printf "/*\n\n" > $@.tmp

> +	sed -e 's|\*/|*//*|g' $< >> $@.tmp
> +	echo "\n*/" >> $@.tmp

Same here.


Thanks,

-- 
Anthony PERARD

Re: [XEN PATCH 1/3] docs/misra: add documentation skeleton for MISRA C:2012 Dir 4.1

[Stefano Stabellini]

On Fri, 8 Sep 2023, Jan Beulich wrote:
> On 08.09.2023 02:20, Stefano Stabellini wrote:
> > On Fri, 1 Sep 2023, Nicola Vetrini wrote:
> >> +Documentation for MISRA C:2012 Dir 4.1: read from uninitialized allocated object
> >> +________________________________________________________________________________
> >> +
> >> +To be written.
> >> +Example:
> >> +The code does not use dynamically allocated storage.
> > 
> > We do use dynamically allocated storage with xzalloc but xzalloc
> > initializes the object to zero
> 
> Just at the example of this: I'm not sure in how far the examples given
> were actually meant to (remotely) apply to our code base.

I thought they were generic examples as Nicola later confirmed. But
surprisingly many of them apply to our code base. I tried to highlight
the ones that are obviously wrong.


> As to your reply - there's also xmalloc() which doesn't, and the page
> allocator, and other more specialized ones.

Yes my reply was wrong in this case: I vastly underestimated the amount
of callers to xmalloc() that we have (and I grepped wrongly).

I think we should say instead:

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.

Re: [XEN PATCH 2/3] docs: make the docs for MISRA C:2012 Dir 4.1 visible to ECLAIR

[Nicola Vetrini]

On 08/09/2023 13:04, Anthony PERARD wrote:
> On Fri, Sep 01, 2023 at 11:06:39AM +0200, Nicola Vetrini wrote:
>> diff --git a/docs/misra/Makefile b/docs/misra/Makefile
>> new file mode 100644
>> index 000000000000..8ea0505c8a20
>> --- /dev/null
>> +++ b/docs/misra/Makefile
>> @@ -0,0 +1,17 @@
>> +TARGETS := C-runtime-failures.o
>> +
>> +all: $(TARGETS)
>> +
>> +# sed is used in place of cat to prevent occurrences of '*/'
>> +# in the .rst from breaking the compilation
>> +$(TARGETS:.o=.c): %.c: %.rst
>> +	echo "/*\n" > $@.tmp
> 
> This doesn't really works as you expect. Depending on the shell used or
> the echo binary used, the "\n" would write a <new-line> or justs "\n".
> Bash just write "\n" for example, while dash does write a <new-line>.
> But, you can use `printf` instead:
>     printf "/*\n\n" > $@.tmp
> 
>> +	sed -e 's|\*/|*//*|g' $< >> $@.tmp
>> +	echo "\n*/" >> $@.tmp
> 
> Same here.
> 
> 

Thanks, I'll fix it in the next version.

-- 
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)

Re: [XEN PATCH 1/3] docs/misra: add documentation skeleton for MISRA C:2012 Dir 4.1

[Nicola Vetrini]

>> +Documentation for MISRA C:2012 Dir 4.1: invariant violation
>> +___________________________________________________________
>> +
>> +To be written.
> 
> What's an invariant violation?
> 
> 

It's the violation of a project invariant (e.g., an assert or 
BUILD_BUG).
Something along the lines of this could fit in the documentation:
"The extensive checks in the code ensure that any violation of a
compile-time invariant will be detected in prior to release builds, and 
failure
of run-time invariant is also extensively tested."

-- 
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)