Move experimental instructions to their own file #20
Conversation
|
|
||
| /* >>> */ | ||
| /* CRAM and CRAP (D.2) <<< */ | ||
|
|
There was a problem hiding this comment.
Crap and cram are used by cheribsd and both are useful. I wonder if we should move them to non-experimental in the spec?
There was a problem hiding this comment.
I was wondering that myself (and in fact have a comment in the docs to that effect). CHERI-RISC-V similarly no longer considers C{Get,Set}Flags experimental.
There was a problem hiding this comment.
It might be worth deciding on a better name for one of those before promoting it in the ISA doc...
There was a problem hiding this comment.
The ISA doc calls them CRepresentableAlignmentMask (CRAM) and CRoundRepresentableLength (CRRL).
And sort them by section of the appendix in the ISA doc.
|
Is this PR now obsolete? |
|
I think we think that some of these things are still experimental; do you think the partition worthwhile? If so, I can update the PR. |
|
I don't really mind. Is there a specific purpose to making the distinction here? Obviously in the manual they need to be separated and I suppose we might want to exclude them from proof in some circumstances... |
|
It was mostly the latter I had in mind, yea. If they're not doing harm right now, I'm content to leave things well enough alone. |
|
In principle separating experimental instructions could be convenient for proof, but given that I am currently focusing on other architectures and nobody else is working on proofs of (Sail-)CHERI-MIPS at the moment AFAIK, I don't think there's a pressing need to change anything right now. |
And sort them by section of the appendix in the ISA doc.