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

[XEN PATCH v3 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.

Note: The previous version of this series already had a release ack from Henry,
which I didn't add in each commit message since I see in the commit history that
tag being the last.

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   |   6 +-
 automation/eclair_analysis/prepare.sh |   7 +-
 docs/Makefile                         |   7 +-
 docs/misra/C-runtime-failures.rst     | 210 ++++++++++++++++++++++++++
 docs/misra/Makefile                   |  22 +++
 docs/misra/rules.rst                  |   7 +
 6 files changed, 252 insertions(+), 7 deletions(-)
 create mode 100644 docs/misra/C-runtime-failures.rst
 create mode 100644 docs/misra/Makefile

-- 
2.34.1

[XEN PATCH v3 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 still needs feedback from the
community.

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

Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
---
Changes in v2:
- Incorporated suggestions from Stefano.
Changes in v3:
- Replaced two leftover entries.
---
 docs/misra/C-runtime-failures.rst | 210 ++++++++++++++++++++++++++++++
 docs/misra/rules.rst              |   7 +
 2 files changed, 217 insertions(+)
 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..77e04a2562b8
--- /dev/null
+++ b/docs/misra/C-runtime-failures.rst
@@ -0,0 +1,210 @@
+===================================================================
+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
+________________________________________________
+
+Pervasive use of assertions and extensive test suite.
+
+
+Documentation for MISRA C:2012 Dir 4.1: unexpected wrapping
+___________________________________________________________
+
+The only wrapping that is present in the code concerns
+unsigned integers and they are all expected.
+
+
+Documentation for MISRA C:2012 Dir 4.1: invalid shift
+_____________________________________________________
+
+Pervasive use of assertions and extensive test suite.
+
+
+Documentation for MISRA C:2012 Dir 4.1: division/remainder by zero
+__________________________________________________________________
+
+The 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
+________________________________________________________________
+
+Code executed in interrupt handlers uses spinlocks or disables interrupts
+at the right locations to avoid unsequenced side effects.
+
+
+Documentation for MISRA C:2012 Dir 4.1: read from uninitialized automatic object
+________________________________________________________________________________
+
+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.
+
+
+Documentation for MISRA C:2012 Dir 4.1: read from uninitialized allocated object
+________________________________________________________________________________
+
+Dynamically allocated storage is used in a controlled manner, to prevent the
+access to uninitialized allocated storage.
+
+
+Documentation for MISRA C:2012 Dir 4.1: write to string literal or const object
+_______________________________________________________________________________
+
+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
+______________________________________________________________________________
+
+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.
+
+
+Documentation for MISRA C:2012 Dir 4.1: access to dead allocated object
+_______________________________________________________________________
+
+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.
+
+
+Documentation for MISRA C:2012 Dir 4.1: access to dead automatic object
+_______________________________________________________________________
+
+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
+____________________________________________________________________
+
+The program does not use per-thread variables.
+
+
+Documentation for MISRA C:2012 Dir 4.1: access using null pointer
+_________________________________________________________________
+
+All possibly null pointers are checked before access.
+
+
+Documentation for MISRA C:2012 Dir 4.1: access using invalid pointer
+____________________________________________________________________
+
+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
+__________________________________________________________________________
+
+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
+______________________________________________________________________
+
+Pointer conversion that may result in unaligned pointers are never used.
+
+
+Documentation for MISRA C:2012 Dir 4.1: mistyped access to object
+_________________________________________________________________
+
+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
+___________________________________________________________________
+
+This behaviour can arise, for instance, from:
+
+- incongruent declarations;
+- functions having no prototypes;
+- casts on function pointers.
+
+The project has adopted various compiler flags and MISRA rules to lessen the
+likelihood of this event.
+
+
+Documentation for MISRA C:2012 Dir 4.1: invalid pointer arithmetic
+__________________________________________________________________
+
+Pointer arithmetic is never used without checking object boundaries.
+
+
+Documentation for MISRA C:2012 Dir 4.1: invalid pointer comparison
+__________________________________________________________________
+
+Pointers to different objects are never compared (except for pointers that are
+actually linker symbols, but those cases are deviated with a justification).
+
+
+Documentation for MISRA C:2012 Dir 4.1: overlapping copy
+________________________________________________________
+
+The code never uses memcpy() to copy overlapping objects. The instances of
+assignments involving overlapping objects are very limited and motivated.
+
+
+Documentation for MISRA C:2012 Dir 4.1: invalid arguments to function
+_____________________________________________________________________
+
+Many parameters to functions are checked for validity; there is ongoing work to
+make this true for all parameters.
+
+
+Documentation for MISRA C:2012 Dir 4.1: returned function error
+_______________________________________________________________
+
+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.
+
+
+Documentation for MISRA C:2012 Dir 4.1: tainted input
+_____________________________________________________
+
+All parameters of all functions in the extenal ABI are checked before being
+used.
+
+
+Documentation for MISRA C:2012 Dir 4.1: data race
+_________________________________________________
+
+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.
+
+
+Documentation for MISRA C:2012 Dir 4.1: invariant violation
+___________________________________________________________
+
+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.
+
+
+Documentation for MISRA C:2012 Dir 4.1: communication error
+___________________________________________________________
+
+This project does not involve any external communication.
diff --git a/docs/misra/rules.rst b/docs/misra/rules.rst
index a2fe01464eec..3139ca7ae6dd 100644
--- a/docs/misra/rules.rst
+++ b/docs/misra/rules.rst
@@ -49,6 +49,13 @@ maintainers if you want to suggest a change.
      - 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 is 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
      - If a function returns error information then that error
-- 
2.34.1

[XEN PATCH v3 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

Changes in v2:
- Added explanative comment to the makefile
- printf instead of echo

Changes in v3:
- Terminate the generated file with a newline
- Build it with -std=c99, so that the documentation
  for D1.1 applies.
---
 docs/Makefile       |  7 ++++++-
 docs/misra/Makefile | 22 ++++++++++++++++++++++
 2 files changed, 28 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..949458ff9e15
--- /dev/null
+++ b/docs/misra/Makefile
@@ -0,0 +1,22 @@
+TARGETS := C-runtime-failures.o
+
+all: $(TARGETS)
+
+# This Makefile will generate the object files indicated in TARGETS by taking
+# the corresponding .rst file, converting its content to a C block comment and
+# then compiling the resulting .c file. This is needed for the file's content to
+# be available when performing static analysis with ECLAIR on the project.
+
+# sed is used in place of cat to prevent occurrences of '*/'
+# in the .rst from breaking the compilation
+$(TARGETS:.o=.c): %.c: %.rst
+	printf "/*\n\n" > $@.tmp
+	sed -e 's|\*/|*//*|g' $< >> $@.tmp
+	printf "\n\n*/\n" >> $@.tmp
+	mv $@.tmp $@
+
+%.o: %.c
+	$(CC) -std=c99 -c $< -o $@
+
+clean:
+	rm -f C-runtime-failures.c *.o *.tmp
-- 
2.34.1

[XEN PATCH v3 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>
---
Changes in v3:
- amended prepare script.
---
 automation/eclair_analysis/build.sh   | 6 +++---
 automation/eclair_analysis/prepare.sh | 7 ++++---
 2 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/automation/eclair_analysis/build.sh b/automation/eclair_analysis/build.sh
index ec087dd822fa..ea7a1e5a59b0 100755
--- a/automation/eclair_analysis/build.sh
+++ b/automation/eclair_analysis/build.sh
@@ -34,11 +34,11 @@ else
 fi
 
 (
-  cd xen
-
+  make -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}"
+       "XEN_TARGET_ARCH=${XEN_TARGET_ARCH}"     \
+       -C xen
 )
diff --git a/automation/eclair_analysis/prepare.sh b/automation/eclair_analysis/prepare.sh
index 0cac5eba00ae..fe9d16e48ecc 100755
--- a/automation/eclair_analysis/prepare.sh
+++ b/automation/eclair_analysis/prepare.sh
@@ -35,11 +35,12 @@ else
 fi
 
 (
-    cd xen
-    cp "${CONFIG_FILE}" .config
+    ./configure
+    cp "${CONFIG_FILE}" xen/.config
     make clean
     find . -type f -name "*.safparse" -print -delete
-    make -f ${script_dir}/Makefile.prepare prepare
+    cd xen
+    make -f "${script_dir}/Makefile.prepare" prepare
     # Translate the /* SAF-n-safe */ comments into ECLAIR CBTs
     scripts/xen-analysis.py --run-eclair --no-build --no-clean
 )
-- 
2.34.1

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

[Stefano Stabellini]

On Mon, 2 Oct 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 still needs feedback from the
> community.
> 
> The 'rules.rst' file is updated accordingly to mention the newly
> added documentation.
> 
> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>

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


> ---
> Changes in v2:
> - Incorporated suggestions from Stefano.
> Changes in v3:
> - Replaced two leftover entries.
> ---
>  docs/misra/C-runtime-failures.rst | 210 ++++++++++++++++++++++++++++++
>  docs/misra/rules.rst              |   7 +
>  2 files changed, 217 insertions(+)
>  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..77e04a2562b8
> --- /dev/null
> +++ b/docs/misra/C-runtime-failures.rst
> @@ -0,0 +1,210 @@
> +===================================================================
> +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
> +________________________________________________
> +
> +Pervasive use of assertions and extensive test suite.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: unexpected wrapping
> +___________________________________________________________
> +
> +The only wrapping that is present in the code concerns
> +unsigned integers and they are all expected.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: invalid shift
> +_____________________________________________________
> +
> +Pervasive use of assertions and extensive test suite.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: division/remainder by zero
> +__________________________________________________________________
> +
> +The 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
> +________________________________________________________________
> +
> +Code executed in interrupt handlers uses spinlocks or disables interrupts
> +at the right locations to avoid unsequenced side effects.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: read from uninitialized automatic object
> +________________________________________________________________________________
> +
> +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.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: read from uninitialized allocated object
> +________________________________________________________________________________
> +
> +Dynamically allocated storage is used in a controlled manner, to prevent the
> +access to uninitialized allocated storage.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: write to string literal or const object
> +_______________________________________________________________________________
> +
> +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
> +______________________________________________________________________________
> +
> +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.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: access to dead allocated object
> +_______________________________________________________________________
> +
> +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.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: access to dead automatic object
> +_______________________________________________________________________
> +
> +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
> +____________________________________________________________________
> +
> +The program does not use per-thread variables.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: access using null pointer
> +_________________________________________________________________
> +
> +All possibly null pointers are checked before access.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: access using invalid pointer
> +____________________________________________________________________
> +
> +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
> +__________________________________________________________________________
> +
> +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
> +______________________________________________________________________
> +
> +Pointer conversion that may result in unaligned pointers are never used.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: mistyped access to object
> +_________________________________________________________________
> +
> +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
> +___________________________________________________________________
> +
> +This behaviour can arise, for instance, from:
> +
> +- incongruent declarations;
> +- functions having no prototypes;
> +- casts on function pointers.
> +
> +The project has adopted various compiler flags and MISRA rules to lessen the
> +likelihood of this event.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: invalid pointer arithmetic
> +__________________________________________________________________
> +
> +Pointer arithmetic is never used without checking object boundaries.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: invalid pointer comparison
> +__________________________________________________________________
> +
> +Pointers to different objects are never compared (except for pointers that are
> +actually linker symbols, but those cases are deviated with a justification).
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: overlapping copy
> +________________________________________________________
> +
> +The code never uses memcpy() to copy overlapping objects. The instances of
> +assignments involving overlapping objects are very limited and motivated.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: invalid arguments to function
> +_____________________________________________________________________
> +
> +Many parameters to functions are checked for validity; there is ongoing work to
> +make this true for all parameters.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: returned function error
> +_______________________________________________________________
> +
> +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.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: tainted input
> +_____________________________________________________
> +
> +All parameters of all functions in the extenal ABI are checked before being
> +used.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: data race
> +_________________________________________________
> +
> +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.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: invariant violation
> +___________________________________________________________
> +
> +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.
> +
> +
> +Documentation for MISRA C:2012 Dir 4.1: communication error
> +___________________________________________________________
> +
> +This project does not involve any external communication.
> diff --git a/docs/misra/rules.rst b/docs/misra/rules.rst
> index a2fe01464eec..3139ca7ae6dd 100644
> --- a/docs/misra/rules.rst
> +++ b/docs/misra/rules.rst
> @@ -49,6 +49,13 @@ maintainers if you want to suggest a change.
>       - 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 is 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
>       - If a function returns error information then that error
> -- 
> 2.34.1
> 

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

[Stefano Stabellini]

On Mon, 2 Oct 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>

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


> ---
> Changes from RFC:
> - Dropped unused/useless code
> - Revised the sed command
> - Revised the clean target
> 
> Changes in v2:
> - Added explanative comment to the makefile
> - printf instead of echo
> 
> Changes in v3:
> - Terminate the generated file with a newline
> - Build it with -std=c99, so that the documentation
>   for D1.1 applies.
> ---
>  docs/Makefile       |  7 ++++++-
>  docs/misra/Makefile | 22 ++++++++++++++++++++++
>  2 files changed, 28 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..949458ff9e15
> --- /dev/null
> +++ b/docs/misra/Makefile
> @@ -0,0 +1,22 @@
> +TARGETS := C-runtime-failures.o
> +
> +all: $(TARGETS)
> +
> +# This Makefile will generate the object files indicated in TARGETS by taking
> +# the corresponding .rst file, converting its content to a C block comment and
> +# then compiling the resulting .c file. This is needed for the file's content to
> +# be available when performing static analysis with ECLAIR on the project.
> +
> +# sed is used in place of cat to prevent occurrences of '*/'
> +# in the .rst from breaking the compilation
> +$(TARGETS:.o=.c): %.c: %.rst
> +	printf "/*\n\n" > $@.tmp
> +	sed -e 's|\*/|*//*|g' $< >> $@.tmp
> +	printf "\n\n*/\n" >> $@.tmp
> +	mv $@.tmp $@
> +
> +%.o: %.c
> +	$(CC) -std=c99 -c $< -o $@
> +
> +clean:
> +	rm -f C-runtime-failures.c *.o *.tmp
> -- 
> 2.34.1
> 

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

[Stefano Stabellini]

On Mon, 2 Oct 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>

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


> ---
> Changes in v3:
> - amended prepare script.
> ---
>  automation/eclair_analysis/build.sh   | 6 +++---
>  automation/eclair_analysis/prepare.sh | 7 ++++---
>  2 files changed, 7 insertions(+), 6 deletions(-)
> 
> diff --git a/automation/eclair_analysis/build.sh b/automation/eclair_analysis/build.sh
> index ec087dd822fa..ea7a1e5a59b0 100755
> --- a/automation/eclair_analysis/build.sh
> +++ b/automation/eclair_analysis/build.sh
> @@ -34,11 +34,11 @@ else
>  fi
>  
>  (
> -  cd xen
> -
> +  make -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}"
> +       "XEN_TARGET_ARCH=${XEN_TARGET_ARCH}"     \
> +       -C xen
>  )
> diff --git a/automation/eclair_analysis/prepare.sh b/automation/eclair_analysis/prepare.sh
> index 0cac5eba00ae..fe9d16e48ecc 100755
> --- a/automation/eclair_analysis/prepare.sh
> +++ b/automation/eclair_analysis/prepare.sh
> @@ -35,11 +35,12 @@ else
>  fi
>  
>  (
> -    cd xen
> -    cp "${CONFIG_FILE}" .config
> +    ./configure
> +    cp "${CONFIG_FILE}" xen/.config
>      make clean
>      find . -type f -name "*.safparse" -print -delete
> -    make -f ${script_dir}/Makefile.prepare prepare
> +    cd xen
> +    make -f "${script_dir}/Makefile.prepare" prepare
>      # Translate the /* SAF-n-safe */ comments into ECLAIR CBTs
>      scripts/xen-analysis.py --run-eclair --no-build --no-clean
>  )
> -- 
> 2.34.1
> 

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

[Stefano Stabellini]

On Mon, 2 Oct 2023, Nicola Vetrini wrote:
> 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.
> 
> Note: The previous version of this series already had a release ack from Henry,
> which I didn't add in each commit message since I see in the commit history that
> tag being the last.
> 
> 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   |   6 +-
>  automation/eclair_analysis/prepare.sh |   7 +-
>  docs/Makefile                         |   7 +-
>  docs/misra/C-runtime-failures.rst     | 210 ++++++++++++++++++++++++++
>  docs/misra/Makefile                   |  22 +++
>  docs/misra/rules.rst                  |   7 +
>  6 files changed, 252 insertions(+), 7 deletions(-)
>  create mode 100644 docs/misra/C-runtime-failures.rst
>  create mode 100644 docs/misra/Makefile


Due to the code freeze, I committed these patches temporarily to:

https://gitlab.com/xen-project/people/sstabellini/xen.git for-4.19

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

[Stefano Stabellini]

+Julien, Andrew

Julien and Andrew raised concerns on this patch on the Xen Matrix
channel. Please provide further details.



On Mon, 2 Oct 2023, Stefano Stabellini wrote:
> On Mon, 2 Oct 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>
> 
> Acked-by: Stefano Stabellini <sstabellini@kernel.org>
> 
> 
> > ---
> > Changes from RFC:
> > - Dropped unused/useless code
> > - Revised the sed command
> > - Revised the clean target
> > 
> > Changes in v2:
> > - Added explanative comment to the makefile
> > - printf instead of echo
> > 
> > Changes in v3:
> > - Terminate the generated file with a newline
> > - Build it with -std=c99, so that the documentation
> >   for D1.1 applies.
> > ---
> >  docs/Makefile       |  7 ++++++-
> >  docs/misra/Makefile | 22 ++++++++++++++++++++++
> >  2 files changed, 28 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..949458ff9e15
> > --- /dev/null
> > +++ b/docs/misra/Makefile
> > @@ -0,0 +1,22 @@
> > +TARGETS := C-runtime-failures.o
> > +
> > +all: $(TARGETS)
> > +
> > +# This Makefile will generate the object files indicated in TARGETS by taking
> > +# the corresponding .rst file, converting its content to a C block comment and
> > +# then compiling the resulting .c file. This is needed for the file's content to
> > +# be available when performing static analysis with ECLAIR on the project.
> > +
> > +# sed is used in place of cat to prevent occurrences of '*/'
> > +# in the .rst from breaking the compilation
> > +$(TARGETS:.o=.c): %.c: %.rst
> > +	printf "/*\n\n" > $@.tmp
> > +	sed -e 's|\*/|*//*|g' $< >> $@.tmp
> > +	printf "\n\n*/\n" >> $@.tmp
> > +	mv $@.tmp $@
> > +
> > +%.o: %.c
> > +	$(CC) -std=c99 -c $< -o $@
> > +
> > +clean:
> > +	rm -f C-runtime-failures.c *.o *.tmp
> > -- 
> > 2.34.1
> > 
> 

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

[Julien Grall]

Hi Stefano,

On 07/11/2023 20:41, Stefano Stabellini wrote:
> +Julien, Andrew
> 
> Julien and Andrew raised concerns on this patch on the Xen Matrix
> channel. Please provide further details.

Thanks! It looks like I was already CCed but this likely got lost with 
all the MISRA patches...

On Matrix, there was concerned raised that the documentation now have a 
dependency on C compiler and you are also build C files in docs.

In addition to that, I have a few more comments.

> 
> 
> On Mon, 2 Oct 2023, Stefano Stabellini wrote:
>> On Mon, 2 Oct 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>
>>
>> Acked-by: Stefano Stabellini <sstabellini@kernel.org>
>>
>>
>>> ---
>>> Changes from RFC:
>>> - Dropped unused/useless code
>>> - Revised the sed command
>>> - Revised the clean target
>>>
>>> Changes in v2:
>>> - Added explanative comment to the makefile
>>> - printf instead of echo
>>>
>>> Changes in v3:
>>> - Terminate the generated file with a newline
>>> - Build it with -std=c99, so that the documentation
>>>    for D1.1 applies.
>>> ---
>>>   docs/Makefile       |  7 ++++++-
>>>   docs/misra/Makefile | 22 ++++++++++++++++++++++
>>>   2 files changed, 28 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

This means you always generate and compile the C files when it seems to 
be only useful for Eclair. I think we should consider to only call 
'misra' for the Eclair build.

The files should also be generated/compiled in an Eclair specific 
directory rather than in docs.

>>>   
>>>   .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..949458ff9e15
>>> --- /dev/null
>>> +++ b/docs/misra/Makefile
>>> @@ -0,0 +1,22 @@
>>> +TARGETS := C-runtime-failures.o

We don't usually have uppercase in the file name. Is this something that 
Eclair mandates? In fact, looking at the series, it is not clear how 
Eclair will find the file. Can you clarify?

>>> +
>>> +all: $(TARGETS)
>>> +
>>> +# This Makefile will generate the object files indicated in TARGETS by taking
>>> +# the corresponding .rst file, converting its content to a C block comment and
>>> +# then compiling the resulting .c file. This is needed for the file's content to
>>> +# be available when performing static analysis with ECLAIR on the project.

I am a bit lost with the explanation. The generated object will be 
empty. So why do you require to generate it?

Furthermore, the content doesn't seem to follow a specific syntax (or at 
least it is not clear that it should follow one). So why do you need to 
expose the content to Eclair?

>>> +
>>> +# sed is used in place of cat to prevent occurrences of '*/'
>>> +# in the .rst from breaking the compilation
>>> +$(TARGETS:.o=.c): %.c: %.rst
>>> +	printf "/*\n\n" > $@.tmp
>>> +	sed -e 's|\*/|*//*|g' $< >> $@.tmp
>>> +	printf "\n\n*/\n" >> $@.tmp
>>> +	mv $@.tmp $@
>>> +
>>> +%.o: %.c
>>> +	$(CC) -std=c99 -c $< -o $@

AFAICT, this will generate a file using the host compiler. This may be 
different from the compiler used to build Xen.

So I will repeat myself, how all of this matters? Maybe it would be 
useful if you provide some documentation from Eclair.

Cheers,

-- 
Julien Grall

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

[Nicola Vetrini]

On 2023-11-08 17:25, Julien Grall wrote:
> Hi Stefano,
> 
> On 07/11/2023 20:41, Stefano Stabellini wrote:
>> +Julien, Andrew
>> 
>> Julien and Andrew raised concerns on this patch on the Xen Matrix
>> channel. Please provide further details.
> 
> Thanks! It looks like I was already CCed but this likely got lost with 
> all the MISRA patches...
> 
> On Matrix, there was concerned raised that the documentation now have a 
> dependency on C compiler and you are also build C files in docs.
> 
> In addition to that, I have a few more comments.
> 

The .rst file was chosen to have a human-readable format for the runtime 
failures
documentation. The other option that is otherwise viable is having a 
dummy .c or .h in
the sources (in this case it would likely be under xen/).

The transformation of this file into a .c file could be done from xen's 
Makefile of course,
but I reckoned that would have been more difficult, as the Makefile for 
the docs is
far shorter.

>>>> 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
> 
> This means you always generate and compile the C files when it seems to 
> be only useful for Eclair. I think we should consider to only call 
> 'misra' for the Eclair build.
> 
> The files should also be generated/compiled in an Eclair specific 
> directory rather than in docs.
> 

Hmm, that is not a bad idea

>>>>     .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..949458ff9e15
>>>> --- /dev/null
>>>> +++ b/docs/misra/Makefile
>>>> @@ -0,0 +1,22 @@
>>>> +TARGETS := C-runtime-failures.o
> 
> We don't usually have uppercase in the file name. Is this something 
> that Eclair mandates? In fact, looking at the series, it is not clear 
> how Eclair will find the file. Can you clarify?
> 

Not really. I was just following the naming convention of 
C-language-toolchain.rst, as the
two files are in some ways related.

ECLAIR intercepts toolchain invocations, so the compilation can happen 
anywhere* in the
repository in the current setup.

* I actually need to test this, but an ECLAIR-specific directory is 
indeed a good fit.

>>>> +
>>>> +all: $(TARGETS)
>>>> +
>>>> +# This Makefile will generate the object files indicated in TARGETS 
>>>> by taking
>>>> +# the corresponding .rst file, converting its content to a C block 
>>>> comment and
>>>> +# then compiling the resulting .c file. This is needed for the 
>>>> file's content to
>>>> +# be available when performing static analysis with ECLAIR on the 
>>>> project.
> 
> I am a bit lost with the explanation. The generated object will be 
> empty. So why do you require to generate it?
> 

See above. The only requirement is that some intercepted toolchain 
invocation happens
and that the processed file has a comment block containing the strings 
specified below.
The resulting artifact isn't needed in any way.

> Furthermore, the content doesn't seem to follow a specific syntax (or 
> at least it is not clear that it should follow one). So why do you need 
> to expose the content to Eclair?
> 

