From patchwork Fri Feb 2 09:37:47 2024 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Simone Ballarin X-Patchwork-Id: 13542564 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 C949FC48294 for ; Fri, 2 Feb 2024 09:38:54 +0000 (UTC) Received: from list by lists.xenproject.org with outflank-mailman.674923.1050130 (Exim 4.92) (envelope-from ) id 1rVq0T-0006q2-If; Fri, 02 Feb 2024 09:38:45 +0000 X-Outflank-Mailman: Message body and most headers restored to incoming version Received: by outflank-mailman (output) from mailman id 674923.1050130; Fri, 02 Feb 2024 09:38:45 +0000 Received: from localhost ([127.0.0.1] helo=lists.xenproject.org) by lists.xenproject.org with esmtp (Exim 4.92) (envelope-from ) id 1rVq0T-0006pt-EO; Fri, 02 Feb 2024 09:38:45 +0000 Received: by outflank-mailman (input) for mailman id 674923; Fri, 02 Feb 2024 09:38:43 +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 1rVq0R-0006GX-Hb for xen-devel@lists.xenproject.org; Fri, 02 Feb 2024 09:38:43 +0000 Received: from support.bugseng.com (mail.bugseng.com [162.55.131.47]) by se1-gles-sth1.inumbo.com (Halon) with ESMTPS id d962f27c-c1ae-11ee-8a43-1f161083a0e0; Fri, 02 Feb 2024 10:38:41 +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 5D9C64EE073E; Fri, 2 Feb 2024 10:38:40 +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: d962f27c-c1ae-11ee-8a43-1f161083a0e0 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: [PATCH v3 4/4] eclair: add and manage properties Date: Fri, 2 Feb 2024 10:37:47 +0100 Message-Id: X-Mailer: git-send-email 2.34.1 In-Reply-To: References: MIME-Version: 1.0 From: Maria Celeste Cesario Add JSON file containing properties. Add rst file containing explanation on how to update properties.json. Add instruction to eclair_analysis/prepare.sh to parse the JSON file. Signed-off-by: Maria Celeste Cesario Signed-off-by: Simone Ballarin --- .../eclair_analysis/ECLAIR/analysis.ecl | 1 + automation/eclair_analysis/prepare.sh | 2 + docs/properties.json | 841 ++++++++++++++++++ docs/properties.rst | 58 ++ 4 files changed, 902 insertions(+) create mode 100644 docs/properties.json create mode 100644 docs/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/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/docs/properties.json b/docs/properties.json new file mode 100644 index 0000000000..74058297b5 --- /dev/null +++ b/docs/properties.json @@ -0,0 +1,841 @@ +{ + "version": "1.0", + "content": [ + { + "type": "function", + "value": "^printk.*$", + "properties":{ + "pointee_write": "1..=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^debugtrace_printk.*$", + "properties":{ + "pointee_write": "1..=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^panic.*$", + "properties":{ + "pointee_write": "1..=never", + "taken": "" + } + }, + { + "type": "macro", + "value": "^domain_crash$", + "properties":{ + "pointee_write": "2..=never", + "taken": "" + } + }, + { + "type": "macro", + "value": "^(g?d|mm_)?printk$", + "properties":{ + "pointee_write": "2..=never", + "taken": "" + } + }, + { + "type": "macro", + "value": "^guest_bug_on_failed$", + "properties":{ + "pointee_write": "1=never", + "taken": "" + } + }, + { + "type": "macro", + "value": "^spin_lock_init_prof$", + "properties":{ + "pointee_write": "2=never", + "taken": "" + } + }, + { + "type": "macro", + "value": "^sched_test_func$", + "properties":{ + "pointee_write": "1..=never", + "taken": "" + } + }, + { + "type": "macro", + "value": "^dev_(info|warn)$", + "properties":{ + "pointee_write": "1..=never", + "taken": "" + } + }, + { + "type": "macro", + "value": "^PAGING_DEBUG$", + "properties":{ + "pointee_write": "1..=never", + "taken": "" + } + }, + { + "type": "macro", + "value": "^ACPI_(WARNING|ERROR|INFO)$", + "properties":{ + "pointee_write": "1..=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^fdt_get_property_by_offset_.*$", + "properties":{ + "pointee_write": "3=always", + "pointee_read": "3=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^read_atomic_size.*$", + "properties":{ + "pointee_write": "2=always", + "pointee_read": "2=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^device_tree_get_reg.*$", + "properties":{ + "pointee_write": "4..=always", + "pointee_read": "4..=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^dt_get_range.*$", + "properties":{ + "pointee_write": "3..=always", + "pointee_read": "3..=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^parse_static_mem_prop.*$", + "properties":{ + "pointee_write": "2..=always", + "pointee_read": "2..=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^get_ttbr_and_gran_64bit.*$", + "properties":{ + "pointee_write": "1..2=always", + "pointee_read": "1..2=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^hvm_emulate_init_once.*$", + "properties":{ + "pointee_write": "1=always", + "pointee_read": "1=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^__vmread.*$", + "properties":{ + "pointee_write": "2=always", + "pointee_read": "2=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^hvm_pci_decode_addr.*$", + "properties":{ + "pointee_write": "3=always", + "pointee_read": "3=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^vpci_mmcfg_decode_addr.*$", + "properties":{ + "pointee_write": "3=always", + "pointee_read": "3=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^x86emul_decode.*$", + "properties":{ + "pointee_write": "1=always", + "pointee_read": "1=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^unmap_grant_ref.*$", + "properties":{ + "pointee_write": "2=always", + "pointee_read": "2=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^arm_smmu_cmdq_build_cmd.*$", + "properties":{ + "pointee_write": "1=always", + "pointee_read": "1=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^pci_size_mem_bar.*$", + "properties":{ + "pointee_write": "4=always", + "pointee_read": "4=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^_hvm_read_entry.*$", + "properties":{ + "pointee_write": "2=always", + "pointee_read": "2=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^hvm_map_guest_frame_rw.*$", + "properties":{ + "pointee_write": "3=always", + "pointee_read": "3=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^guest_cpuid.*$", + "properties":{ + "pointee_write": "4=always", + "pointee_read": "4=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^epte_get_entry_emt.*$", + "properties":{ + "pointee_write": "5=always", + "pointee_read": "5=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^mcheck_mca_logout.*$", + "properties":{ + "pointee_write": "3=always", + "pointee_read": "3=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^set_field_in_reg_u32.*$", + "properties":{ + "pointee_write": "5=always", + "pointee_read": "5=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^alloc_affinity_masks.*$", + "properties":{ + "pointee_write": "1=always", + "pointee_read": "1=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^xasprintf.*$", + "properties":{ + "pointee_write": "1=always", + "pointee_read": "1=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^find_non_smt.*$", + "properties":{ + "pointee_write": "2=always", + "pointee_read": "2=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^call_rcu.*$", + "properties":{ + "pointee_write": "1=always", + "pointee_read": "1=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^getdomaininfo.*$", + "properties":{ + "pointee_write": "2=always", + "pointee_read": "2=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^MAPPING_(INSERT|SEARCH)\\(.*$", + "properties":{ + "pointee_write": "2..=always", + "pointee_read": "2..=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^FormatDec.*$", + "properties":{ + "pointee_write": "2=always", + "pointee_read": "2=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^FormatHex.*$", + "properties":{ + "pointee_write": "3=always", + "pointee_read": "3=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^p2m_get_ioreq_server.*$", + "properties":{ + "pointee_write": "2=always", + "pointee_read": "2=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^elf_memset_unchecked.*$", + "properties":{ + "pointee_write": "1=always", + "pointee_read": "1=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^set_iommu_pte_present.*$", + "properties":{ + "pointee_write": "7=always", + "pointee_read": "7=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^clear_iommu_pte_present.*$", + "properties":{ + "pointee_write": "4=always", + "pointee_read": "4=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^vcpu_runstate_get.*$", + "properties":{ + "pointee_write": "2=always", + "pointee_read": "2=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^va_start.*$", + "properties":{ + "pointee_write": "1=always", + "pointee_read": "1=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^sgi_target_init.*$", + "properties":{ + "pointee_write": "1=always", + "pointee_read": "1=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^get_hw_residencies.*$", + "properties":{ + "pointee_write": "2=always", + "pointee_read": "2=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^x86_cpu_policy_to_featureset.*$", + "properties":{ + "pointee_write": "2=always", + "pointee_read": "2=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^simple_strtou?ll?\\(.*$", + "properties":{ + "pointee_write": "2=always", + "pointee_read": "2=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^msi_compose_msg.*$", + "properties":{ + "pointee_write": "3=always", + "pointee_read": "3=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^print_tainted.*$", + "properties":{ + "pointee_write": "1=always", + "pointee_read": "1=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^get_hvm_registers.*$", + "properties":{ + "pointee_write": "3=always", + "pointee_read": "3=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^x86_insn_modrm.*$", + "properties":{ + "pointee_write": "2..3=always", + "pointee_read": "2..3=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^cpuid_count_leaf.*$", + "properties":{ + "pointee_write": "3=always", + "pointee_read": "3=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^rcu_lock_remote_domain_by_id.*$", + "properties":{ + "pointee_write": "2=always", + "pointee_read": "2=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^cpuid_count.*$", + "properties":{ + "pointee_write": "3..=always", + "pointee_read": "3..=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^.*efi_boot_mem_unused.*$", + "properties":{ + "pointee_write": "1..=always", + "pointee_read": "1..=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^collect_time_info.*$", + "properties":{ + "pointee_write": "2=always", + "pointee_read": "2=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^setup_xstate_comp.*$", + "properties":{ + "pointee_write": "1=always", + "pointee_read": "1=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^map_domain_gfn.*$", + "properties":{ + "pointee_read": "5=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^fdt_getprop.*$", + "properties":{ + "pointee_read": "4=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^fdt_get_name.*$", + "properties":{ + "pointee_read": "3=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^fdt_get_property.*$", + "properties":{ + "pointee_read": "4=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^pci_get_host_bridge_segment.*$", + "properties":{ + "pointee_read": "2=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^dt_get_property.*$", + "properties":{ + "pointee_read": "3=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^dt_property_read_u32.*$", + "properties":{ + "pointee_read": "3=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^dt_device_get_paddr.*$", + "properties":{ + "pointee_read": "3..4=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^get_evtchn_dt_property.*$", + "properties":{ + "pointee_write": "2..3=maybe", + "pointee_read": "2..3=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^setup_chosen_node.*$", + "properties":{ + "pointee_write": "2..3=maybe", + "pointee_read": "2..3=never", + "taken": "" + } + }, + { + "type": "function", + "value": "^queue_remove_raw.*$", + "properties":{ + "pointee_read": "2=never", + "taken": "" + } + }, + { + "type": "macro", + "value": "^memset$", + "properties":{ + "pointee_write": "1=always", + "pointee_read": "1=never", + "taken": "" + } + }, + { + "type": "macro", + "value": "^va_start$", + "properties":{ + "pointee_write": "1=always", + "pointee_read": "1=never", + "taken": "" + } + }, + { + "type": "macro", + "value": "^memcmp$", + "properties":{ + "pointee_write": "1..2=never", + "taken": "" + } + }, + { + "type": "macro", + "value": "^memcpy$", + "properties":{ + "pointee_write": "1=always&&2..=never", + "pointee_read": "1=never&&2..=always", + "taken": "" + } + }, + { + "type": "function", + "value": "^get_cpu_info.*$", + "properties":{ + "attribute": "pure" + } + }, + { + "type": "function", + "value": "^pdx_to_pfn.*$", + "properties":{ + "attribute": "pure" + } + }, + { + "type": "function", + "value": "^is_pci_passthrough_enabled.*$", + "properties":{ + "attribute": "const" + } + }, + { + "type": "function", + "value": "^get_cycles.*$", + "properties":{ + "attribute": "noeffect" + } + }, + { + "type": "function", + "value": "^msi_gflags.*$", + "properties":{ + "attribute": "const" + } + }, + { + "type": "function", + "value": "^hvm_save_size.*$", + "properties":{ + "attribute": "pure" + } + }, + { + "type": "function", + "value": "^cpu_has.*$", + "properties":{ + "attribute": "pure" + } + }, + { + "type": "function", + "value": "^boot_cpu_has.*$", + "properties":{ + "attribute": "pure" + } + }, + { + "type": "function", + "value": "^get_cpu_info.*$", + "properties":{ + "attribute": "pure" + } + }, + { + "type": "function", + "value": "^put_pte_flags.*$", + "properties":{ + "attribute": "const" + } + }, + { + "type": "function", + "value": "^is_pv_cpu.*$", + "properties":{ + "attribute": "pure" + } + }, + { + "description": "Property inferred as a consequence of the semantics of device_tree_get_reg", + "type": "function", + "value": "^acquire_static_memory_bank.*$", + "properties":{ + "pointee_write": "4..=always", + "pointee_read": "4..=never", + "taken": "" + } + }, + { + "description": "Property inferred as a consequence of the semantics of dt_set_cell", + "type": "function", + "value": "^set_interrupt.*$", + "properties":{ + "pointee_write": "1=always", + "pointee_read": "1=never", + "taken": "" + } + }, + { + "description":"Property inferred as a consequence of the semantics of __p2m_get_mem_access", + "type": "function", + "value": "^p2m_get_mem_access.*$", + "properties":{ + "pointee_write": "3=always", + "pointee_read": "3=never", + "taken": "" + } + }, + { + "description": "This function has alternative definitions with props {write=always,read=never} and {write=never,read=never}", + "type": "function", + "value": "^alloc_cpumask_var.*$", + "properties":{ + "pointee_write": "1=maybe", + "pointee_read": "1=never", + "taken": "" + } + }, + { + "description": "Property inferred as a consequence of the semantics of alloc_cpumask_var", + "type": "function", + "value": "^xenctl_bitmap_to_cpumask.*$", + "properties":{ + "pointee_write": "1=always", + "pointee_read": "1=never", + "taken": "" + } + }, + { + "description": "The call to bitmap_and causes the pointee of dstp to be always written", + "type": "function", + "value": "^cpumask_(and|andnot|clear|copy|complement).*$", + "properties":{ + "pointee_write": "1=always", + "pointee_read": "1=never", + "taken": "" + } + }, + { + "description": "The call to bitmap_and causes the pointee of dstp to be always written", + "type": "function", + "value": "^bitmap_(andnot|complement|fill).*$", + "properties":{ + "pointee_write": "1=always", + "pointee_read": "1=never", + "taken": "" + } + }, + { + "description": "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.", + "type": "macro", + "value": "^(__)?(raw_)?copy_from_(paddr|guest|compat)(_offset)?$", + "properties":{ + "pointee_write": "1=always", + "pointee_read": "1=never", + "taken": "" + } + }, + { + "description":"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.", + "type": "macro", + "value": "^(__)?copy_to_(guest|compat)(_offset)?$", + "properties":{ + "pointee_write": "2=always", + "pointee_read": "2=never", + "taken": "" + } + }, + { + "description": "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.", + "type": "function", + "value": "^read_u(8|16|32|64|int)_atomic.*$", + "properties":{ + "attribute": "noeffect" + } + }, + { + "description": "Functions generated by TYPE_SAFE are const.", + "type": "function", + "value": "^(mfn|gfn|pfn)_x\\(.*$", + "properties":{ + "attribute": "const" + } + }, + { + "description": "Functions generated by TYPE_SAFE are const.", + "type": "function", + "value": "^_(mfn|gfn|pfn)\\(.*$", + "properties":{ + "attribute": "const" + } + } + ] +} diff --git a/docs/properties.rst b/docs/properties.rst new file mode 100644 index 0000000000..790f1ede1e --- /dev/null +++ b/docs/properties.rst @@ -0,0 +1,58 @@ +.. SPDX-License-Identifier: CC-BY-4.0 + +Properties list for Xen +======================= + +Some functions and macros are found to have properties relevant to +the Xen codebase. For this reason, the file docs/properties.json +contains all the needed properties. + +Here is an example of the properties.json file:: + + { + "version": "1.0", + "content": [ + { + "description": "" + "type": "function", // required + "value:": "^printk*.$", // required + "properties":{ + "pointee_write": "1..2=never", + "pointee_read": "", + "taken": "" + "attribute": "" + } + } + ] + } + +Here is an explanation of the fields inside an object of the "content" array: + + - description: a brief description of why the properties apply + - type: this is the kind of the element called: it may be either ``macro`` or ``function`` + - value: must be a regex, starting with ^ and ending with $ and matching function fully + qualified name or macro name. + - properties: a list of properties applied to said function. + Possible values are: + + - pointee_write: indicate the write use for call arguments that correspond to + parameters whose pointee types are non-const + - pointee_read: indicate the read use for call arguments that correspond to + parameters whose pointee types are non-const + - taken: indicates that the specified address arguments may be stored in objects + that persist after the function has ceased to exist (excluding the returned value); + address arguments not listed are never taken + - attribute: attributes a function may have. Possible values are pure, const and noeffect. + + pointee_read and pointee_write use a specific kind of argument, structured as pointee_arg=rw: + + - pointee_arg: argument index for callee. Index 0 refers to the return value, + the indices of the arguments start from 1. It can be either a single value or a range. + - rw: a value that's either always, maybe or never + + - always: for pointee_read: argument pointee is expected to be fully initialized at function enter, + for pointee_write: argument pointee is fully initialized at function exit + - maybe: for pointee_read: argument pointee may be expected to be initialized at function enter, + for pointee_write: argument pointee may be written by function body + - never: for pointee_read: argument pointee is not expected to be read in the functions's body, + for pointee_write: argument pointee is never written by function body