From nobody Fri May 17 16:45:31 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 1706887027034139.39107300215926; Fri, 2 Feb 2024 07:17:07 -0800 (PST) Received: from list by lists.xenproject.org with outflank-mailman.675077.1050255 (Exim 4.92) (envelope-from ) id 1rVvHg-0006Pq-NF; Fri, 02 Feb 2024 15:16:52 +0000 Received: by outflank-mailman (output) from mailman id 675077.1050255; Fri, 02 Feb 2024 15:16:52 +0000 Received: from localhost ([127.0.0.1] helo=lists.xenproject.org) by lists.xenproject.org with esmtp (Exim 4.92) (envelope-from ) id 1rVvHg-0006PM-Gh; Fri, 02 Feb 2024 15:16:52 +0000 Received: by outflank-mailman (input) for mailman id 675077; Fri, 02 Feb 2024 15:16:50 +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 1rVvHe-0006ME-OC for xen-devel@lists.xenproject.org; Fri, 02 Feb 2024 15:16:50 +0000 Received: from support.bugseng.com (mail.bugseng.com [162.55.131.47]) by se1-gles-sth1.inumbo.com (Halon) with ESMTPS id 161edc99-c1de-11ee-8a43-1f161083a0e0; Fri, 02 Feb 2024 16:16:49 +0100 (CET) Received: from beta.station (net-188-218-67-100.cust.vodafonedsl.it [188.218.67.100]) by support.bugseng.com (Postfix) with ESMTPSA id 6C70D4EE073C; Fri, 2 Feb 2024 16:16:48 +0100 (CET) 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: 161edc99-c1de-11ee-8a43-1f161083a0e0 From: Simone Ballarin To: xen-devel@lists.xenproject.org Cc: consulting@bugseng.com, sstabellini@kernel.org, Simone Ballarin , Andrew Cooper , George Dunlap , Jan Beulich , Julien Grall , Wei Liu , Bertrand Marquis , Michal Orzel , Volodymyr Babchuk , =?UTF-8?q?Roger=20Pau=20Monn=C3=A9?= , Dario Faggioli , Maria Celeste Cesario Subject: [XEN PATCH v4 1/4] xen: add SAF deviation for debugging and logging effects Date: Fri, 2 Feb 2024 16:16:02 +0100 Message-Id: <7c6aeedac626b171ed44df50ce5e3e2c76593f60.1706886631.git.simone.ballarin@bugseng.com> X-Mailer: git-send-email 2.34.1 In-Reply-To: References: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable X-ZM-MESSAGEID: 1706887029769100003 Content-Type: text/plain; charset="utf-8" Rule 13.1: Initializer lists shall not contain persistent side effects Effects caused by debug/logging macros and functions (like ASSERT, __bad_at= omic_size, LOG, etc ...) that crash execution or produce logs are not dangerous in ini= tializer lists. The evaluation order in abnormal conditions is not relevant. Evaluat= ion order of logging effects is always safe. Function hvm_get_guest_tsc_fixed (indirectly) performs different side effec= ts. For example it calls hvm_get_guest_time_fixed that contains an ASSERT and c= alls to spin_lock and spin_unlock. These side effects are not dangerous: they can be executed regardless of the initializer list evaluation order This patch deviates violations using SAF commits caused by debug/logging ma= cros and functions. Asm volatile statements in initializer lists that do not perform any persis= tent side effect are safe: this patch deviates violations caused by uses of the curre= nt macro (that contains an asm volatile) in initializer lists. No functional changes. Signed-off-by: Simone Ballarin Signed-off-by: Maria Celeste Cesario --- Changes in v3: - change commit prefix from xen/arm to xen - specify where saf-3-safe comments are applied in guestcopy.c - reword SAF text Changes in v2: New patch based on the discussion for "xen/arm: address violations of MISRA= C:2012 Rule 13.1". --- docs/misra/safe.json | 16 ++++++++++++++++ xen/arch/arm/device.c | 1 + xen/arch/arm/guestcopy.c | 16 ++++++++++++---- xen/arch/x86/hvm/hvm.c | 1 + xen/common/sched/core.c | 3 +++ 5 files changed, 33 insertions(+), 4 deletions(-) diff --git a/docs/misra/safe.json b/docs/misra/safe.json index 952324f85c..5539e8dfda 100644 --- a/docs/misra/safe.json +++ b/docs/misra/safe.json @@ -28,6 +28,22 @@ }, { "id": "SAF-3-safe", + "analyser": { + "eclair": "MC3R1.R13.1" + }, + "name": "MC3R1.R13.1: effects for debugging and logging", + "text": "Effects for debugging and loggings reasons that crash= execution or produce logs are allowed in initializer lists. The evaluation= order in abnormal conditions is not relevant." + }, + { + "id": "SAF-4-safe", + "analyser": { + "eclair": "MC3R1.R13.1" + }, + "name": "MC3R1.R13.1: volatile asm statements that do not perf= orm any persistent side effect", + "text": "Volatile asm statement in an initializer list that do= es not perform persistent side effects is safe." + }, + { + "id": "SAF-5-safe", "analyser": {}, "name": "Sentinel", "text": "Next ID to be used" diff --git a/xen/arch/arm/device.c b/xen/arch/arm/device.c index 1f631d3274..fa331f164d 100644 --- a/xen/arch/arm/device.c +++ b/xen/arch/arm/device.c @@ -331,6 +331,7 @@ int handle_device(struct domain *d, struct dt_device_no= de *dev, p2m_type_t p2mt, .p2mt =3D p2mt, .skip_mapping =3D !own_device || (is_pci_passthrough_enabled() && + /* SAF-3-safe effects for debugging/logging reason= s are safe */ (device_get_class(dev) =3D=3D DEVICE_PCI_HOSTBRIDG= E)), .iomem_ranges =3D iomem_ranges, .irq_ranges =3D irq_ranges diff --git a/xen/arch/arm/guestcopy.c b/xen/arch/arm/guestcopy.c index 6716b03561..b75538252a 100644 --- a/xen/arch/arm/guestcopy.c +++ b/xen/arch/arm/guestcopy.c @@ -110,26 +110,34 @@ static unsigned long copy_guest(void *buf, uint64_t a= ddr, unsigned int len, unsigned long raw_copy_to_guest(void *to, const void *from, unsigned int l= en) { return copy_guest((void *)from, (vaddr_t)to, len, - GVA_INFO(current), COPY_to_guest | COPY_linear); + /* SAF-4-safe No persistent side effects */ + GVA_INFO(current), + COPY_to_guest | COPY_linear); } =20 unsigned long raw_copy_to_guest_flush_dcache(void *to, const void *from, unsigned int len) { - return copy_guest((void *)from, (vaddr_t)to, len, GVA_INFO(current), + return copy_guest((void *)from, (vaddr_t)to, len, + /* SAF-4-safe No persistent side effects */ + GVA_INFO(current), COPY_to_guest | COPY_flush_dcache | COPY_linear); } =20 unsigned long raw_clear_guest(void *to, unsigned int len) { - return copy_guest(NULL, (vaddr_t)to, len, GVA_INFO(current), + return copy_guest(NULL, (vaddr_t)to, len, + /* SAF-4-safe No persistent side effects */ + GVA_INFO(current), COPY_to_guest | COPY_linear); } =20 unsigned long raw_copy_from_guest(void *to, const void __user *from, unsigned int len) { - return copy_guest(to, (vaddr_t)from, len, GVA_INFO(current), + return copy_guest(to, (vaddr_t)from, len, + /* SAF-4-safe No persistent side effects */ + GVA_INFO(current), COPY_from_guest | COPY_linear); } =20 diff --git a/xen/arch/x86/hvm/hvm.c b/xen/arch/x86/hvm/hvm.c index e8deeb0222..19322fbb56 100644 --- a/xen/arch/x86/hvm/hvm.c +++ b/xen/arch/x86/hvm/hvm.c @@ -800,6 +800,7 @@ static int cf_check hvm_save_cpu_ctxt(struct vcpu *v, h= vm_domain_context_t *h) { struct segment_register seg; struct hvm_hw_cpu ctxt =3D { + /* SAF-3-safe effects for debugging/logging reasons are safe */ .tsc =3D hvm_get_guest_tsc_fixed(v, v->domain->arch.hvm.sync_tsc), .msr_tsc_aux =3D v->arch.msrs->tsc_aux, .rax =3D v->arch.user_regs.rax, diff --git a/xen/common/sched/core.c b/xen/common/sched/core.c index d177c675c8..9e973fcf31 100644 --- a/xen/common/sched/core.c +++ b/xen/common/sched/core.c @@ -1521,6 +1521,7 @@ long vcpu_yield(void) =20 SCHED_STAT_CRANK(vcpu_yield); =20 + /* SAF-4-safe No persistent side effects */ TRACE_2D(TRC_SCHED_YIELD, current->domain->domain_id, current->vcpu_id= ); raise_softirq(SCHEDULE_SOFTIRQ); return 0; @@ -1899,6 +1900,7 @@ ret_t do_sched_op(int cmd, XEN_GUEST_HANDLE_PARAM(voi= d) arg) if ( copy_from_guest(&sched_shutdown, arg, 1) ) break; =20 + /* SAF-4-safe No persistent side effects */ TRACE_3D(TRC_SCHED_SHUTDOWN, current->domain->domain_id, current->vcpu_id, sched_shutdown.reason); @@ -1916,6 +1918,7 @@ ret_t do_sched_op(int cmd, XEN_GUEST_HANDLE_PARAM(voi= d) arg) if ( copy_from_guest(&sched_shutdown, arg, 1) ) break; =20 + /* SAF-4-safe No persistent side effects */ TRACE_3D(TRC_SCHED_SHUTDOWN_CODE, d->domain_id, current->vcpu_id, sched_shutdown.reason); =20 --=20 2.34.1 From nobody Fri May 17 16:45:31 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 1706887029610275.97788844564036; Fri, 2 Feb 2024 07:17:09 -0800 (PST) Received: from list by lists.xenproject.org with outflank-mailman.675078.1050262 (Exim 4.92) (envelope-from ) id 1rVvHh-0006T2-2s; Fri, 02 Feb 2024 15:16:53 +0000 Received: by outflank-mailman (output) from mailman id 675078.1050262; Fri, 02 Feb 2024 15:16:53 +0000 Received: from localhost ([127.0.0.1] helo=lists.xenproject.org) by lists.xenproject.org with esmtp (Exim 4.92) (envelope-from ) id 1rVvHg-0006RZ-P3; Fri, 02 Feb 2024 15:16:52 +0000 Received: by outflank-mailman (input) for mailman id 675078; Fri, 02 Feb 2024 15:16:51 +0000 Received: from se1-gles-flk1-in.inumbo.com ([94.247.172.50] helo=se1-gles-flk1.inumbo.com) by lists.xenproject.org with esmtp (Exim 4.92) (envelope-from ) id 1rVvHf-0005mR-Kl for xen-devel@lists.xenproject.org; Fri, 02 Feb 2024 15:16:51 +0000 Received: from support.bugseng.com (mail.bugseng.com [162.55.131.47]) by se1-gles-flk1.inumbo.com (Halon) with ESMTPS id 1681f954-c1de-11ee-98f5-efadbce2ee36; Fri, 02 Feb 2024 16:16:50 +0100 (CET) Received: from beta.station (net-188-218-67-100.cust.vodafonedsl.it [188.218.67.100]) by support.bugseng.com (Postfix) with ESMTPSA id 55B664EE073F; Fri, 2 Feb 2024 16:16:49 +0100 (CET) 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: 1681f954-c1de-11ee-98f5-efadbce2ee36 From: Simone Ballarin To: xen-devel@lists.xenproject.org Cc: consulting@bugseng.com, sstabellini@kernel.org, Simone Ballarin , Andrew Cooper , George Dunlap , Jan Beulich , Julien Grall , Wei Liu , Maria Celeste Cesario Subject: [XEN PATCH v4 2/4] xen/ns16550: address violations of MISRA C:2012 Rule 13.1 Date: Fri, 2 Feb 2024 16:16:03 +0100 Message-Id: <08f1d4a7475c557da016482025067f54e2e56b99.1706886631.git.simone.ballarin@bugseng.com> X-Mailer: git-send-email 2.34.1 In-Reply-To: References: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable X-ZM-MESSAGEID: 1706887031319100005 Content-Type: text/plain; charset="utf-8" Rule 13.1: Initializer lists shall not contain persistent side effects The assignment operation in: .irq =3D rc =3D uart->irq, is a persistent side effect in a struct initializer list. This patch assigns rc separately outside the structure. No functional change. Signed-off-by: Simone Ballarin Signed-off-by: Maria Celeste Cesario Acked-by: Jan Beulich --- Changes in v3: - add assignment of rc; - use rc as controlling expression in the following if-statement; - change prefix from xen to xen/ns16550. Changes in v2: - avoid assignment of rc; - drop changes in vcpu_yield(void). --- xen/drivers/char/ns16550.c | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/xen/drivers/char/ns16550.c b/xen/drivers/char/ns16550.c index afe3d514b9..97bf098534 100644 --- a/xen/drivers/char/ns16550.c +++ b/xen/drivers/char/ns16550.c @@ -441,10 +441,12 @@ static void __init cf_check ns16550_init_postirq(stru= ct serial_port *port) struct msi_info msi =3D { .sbdf =3D PCI_SBDF(0, uart->ps_bdf[0], uart->ps_bdf[1], uart->ps_bdf[2]), - .irq =3D rc =3D uart->irq, + .irq =3D uart->irq, .entry_nr =3D 1 }; =20 + rc =3D uart->irq; + if ( rc > 0 ) { struct msi_desc *msi_desc =3D NULL; --=20 2.34.1 From nobody Fri May 17 16:45:31 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 1706887033053708.347353919077; Fri, 2 Feb 2024 07:17:13 -0800 (PST) Received: from list by lists.xenproject.org with outflank-mailman.675079.1050280 (Exim 4.92) (envelope-from ) id 1rVvHi-000724-8D; Fri, 02 Feb 2024 15:16:54 +0000 Received: by outflank-mailman (output) from mailman id 675079.1050280; Fri, 02 Feb 2024 15:16:54 +0000 Received: from localhost ([127.0.0.1] helo=lists.xenproject.org) by lists.xenproject.org with esmtp (Exim 4.92) (envelope-from ) id 1rVvHi-00070O-1Z; Fri, 02 Feb 2024 15:16:54 +0000 Received: by outflank-mailman (input) for mailman id 675079; Fri, 02 Feb 2024 15:16:52 +0000 Received: from se1-gles-flk1-in.inumbo.com ([94.247.172.50] helo=se1-gles-flk1.inumbo.com) by lists.xenproject.org with esmtp (Exim 4.92) (envelope-from ) id 1rVvHg-0005mR-HE for xen-devel@lists.xenproject.org; Fri, 02 Feb 2024 15:16:52 +0000 Received: from support.bugseng.com (mail.bugseng.com [162.55.131.47]) by se1-gles-flk1.inumbo.com (Halon) with ESMTPS id 16da0948-c1de-11ee-98f5-efadbce2ee36; Fri, 02 Feb 2024 16:16:50 +0100 (CET) Received: from beta.station (net-188-218-67-100.cust.vodafonedsl.it [188.218.67.100]) by support.bugseng.com (Postfix) with ESMTPSA id 03D944EE0741; Fri, 2 Feb 2024 16:16:49 +0100 (CET) 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: 16da0948-c1de-11ee-98f5-efadbce2ee36 From: Simone Ballarin To: xen-devel@lists.xenproject.org Cc: consulting@bugseng.com, sstabellini@kernel.org, Simone Ballarin , Jan Beulich , Andrew Cooper , =?UTF-8?q?Roger=20Pau=20Monn=C3=A9?= , Wei Liu Subject: [XEN PATCH v4 3/4] xen/x86: address violations of MISRA C:2012 Rule 13.1 Date: Fri, 2 Feb 2024 16:16:04 +0100 Message-Id: <16bb514ac0a5fe0d6e9a2c95279a8200ff4495c6.1706886631.git.simone.ballarin@bugseng.com> X-Mailer: git-send-email 2.34.1 In-Reply-To: References: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable X-ZM-MESSAGEID: 1706887033388100001 Content-Type: text/plain; charset="utf-8" Rule 13.1: Initializer lists shall not contain persistent side effects This patch moves expressions with side-effects into new variables before the initializer lists. No functional changes. Signed-off-by: Simone Ballarin --- xen/arch/x86/io_apic.c | 9 ++++++--- xen/arch/x86/mpparse.c | 3 ++- xen/arch/x86/setup.c | 3 ++- 3 files changed, 10 insertions(+), 5 deletions(-) diff --git a/xen/arch/x86/io_apic.c b/xen/arch/x86/io_apic.c index b48a642465..4a6ab85689 100644 --- a/xen/arch/x86/io_apic.c +++ b/xen/arch/x86/io_apic.c @@ -2559,9 +2559,12 @@ integer_param("max_gsi_irqs", max_gsi_irqs); =20 static __init bool bad_ioapic_register(unsigned int idx) { - union IO_APIC_reg_00 reg_00 =3D { .raw =3D io_apic_read(idx, 0) }; - union IO_APIC_reg_01 reg_01 =3D { .raw =3D io_apic_read(idx, 1) }; - union IO_APIC_reg_02 reg_02 =3D { .raw =3D io_apic_read(idx, 2) }; + uint32_t reg_00_raw =3D io_apic_read(idx, 0); + uint32_t reg_01_raw =3D io_apic_read(idx, 1); + uint32_t reg_02_raw =3D io_apic_read(idx, 2); + union IO_APIC_reg_00 reg_00 =3D { .raw =3D reg_00_raw }; + union IO_APIC_reg_01 reg_01 =3D { .raw =3D reg_01_raw }; + union IO_APIC_reg_02 reg_02 =3D { .raw =3D reg_02_raw }; =20 if ( reg_00.raw =3D=3D -1 && reg_01.raw =3D=3D -1 && reg_02.raw =3D=3D= -1 ) { diff --git a/xen/arch/x86/mpparse.c b/xen/arch/x86/mpparse.c index d8ccab2449..81a819403b 100644 --- a/xen/arch/x86/mpparse.c +++ b/xen/arch/x86/mpparse.c @@ -798,11 +798,12 @@ void __init mp_register_lapic_address ( =20 int mp_register_lapic(u32 id, bool enabled, bool hotplug) { + u32 apic =3D apic_read(APIC_LVR); struct mpc_config_processor processor =3D { .mpc_type =3D MP_PROCESSOR, /* Note: We don't fill in fields not consumed anywhere. */ .mpc_apicid =3D id, - .mpc_apicver =3D GET_APIC_VERSION(apic_read(APIC_LVR)), + .mpc_apicver =3D GET_APIC_VERSION(apic), .mpc_cpuflag =3D (enabled ? CPU_ENABLED : 0) | (id =3D=3D boot_cpu_physical_apicid ? CPU_BOOTPROCESSOR : 0), diff --git a/xen/arch/x86/setup.c b/xen/arch/x86/setup.c index ee682dd136..886031d86a 100644 --- a/xen/arch/x86/setup.c +++ b/xen/arch/x86/setup.c @@ -885,13 +885,14 @@ static struct domain *__init create_dom0(const module= _t *image, { static char __initdata cmdline[MAX_GUEST_CMDLINE]; =20 + unsigned int max_vcpus =3D dom0_max_vcpus(); struct xen_domctl_createdomain dom0_cfg =3D { .flags =3D IS_ENABLED(CONFIG_TBOOT) ? XEN_DOMCTL_CDF_s3_integrity = : 0, .max_evtchn_port =3D -1, .max_grant_frames =3D -1, .max_maptrack_frames =3D -1, .grant_opts =3D XEN_DOMCTL_GRANT_version(opt_gnttab_max_version), - .max_vcpus =3D dom0_max_vcpus(), + .max_vcpus =3D max_vcpus, .arch =3D { .misc_flags =3D opt_dom0_msr_relaxed ? XEN_X86_MSR_RELAXED : 0, }, --=20 2.34.1 From nobody Fri May 17 16:45:31 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 1706887035965129.66395946947023; Fri, 2 Feb 2024 07:17:15 -0800 (PST) Received: from list by lists.xenproject.org with outflank-mailman.675080.1050290 (Exim 4.92) (envelope-from ) id 1rVvHj-0007Lh-BZ; Fri, 02 Feb 2024 15:16:55 +0000 Received: by outflank-mailman (output) from mailman id 675080.1050290; Fri, 02 Feb 2024 15:16:55 +0000 Received: from localhost ([127.0.0.1] helo=lists.xenproject.org) by lists.xenproject.org with esmtp (Exim 4.92) (envelope-from ) id 1rVvHj-0007Ko-88; Fri, 02 Feb 2024 15:16:55 +0000 Received: by outflank-mailman (input) for mailman id 675080; Fri, 02 Feb 2024 15:16:54 +0000 Received: from se1-gles-flk1-in.inumbo.com ([94.247.172.50] helo=se1-gles-flk1.inumbo.com) by lists.xenproject.org with esmtp (Exim 4.92) (envelope-from ) id 1rVvHi-0005mR-4D for xen-devel@lists.xenproject.org; Fri, 02 Feb 2024 15:16:54 +0000 Received: from support.bugseng.com (mail.bugseng.com [162.55.131.47]) by se1-gles-flk1.inumbo.com (Halon) with ESMTPS id 174f9951-c1de-11ee-98f5-efadbce2ee36; Fri, 02 Feb 2024 16:16:51 +0100 (CET) Received: from beta.station (net-188-218-67-100.cust.vodafonedsl.it [188.218.67.100]) by support.bugseng.com (Postfix) with ESMTPSA id 90D444EE0740; Fri, 2 Feb 2024 16:16:50 +0100 (CET) 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: 174f9951-c1de-11ee-98f5-efadbce2ee36 From: Simone Ballarin To: xen-devel@lists.xenproject.org Cc: consulting@bugseng.com, sstabellini@kernel.org, Maria Celeste Cesario , Simone Ballarin , Doug Goldstein , Andrew Cooper , George Dunlap , Jan Beulich , Julien Grall , Wei Liu Subject: [XEN PATCH v4 4/4] eclair: move function and macro properties outside ECLAIR Date: Fri, 2 Feb 2024 16:16:05 +0100 Message-Id: <387b160ae93c221c4bc2426605b96b432b26224e.1706886631.git.simone.ballarin@bugseng.com> X-Mailer: git-send-email 2.34.1 In-Reply-To: References: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable X-ZM-MESSAGEID: 1706887037485100001 Content-Type: text/plain; charset="utf-8" From: Maria Celeste Cesario Function and macro properties contained in ECLAIR/call_properties.ecl are of general interest: this patch moves these annotations in a generaric JSON fi= le in docs. In this way, they can be exploited for other purposes (i.e. docume= ntation, other tools). Add rst file containing explanation on how to update function_macro_propert= ies.json. Add script to convert the JSON file in ECL configurations. Remove ECLAIR/call_properties.ecl: the file is now automatically generated = from the JSON file. Signed-off-by: Maria Celeste Cesario Signed-off-by: Simone Ballarin Acked-by: Stefano Stabellini --- Changes in v4: - add missing script for converting the JSON file in ECL configurations; - improve commit message; - remove call_properties.ecs. --- .../eclair_analysis/ECLAIR/analysis.ecl | 1 + .../ECLAIR/call_properties.ecl | 128 --- automation/eclair_analysis/prepare.sh | 2 + automation/eclair_analysis/propertyparser.py | 37 + docs/function_macro_properties.json | 841 ++++++++++++++++++ docs/function_macro_properties.rst | 58 ++ 6 files changed, 939 insertions(+), 128 deletions(-) delete mode 100644 automation/eclair_analysis/ECLAIR/call_properties.ecl create mode 100644 automation/eclair_analysis/propertyparser.py create mode 100644 docs/function_macro_properties.json create mode 100644 docs/function_macro_properties.rst diff --git a/automation/eclair_analysis/ECLAIR/analysis.ecl b/automation/ec= lair_analysis/ECLAIR/analysis.ecl index a604582da3..684c5b0b39 100644 --- a/automation/eclair_analysis/ECLAIR/analysis.ecl +++ b/automation/eclair_analysis/ECLAIR/analysis.ecl @@ -30,6 +30,7 @@ if(not(scheduled_analysis), -eval_file=3Ddeviations.ecl -eval_file=3Dcall_properties.ecl -eval_file=3Dtagging.ecl +-eval_file=3Dproperties.ecl -eval_file=3Dconcat(set,".ecl") =20 -doc=3D"Hide reports in external code." diff --git a/automation/eclair_analysis/ECLAIR/call_properties.ecl b/automa= tion/eclair_analysis/ECLAIR/call_properties.ecl deleted file mode 100644 index c2b2a6182e..0000000000 --- a/automation/eclair_analysis/ECLAIR/call_properties.ecl +++ /dev/null @@ -1,128 +0,0 @@ - --call_properties+=3D{"name(printk)", {"pointee_write(1..=3Dnever)", "taken= ()"}} --call_properties+=3D{"name(debugtrace_printk)", {"pointee_write(1..=3Dneve= r)", "taken()"}} --call_properties+=3D{"name(panic)", {"pointee_write(1..=3Dnever)", "taken(= )"}} --call_properties+=3D{"macro(^domain_crash$)", {"pointee_write(2..=3Dnever)= ", "taken()"}} --call_properties+=3D{"macro(^(g?d|mm_)?printk$)", {"pointee_write(2..=3Dne= ver)", "taken()"}} --call_properties+=3D{"macro(^guest_bug_on_failed$)", {"pointee_write(1=3Dn= ever)", "taken()"}} --call_properties+=3D{"macro(^spin_lock_init_prof$)", {"pointee_write(2=3Dn= ever)", "taken()"}} --call_properties+=3D{"macro(^sched_test_func$)", {"pointee_write(1..=3Dnev= er)", "taken()"}} --call_properties+=3D{"macro(^dev_(info|warn)$)", {"pointee_write(1..=3Dnev= er)", "taken()"}} --call_properties+=3D{"macro(^PAGING_DEBUG$)", {"pointee_write(1..=3Dnever)= ", "taken()"}} --call_properties+=3D{"macro(^ACPI_(WARNING|ERROR|INFO)$)", {"pointee_write= (1..=3Dnever)", "taken()"}} --call_properties+=3D{"name(fdt_get_property_by_offset_)", {"pointee_write(= 3=3Dalways)", "pointee_read(3=3Dnever)", "taken()"}} --call_properties+=3D{"name(read_atomic_size)", {"pointee_write(2=3Dalways)= ", "pointee_read(2=3Dnever)", "taken()"}} --call_properties+=3D{"name(device_tree_get_reg)", {"pointee_write(4..=3Dal= ways)", "pointee_read(4..=3Dnever)", "taken()"}} --call_properties+=3D{"name(dt_get_range)", {"pointee_write(3..=3Dalways)",= "pointee_read(3..=3Dnever)", "taken()"}} --call_properties+=3D{"name(parse_static_mem_prop)", {"pointee_write(2..=3D= always)", "pointee_read(2..=3Dnever)", "taken()"}} --call_properties+=3D{"name(get_ttbr_and_gran_64bit)", {"pointee_write(1..2= =3Dalways)", "pointee_read(1..2=3Dnever)", "taken()"}} --call_properties+=3D{"name(hvm_emulate_init_once)", {"pointee_write(1=3Dal= ways)", "pointee_read(1=3Dnever)", "taken()"}} --call_properties+=3D{"name(__vmread)", {"pointee_write(2=3Dalways)", "poin= tee_read(2=3Dnever)", "taken()"}} --call_properties+=3D{"name(hvm_pci_decode_addr)", {"pointee_write(3=3Dalwa= ys)", "pointee_read(3=3Dnever)", "taken()"}} --call_properties+=3D{"name(vpci_mmcfg_decode_addr)", {"pointee_write(3=3Da= lways)", "pointee_read(3=3Dnever)", "taken()"}} --call_properties+=3D{"name(x86emul_decode)", {"pointee_write(1=3Dalways)",= "pointee_read(1=3Dnever)", "taken()"}} --call_properties+=3D{"name(unmap_grant_ref)", {"pointee_write(2=3Dalways)"= , "pointee_read(2=3Dnever)", "taken()"}} --call_properties+=3D{"name(arm_smmu_cmdq_build_cmd)", {"pointee_write(1=3D= always)", "pointee_read(1=3Dnever)", "taken()"}} --call_properties+=3D{"name(pci_size_mem_bar)", {"pointee_write(4=3Dalways)= ", "pointee_read(4=3Dnever)", "taken()"}} --call_properties+=3D{"name(_hvm_read_entry)", {"pointee_write(2=3Dalways)"= , "pointee_read(2=3Dnever)", "taken()"}} --call_properties+=3D{"name(hvm_map_guest_frame_rw)", {"pointee_write(3=3Da= lways)", "pointee_read(3=3Dnever)", "taken()"}} --call_properties+=3D{"name(guest_cpuid)", {"pointee_write(4=3Dalways)", "p= ointee_read(4=3Dnever)", "taken()"}} --call_properties+=3D{"name(epte_get_entry_emt)", {"pointee_write(5=3Dalway= s)", "pointee_read(5=3Dnever)", "taken()"}} --call_properties+=3D{"name(mcheck_mca_logout)", {"pointee_write(3=3Dalways= )", "pointee_read(3=3Dnever)", "taken()"}} --call_properties+=3D{"name(set_field_in_reg_u32)", {"pointee_write(5=3Dalw= ays)", "pointee_read(5=3Dnever)", "taken()"}} --call_properties+=3D{"name(alloc_affinity_masks)", {"pointee_write(1=3Dalw= ays)", "pointee_read(1=3Dnever)", "taken()"}} --call_properties+=3D{"name(xasprintf)", {"pointee_write(1=3Dalways)", "poi= ntee_read(1=3Dnever)", "taken()"}} --call_properties+=3D{"name(find_non_smt)", {"pointee_write(2=3Dalways)", "= pointee_read(2=3Dnever)", "taken()"}} --call_properties+=3D{"name(call_rcu)", {"pointee_write(1=3Dalways)", "poin= tee_read(1=3Dnever)", "taken()"}} --call_properties+=3D{"name(getdomaininfo)", {"pointee_write(2=3Dalways)", = "pointee_read(2=3Dnever)", "taken()"}} --call_properties+=3D{"^MAPPING_(INSERT|SEARCH)\\(.*$", {"pointee_write(2..= =3Dalways)", "pointee_read(2..=3Dnever)", "taken()"}} --call_properties+=3D{"name(FormatDec)", {"pointee_write(2=3Dalways)", "poi= ntee_read(2=3Dnever)", "taken()"}} --call_properties+=3D{"name(FormatHex)", {"pointee_write(3=3Dalways)", "poi= ntee_read(3=3Dnever)", "taken()"}} --call_properties+=3D{"name(p2m_get_ioreq_server)", {"pointee_write(2=3Dalw= ays)", "pointee_read(2=3Dnever)", "taken()"}} --call_properties+=3D{"name(elf_memset_unchecked)", {"pointee_write(1=3Dalw= ays)", "pointee_read(1=3Dnever)", "taken()"}} --call_properties+=3D{"name(set_iommu_pte_present)", {"pointee_write(7=3Dal= ways)", "pointee_read(7=3Dnever)", "taken()"}} --call_properties+=3D{"name(clear_iommu_pte_present)", {"pointee_write(4=3D= always)", "pointee_read(4=3Dnever)", "taken()"}} --call_properties+=3D{"name(vcpu_runstate_get)", {"pointee_write(2=3Dalways= )", "pointee_read(2=3Dnever)", "taken()"}} --call_properties+=3D{"name(va_start)", {"pointee_write(1=3Dalways)", "poin= tee_read(1=3Dnever)", "taken()"}} --call_properties+=3D{"name(sgi_target_init)", {"pointee_write(1=3Dalways)"= , "pointee_read(1=3Dnever)", "taken()"}} --call_properties+=3D{"name(get_hw_residencies)", {"pointee_write(2=3Dalway= s)", "pointee_read(2=3Dnever)", "taken()"}} --call_properties+=3D{"name(x86_cpu_policy_to_featureset)", {"pointee_write= (2=3Dalways)", "pointee_read(2=3Dnever)", "taken()"}} --call_properties+=3D{"^simple_strtou?ll?\\(.*$", {"pointee_write(2=3Dalway= s)", "pointee_read(2=3Dnever)", "taken()"}} --call_properties+=3D{"name(msi_compose_msg)", {"pointee_write(3=3Dalways)"= , "pointee_read(3=3Dnever)", "taken()"}} --call_properties+=3D{"name(print_tainted)", {"pointee_write(1=3Dalways)", = "pointee_read(1=3Dnever)", "taken()"}} --call_properties+=3D{"name(get_hvm_registers)", {"pointee_write(3=3Dalways= )", "pointee_read(3=3Dnever)", "taken()"}} --call_properties+=3D{"name(x86_insn_modrm)", {"pointee_write(2..3=3Dalways= )", "pointee_read(2..3=3Dnever)", "taken()"}} --call_properties+=3D{"name(cpuid_count_leaf)", {"pointee_write(3=3Dalways)= ", "pointee_read(3=3Dnever)", "taken()"}} --call_properties+=3D{"name(rcu_lock_remote_domain_by_id)", {"pointee_write= (2=3Dalways)", "pointee_read(2=3Dnever)", "taken()"}} --call_properties+=3D{"name(cpuid_count)", {"pointee_write(3..=3Dalways)", = "pointee_read(3..=3Dnever)", "taken()"}} --call_properties+=3D{"name(efi_boot_mem_unused)", {"pointee_write(1..=3Dal= ways)", "pointee_read(1..=3Dnever)", "taken()"}} --call_properties+=3D{"name(collect_time_info)", {"pointee_write(2=3Dalways= )", "pointee_read(2=3Dnever)", "taken()"}} --call_properties+=3D{"name(setup_xstate_comp)", {"pointee_write(1=3Dalways= )", "pointee_read(1=3Dnever)", "taken()"}} --call_properties+=3D{"name(map_domain_gfn)", {"pointee_read(5=3Dnever)", "= taken()"}} --call_properties+=3D{"name(fdt_getprop)", {"pointee_read(4=3Dnever)", "tak= en()"}} --call_properties+=3D{"name(fdt_get_name)", {"pointee_read(3=3Dnever)", "ta= ken()"}} --call_properties+=3D{"name(fdt_get_property)", {"pointee_read(4=3Dnever)",= "taken()"}} --call_properties+=3D{"name(pci_get_host_bridge_segment)", {"pointee_read(2= =3Dnever)", "taken()"}} --call_properties+=3D{"name(dt_get_property)", {"pointee_read(3=3Dnever)", = "taken()"}} --call_properties+=3D{"name(dt_property_read_u32)", {"pointee_read(3=3Dneve= r)", "taken()"}} --call_properties+=3D{"name(dt_device_get_paddr)", {"pointee_read(3..4=3Dne= ver)", "taken()"}} --call_properties+=3D{"name(get_evtchn_dt_property)", {"pointee_write(2..3= =3Dmaybe)", "pointee_read(2..3=3Dnever)", "taken()"}} --call_properties+=3D{"name(setup_chosen_node)", {"pointee_write(2..3=3Dmay= be)", "pointee_read(2..3=3Dnever)", "taken()"}} --call_properties+=3D{"name(queue_remove_raw)", {"pointee_read(2=3Dnever)",= "taken()"}} --call_properties+=3D{"macro(^memset$)", {"pointee_write(1=3Dalways)", "poi= ntee_read(1=3Dnever)", "taken()"}} --call_properties+=3D{"macro(^va_start$)", {"pointee_write(1=3Dalways)", "p= ointee_read(1=3Dnever)", "taken()"}} --call_properties+=3D{"macro(^memcmp$)", {"pointee_write(1..2=3Dnever)", "t= aken()"}} --call_properties+=3D{"macro(^memcpy$)", {"pointee_write(1=3Dalways&&2..=3D= never)", "pointee_read(1=3Dnever&&2..=3Dalways)", "taken()"}} --call_properties+=3D{"name(get_cpu_info)",{pure}} --call_properties+=3D{"name(pdx_to_pfn)",{pure}} --call_properties+=3D{"name(is_pci_passthrough_enabled)",{const}} --call_properties+=3D{"name(get_cycles)", {"noeffect"}} --call_properties+=3D{"name(msi_gflags)",{const}} --call_properties+=3D{"name(hvm_save_size)",{pure}} --call_properties+=3D{"name(cpu_has)",{pure}} --call_properties+=3D{"name(boot_cpu_has)",{pure}} --call_properties+=3D{"name(get_cpu_info)",{pure}} --call_properties+=3D{"name(put_pte_flags)",{const}} --call_properties+=3D{"name(is_pv_vcpu)",{pure}} - --doc_begin=3D"Property inferred as a consequence of the semantics of devic= e_tree_get_reg" --call_properties+=3D{"name(acquire_static_memory_bank)", {"pointee_write(4= ..=3Dalways)", "pointee_read(4..=3Dnever)", "taken()"}} --doc_end - --doc_begin=3D"Property inferred as a consequence of the semantics of dt_se= t_cell" --call_properties+=3D{"name(set_interrupt)", {"pointee_write(1=3Dalways)", = "pointee_read(1=3Dnever)", "taken()"}} --doc_end - --doc_begin=3D"Property inferred as a consequence of the semantics of __p2m= _get_mem_access" --call_properties+=3D{"name(p2m_get_mem_access)", {"pointee_write(3=3Dalway= s)", "pointee_read(3=3Dnever)", "taken()"}} --doc_end - --doc_begin=3D"This function has alternative definitions with props {write= =3Dalways,read=3Dnever} and {write=3Dnever,read=3Dnever}" --call_properties+=3D{"name(alloc_cpumask_var)", {"pointee_write(1=3Dmaybe)= ", "pointee_read(1=3Dnever)", "taken()"}} --doc_end - --doc_begin=3D"Property inferred as a consequence of the semantics of alloc= _cpumask_var" --call_properties+=3D{"name(xenctl_bitmap_to_cpumask)", {"pointee_write(1= =3Dalways)", "pointee_read(1=3Dnever)", "taken()"}} --doc_end - --doc_begin=3D"The call to bitmap_and causes the pointee of dstp to be alwa= ys written" --call_properties+=3D{"^cpumask_(and|andnot|clear|copy|complement).*$", {"p= ointee_write(1=3Dalways)", "pointee_read(1=3Dnever)" "taken()"}} --call_properties+=3D{"^bitmap_(andnot|complement|fill).*$", {"pointee_writ= e(1=3Dalways)", "pointee_read(1=3Dnever)", "taken()"}} --doc_end - --doc_begin=3D"The .*copy_(to|from).* helpers all have a memcpy-like expect= ation that the destination is a copy of the source. -Furthermore, their uses do initialize the involved variables as needed by = futher uses in the caller." --call_properties+=3D{"macro(^(__)?(raw_)?copy_from_(paddr|guest|compat)(_o= ffset)?$)", {"pointee_write(1=3Dalways)", "pointee_read(1=3Dnever)", "taken= ()"}} --call_properties+=3D{"macro(^(__)?copy_to_(guest|compat)(_offset)?$)", {"p= ointee_write(2=3Dalways)", "pointee_read(2=3Dnever)", "taken()"}} --doc_end - --doc_begin=3D"Functions generated by build_atomic_read cannot be considere= d pure -since the input pointer is volatile, but they do not produce any persisten= t side -effect." --call_properties+=3D{"^read_u(8|16|32|64|int)_atomic.*$", {noeffect}} --doc_end - --doc_begin=3D"Functions generated by TYPE_SAFE are const." --call_properties+=3D{"^(mfn|gfn|pfn)_x\\(.*$",{const}} --call_properties+=3D{"^_(mfn|gfn|pfn)\\(.*$",{const}} --doc_end diff --git a/automation/eclair_analysis/prepare.sh b/automation/eclair_anal= ysis/prepare.sh index fe9d16e48e..47b2a2f32a 100755 --- a/automation/eclair_analysis/prepare.sh +++ b/automation/eclair_analysis/prepare.sh @@ -43,4 +43,6 @@ fi make -f "${script_dir}/Makefile.prepare" prepare # Translate the /* SAF-n-safe */ comments into ECLAIR CBTs scripts/xen-analysis.py --run-eclair --no-build --no-clean + # Translate function-properties.json into ECLAIR properties + python3 ${script_dir}/propertyparser.py ) diff --git a/automation/eclair_analysis/propertyparser.py b/automation/ecla= ir_analysis/propertyparser.py new file mode 100644 index 0000000000..0d02f505a6 --- /dev/null +++ b/automation/eclair_analysis/propertyparser.py @@ -0,0 +1,37 @@ +import json +import os + +script_dir =3D os.path.dirname(__file__) +properties_path =3D os.path.join(script_dir, "../../docs/function_macro_pr= operties.json") +output_path =3D os.path.join(script_dir, "ECLAIR/call_properties.ecl") + +with open(properties_path) as fp: + properties =3D json.load(fp)['content'] + +ecl =3D open(output_path, 'w') + +for record in properties: + + string =3D "-call_properties+=3D{\"" + if record['type'] =3D=3D "function": + string +=3D f"{record['value']}\", {{".replace("\\", "\\\\") + else: + string +=3D f"{record['type']}({record['value']})\", {{".replace("= \\", "\\\\") + + i=3D0 + for prop in record['properties'].items(): + if prop[0] =3D=3D 'attribute': + string +=3D prop[1] + i+=3D1 + else: + string +=3D f"\"{prop[0]}({prop[1]})\"" + i+=3D1 + + if i