PTEs are invalid if reserved bits are non-zero #677
Conversation
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.
| // Machine and Supervisor Architectures v1.12 | ||
| function clause extensionEnabled(Ext_Sx1p12) = extensionEnabled(Ext_Sx1p11) | true | ||
| // Machine and Supervisor Architectures v1.13 | ||
| function clause extensionEnabled(Ext_Sx1p13) = extensionEnabled(Ext_Sx1p12) | true |
There was a problem hiding this comment.
Should this be an & instead of an | ? I.e. 1.13 requires 1.12?
Not that it really matters since it's all hardcoded to 1.
There was a problem hiding this comment.
Yeah I think you're right. I'll change it.
There was a problem hiding this comment.
If we are going to go with this approach and not a proper extension version function, then I think the following would make more sense. The current use of | is definitely not right (enabling 1.11 would result in 1.13 being enabled), but I think using & is also cumbersome because enabling 1.13 would require also manually enabling 1.11 and 1.12.
// Machine and Supervisor Architectures v1.11
function clause extensionEnabled(Ext_Sx1p11) = extensionEnabled(Ext_Sx1p12) | true
// Machine and Supervisor Architectures v1.12
function clause extensionEnabled(Ext_Sx1p12) = extensionEnabled(Ext_Sx1p13) | true
// Machine and Supervisor Architectures v1.13
function clause extensionEnabled(Ext_Sx1p13) = true
That way the user just needs to enable the latest version that they support and other versions would implicitly be enabled as well. This probably covers most cases (since there are very few backwards incompatible changes) and the few backwards incompatible scenarios can use something like if extensionEnabled(Ext_Sx1p12) & not(extensionEnabled(Ext_Sx1p13))
There was a problem hiding this comment.
Yeah I think Jessica is right - I'm going to rework this to use a proper versioning function.
There was a problem hiding this comment.
Sounds good. That is definitely the more robust approach.
There was a problem hiding this comment.
Great. Happy to review that when you have it.
| @@ -11,6 +11,13 @@ scattered enum extension | |||
| // Note, these are sorted according to the canonical ordering vaguely described | |||
| // in the `Subset Naming Convention` section of the unprivileged spec. | |||
|
|
|||
| // Machine and Supervisor Architectures v1.11 | |||
| enum clause extension = Ext_Sx1p11 | |||
There was a problem hiding this comment.
There is no such thing as Sx1p11 etc. Ss1p11 and Sm1p11 are the extension names. We shouldn't be using non-existent extension names in the official model.
There was a problem hiding this comment.
Yeah true, I just thought it was probably overkill to have both (I'm not even entirely sure what it would mean to support Ss1p11 and Sm1p12 for example) so this was an attempt to combine them. I agree it's not very obvious though and unfortunate that it's not a real extension name.
Do you think we should have both separately, or use a different name to combine them?
There was a problem hiding this comment.
They should be separate, because from an ISA model reading perspective it's important to know whether something's attributed to Ss or Sm. But I think it's perfectly fine to have an invariant that the versions match between them (and expect that's an implicit assumption made by the privileged spec; it hurts my head to think about what mixing would even look like...).
There was a problem hiding this comment.
Ok that makes sense, I'll change it.
| // Machine and Supervisor Architectures v1.11 | ||
| function clause extensionEnabled(Ext_Sx1p11) = true | ||
| // Machine and Supervisor Architectures v1.12 | ||
| function clause extensionEnabled(Ext_Sx1p12) = extensionEnabled(Ext_Sx1p11) | true |
There was a problem hiding this comment.
This doesn't make sense to me. You can't have multiple versions of an extension implemented. Ss1p12 is implemented if and only if priv 1.12 is the version your implementation chose. You have the Ss and Sm extensions and they have a version corresponding to whatever's implemented.
What you're after is some extensionVersion function that, given Ss or Sm (NB: no suffix on the extension name in the enum), tells you what version is implemented, so you can do >= 1.12 etc where needed.
There was a problem hiding this comment.
Hmm yeah that is definitely the more correct way to do it, but it seemed a lot simpler to pretend they are separate extensions and then ensure that version N implies versions <N.
Open to other options though.
There was a problem hiding this comment.
Simpler, sure, but definitely wrong, and for the official model that's a real problem.
There was a problem hiding this comment.
Is it actually wrong? If a chip supports Ss1p12 and some instruction requires Ss1p11 then isn't it fair to say the chip supports Ss1p12 and Ss1p11... Unless the versions aren't backwards compatible I guess. Which tbf is the sometimes the case.
There was a problem hiding this comment.
Exactly, they're not backwards compatible. PTE reserved bit handling being such a case. Each SsXpY is its own independent thing, where a later version is generally a superset of the previous version, but not always entirely.
There was a problem hiding this comment.
Ah ok I understand. I'll try and come up with something better.
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.