On Wed, 2024-06-26 at 17:41 -0700, Stefano Stabellini wrote:
> On Wed, 26 Jun 2024, Federico Serafini wrote:
> > Update ECLAIR configuration to take into account the deviations
> > agreed during the MISRA meetings.
> >
> > While doing this, remove the obsolete "Set [123]" comments.
> >
> > Signed-off-by: Federico Serafini <federico.seraf...@bugseng.com>
>
> Reviewed-by: Stefano Stabellini <sstabell...@kernel.org>
>
> release-ack requested
Release-Acked-By: Oleksii Kurochko <oleksii.kuroc...@gmail.com>
~ Oleksii
>
>
> > ---
> > Changes in v2:
> > - keep sync between deviations.ecl and deviations.rst;
> > - use 'deliberate' tag for all the deviations of R14.3;
> > - do not use the term "project-wide deviation" since it does not
> > add useful
> > information.
> > ---
> > .../eclair_analysis/ECLAIR/deviations.ecl | 93
> > +++++++++++++++++--
> > docs/misra/deviations.rst | 81 ++++++++++++++-
> > -
> > 2 files changed, 158 insertions(+), 16 deletions(-)
> >
> > diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl
> > b/automation/eclair_analysis/ECLAIR/deviations.ecl
> > index ae2eaf50f7..37cad8bf68 100644
> > --- a/automation/eclair_analysis/ECLAIR/deviations.ecl
> > +++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
> > @@ -1,5 +1,3 @@
> > -### Set 1 ###
> > -
> > #
> > # Series 2.
> > #
> > @@ -23,6 +21,11 @@ Constant expressions and unreachable branches of
> > if and switch statements are ex
> > -config=MC3R1.R2.1,reports+={deliberate,
> > "any_area(any_loc(any_exp(macro(name(ASSERT_UNREACHABLE||PARSE_ERR_
> > RET||PARSE_ERR||FAIL_MSR||FAIL_CPUID)))))"}
> > -doc_end
> >
> > +-doc_begin="The asm-offset files are not linked deliberately,
> > since they are used to generate definitions for asm modules."
> > +-file_tag+={asm_offsets,
> > "^xen/arch/(arm|x86)/(arm32|arm64|x86_64)/asm-offsets\\.c$"}
> > +-config=MC3R1.R2.1,reports+={deliberate,
> > "any_area(any_loc(file(asm_offsets)))"}
> > +-doc_end
> > +
> > -doc_begin="Pure declarations (i.e., declarations without
> > initialization) are
> > not executable, and therefore it is safe for them to be
> > unreachable."
> > -config=MC3R1.R2.1,ignored_stmts+={"any()", "pure_decl()"}
> > @@ -63,6 +66,12 @@ they are not instances of commented-out code."
> > -
> > config=MC3R1.D4.3,reports+={disapplied,"!(any_area(any_loc(file(^xe
> > n/arch/arm/arm64/.*$))))"}
> > -doc_end
> >
> > +-doc_begin="The inline asm in 'arm64/lib/bitops.c' is tightly
> > coupled with the surronding C code that acts as a wrapper, so it
> > has been decided not to add an additional encapsulation layer."
> > +-file_tag+={arm64_bitops, "^xen/arch/arm/arm64/lib/bitops\\.c$"}
> > +-config=MC3R1.D4.3,reports+={deliberate,
> > "all_area(any_loc(file(arm64_bitops)&&any_exp(macro(^(bit|test)op$)
> > )))"}
> > +-config=MC3R1.D4.3,reports+={deliberate,
> > "any_area(any_loc(file(arm64_bitops))&&context(name(int_clear_mask1
> > 6)))"}
> > +-doc_end
> > +
> > -doc_begin="This header file is autogenerated or empty, therefore
> > it poses no
> > risk if included more than once."
> > -file_tag+={empty_header, "^xen/arch/arm/efi/runtime\\.h$"}
> > @@ -213,10 +222,25 @@ Therefore the absence of prior declarations
> > is safe."
> > -config=MC3R1.R8.4,declarations+={safe,
> > "loc(file(asm_defns))&&^current_stack_pointer$"}
> > -doc_end
> >
> > +-doc_begin="The function apei_(read|check|clear)_mce are dead code
> > and are excluded from non-debug builds, therefore the absence of
> > prior declarations is safe."
> > +-config=MC3R1.R8.4,declarations+={safe,
> > "^apei_(read|check|clear)_mce\\(.*$"}
> > +-doc_end
> > +
> > -doc_begin="asmlinkage is a marker to indicate that the function
> > is only used to interface with asm modules."
> > -
> > config=MC3R1.R8.4,declarations+={safe,"loc(text(^(?s).*asmlinkage.*
> > $, -1..0))"}
> > -doc_end
> >
> > +-doc_begin="Given that bsearch and sort are defined with the
> > attribute 'gnu_inline', it's deliberate not to have a prior
> > declaration.
> > +See Section \"6.33.1 Common Function Attributes\" of
> > \"GCC_MANUAL\" for a full explanation of gnu_inline."
> > +-file_tag+={bsearch_sort, "^xen/include/xen/(sort|lib)\\.h$"}
> > +-config=MC3R1.R8.4,reports+={deliberate,
> > "any_area(any_loc(file(bsearch_sort))&&decl(name(bsearch||sort)))"}
> > +-doc_end
> > +
> > +-doc_begin="first_valid_mfn is defined in this way because the
> > current lack of NUMA support in Arm and PPC requires it."
> > +-file_tag+={first_valid_mfn, "^xen/common/page_alloc\\.c$"}
> > +-
> > config=MC3R1.R8.4,declarations+={deliberate,"loc(file(first_valid_m
> > fn))"}
> > +-doc_end
> > +
> > -doc_begin="The following variables are compiled in multiple
> > translation units
> > belonging to different executables and therefore are safe."
> > -config=MC3R1.R8.6,declarations+={safe,
> > "name(current_stack_pointer||bsearch||sort)"}
> > @@ -257,8 +281,6 @@ dimension is higher than omitting the
> > dimension."
> > -config=MC3R1.R9.5,reports+={deliberate, "any()"}
> > -doc_end
> >
> > -### Set 2 ###
> > -
> > #
> > # Series 10.
> > #
> > @@ -299,7 +321,6 @@ integers arguments on two's complement
> > architectures
> > -config=MC3R1.R10.1,reports+={safe,
> > "any_area(any_loc(any_exp(macro(^ISOLATE_LSB$))))"}
> > -doc_end
> >
> > -### Set 3 ###
> > -doc_begin="XEN only supports architectures where signed integers
> > are
> > representend using two's complement and all the XEN developers are
> > aware of
> > this."
> > @@ -323,6 +344,49 @@ constant expressions are required.\""
> > # Series 11
> > #
> >
> > +-doc_begin="The conversion from a function pointer to unsigned
> > long or (void *) does not lose any information, provided that the
> > target type has enough bits to store it."
> > +-config=MC3R1.R11.1,casts+={safe,
> > + "from(type(canonical(__function_pointer_types)))
> > + &&to(type(canonical(builtin(unsigned
> > long)||pointer(builtin(void)))))
> > + &&relation(definitely_preserves_value)"
> > +}
> > +-doc_end
> > +
> > +-doc_begin="The conversion from a function pointer to a boolean
> > has a well-known semantics that do not lead to unexpected
> > behaviour."
> > +-config=MC3R1.R11.1,casts+={safe,
> > + "from(type(canonical(__function_pointer_types)))
> > + &&kind(pointer_to_boolean)"
> > +}
> > +-doc_end
> > +
> > +-doc_begin="The conversion from a pointer to an incomplete type to
> > unsigned long does not lose any information, provided that the
> > target type has enough bits to store it."
> > +-config=MC3R1.R11.2,casts+={safe,
> > + "from(type(any()))
> > + &&to(type(canonical(builtin(unsigned long))))
> > + &&relation(definitely_preserves_value)"
> > +}
> > +-doc_end
> > +
> > +-doc_begin="Conversions to object pointers that have a pointee
> > type with a smaller (i.e., less strict) alignment requirement are
> > safe."
> > +-config=MC3R1.R11.3,casts+={safe,
> > + "!relation(more_aligned_pointee)"
> > +}
> > +-doc_end
> > +
> > +-doc_begin="Conversions from and to integral types are safe, in
> > the assumption that the target type has enough bits to store the
> > value.
> > +See also Section \"4.7 Arrays and Pointers\" of \"GCC_MANUAL\""
> > +-config=MC3R1.R11.6,casts+={safe,
> > +
> > "(from(type(canonical(integral())))||to(type(canonical(integral()))
> > ))
> > + &&relation(definitely_preserves_value)"}
> > +-doc_end
> > +
> > +-doc_begin="The conversion from a pointer to a boolean has a well-
> > known semantics that do not lead to unexpected behaviour."
> > +-config=MC3R1.R11.6,casts+={safe,
> > + "from(type(canonical(__pointer_types)))
> > + &&kind(pointer_to_boolean)"
> > +}
> > +-doc_end
> > +
> > -doc_begin="Violations caused by container_of are due to pointer
> > arithmetic operations
> > with the provided offset. The resulting pointer is then
> > immediately cast back to its
> > original type, which preserves the qualifier. This use is deemed
> > safe.
> > @@ -354,9 +418,18 @@ activity."
> > -config=MC3R1.R14.2,reports+={disapplied,"any()"}
> > -doc_end
> >
> > --doc_begin="The XEN team relies on the fact that invariant
> > conditions of 'if'
> > -statements are deliberate"
> > --config=MC3R1.R14.3,statements={deliberate ,
> > "wrapped(any(),node(if_stmt))" }
> > +-doc_begin="The XEN team relies on the fact that invariant
> > conditions of 'if' statements and conditional operators are
> > deliberate"
> > +-config=MC3R1.R14.3,statements+={deliberate,
> > "wrapped(any(),node(if_stmt||conditional_operator||binary_condition
> > al_operator))" }
> > +-doc_end
> > +
> > +-doc_begin="Switches having a 'sizeof' operator as the condition
> > are deliberate and have limited scope."
> > +-config=MC3R1.R14.3,statements+={deliberate,
> > "wrapped(any(),node(switch_stmt)&&child(cond, operator(sizeof)))" }
> > +-doc_end
> > +
> > +-doc_begin="The use of an invariant size argument in
> > {put,get}_unsafe_size and array_access_ok, as defined in
> > arch/x86(_64)?/include/asm/uaccess.h is deliberate and is deemed
> > safe."
> > +-file_tag+={x86_uaccess,
> > "^xen/arch/x86(_64)?/include/asm/uaccess\\.h$"}
> > +-config=MC3R1.R14.3,reports+={deliberate,
> > "any_area(any_loc(file(x86_uaccess)&&any_exp(macro(^(put|get)_unsaf
> > e_size$))))"}
> > +-config=MC3R1.R14.3,reports+={deliberate,
> > "any_area(any_loc(file(x86_uaccess)&&any_exp(macro(^array_access_ok
> > $))))"}
> > -doc_end
> >
> > -doc_begin="A controlling expression of 'if' and iteration
> > statements having integer, character or pointer type has a
> > semantics that is well-known to all Xen developers."
> > @@ -527,8 +600,8 @@ falls under the jurisdiction of other MISRA
> > rules."
> > # General
> > #
> >
> > --doc_begin="do-while-0 is a well recognized loop idiom by the xen
> > community."
> > --loop_idioms={do_stmt, "literal(0)"}
> > +-doc_begin="do-while-[01] is a well recognized loop idiom by the
> > xen community."
> > +-loop_idioms={do_stmt, "literal(0)||literal(1)"}
> > -doc_end
> > -doc_begin="while-[01] is a well recognized loop idiom by the xen
> > community."
> > -loop_idioms+={while_stmt, "literal(0)||literal(1)"}
> > diff --git a/docs/misra/deviations.rst b/docs/misra/deviations.rst
> > index 16fc345756..d682616796 100644
> > --- a/docs/misra/deviations.rst
> > +++ b/docs/misra/deviations.rst
> > @@ -63,6 +63,11 @@ Deviations related to MISRA C:2012 Rules:
> > switch statement.
> > - ECLAIR has been configured to ignore those statements.
> >
> > + * - R2.1
> > + - The asm-offset files are not linked deliberately, since
> > they are used to
> > + generate definitions for asm modules.
> > + - Tagged as `deliberate` for ECLAIR.
> > +
> > * - R2.2
> > - Proving compliance with respect to Rule 2.2 is generally
> > impossible:
> > see `<https://arxiv.org/abs/2212.13933>`_ for details.
> > Moreover, peer
> > @@ -203,6 +208,26 @@ Deviations related to MISRA C:2012 Rules:
> > it.
> > - Tagged as `safe` for ECLAIR.
> >
> > + * - R8.4
> > + - Some functions are excluded from non-debug build, therefore
> > the absence
> > + of declaration is safe.
> > + - Tagged as `safe` for ECLAIR, such functions are:
> > + - apei_read_mce()
> > + - apei_check_mce()
> > + - apei_clear_mce()
> > +
> > + * - R8.4
> > + - Given that bsearch and sort are defined with the attribute
> > 'gnu_inline',
> > + it's deliberate not to have a prior declaration.
> > + See Section \"6.33.1 Common Function Attributes\" of
> > \"GCC_MANUAL\" for
> > + a full explanation of gnu_inline.
> > + - Tagged as `deliberate` for ECLAIR.
> > +
> > + * - R8.4
> > + - first_valid_mfn is defined in this way because the current
> > lack of NUMA
> > + support in Arm and PPC requires it.
> > + - Tagged as `deliberate` for ECLAIR.
> > +
> > * - R8.6
> > - The following variables are compiled in multiple
> > translation units
> > belonging to different executables and therefore are safe.
> > @@ -282,6 +307,39 @@ Deviations related to MISRA C:2012 Rules:
> > If no bits are set, 0 is returned.
> > - Tagged as `safe` for ECLAIR.
> >
> > + * - R11.1
> > + - The conversion from a function pointer to unsigned long or
> > (void \*) does
> > + not lose any information, provided that the target type has
> > enough bits
> > + to store it.
> > + - Tagged as `safe` for ECLAIR.
> > +
> > + * - R11.1
> > + - The conversion from a function pointer to a boolean has a
> > well-known
> > + semantics that do not lead to unexpected behaviour.
> > + - Tagged as `safe` for ECLAIR.
> > +
> > + * - R11.2
> > + - The conversion from a pointer to an incomplete type to
> > unsigned long
> > + does not lose any information, provided that the target
> > type has enough
> > + bits to store it.
> > + - Tagged as `safe` for ECLAIR.
> > +
> > + * - R11.3
> > + - Conversions to object pointers that have a pointee type
> > with a smaller
> > + (i.e., less strict) alignment requirement are safe.
> > + - Tagged as `safe` for ECLAIR.
> > +
> > + * - R11.6
> > + - Conversions from and to integral types are safe, in the
> > assumption that
> > + the target type has enough bits to store the value.
> > + See also Section \"4.7 Arrays and Pointers\" of
> > \"GCC_MANUAL\"
> > + - Tagged as `safe` for ECLAIR.
> > +
> > + * - R11.6
> > + - The conversion from a pointer to a boolean has a well-known
> > semantics
> > + that do not lead to unexpected behaviour.
> > + - Tagged as `safe` for ECLAIR.
> > +
> > * - R11.8
> > - Violations caused by container_of are due to pointer
> > arithmetic operations
> > with the provided offset. The resulting pointer is then
> > immediately cast back to its
> > @@ -308,8 +366,19 @@ Deviations related to MISRA C:2012 Rules:
> >
> > * - R14.3
> > - The Xen team relies on the fact that invariant conditions
> > of 'if'
> > - statements are deliberate.
> > - - Project-wide deviation; tagged as `disapplied` for ECLAIR.
> > + statements and conditional operators are deliberate.
> > + - Tagged as `deliberate` for ECLAIR.
> > +
> > + * - R14.3
> > + - Switches having a 'sizeof' operator as the condition are
> > deliberate and
> > + have limited scope.
> > + - Tagged as `deliberate` for ECLAIR.
> > +
> > + * - R14.3
> > + - The use of an invariant size argument in
> > {put,get}_unsafe_size and
> > + array_access_ok, as defined in
> > arch/x86(_64)?/include/asm/uaccess.h is
> > + deliberate and is deemed safe.
> > + - Tagged as `deliberate` for ECLAIR.
> >
> > * - R14.4
> > - A controlling expression of 'if' and iteration statements
> > having
> > @@ -475,10 +544,10 @@ Other deviations:
> > * - Deviation
> > - Justification
> >
> > - * - do-while-0 loops
> > - - The do-while-0 is a well-recognized loop idiom used by the
> > Xen community
> > - and can therefore be used, even though it would cause a
> > number of
> > - violations in some instances.
> > + * - do-while-0 and do-while-1 loops
> > + - The do-while-0 and do-while-1 loops are well-recognized
> > loop idioms used
> > + by the Xen community and can therefore be used, even though
> > they would
> > + cause a number of violations in some instances.
> >
> > * - while-0 and while-1 loops
> > - while-0 and while-1 are well-recognized loop idioms used by
> > the Xen
> > --
> > 2.34.1
> >
