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

[Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>]

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)