Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

PTEs are invalid if reserved bits are non-zero #677

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
+22 −7
Open

PTEs are invalid if reserved bits are non-zero #677

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a416d0e
PTEs are invalid if reserved bits are non-zero
Timmmm Dec 20, 2024
fc31269
Switch to date based version
Timmmm Mar 3, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions model/riscv_extensions.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,17 @@
/* SPDX-License-Identifier: BSD-2-Clause */
/*=======================================================================================*/

// 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.
let configPrivVersion : SpecVersion = 20240411
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe the easiest approach here to allow using relational operators would be to add variables such as Priv_1_12 = 20211203 and use those in the comparisons?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

And a comment above with a commit hash and a link to the release on github?

let configUnprivVersion : SpecVersion = 20240411

scattered enum extension

// Note, these are sorted according to the canonical ordering vaguely described
Expand Down
18 changes: 11 additions & 7 deletions model/riscv_vmem_pte.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 spec commit 31bc179b214fc0374075ea9284aa939b8341b843, reserved bits must be zero.
| configPrivVersion >= 20211101 & (
// All bits are currently reserved for non-leaf PTEs.
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a fix btw; the current code is missing it.

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 = {
Expand Down
Loading