Under the hood there's a regex matching the resulting comment block 
against a set of default
templates used to indicate that the project has some form of 
documentation around runtime
failures. The default templates are along these lines (the comment begin 
and end markers
need not be on the same line):

/* Documentation for MISRA C:2012 Dir 4.1: overflow <description> */

If the string is matched, then documentation for that particular 
category of runtime
failures is deemed present, otherwise a violation will be reported (one 
for each category).
Both the categories and format of the string to be matched can be 
customized, but I'd like
to avoid doing that.

>>>> +
>>>> +# sed is used in place of cat to prevent occurrences of '*/'
>>>> +# in the .rst from breaking the compilation
>>>> +$(TARGETS:.o=.c): %.c: %.rst
>>>> +	printf "/*\n\n" > $@.tmp
>>>> +	sed -e 's|\*/|*//*|g' $< >> $@.tmp
>>>> +	printf "\n\n*/\n" >> $@.tmp
>>>> +	mv $@.tmp $@
>>>> +
>>>> +%.o: %.c
>>>> +	$(CC) -std=c99 -c $< -o $@
> 
> AFAICT, this will generate a file using the host compiler. This may be 
> different from the compiler used to build Xen.
> 
> So I will repeat myself, how all of this matters? Maybe it would be 
> useful if you provide some documentation from Eclair.
> 
> Cheers,

