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

Jump to bottom

Add missing PTE checks #387

Closed
wants to merge 1 commit into from
Closed

Add missing PTE checks #387

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
5 changes: 4 additions & 1 deletion model/riscv_pte.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -106,7 +106,10 @@ function isPTEPtr(p : pteAttribs, ext : extPte) -> bool = {

function isInvalidPTE(p : pteAttribs, ext : extPte) -> bool = {
let a = Mk_PTE_Bits(p);
a.V() == 0b0 | (a.W() == 0b1 & a.R() == 0b0)
a.V() == 0b0 |
(a.W() == 0b1 & a.R() == 0b0) |
(ext != 0b0000000000) |
Copy link
Collaborator

Choose a reason for hiding this comment

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

This breaks extensions (e.g. CHERI) that do assign meaning to these bits and exist as users of the Sail model

Copy link
Collaborator

Choose a reason for hiding this comment

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

If the base priv spec says we need to raise a page fault when these bits are non-zero, I'm not sure we can ignore it. Maybe we need to add some kind of mechanism so CHERI can override the behaviour of isInvalidPTE and similar functions with its own implementations?

Copy link
Contributor Author

@ved-rivos ved-rivos Jan 12, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

The privileged specification reserves these bits for future standard use. There are two extensions - Svpbmt and Svnapot - that use some of the bits that are not present in our golden reference model. The use of bits by extensions needs to be enabled by the governing xenvcfg register. Not having these checks makes it a problem to use it as a golden reference as these mismatches need to be waived. I hope to provide the models for the other missing pieces in the virtual memory system architecture - Svnapot, Svpbmt, and Sv57 - and this bug fix is needed to build those. When CHERI becomes a standard extension I think it would follow the architecture and add the environment controls to enable the use of a subset of those bits that get allocated for CHERI use.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I sent PR #393 with the Svnapot and Svpbmt extensions. Sorry, i had to duplicate contents of this PR in #393. Was trying to make updates incrementally but since this did not get merged, had to do the duplication. Please let me know if I should just close this PR since #393 is the superset.

(isPTEPtr(p, ext) & (a.D() == 0b1 | a.A() == 0b1 | a.U() == 0b1))
}

union PTE_Check = {
Expand Down