Add missing PTE checks

[ved-rivos]

The PTE checking in the sail model is missing part of the following rule that requires raising a page fault if reserved bits are set:

If pte.v = 0, or if pte.r = 0 and pte.w = 1, or if any bits or encodings that are reserved for future standard use are set within pte, stop and raise a page-fault exception corresponding to the original access type

• The bits 63:54 are reserved for future standard extensions. The bit 63 is defined by Svnapot and bits 62:61 by Svpbmt - but both these extensions are not in the model presently.
• For non-leaf PTEs, the D, A, and U bits are reserved for future standard use.

All tests pass.

[jrtc27]

IIRC these checks didn't used to be in the spec, so it's not that they're missing, it's that you want to make the model conform to a newer version of the priv spec?

[jrtc27]

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

[Alasdair]

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?

[ved-rivos]

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.

[ved-rivos]

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.

[allenjbaum]

Cheri isn't a ratified spec, it's being developed, so for the arch-test use cases, it has to have that check. So either we have to add a CLI switch that enables Cheri (i.e. disables this check) & enables all the other Cheri functionality), or Cheri development is done in a separate branch, right?

…

On Thu, Jan 11, 2024 at 6:02 PM Jessica Clarke ***@***.***> wrote: ***@***.**** requested changes on this pull request. IIRC these checks didn't used to be in the spec, so it's not that they're missing, it's that you want to make the model conform to a newer version of the priv spec? ------------------------------ In model/riscv_pte.sail <#387 (comment)>: > @@ -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) | This breaks extensions (e.g. CHERI) that *do* assign meaning to these bits and exist as users of the Sail model — Reply to this email directly, view it on GitHub <#387 (review)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AHPXVJXEB62MULM5AEFMY23YOCKRXAVCNFSM6AAAAABBXMSJMOVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMYTQMJXGIZTQNBWHE> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>