The only non-trivial bit is that the file 
automation/eclair_analysis/ECLAIR/toolchain.ecl
specifies some compilers (if this needs to be adjusted to something 
other that $(CC), then I
may need some additional guidance) and the c99 standard, hence if you 
use a different
compiler ECLAIR will complain that you didn't document the toolchain 
assumptions according
to D1.1 (which is incidentally why we created the file 
C-language-toolchain.rst).

I hope this clears up any doubts about the patch.

Kind Regards,

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

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

[Julien Grall]

Hi,

On 08/11/2023 17:12, Nicola Vetrini wrote:
> On 2023-11-08 17:25, Julien Grall wrote:
>> Hi Stefano,
>>
>> On 07/11/2023 20:41, Stefano Stabellini wrote:
>>> +Julien, Andrew
>>>
>>> Julien and Andrew raised concerns on this patch on the Xen Matrix
>>> channel. Please provide further details.
>>
>> Thanks! It looks like I was already CCed but this likely got lost with 
>> all the MISRA patches...
>>
>> On Matrix, there was concerned raised that the documentation now have 
>> a dependency on C compiler and you are also build C files in docs.
>>
>> In addition to that, I have a few more comments.
>>
> 
> The .rst file was chosen to have a human-readable format for the runtime 
> failures
> documentation. The other option that is otherwise viable is having a 
> dummy .c or .h in
> the sources (in this case it would likely be under xen/).
> 
> The transformation of this file into a .c file could be done from xen's 
> Makefile of course,
> but I reckoned that would have been more difficult, as the Makefile for 
> the docs is
> far shorter

