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

[Julien Grall <julien@xxxxxxx>]

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@xxxxxxxxxxx>
> > Acked-by: Stefano Stabellini <sstabellini@xxxxxxxxxx>
> >
> >
> > > ---
> > > 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