From nobody Mon Sep 16 19:47:10 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 1719329037577235.52198385730208; Tue, 25 Jun 2024 08:23:57 -0700 (PDT) Received: from list by lists.xenproject.org with outflank-mailman.747916.1155441 (Exim 4.92) (envelope-from ) id 1sM81E-0000XO-75; Tue, 25 Jun 2024 15:23:40 +0000 Received: by outflank-mailman (output) from mailman id 747916.1155441; Tue, 25 Jun 2024 15:23:40 +0000 Received: from localhost ([127.0.0.1] helo=lists.xenproject.org) by lists.xenproject.org with esmtp (Exim 4.92) (envelope-from ) id 1sM81E-0000XH-4U; Tue, 25 Jun 2024 15:23:40 +0000 Received: by outflank-mailman (input) for mailman id 747916; Tue, 25 Jun 2024 15:23:38 +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 1sM81C-0000X8-Qa for xen-devel@lists.xenproject.org; Tue, 25 Jun 2024 15:23:38 +0000 Received: from support.bugseng.com (mail.bugseng.com [162.55.131.47]) by se1-gles-sth1.inumbo.com (Halon) with ESMTPS id e4a5edbf-3306-11ef-90a3-e314d9c70b13; Tue, 25 Jun 2024 17:23:37 +0200 (CEST) Received: from truciolo.bugseng.com (unknown [37.161.92.237]) by support.bugseng.com (Postfix) with ESMTPSA id 2F00C4EE0738; Tue, 25 Jun 2024 17:23:35 +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: e4a5edbf-3306-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 for 4.19] automation/eclair: add deviations agreed in MISRA meetings Date: Tue, 25 Jun 2024 17:23:29 +0200 Message-Id: <4a65e064768ad5ddce96d749f24f0bdae2c3b9da.1719328656.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: 1719329038450100001 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 --- .../eclair_analysis/ECLAIR/deviations.ecl | 93 +++++++++++++++++-- docs/misra/deviations.rst | 68 +++++++++++++- 2 files changed, 149 insertions(+), 12 deletions(-) diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl b/automation/= eclair_analysis/ECLAIR/deviations.ecl index ae2eaf50f7..e6517a9142 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_s= tmt||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{safe , "wrapped(any(),node(switch_stm= t)&&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..0b048dc225 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,14 @@ 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. + - Project-wide deviation; 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. + - Project-wide deviation; tagged as `deliberate` for ECLAIR. =20 * - R14.4 - A controlling expression of 'if' and iteration statements having --=20 2.34.1