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

[Nicola Vetrini <nicola.vetrini@bugseng.com>]

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)