I understand that the Makefile for docs is shorter. However this seems 
to be the wrong place to "compile" a file.

I think it makes more sense to do it from xen/ as those deviations are 
only for the hypervisor. IOW they don't apply for the tools.

[....]

>>>>> +
>>>>> +all: $(TARGETS)
>>>>> +
>>>>> +# This Makefile will generate the object files indicated in 
>>>>> TARGETS by taking
>>>>> +# the corresponding .rst file, converting its content to a C block 
>>>>> comment and
>>>>> +# then compiling the resulting .c file. This is needed for the 
>>>>> file's content to
>>>>> +# be available when performing static analysis with ECLAIR on the 
>>>>> project.
>>
>> I am a bit lost with the explanation. The generated object will be 
>> empty. So why do you require to generate it?
>>
> 
> See above. The only requirement is that some intercepted toolchain 
> invocation happens
> and that the processed file has a comment block containing the strings 
> specified below.
> The resulting artifact isn't needed in any way.

Just to confirm, there is no way for Eclair to specify some extra file 
that don't require "compilation"?

> 
>> Furthermore, the content doesn't seem to follow a specific syntax (or 
>> at least it is not clear that it should follow one). So why do you 
>> need to expose the content to Eclair?
>>
> 
> Under the hood there's a regex matching the resulting comment block 
> against a set of default
> templates used to indicate that the project has some form of 
> documentation around runtime
> failures. The default templates are along these lines (the comment begin 
> and end markers
> need not be on the same line):
> 
> /* Documentation for MISRA C:2012 Dir 4.1: overflow <description> */
> 
> If the string is matched, then documentation for that particular 
> category of runtime
> failures is deemed present, otherwise a violation will be reported (one 
> for each category).
> Both the categories and format of the string to be matched can be 
> customized, but I'd like
> to avoid doing that.

