From a416d0eadbc402d3a3f635ae464a3c97e5ca580e Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Fri, 20 Dec 2024 14:46:17 +0000 Subject: [PATCH 1/2] PTEs are invalid if reserved bits are non-zero This has only been the case since version 1.12 of the spec, so I added support for setting the spec version. It isn't exposed on the command line yet since hopefully we'll be using the new config system soon. --- model/riscv_extensions.sail | 38 +++++++++++++++++++++++++++++++++++++ model/riscv_vmem_pte.sail | 18 +++++++++++------- 2 files changed, 49 insertions(+), 7 deletions(-) diff --git a/model/riscv_extensions.sail b/model/riscv_extensions.sail index 8b5bf2bd8..50d8dc7ba 100644 --- a/model/riscv_extensions.sail +++ b/model/riscv_extensions.sail @@ -6,6 +6,44 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ +// Privileged and unprivileged spec versions. +// These must be listed in order so the comparison operators work as expected. +enum PrivSpecVersion = { + Version_1_11, + Version_1_12, // AKA 20211203 + // ???, // 20240411 + Version_1_13, // AKA 20241017 ? +} + +enum UnprivSpecVersion = { + Version_2_0, + Version_2_1, + Version_2_2, + Version_20190608, + Version_20191213, +} + +// TODO: Replace with 'config ...priv_version' or similar when the config system is available. +function privVersion() -> PrivSpecVersion = Version_1_11 +function unprivVersion() -> UnprivSpecVersion = Version_2_1 + +// For convenience, version comparison operators. +function priv_version_lt(x : PrivSpecVersion, y : PrivSpecVersion) -> bool = num_of_PrivSpecVersion(x) < num_of_PrivSpecVersion(y) +function priv_version_gt(x : PrivSpecVersion, y : PrivSpecVersion) -> bool = num_of_PrivSpecVersion(x) > num_of_PrivSpecVersion(y) +function priv_version_le(x : PrivSpecVersion, y : PrivSpecVersion) -> bool = num_of_PrivSpecVersion(x) <= num_of_PrivSpecVersion(y) +function priv_version_ge(x : PrivSpecVersion, y : PrivSpecVersion) -> bool = num_of_PrivSpecVersion(x) >= num_of_PrivSpecVersion(y) + +function unpriv_version_lt(x : UnprivSpecVersion, y : UnprivSpecVersion) -> bool = num_of_UnprivSpecVersion(x) < num_of_UnprivSpecVersion(y) +function unpriv_version_gt(x : UnprivSpecVersion, y : UnprivSpecVersion) -> bool = num_of_UnprivSpecVersion(x) > num_of_UnprivSpecVersion(y) +function unpriv_version_le(x : UnprivSpecVersion, y : UnprivSpecVersion) -> bool = num_of_UnprivSpecVersion(x) <= num_of_UnprivSpecVersion(y) +function unpriv_version_ge(x : UnprivSpecVersion, y : UnprivSpecVersion) -> bool = num_of_UnprivSpecVersion(x) >= num_of_UnprivSpecVersion(y) + +overload operator < = {priv_version_lt, unpriv_version_lt} +overload operator > = {priv_version_gt, unpriv_version_gt} +overload operator <= = {priv_version_le, unpriv_version_le} +overload operator >= = {priv_version_ge, unpriv_version_ge} + + scattered enum extension // Note, these are sorted according to the canonical ordering vaguely described diff --git a/model/riscv_vmem_pte.sail b/model/riscv_vmem_pte.sail index ce5b19d7a..9ab983b8e 100644 --- a/model/riscv_vmem_pte.sail +++ b/model/riscv_vmem_pte.sail @@ -77,18 +77,22 @@ function clause extensionEnabled(Ext_Svpbmt) = false function pte_is_invalid(pte_flags : PTE_Flags, pte_ext : PTE_Ext) -> bool = pte_flags[V] == 0b0 | (pte_flags[W] == 0b1 & pte_flags[R] == 0b0) - // Note, the following requirements depend on the privileged spec version. - // Early versions do not require this check. This will need to be behind - // a flag when the Sail model allows specifying the spec version. - | (pte_ext[N] != 0b0 & not(extensionEnabled(Ext_Svnapot))) - | (pte_ext[PBMT] != zeros() & not(extensionEnabled(Ext_Svpbmt))) - | pte_ext[reserved] != zeros() + // Since version 1.12 of the spec, reserved bits must be zero. + | privVersion() >= Version_1_12 & ( + // All bits are currently reserved for non-leaf PTEs. + pte_is_ptr(pte_flags) & pte_ext.bits != zeros() + // N/PBMT are reserved if not implemented. + | pte_ext[N] != zeros() & not(extensionEnabled(Ext_Svnapot)) + | pte_ext[PBMT] != zeros() & not(extensionEnabled(Ext_Svpbmt)) + // Other bits are reserved even for leaf PTEs. + | pte_ext[reserved] != zeros() + ) // ---------------- // Check access permissions in PTE // For (non-standard) extensions: this function gets the extension-available bits -// of the PTE in extPte, and the accumulated information of the page-table-walk +// of the PTE in PTE_Ext, and the accumulated information of the page-table-walk // in ext_ptw. It should return the updated ext_ptw in both success and failure cases. union PTE_Check = { From fc31269cc11ea9957ac30bdda97f9877596e5f63 Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Mon, 3 Mar 2025 16:18:42 +0000 Subject: [PATCH 2/2] Switch to date based version --- model/riscv_extensions.sail | 43 +++++++------------------------------ model/riscv_vmem_pte.sail | 4 ++-- 2 files changed, 10 insertions(+), 37 deletions(-) diff --git a/model/riscv_extensions.sail b/model/riscv_extensions.sail index 50d8dc7ba..e7083c014 100644 --- a/model/riscv_extensions.sail +++ b/model/riscv_extensions.sail @@ -6,43 +6,16 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ -// Privileged and unprivileged spec versions. -// These must be listed in order so the comparison operators work as expected. -enum PrivSpecVersion = { - Version_1_11, - Version_1_12, // AKA 20211203 - // ???, // 20240411 - Version_1_13, // AKA 20241017 ? -} - -enum UnprivSpecVersion = { - Version_2_0, - Version_2_1, - Version_2_2, - Version_20190608, - Version_20191213, -} +// Privileged and unprivileged spec versions. The versioning system for specifications +// is unclear so we just use the commit date. This also allows versioning for specs changes +// that are between releases. If there was an official release for this day (for example +// 20240411) then this is the commit of that release. Otherwise it is for the *last* +// commit on the given day. +type SpecVersion = range(20000000, 21000000) // TODO: Replace with 'config ...priv_version' or similar when the config system is available. -function privVersion() -> PrivSpecVersion = Version_1_11 -function unprivVersion() -> UnprivSpecVersion = Version_2_1 - -// For convenience, version comparison operators. -function priv_version_lt(x : PrivSpecVersion, y : PrivSpecVersion) -> bool = num_of_PrivSpecVersion(x) < num_of_PrivSpecVersion(y) -function priv_version_gt(x : PrivSpecVersion, y : PrivSpecVersion) -> bool = num_of_PrivSpecVersion(x) > num_of_PrivSpecVersion(y) -function priv_version_le(x : PrivSpecVersion, y : PrivSpecVersion) -> bool = num_of_PrivSpecVersion(x) <= num_of_PrivSpecVersion(y) -function priv_version_ge(x : PrivSpecVersion, y : PrivSpecVersion) -> bool = num_of_PrivSpecVersion(x) >= num_of_PrivSpecVersion(y) - -function unpriv_version_lt(x : UnprivSpecVersion, y : UnprivSpecVersion) -> bool = num_of_UnprivSpecVersion(x) < num_of_UnprivSpecVersion(y) -function unpriv_version_gt(x : UnprivSpecVersion, y : UnprivSpecVersion) -> bool = num_of_UnprivSpecVersion(x) > num_of_UnprivSpecVersion(y) -function unpriv_version_le(x : UnprivSpecVersion, y : UnprivSpecVersion) -> bool = num_of_UnprivSpecVersion(x) <= num_of_UnprivSpecVersion(y) -function unpriv_version_ge(x : UnprivSpecVersion, y : UnprivSpecVersion) -> bool = num_of_UnprivSpecVersion(x) >= num_of_UnprivSpecVersion(y) - -overload operator < = {priv_version_lt, unpriv_version_lt} -overload operator > = {priv_version_gt, unpriv_version_gt} -overload operator <= = {priv_version_le, unpriv_version_le} -overload operator >= = {priv_version_ge, unpriv_version_ge} - +let configPrivVersion : SpecVersion = 20240411 +let configUnprivVersion : SpecVersion = 20240411 scattered enum extension diff --git a/model/riscv_vmem_pte.sail b/model/riscv_vmem_pte.sail index 9ab983b8e..84ed05a9a 100644 --- a/model/riscv_vmem_pte.sail +++ b/model/riscv_vmem_pte.sail @@ -77,8 +77,8 @@ function clause extensionEnabled(Ext_Svpbmt) = false function pte_is_invalid(pte_flags : PTE_Flags, pte_ext : PTE_Ext) -> bool = pte_flags[V] == 0b0 | (pte_flags[W] == 0b1 & pte_flags[R] == 0b0) - // Since version 1.12 of the spec, reserved bits must be zero. - | privVersion() >= Version_1_12 & ( + // Since spec commit 31bc179b214fc0374075ea9284aa939b8341b843, reserved bits must be zero. + | configPrivVersion >= 20211101 & ( // All bits are currently reserved for non-leaf PTEs. pte_is_ptr(pte_flags) & pte_ext.bits != zeros() // N/PBMT are reserved if not implemented.