Lack of specification modularity

[nwf]

Despite extensive efforts over in the prose to keep things like capability encoding separate and to define platform hooks for extensions, these are not reflected in the sail. Fairly severe refactoring seems requisite. Please advise.

[Timmmm]

Capability encoding

The Sail code was written before the encoding format was separated into the appendix in the spec. I think the best thing to do there is make sure the encoding stuff is in its own file, then we can use the new riscv.sail_project file to allow easily customising it by replacing that file with your own encoding.

I don't think the refactoring needed here will be too bad - we basically need to split cheri_cap_common.sail up into two at around line 180. Then I think you can change the encoding by replacing the top half of that file, plus cheri_prelude_*.sail. (Don't quite me on that; been a long time since I looked at that code!)

File replacement was my initial plan for getting CHERI merged nicely into the upstream repo anyway - basically have a load of if $CHERI then [cheri_reg_types.sail] else [riscv_reg_types.sail] things. This is effectively how the old Makefile worked.

ext_ hooks (I assume that's what you meant by "platform hooks for extensions"?)

I was planning to get rid of most of ext_ hooks and just rename them to cheri_.... They were written as if they are a generic extension mechanism, but in reality:

1. They are fairly CHERI-specific - we've had to change some of them as the CHERI spec has evolved.
2. CHERI is the only thing that ever used them as far as I know.
3. They aren't even sufficient for CHERI - it uses the hooks some of the time, but in other places it simply replaces entire files.
4. They don't compose well - you can only ever really have one "extension".

Does that sound reasonable? Sorry for not answering earlier - I didn't get a notification for this for some reason!

[nwf]

By "platform hooks" I mean, at least, things for compositing the various extensions that define a CHERI system together; consider the changes to jalr to support Ysentry in riscv/riscv-cheri#627 by way of example.

[Timmmm]

Ah, yeah if I've understood correctly my preference would be not to have ext_ style hooks but to implement custom extensions as a git branch, but to make it as easy as possible to do that (ideally you would only need to modify riscv.sail_project).

The code is currently missing fine-grained extension flags - at the moment you get all of CHERI or nothing. We definitely need to fix that too, and ideally split the CHERI extensions into separate files/modules so they can be conditionally included.

Is there still a Cheri meeting on Thursdays? Maybe we could discuss this then?

[nwf]

"All of CHERI or nothing" isn't (IMHO) really viable the way I've been arguing to structure the spec (and I thought people generally agreed with, though I acknowledge that it might have to be otherwise if RVI insists on their current position). (See, again, riscv/riscv-cheri#627 and riscv/riscv-cheri#628 and similar factoring); since there is no singular thing that is "all of" in the superset/inclusion sense. I don't think long-lived branches are a good idea either, but I will spare you my ranting about the disappointment that is modern software version control.

More specifically, I think the current "base" factors into something like RVnnY+Zycbld+Zylevels1+Zysentry+Zysupervisor+Zybaseencoding, while CHERIoT ends up being something like (the surprisingly similar despite the name's edit distance) RV32+Zylevels1+Zyseals+Zycheriotsentry+Zycheriotencoding, and I don't know how to express a codebase that can at once be either of those without expressing it as a series of "mixin" components, and AFAIK, in Sail, at least, that means having explicit values in the code providing the Y base for the various mixins to supplant (by changing which files are involved, or perhaps through some of the more recently introduced module features?) and having suitable interface(s) to the encodings.

If that structure to the spec is untenable, or there's desire to have separate, long-lived forks of a common Sail base that implement particular platforms' combination of extensions holographically (that is, by directly editing definitions rather than by composing mixins), I guess I'll acquiesce, but that just seems like it's inviting trouble down the road.

[Timmmm]

Yeah totally - I think the different extensions will go in different files and you choose which one you want (Zybaseencoding or Zycheriotencoding) by compiling different files (by changing riscv.sail_project).

The part where I was thinking it's easier to have a branch is where you have to modify the base instructions to add CHERI hooks. But with the goal of eventually merging the branch into upstream master (assuming CHERI gets ratified).

[nwf]

Great, I think we're mostly on the same page. Just to check... AFAICT, this is the branch where we modify the base instructions, at least for the extensions we want to ratify at the same time as the Y base, and at least two sentry extensions are on that list, and those need hooks in jalr. Yes?

[Timmmm]

Yes. The branch is currently called codasip but I think it really should be renamed to cheri (I think I originally did that but some people asked me to change it for reasons I've forgotten). Also it's currently quite out of date with respect to upstream, so there's a mega merge/rebase that needs to happen before we can start reorganising the code into separate files per sub-extension. Hopefully that will happen in a few months though (see step 2 in #1).