Ok. The format should be documented at top of the rst file so a 
developper knows how to modify the file correctly.

> 
>>>>> +
>>>>> +# sed is used in place of cat to prevent occurrences of '*/'
>>>>> +# in the .rst from breaking the compilation
>>>>> +$(TARGETS:.o=.c): %.c: %.rst
>>>>> +    printf "/*\n\n" > $@.tmp
>>>>> +    sed -e 's|\*/|*//*|g' $< >> $@.tmp
>>>>> +    printf "\n\n*/\n" >> $@.tmp
>>>>> +    mv $@.tmp $@
>>>>> +
>>>>> +%.o: %.c
>>>>> +    $(CC) -std=c99 -c $< -o $@
>>
>> AFAICT, this will generate a file using the host compiler. This may be 
>> different from the compiler used to build Xen.
>>
>> So I will repeat myself, how all of this matters? Maybe it would be 
>> useful if you provide some documentation from Eclair.
>>
>> Cheers,
> 
> The only non-trivial bit is that the file 
> automation/eclair_analysis/ECLAIR/toolchain.ecl
> specifies some compilers (if this needs to be adjusted to something 
> other that $(CC), then I
> may need some additional guidance) and the c99 standard, hence if you 
> use a different
> compiler ECLAIR will complain that you didn't document the toolchain 
> assumptions according
> to D1.1 (which is incidentally why we created the file 
> C-language-toolchain.rst).

