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-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)