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

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

CC-ing also Henry Wang, as these are just documentation and CI changes

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 |   4 +-
 docs/Makefile                         |   7 +-
 docs/misra/C-runtime-failures.rst     | 200 ++++++++++++++++++++++++++
 docs/misra/Makefile                   |  22 +++
 docs/misra/rules.rst                  |   8 +-
 6 files changed, 240 insertions(+), 7 deletions(-)
 create mode 100644 docs/misra/C-runtime-failures.rst
 create mode 100644 docs/misra/Makefile

--
2.34.1

[XEN PATCH v2 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.
---
 docs/misra/C-runtime-failures.rst | 200 ++++++++++++++++++++++++++++++
 docs/misra/rules.rst              |   8 +-
 2 files changed, 207 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..325d3fab1fa5
--- /dev/null
+++ b/docs/misra/C-runtime-failures.rst
@@ -0,0 +1,200 @@
+===================================================================
+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 the 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
+___________________________________________________________________
+
+The code never uses function pointers.
+
+
+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
+___________________________________________________________
+
+To be written.
+
+
+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 8e7d17d242a0..dd71fbe87f43 100644
--- a/docs/misra/rules.rst
+++ b/docs/misra/rules.rst
@@ -47,7 +47,13 @@ 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 is 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 v2 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
---
 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..8fd89404e96b
--- /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*/" >> $@.tmp
+	mv $@.tmp $@
+
+%.o: %.c
+	$(CC) -c $< -o $@
+
+clean:
+	rm -f C-runtime-failures.c *.o *.tmp
-- 
2.34.1

[XEN PATCH v2 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 v2:
- removed useless make flags
---
 automation/eclair_analysis/build.sh   | 6 +++---
 automation/eclair_analysis/prepare.sh | 4 ++--
 2 files changed, 5 insertions(+), 5 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..ebd5a2dde676 100755
--- a/automation/eclair_analysis/prepare.sh
+++ b/automation/eclair_analysis/prepare.sh
@@ -35,8 +35,8 @@ 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
-- 
2.34.1

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

[Henry Wang]

Hi Nicola,

> On Sep 27, 2023, at 17:52, Nicola Vetrini <nicola.vetrini@bugseng.com> 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.
> 
> CC-ing also Henry Wang, as these are just documentation and CI changes

Indeed, so technically it is safe to include this series to 4.18, if this series can
be properly reviewed, I am ok to add my release-ack tag for each patch:

Release-acked-by: Henry Wang <Henry.Wang@arm.com>

Kind regards,
Henry


> 
> 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 |   4 +-
> docs/Makefile                         |   7 +-
> docs/misra/C-runtime-failures.rst     | 200 ++++++++++++++++++++++++++
> docs/misra/Makefile                   |  22 +++
> docs/misra/rules.rst                  |   8 +-
> 6 files changed, 240 insertions(+), 7 deletions(-)
> create mode 100644 docs/misra/C-runtime-failures.rst
> create mode 100644 docs/misra/Makefile
> 
> --
> 2.34.1

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

[Nicola Vetrini]

On 27/09/2023 11:52, 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>
> ---
> Changes in v2:
> - removed useless make flags
> ---
>  automation/eclair_analysis/build.sh   | 6 +++---
>  automation/eclair_analysis/prepare.sh | 4 ++--
>  2 files changed, 5 insertions(+), 5 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..ebd5a2dde676 100755
> --- a/automation/eclair_analysis/prepare.sh
> +++ b/automation/eclair_analysis/prepare.sh
> @@ -35,8 +35,8 @@ 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

Hi, I observed a failure when running the analysis job of this series 
through patchew, so
I think it's a good idea to put this patch on hold until I've figured 
out what's wrong.
Sorry for the inconvenience.

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

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

[Anthony PERARD]

On Wed, Sep 27, 2023 at 11:52:31AM +0200, 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
> 
> Changes in v2:
> - Added explanative comment to the makefile
> - printf instead of echo

Reviewed-by: Anthony PERARD <anthony.perard@citrix.com>

Thanks,

-- 
Anthony PERARD

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

[Stefano Stabellini]

On Wed, 27 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>

Reviewed-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
> ---
>  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..8fd89404e96b
> --- /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*/" >> $@.tmp
> +	mv $@.tmp $@
> +
> +%.o: %.c
> +	$(CC) -c $< -o $@
> +
> +clean:
> +	rm -f C-runtime-failures.c *.o *.tmp
> -- 
> 2.34.1
> 

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

[Henry Wang]

> On Sep 28, 2023, at 08:49, Stefano Stabellini <sstabellini@kernel.org> wrote:
> 
> On Wed, 27 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>
> 
> Reviewed-by: Stefano Stabellini <sstabellini@kernel.org>

Release-acked-by: Henry Wang <Henry.Wang@arm.com>

Kind regards,
Henry
> 
> 
>> ---
>> 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
>> ---
>> 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..8fd89404e96b
>> --- /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*/" >> $@.tmp
>> + mv $@.tmp $@
>> +
>> +%.o: %.c
>> + $(CC) -c $< -o $@
>> +
>> +clean:
>> + rm -f C-runtime-failures.c *.o *.tmp
>> -- 
>> 2.34.1
>> 

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

[Stefano Stabellini]

On Wed, 27 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 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.
> ---
>  docs/misra/C-runtime-failures.rst | 200 ++++++++++++++++++++++++++++++
>  docs/misra/rules.rst              |   8 +-
>  2 files changed, 207 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..325d3fab1fa5
> --- /dev/null
> +++ b/docs/misra/C-runtime-failures.rst
> @@ -0,0 +1,200 @@
> +===================================================================
> +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 the is present in the code concerns
                     ^ that


> +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
> +___________________________________________________________________
> +
> +The code never uses function pointers.

You missed my previous comment on this one



> +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
> +___________________________________________________________
> +
> +To be written.

Also this one escaped.

Overall, this is much better!



> +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 8e7d17d242a0..dd71fbe87f43 100644
> --- a/docs/misra/rules.rst
> +++ b/docs/misra/rules.rst
> @@ -47,7 +47,13 @@ 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 is 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
> 

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

[Nicola Vetrini]

On 27/09/2023 15:29, Nicola Vetrini wrote:
> On 27/09/2023 11:52, 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>
>> ---
>> Changes in v2:
>> - removed useless make flags
>> ---
>>  automation/eclair_analysis/build.sh   | 6 +++---
>>  automation/eclair_analysis/prepare.sh | 4 ++--
>>  2 files changed, 5 insertions(+), 5 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..ebd5a2dde676 100755
>> --- a/automation/eclair_analysis/prepare.sh
>> +++ b/automation/eclair_analysis/prepare.sh
>> @@ -35,8 +35,8 @@ 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
> 
> Hi, I observed a failure when running the analysis job of this series
> through patchew, so
> I think it's a good idea to put this patch on hold until I've figured
> out what's wrong.
> Sorry for the inconvenience.

I found the culprit; there is a minor issue with patches 2/3 and 3/3.
I'll submit a new one and address the other review comments as well.
The changes will be minimal, so perhaps I will be able to retain the 
R-by-s.

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

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

[Nicola Vetrini]

On 28/09/2023 02:55, Stefano Stabellini wrote:
> On Wed, 27 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.

>> +
>> +Documentation for MISRA C:2012 Dir 4.1: mistyped access to function
>> +___________________________________________________________________
>> +
>> +The code never uses function pointers.
> 
> You missed my previous comment on this one
> 

You're right.
This is about the usage of a function having a certain signature as 
having another.
It could happen for instance:
- with incongruent declarations
- no prototypes
- casts on function pointers
Most of these can be caught by complying with other rules, but I'm not 
sure if they
fully cover every case, and besides there are still violations on the 
rules tied to this.
I guess we can say that this is a WIP.

>> +
>> +Documentation for MISRA C:2012 Dir 4.1: invariant violation
>> +___________________________________________________________
>> +
>> +To be written.
> 
> Also this one escaped.
> 
> Overall, this is much better!
> 

I replied on v1, but maybe I missed some further reply:
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)

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

[Stefano Stabellini]

On Thu, 28 Sep 2023, Nicola Vetrini wrote:
> On 28/09/2023 02:55, Stefano Stabellini wrote:
> > On Wed, 27 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.
> 
> > > +
> > > +Documentation for MISRA C:2012 Dir 4.1: mistyped access to function
> > > +___________________________________________________________________
> > > +
> > > +The code never uses function pointers.
> > 
> > You missed my previous comment on this one
> > 
> 
> You're right.
> This is about the usage of a function having a certain signature as having
> another.
> It could happen for instance:
> - with incongruent declarations
> - no prototypes
> - casts on function pointers
> Most of these can be caught by complying with other rules, but I'm not sure if
> they
> fully cover every case, and besides there are still violations on the rules
> tied to this.
> I guess we can say that this is a WIP.

We do want to follow these guidelines and like you wrote they are
covered by other MISRA rules that we have adopted and we are already
scanning for (or planning to) using ECLAIR. I think we should highlight
that, especially we have done a lot of work on incongruent declarations
and missing prototypes.


> > > +
> > > +Documentation for MISRA C:2012 Dir 4.1: invariant violation
> > > +___________________________________________________________
> > > +
> > > +To be written.
> > 
> > Also this one escaped.
> > 
> > Overall, this is much better!
> > 
> 
> I replied on v1, but maybe I missed some further reply:
> 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."

We can also add the number of invariants is drastically reduced in
release builds.

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

[Nicola Vetrini]

On 27/09/2023 11:52, 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.
> 
> CC-ing also Henry Wang, as these are just documentation and CI changes
> 
> 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 |   4 +-
>  docs/Makefile                         |   7 +-
>  docs/misra/C-runtime-failures.rst     | 200 ++++++++++++++++++++++++++
>  docs/misra/Makefile                   |  22 +++
>  docs/misra/rules.rst                  |   8 +-
>  6 files changed, 240 insertions(+), 7 deletions(-)
>  create mode 100644 docs/misra/C-runtime-failures.rst
>  create mode 100644 docs/misra/Makefile
> 
> --
> 2.34.1

CC-ing Luca as well:
I'm testing the next version of this series, and I'm seeing a failure on 
cppcheck
containers on this pipeline [1]. I'm not sure about what is causing that 
conversion script
to fail. Any pointer in debugging this would be greatly appreciated.

[1] 
https://gitlab.com/xen-project/people/bugseng/xen/-/pipelines/1020917280

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

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

[Luca Fancellu]

> 
> CC-ing Luca as well:
> I'm testing the next version of this series, and I'm seeing a failure on cppcheck
> containers on this pipeline [1]. I'm not sure about what is causing that conversion script
> to fail. Any pointer in debugging this would be greatly appreciated.
> 
> [1] https://gitlab.com/xen-project/people/bugseng/xen/-/pipelines/1020917280

Hi Nicola,

In the logs I can see:

+ xen/scripts/xen-analysis.py --run-cppcheck --cppcheck-misra -- -j80
No notes for rule 2.1
WARNING: Can't open /builds/xen-project/people/bugseng/xen/xen/drivers/video/font_8x14.c: 'utf-8' codec can't decode byte 0x9f in position 7228: invalid start byte
WARNING: Can't open /builds/xen-project/people/bugseng/xen/xen/drivers/video/font_8x16.c: 'utf-8' codec can't decode byte 0x80 in position 5436: invalid start byte
WARNING: Can't open /builds/xen-project/people/bugseng/xen/xen/drivers/video/font_8x8.c: 'utf-8' codec can't decode byte 0x80 in position 4410: invalid start byte
ERROR: An error occured when running:
/builds/xen-project/people/bugseng/xen/xen/tools/convert_misra_doc.py -i /builds/xen-project/people/bugseng/xen/docs/misra/rules.rst -o /builds/xen-project/people/bugseng/xen/xen/cppcheck-misra.txt -j /builds/xen-project/people/bugseng/xen/xen/cppcheck-misra.json

So I think that the rules.rst doesn’t have the expected syntax, on patch 1 try to leave the third ‘-‘ on the rule 2.1:

* - `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
-

Cheers,
Luca