We should use the same/compiler as used by the hypervisor. I feel 
anything else is just a gross hack and may break in the long term. Hence 
why it makes a lot more sense to generate/"compile" the file from the 
hypervisor Makefile.

Cheers,

-- 
Julien Grall

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

[Nicola Vetrini]

On 2023-11-09 13:05, Julien Grall wrote:
> Hi,
> 
> On 08/11/2023 17:12, Nicola Vetrini wrote:
>> On 2023-11-08 17:25, Julien Grall wrote:
>>> Hi Stefano,
>>> 
>>> On 07/11/2023 20:41, Stefano Stabellini wrote:
>>>> +Julien, Andrew
>>>> 
>>>> Julien and Andrew raised concerns on this patch on the Xen Matrix
>>>> channel. Please provide further details.
>>> 
>>> Thanks! It looks like I was already CCed but this likely got lost 
>>> with all the MISRA patches...
>>> 
>>> On Matrix, there was concerned raised that the documentation now have 
>>> a dependency on C compiler and you are also build C files in docs.
>>> 
>>> In addition to that, I have a few more comments.
>>> 
>> 
>> The .rst file was chosen to have a human-readable format for the 
>> runtime failures
>> documentation. The other option that is otherwise viable is having a 
>> dummy .c or .h in
>> the sources (in this case it would likely be under xen/).
>> 
>> The transformation of this file into a .c file could be done from 
>> xen's Makefile of course,
>> but I reckoned that would have been more difficult, as the Makefile 
>> for the docs is
>> far shorter
> 
> I understand that the Makefile for docs is shorter. However this seems 
> to be the wrong place to "compile" a file.
> 
> I think it makes more sense to do it from xen/ as those deviations are 
> only for the hypervisor. IOW they don't apply for the tools.
> 
> [....]
> 

