From patchwork Fri Feb 2 15:16:05 2024 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Simone Ballarin X-Patchwork-Id: 13543019 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from lists.xenproject.org (lists.xenproject.org [192.237.175.120]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.lore.kernel.org (Postfix) with ESMTPS id 42304C4828F for ; Fri, 2 Feb 2024 15:17:04 +0000 (UTC) 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 X-Outflank-Mailman: Message body and most headers restored to incoming version 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-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 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 file in docs. In this way, they can be exploited for other purposes (i.e. documentation, other tools). Add rst file containing explanation on how to update function_macro_properties.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/eclair_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=deviations.ecl -eval_file=call_properties.ecl -eval_file=tagging.ecl +-eval_file=properties.ecl -eval_file=concat(set,".ecl") -doc="Hide reports in external code." diff --git a/automation/eclair_analysis/ECLAIR/call_properties.ecl b/automation/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+={"name(printk)", {"pointee_write(1..=never)", "taken()"}} --call_properties+={"name(debugtrace_printk)", {"pointee_write(1..=never)", "taken()"}} --call_properties+={"name(panic)", {"pointee_write(1..=never)", "taken()"}} --call_properties+={"macro(^domain_crash$)", {"pointee_write(2..=never)", "taken()"}} --call_properties+={"macro(^(g?d|mm_)?printk$)", {"pointee_write(2..=never)", "taken()"}} --call_properties+={"macro(^guest_bug_on_failed$)", {"pointee_write(1=never)", "taken()"}} --call_properties+={"macro(^spin_lock_init_prof$)", {"pointee_write(2=never)", "taken()"}} --call_properties+={"macro(^sched_test_func$)", {"pointee_write(1..=never)", "taken()"}} --call_properties+={"macro(^dev_(info|warn)$)", {"pointee_write(1..=never)", "taken()"}} --call_properties+={"macro(^PAGING_DEBUG$)", {"pointee_write(1..=never)", "taken()"}} --call_properties+={"macro(^ACPI_(WARNING|ERROR|INFO)$)", {"pointee_write(1..=never)", "taken()"}} --call_properties+={"name(fdt_get_property_by_offset_)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}} --call_properties+={"name(read_atomic_size)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}} --call_properties+={"name(device_tree_get_reg)", {"pointee_write(4..=always)", "pointee_read(4..=never)", "taken()"}} --call_properties+={"name(dt_get_range)", {"pointee_write(3..=always)", "pointee_read(3..=never)", "taken()"}} --call_properties+={"name(parse_static_mem_prop)", {"pointee_write(2..=always)", "pointee_read(2..=never)", "taken()"}} --call_properties+={"name(get_ttbr_and_gran_64bit)", {"pointee_write(1..2=always)", "pointee_read(1..2=never)", "taken()"}} --call_properties+={"name(hvm_emulate_init_once)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}} --call_properties+={"name(__vmread)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}} --call_properties+={"name(hvm_pci_decode_addr)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}} --call_properties+={"name(vpci_mmcfg_decode_addr)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}} --call_properties+={"name(x86emul_decode)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}} --call_properties+={"name(unmap_grant_ref)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}} --call_properties+={"name(arm_smmu_cmdq_build_cmd)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}} --call_properties+={"name(pci_size_mem_bar)", {"pointee_write(4=always)", "pointee_read(4=never)", "taken()"}} --call_properties+={"name(_hvm_read_entry)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}} --call_properties+={"name(hvm_map_guest_frame_rw)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}} --call_properties+={"name(guest_cpuid)", {"pointee_write(4=always)", "pointee_read(4=never)", "taken()"}} --call_properties+={"name(epte_get_entry_emt)", {"pointee_write(5=always)", "pointee_read(5=never)", "taken()"}} --call_properties+={"name(mcheck_mca_logout)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}} --call_properties+={"name(set_field_in_reg_u32)", {"pointee_write(5=always)", "pointee_read(5=never)", "taken()"}} --call_properties+={"name(alloc_affinity_masks)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}} --call_properties+={"name(xasprintf)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}} --call_properties+={"name(find_non_smt)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}} --call_properties+={"name(call_rcu)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}} --call_properties+={"name(getdomaininfo)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}} --call_properties+={"^MAPPING_(INSERT|SEARCH)\\(.*$", {"pointee_write(2..=always)", "pointee_read(2..=never)", "taken()"}} --call_properties+={"name(FormatDec)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}} --call_properties+={"name(FormatHex)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}} --call_properties+={"name(p2m_get_ioreq_server)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}} --call_properties+={"name(elf_memset_unchecked)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}} --call_properties+={"name(set_iommu_pte_present)", {"pointee_write(7=always)", "pointee_read(7=never)", "taken()"}} --call_properties+={"name(clear_iommu_pte_present)", {"pointee_write(4=always)", "pointee_read(4=never)", "taken()"}} --call_properties+={"name(vcpu_runstate_get)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}} --call_properties+={"name(va_start)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}} --call_properties+={"name(sgi_target_init)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}} --call_properties+={"name(get_hw_residencies)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}} --call_properties+={"name(x86_cpu_policy_to_featureset)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}} --call_properties+={"^simple_strtou?ll?\\(.*$", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}} --call_properties+={"name(msi_compose_msg)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}} --call_properties+={"name(print_tainted)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}} --call_properties+={"name(get_hvm_registers)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}} --call_properties+={"name(x86_insn_modrm)", {"pointee_write(2..3=always)", "pointee_read(2..3=never)", "taken()"}} --call_properties+={"name(cpuid_count_leaf)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}} --call_properties+={"name(rcu_lock_remote_domain_by_id)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}} --call_properties+={"name(cpuid_count)", {"pointee_write(3..=always)", "pointee_read(3..=never)", "taken()"}} --call_properties+={"name(efi_boot_mem_unused)", {"pointee_write(1..=always)", "pointee_read(1..=never)", "taken()"}} --call_properties+={"name(collect_time_info)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}} --call_properties+={"name(setup_xstate_comp)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}} --call_properties+={"name(map_domain_gfn)", {"pointee_read(5=never)", "taken()"}} --call_properties+={"name(fdt_getprop)", {"pointee_read(4=never)", "taken()"}} --call_properties+={"name(fdt_get_name)", {"pointee_read(3=never)", "taken()"}} --call_properties+={"name(fdt_get_property)", {"pointee_read(4=never)", "taken()"}} --call_properties+={"name(pci_get_host_bridge_segment)", {"pointee_read(2=never)", "taken()"}} --call_properties+={"name(dt_get_property)", {"pointee_read(3=never)", "taken()"}} --call_properties+={"name(dt_property_read_u32)", {"pointee_read(3=never)", "taken()"}} --call_properties+={"name(dt_device_get_paddr)", {"pointee_read(3..4=never)", "taken()"}} --call_properties+={"name(get_evtchn_dt_property)", {"pointee_write(2..3=maybe)", "pointee_read(2..3=never)", "taken()"}} --call_properties+={"name(setup_chosen_node)", {"pointee_write(2..3=maybe)", "pointee_read(2..3=never)", "taken()"}} --call_properties+={"name(queue_remove_raw)", {"pointee_read(2=never)", "taken()"}} --call_properties+={"macro(^memset$)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}} --call_properties+={"macro(^va_start$)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}} --call_properties+={"macro(^memcmp$)", {"pointee_write(1..2=never)", "taken()"}} --call_properties+={"macro(^memcpy$)", {"pointee_write(1=always&&2..=never)", "pointee_read(1=never&&2..=always)", "taken()"}} --call_properties+={"name(get_cpu_info)",{pure}} --call_properties+={"name(pdx_to_pfn)",{pure}} --call_properties+={"name(is_pci_passthrough_enabled)",{const}} --call_properties+={"name(get_cycles)", {"noeffect"}} --call_properties+={"name(msi_gflags)",{const}} --call_properties+={"name(hvm_save_size)",{pure}} --call_properties+={"name(cpu_has)",{pure}} --call_properties+={"name(boot_cpu_has)",{pure}} --call_properties+={"name(get_cpu_info)",{pure}} --call_properties+={"name(put_pte_flags)",{const}} --call_properties+={"name(is_pv_vcpu)",{pure}} - --doc_begin="Property inferred as a consequence of the semantics of device_tree_get_reg" --call_properties+={"name(acquire_static_memory_bank)", {"pointee_write(4..=always)", "pointee_read(4..=never)", "taken()"}} --doc_end - --doc_begin="Property inferred as a consequence of the semantics of dt_set_cell" --call_properties+={"name(set_interrupt)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}} --doc_end - --doc_begin="Property inferred as a consequence of the semantics of __p2m_get_mem_access" --call_properties+={"name(p2m_get_mem_access)", {"pointee_write(3=always)", "pointee_read(3=never)", "taken()"}} --doc_end - --doc_begin="This function has alternative definitions with props {write=always,read=never} and {write=never,read=never}" --call_properties+={"name(alloc_cpumask_var)", {"pointee_write(1=maybe)", "pointee_read(1=never)", "taken()"}} --doc_end - --doc_begin="Property inferred as a consequence of the semantics of alloc_cpumask_var" --call_properties+={"name(xenctl_bitmap_to_cpumask)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}} --doc_end - --doc_begin="The call to bitmap_and causes the pointee of dstp to be always written" --call_properties+={"^cpumask_(and|andnot|clear|copy|complement).*$", {"pointee_write(1=always)", "pointee_read(1=never)" "taken()"}} --call_properties+={"^bitmap_(andnot|complement|fill).*$", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}} --doc_end - --doc_begin="The .*copy_(to|from).* helpers all have a memcpy-like expectation 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+={"macro(^(__)?(raw_)?copy_from_(paddr|guest|compat)(_offset)?$)", {"pointee_write(1=always)", "pointee_read(1=never)", "taken()"}} --call_properties+={"macro(^(__)?copy_to_(guest|compat)(_offset)?$)", {"pointee_write(2=always)", "pointee_read(2=never)", "taken()"}} --doc_end - --doc_begin="Functions generated by build_atomic_read cannot be considered pure -since the input pointer is volatile, but they do not produce any persistent side -effect." --call_properties+={"^read_u(8|16|32|64|int)_atomic.*$", {noeffect}} --doc_end - --doc_begin="Functions generated by TYPE_SAFE are const." --call_properties+={"^(mfn|gfn|pfn)_x\\(.*$",{const}} --call_properties+={"^_(mfn|gfn|pfn)\\(.*$",{const}} --doc_end diff --git a/automation/eclair_analysis/prepare.sh b/automation/eclair_analysis/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/eclair_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 = os.path.dirname(__file__) +properties_path = os.path.join(script_dir, "../../docs/function_macro_properties.json") +output_path = os.path.join(script_dir, "ECLAIR/call_properties.ecl") + +with open(properties_path) as fp: + properties = json.load(fp)['content'] + +ecl = open(output_path, 'w') + +for record in properties: + + string = "-call_properties+={\"" + if record['type'] == "function": + string += f"{record['value']}\", {{".replace("\\", "\\\\") + else: + string += f"{record['type']}({record['value']})\", {{".replace("\\", "\\\\") + + i=0 + for prop in record['properties'].items(): + if prop[0] == 'attribute': + string += prop[1] + i+=1 + else: + string += f"\"{prop[0]}({prop[1]})\"" + i+=1 + + if i