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)