I have the intention to place this in the eclair analysis build script, 
to keep the
modifications to a minimum.

>>>>>> +
>>>>>> +all: $(TARGETS)
>>>>>> +
>>>>>> +# This Makefile will generate the object files indicated in 
>>>>>> TARGETS by taking
>>>>>> +# the corresponding .rst file, converting its content to a C 
>>>>>> block comment and
>>>>>> +# then compiling the resulting .c file. This is needed for the 
>>>>>> file's content to
>>>>>> +# be available when performing static analysis with ECLAIR on the 
>>>>>> project.
>>> 
>>> I am a bit lost with the explanation. The generated object will be 
>>> empty. So why do you require to generate it?
>>> 
>> 
>> See above. The only requirement is that some intercepted toolchain 
>> invocation happens
>> and that the processed file has a comment block containing the strings 
>> specified below.
>> The resulting artifact isn't needed in any way.
> 
> Just to confirm, there is no way for Eclair to specify some extra file 
> that don't require "compilation"?
> 

Correct.

>> 
>>> Furthermore, the content doesn't seem to follow a specific syntax (or 
>>> at least it is not clear that it should follow one). So why do you 
>>> need to expose the content to Eclair?
>>> 
>> 
>> Under the hood there's a regex matching the resulting comment block 
>> against a set of default
>> templates used to indicate that the project has some form of 
>> documentation around runtime
>> failures. The default templates are along these lines (the comment 
>> begin and end markers
>> need not be on the same line):
>> 
>> /* Documentation for MISRA C:2012 Dir 4.1: overflow <description> */
>> 
>> If the string is matched, then documentation for that particular 
>> category of runtime
>> failures is deemed present, otherwise a violation will be reported 
>> (one for each category).
>> Both the categories and format of the string to be matched can be 
>> customized, but I'd like
>> to avoid doing that.
> 
> Ok. The format should be documented at top of the rst file so a 
> developper knows how to modify the file correctly.
> 

