| Message ID | 816b323f5e325784947d09502f9352188bd325cf.1719381829.git.federico.serafini@bugseng.com (mailing list archive) |
|---|---|
| State | New |
| Headers | show |
| Series | [XEN,v2,for-4.19] automation/eclair: add deviations agreed in MISRA meetings | expand |
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.serafini@bugseng.com> Reviewed-by: Stefano Stabellini <sstabellini@kernel.org> release-ack requested > --- > 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(^xen/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_mask16)))"} > +-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_mfn))"} > +-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_conditional_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)_unsafe_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 >
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.serafini@bugseng.com> > > Reviewed-by: Stefano Stabellini <sstabellini@kernel.org> > > release-ack requested Release-Acked-By: Oleksii Kurochko <oleksii.kurochko@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 > >
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(^xen/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_mask16)))"} +-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_mfn))"} +-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_conditional_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)_unsafe_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
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.serafini@bugseng.com> --- 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(-)