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)