Ok. Although the authoritative reference is the ECLAIR User Manual, so 
what I'll put here is to be taken as an example.

>> 
>>>>>> +
>>>>>> +# sed is used in place of cat to prevent occurrences of '*/'
>>>>>> +# in the .rst from breaking the compilation
>>>>>> +$(TARGETS:.o=.c): %.c: %.rst
>>>>>> +    printf "/*\n\n" > $@.tmp
>>>>>> +    sed -e 's|\*/|*//*|g' $< >> $@.tmp
>>>>>> +    printf "\n\n*/\n" >> $@.tmp
>>>>>> +    mv $@.tmp $@
>>>>>> +
>>>>>> +%.o: %.c
>>>>>> +    $(CC) -std=c99 -c $< -o $@
>>> 
>>> AFAICT, this will generate a file using the host compiler. This may 
>>> be different from the compiler used to build Xen.
>>> 
>>> So I will repeat myself, how all of this matters? Maybe it would be 
>>> useful if you provide some documentation from Eclair.
>>> 
>>> Cheers,
>> 
>> The only non-trivial bit is that the file 
>> automation/eclair_analysis/ECLAIR/toolchain.ecl
>> specifies some compilers (if this needs to be adjusted to something 
>> other that $(CC), then I
>> may need some additional guidance) and the c99 standard, hence if you 
>> use a different
>> compiler ECLAIR will complain that you didn't document the toolchain 
>> assumptions according
>> to D1.1 (which is incidentally why we created the file 
>> C-language-toolchain.rst).
> 
> We should use the same/compiler as used by the hypervisor. I feel 
> anything else is just a gross hack and may break in the long term. 
> Hence why it makes a lot more sense to generate/"compile" the file from 
> the hypervisor Makefile.
> 

See above. Placing the compilation in the analysis script will use the 
same compiler used for the hypervisor.

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