From nobody Mon Sep 16 19:44:21 2024 Delivered-To: importer@patchew.org Received-SPF: pass (zohomail.com: domain of lists.xenproject.org designates 192.237.175.120 as permitted sender) client-ip=192.237.175.120; envelope-from=xen-devel-bounces@lists.xenproject.org; helo=lists.xenproject.org; Authentication-Results: mx.zohomail.com; spf=pass (zohomail.com: domain of lists.xenproject.org designates 192.237.175.120 as permitted sender) smtp.mailfrom=xen-devel-bounces@lists.xenproject.org Return-Path: Received: from lists.xenproject.org (lists.xenproject.org [192.237.175.120]) by mx.zohomail.com with SMTPS id 1719382294148546.9493348106904; Tue, 25 Jun 2024 23:11:34 -0700 (PDT) Received: from list by lists.xenproject.org with outflank-mailman.748361.1156051 (Exim 4.92) (envelope-from ) id 1sMLrz-00052O-BX; Wed, 26 Jun 2024 06:11:03 +0000 Received: by outflank-mailman (output) from mailman id 748361.1156051; Wed, 26 Jun 2024 06:11:03 +0000 Received: from localhost ([127.0.0.1] helo=lists.xenproject.org) by lists.xenproject.org with esmtp (Exim 4.92) (envelope-from ) id 1sMLrz-00052H-8S; Wed, 26 Jun 2024 06:11:03 +0000 Received: by outflank-mailman (input) for mailman id 748361; Wed, 26 Jun 2024 06:11:01 +0000 Received: from se1-gles-sth1-in.inumbo.com ([159.253.27.254] helo=se1-gles-sth1.inumbo.com) by lists.xenproject.org with esmtp (Exim 4.92) (envelope-from ) id 1sMLrx-00052A-Jl for xen-devel@lists.xenproject.org; Wed, 26 Jun 2024 06:11:01 +0000 Received: from support.bugseng.com (mail.bugseng.com [162.55.131.47]) by se1-gles-sth1.inumbo.com (Halon) with ESMTPS id db6e3ad3-3382-11ef-90a3-e314d9c70b13; Wed, 26 Jun 2024 08:10:59 +0200 (CEST) Received: from truciolo.bugseng.com (unknown [78.209.201.39]) by support.bugseng.com (Postfix) with ESMTPSA id B910E4EE0738; Wed, 26 Jun 2024 08:10:57 +0200 (CEST) X-Outflank-Mailman: Message body and most headers restored to incoming version X-BeenThere: xen-devel@lists.xenproject.org List-Id: Xen developer discussion List-Unsubscribe: , List-Post: List-Help: List-Subscribe: , Errors-To: xen-devel-bounces@lists.xenproject.org Precedence: list Sender: "Xen-devel" X-Inumbo-ID: db6e3ad3-3382-11ef-90a3-e314d9c70b13 From: Federico Serafini To: xen-devel@lists.xenproject.org Cc: consulting@bugseng.com, Federico Serafini , Simone Ballarin , Doug Goldstein , Stefano Stabellini , Andrew Cooper , George Dunlap , Jan Beulich , Julien Grall , Oleksii Kurochko Subject: [XEN PATCH v2 for-4.19] automation/eclair: add deviations agreed in MISRA meetings Date: Wed, 26 Jun 2024 08:10:50 +0200 Message-Id: <816b323f5e325784947d09502f9352188bd325cf.1719381829.git.federico.serafini@bugseng.com> X-Mailer: git-send-email 2.34.1 MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable X-ZM-MESSAGEID: 1719382295790100001 Content-Type: text/plain; charset="utf-8" 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 Reviewed-by: Stefano Stabellini --- 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=3DMC3R1.R2.1,reports+=3D{deliberate, "any_area(any_loc(any_exp(mac= ro(name(ASSERT_UNREACHABLE||PARSE_ERR_RET||PARSE_ERR||FAIL_MSR||FAIL_CPUID)= ))))"} -doc_end =20 +-doc_begin=3D"The asm-offset files are not linked deliberately, since they= are used to generate definitions for asm modules." +-file_tag+=3D{asm_offsets, "^xen/arch/(arm|x86)/(arm32|arm64|x86_64)/asm-o= ffsets\\.c$"} +-config=3DMC3R1.R2.1,reports+=3D{deliberate, "any_area(any_loc(file(asm_of= fsets)))"} +-doc_end + -doc_begin=3D"Pure declarations (i.e., declarations without initialization= ) are not executable, and therefore it is safe for them to be unreachable." -config=3DMC3R1.R2.1,ignored_stmts+=3D{"any()", "pure_decl()"} @@ -63,6 +66,12 @@ they are not instances of commented-out code." -config=3DMC3R1.D4.3,reports+=3D{disapplied,"!(any_area(any_loc(file(^xen/= arch/arm/arm64/.*$))))"} -doc_end =20 +-doc_begin=3D"The inline asm in 'arm64/lib/bitops.c' is tightly coupled wi= th the surronding C code that acts as a wrapper, so it has been decided not= to add an additional encapsulation layer." +-file_tag+=3D{arm64_bitops, "^xen/arch/arm/arm64/lib/bitops\\.c$"} +-config=3DMC3R1.D4.3,reports+=3D{deliberate, "all_area(any_loc(file(arm64_= bitops)&&any_exp(macro(^(bit|test)op$))))"} +-config=3DMC3R1.D4.3,reports+=3D{deliberate, "any_area(any_loc(file(arm64_= bitops))&&context(name(int_clear_mask16)))"} +-doc_end + -doc_begin=3D"This header file is autogenerated or empty, therefore it pos= es no risk if included more than once." -file_tag+=3D{empty_header, "^xen/arch/arm/efi/runtime\\.h$"} @@ -213,10 +222,25 @@ Therefore the absence of prior declarations is safe." -config=3DMC3R1.R8.4,declarations+=3D{safe, "loc(file(asm_defns))&&^curren= t_stack_pointer$"} -doc_end =20 +-doc_begin=3D"The function apei_(read|check|clear)_mce are dead code and a= re excluded from non-debug builds, therefore the absence of prior declarati= ons is safe." +-config=3DMC3R1.R8.4,declarations+=3D{safe, "^apei_(read|check|clear)_mce\= \(.*$"} +-doc_end + -doc_begin=3D"asmlinkage is a marker to indicate that the function is only= used to interface with asm modules." -config=3DMC3R1.R8.4,declarations+=3D{safe,"loc(text(^(?s).*asmlinkage.*$,= -1..0))"} -doc_end =20 +-doc_begin=3D"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+=3D{bsearch_sort, "^xen/include/xen/(sort|lib)\\.h$"} +-config=3DMC3R1.R8.4,reports+=3D{deliberate, "any_area(any_loc(file(bsearc= h_sort))&&decl(name(bsearch||sort)))"} +-doc_end + +-doc_begin=3D"first_valid_mfn is defined in this way because the current l= ack of NUMA support in Arm and PPC requires it." +-file_tag+=3D{first_valid_mfn, "^xen/common/page_alloc\\.c$"} +-config=3DMC3R1.R8.4,declarations+=3D{deliberate,"loc(file(first_valid_mfn= ))"} +-doc_end + -doc_begin=3D"The following variables are compiled in multiple translation= units belonging to different executables and therefore are safe." -config=3DMC3R1.R8.6,declarations+=3D{safe, "name(current_stack_pointer||b= search||sort)"} @@ -257,8 +281,6 @@ dimension is higher than omitting the dimension." -config=3DMC3R1.R9.5,reports+=3D{deliberate, "any()"} -doc_end =20 -### Set 2 ### - # # Series 10. # @@ -299,7 +321,6 @@ integers arguments on two's complement architectures -config=3DMC3R1.R10.1,reports+=3D{safe, "any_area(any_loc(any_exp(macro(^I= SOLATE_LSB$))))"} -doc_end =20 -### Set 3 ### -doc_begin=3D"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 # =20 +-doc_begin=3D"The conversion from a function pointer to unsigned long or (= void *) does not lose any information, provided that the target type has en= ough bits to store it." +-config=3DMC3R1.R11.1,casts+=3D{safe, + "from(type(canonical(__function_pointer_types))) + &&to(type(canonical(builtin(unsigned long)||pointer(builtin(void))))) + &&relation(definitely_preserves_value)" +} +-doc_end + +-doc_begin=3D"The conversion from a function pointer to a boolean has a we= ll-known semantics that do not lead to unexpected behaviour." +-config=3DMC3R1.R11.1,casts+=3D{safe, + "from(type(canonical(__function_pointer_types))) + &&kind(pointer_to_boolean)" +} +-doc_end + +-doc_begin=3D"The conversion from a pointer to an incomplete type to unsig= ned long does not lose any information, provided that the target type has e= nough bits to store it." +-config=3DMC3R1.R11.2,casts+=3D{safe, + "from(type(any())) + &&to(type(canonical(builtin(unsigned long)))) + &&relation(definitely_preserves_value)" +} +-doc_end + +-doc_begin=3D"Conversions to object pointers that have a pointee type with= a smaller (i.e., less strict) alignment requirement are safe." +-config=3DMC3R1.R11.3,casts+=3D{safe, + "!relation(more_aligned_pointee)" +} +-doc_end + +-doc_begin=3D"Conversions from and to integral types are safe, in the assu= mption that the target type has enough bits to store the value. +See also Section \"4.7 Arrays and Pointers\" of \"GCC_MANUAL\"" +-config=3DMC3R1.R11.6,casts+=3D{safe, + "(from(type(canonical(integral())))||to(type(canonical(integral())))) + &&relation(definitely_preserves_value)"} +-doc_end + +-doc_begin=3D"The conversion from a pointer to a boolean has a well-known = semantics that do not lead to unexpected behaviour." +-config=3DMC3R1.R11.6,casts+=3D{safe, + "from(type(canonical(__pointer_types))) + &&kind(pointer_to_boolean)" +} +-doc_end + -doc_begin=3D"Violations caused by container_of are due to pointer arithme= tic operations with the provided offset. The resulting pointer is then immediately cast b= ack to its original type, which preserves the qualifier. This use is deemed safe. @@ -354,9 +418,18 @@ activity." -config=3DMC3R1.R14.2,reports+=3D{disapplied,"any()"} -doc_end =20 --doc_begin=3D"The XEN team relies on the fact that invariant conditions of= 'if' -statements are deliberate" --config=3DMC3R1.R14.3,statements=3D{deliberate , "wrapped(any(),node(if_st= mt))" } +-doc_begin=3D"The XEN team relies on the fact that invariant conditions of= 'if' statements and conditional operators are deliberate" +-config=3DMC3R1.R14.3,statements+=3D{deliberate, "wrapped(any(),node(if_st= mt||conditional_operator||binary_conditional_operator))" } +-doc_end + +-doc_begin=3D"Switches having a 'sizeof' operator as the condition are del= iberate and have limited scope." +-config=3DMC3R1.R14.3,statements+=3D{deliberate, "wrapped(any(),node(switc= h_stmt)&&child(cond, operator(sizeof)))" } +-doc_end + +-doc_begin=3D"The use of an invariant size argument in {put,get}_unsafe_si= ze and array_access_ok, as defined in arch/x86(_64)?/include/asm/uaccess.h = is deliberate and is deemed safe." +-file_tag+=3D{x86_uaccess, "^xen/arch/x86(_64)?/include/asm/uaccess\\.h$"} +-config=3DMC3R1.R14.3,reports+=3D{deliberate, "any_area(any_loc(file(x86_u= access)&&any_exp(macro(^(put|get)_unsafe_size$))))"} +-config=3DMC3R1.R14.3,reports+=3D{deliberate, "any_area(any_loc(file(x86_u= access)&&any_exp(macro(^array_access_ok$))))"} -doc_end =20 -doc_begin=3D"A controlling expression of 'if' and iteration statements ha= ving 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 # =20 --doc_begin=3D"do-while-0 is a well recognized loop idiom by the xen commun= ity." --loop_idioms=3D{do_stmt, "literal(0)"} +-doc_begin=3D"do-while-[01] is a well recognized loop idiom by the xen com= munity." +-loop_idioms=3D{do_stmt, "literal(0)||literal(1)"} -doc_end -doc_begin=3D"while-[01] is a well recognized loop idiom by the xen commun= ity." -loop_idioms+=3D{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. =20 + * - R2.1 + - The asm-offset files are not linked deliberately, since they are us= ed 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 ``_ for details. Moreover, pe= er @@ -203,6 +208,26 @@ Deviations related to MISRA C:2012 Rules: it. - Tagged as `safe` for ECLAIR. =20 + * - R8.4 + - Some functions are excluded from non-debug build, therefore the abs= ence + 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_inl= ine', + 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. =20 + * - 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 en= ough + bits to store it. + - Tagged as `safe` for ECLAIR. + + * - R11.3 + - Conversions to object pointers that have a pointee type with a smal= ler + (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 semanti= cs + that do not lead to unexpected behaviour. + - Tagged as `safe` for ECLAIR. + * - R11.8 - Violations caused by container_of are due to pointer arithmetic ope= rations 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: =20 * - 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. =20 * - R14.4 - A controlling expression of 'if' and iteration statements having @@ -475,10 +544,10 @@ Other deviations: * - Deviation - Justification =20 - * - do-while-0 loops - - The do-while-0 is a well-recognized loop idiom used by the Xen comm= unity - 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 wo= uld + cause a number of violations in some instances. =20 * - while-0 and while-1 loops - while-0 and while-1 are well-recognized loop idioms used by the Xen --=20 2.34.1