Use newtypes for register indices and numbers

[nwf]

In preparation for more seriously tackling #523. This PR...

1. Changes the definition of regidx and regno to be newtypes and updates all use sites appropriately.
2. Splits vregidx from regidx (and friends) for Vector (vext) registers, which, AFAIK, are a completely separate set of 32 registers.
3. Splits fregidx from regidx (and friends) for F/D/Zcd/Zcf/Zfa/Zfh and V (again) extensions. There's a little muss and fuss around the definition to do with Zfinx, but otherwise it's also pretty rote.
4. Stops some punning in Zicsr and splits the CSR ast ctor into CSRImm and CSRReg.

This was a slog. Most of the changes can be described as "type-directed" and "mechanical" but were all done... er, artisanally, so some more careful review is probably merited. Perhaps best viewed with word diff, not line diff.

The curious are welcome to look at https://github.com/nwf/sail-riscv/tree/202411-eext to see how I think we can properly support E atop this base, and indeed, most of these changes were motivated or directed by that work, but I would like to get this reviewed independently of that shuffling and further refactoring.

[github-actions]

Test Results

396 tests  ±0   396 ✅ ±0   0s ⏱️ ±0s
  4 suites ±0     0 💤 ±0 
  1 files   ±0     0 ❌ ±0 

Results for commit 000a17c. ± Comparison against base commit 5f4a8e6.

♻️ This comment has been updated with latest results.

[arichardson]

Not reviewed the full diff in detail but overall I think this is a nice improvement!

[Timmmm]

Is there any chance this could be split up into multiple PRs to make it easier to review? E.g. can the "initial support for E" be a separate PR?

[nwf]

I suppose, but GitHub also allows review commit-by-commit and that's as fine a granularity as I think makes sense to split it?

ETA: I thought having the "Initial support for E extension" as part of the stack would help justify the rest of the changes. I'm happy to punt that to a 2nd PR if it'd make getting the first bit in easier.

[jrtc27]

With Zfinx I'm not sure how good an idea this is, it seems to get messy quickly. Also I can't actually see your E support anywhere, the tip of the linked branch is nwf@359fdd3 but that doesn't add E, only factors I out.

[Timmmm]

Yeah I think I'm happy with the motivation! I think splitting it up has other advantages:

• More commits can get merged into main, tested by CI, be part of git bisect etc.
• It's not all or nothing - hopefully we can get some of it merged before all of it is ready, then rebasing etc. is less of a pain if other people are making simultaneous changes.
• Just a bit easier to keep track and less intimidating IMO.

Could you also split out Simplify Zicsr ast? Actually I think we probably shouldn't do that. It is simpler and totally in the spirit of how it is supposed to work, and in isolation definitely good. Unfortunately there are two future spanners in the works:

1. CLIC, which adds all sorts of crazy CSRs that act differently depending on whether you use csrrwi or csrrw.
2. CHERI, which also treats them differently (because csrrwi/c/s can't write metadata). I think it's way more reasonable in CHERI's case. CLIC is just ... lightly thought through.

[nwf]

OK, I've backed this PR back to 000a17c and have raised #645 and #646 with the two other commits to facilitate discussion.

[nwf]

With Zfinx I'm not sure how good an idea this is, it seems to get messy quickly. Also I can't actually see your E support anywhere, the tip of the linked branch is nwf@359fdd3 but that doesn't add E, only factors I out.

Sorry, I missed a git add. #646 has the files added.

As to the complexity around Zfinx and E, well... I don't think the sail is going to be that hairy, and I think the improved clarity in the type system at all use sites outweighs a little complexity at the one definition site.

[arichardson]

I think being explicit here is a nice improvement and it would be good to merge this ASAP so we don't accumulate merge conflicts.

[jrtc27]

I think being explicit here is a nice improvement and it would be good to merge this ASAP so we don't accumulate merge conflicts.

I'm not sold given Zfinx; this PR introduces some ugliness there. By introducing new types for everything it ends up having to use the wrong explicit type when previously they were all the same and so there was no wrong type.

[nwf]

I'm open to suggestions, but the status quo seems somewhat challenging for E support, especially E machines that reuse the resulting voids in the encoding space, without just forking the whole model.

IMHO Zfinx being a model run-time decision is a deliberate type confusion, and it'd have been better for it to be a model compile-time decision, especially since it cannot (AFAICT) be changed after initialization. It's not surprising, then, that it results in some violence to the types. In particular, I think it is acceptable to the specification to have an implementation of E and F and not-Zfinx that has 16 GPRs and 32 FPU registers, which means that regidx and fregidx really ought to be separable newtypes (perhaps of the same underlying type, of course).

Would you, @jrtc27, accept the first commit, or first two commits, in this PR on its own, without the subsequent refinement of (vregidx and) fregidx as a types-as-documentation improvement, even if you disagree with the approach of "statically E with a smaller regidx" that motivated this series of PRs?

[arichardson]

I think being explicit here is a nice improvement and it would be good to merge this ASAP so we don't accumulate merge conflicts.

I'm not sold given Zfinx; this PR introduces some ugliness there. By introducing new types for everything it ends up having to use the wrong explicit type when previously they were all the same and so there was no wrong type.

Can't we solve the zfinx problem by adding an explicit conversion? IMO you're still using a freg index in the instruction, it just happens to be mapped to a for internally?

I also think it's odd this is a runtime option an IMO would be cleaner as compile time.

[nwf]

Can't we solve the zfinx problem by adding an explicit conversion? IMO you're still using a freg index in the instruction, it just happens to be mapped to a for internally?

Yeah, fregidx-en are decoded (encdec_freg) and passed through the model until they get to the Zfinx-aware register accessors, [rw]F_or_X_[FDH](), which use fregidx_to_regidx() if they need something to pass to X().

I also think it's odd this is a runtime option an IMO would be cleaner as compile time.

A future PR, perhaps.

[jrtc27]

I think being explicit here is a nice improvement and it would be good to merge this ASAP so we don't accumulate merge conflicts.

I'm not sold given Zfinx; this PR introduces some ugliness there. By introducing new types for everything it ends up having to use the wrong explicit type when previously they were all the same and so there was no wrong type.

Can't we solve the zfinx problem by adding an explicit conversion? IMO you're still using a freg index in the instruction, it just happens to be mapped to a for internally?

No you're not, you're using an X register, there are no F registers.

I also think it's odd this is a runtime option an IMO would be cleaner as compile time.

The whole intent is to reduce compile-time options and have as much configurable at run time as possible. Having something like Zfinx be compile-time option would completely go against that.

[arichardson]

I think being explicit here is a nice improvement and it would be good to merge this ASAP so we don't accumulate merge conflicts.

I'm not sold given Zfinx; this PR introduces some ugliness there. By introducing new types for everything it ends up having to use the wrong explicit type when previously they were all the same and so there was no wrong type.

Can't we solve the zfinx problem by adding an explicit conversion? IMO you're still using a freg index in the instruction, it just happens to be mapped to a for internally?

No you're not, you're using an X register, there are no F registers.

That's true, but we can still have a type abstraction for "register index of a floating point value"? For RV32 Zdinx we could even assert that it's always an even index when converting it to a GPR index?

I also think it's odd this is a runtime option an IMO would be cleaner as compile time.

The whole intent is to reduce compile-time options and have as much configurable at run time as possible. Having something like Zfinx be compile-time option would completely go against that.

Reading the spec there is no way to dynamically switch this behaviour at runtime since it seems to be gated on the extension being implemented:

In the standard privileged architecture defined in Volume II, the mstatus field FS is hardwired to 0 if the Zfinx extension is implemented, and FS no longer affects the trapping behavior of floating-point instructions or fcsr accesses.

The misa bits F, D, and Q are hardwired to 0 when the Zfinx extension is implemented.

But that point I don't really care about, I just think being explicit about what type of register we are indexing is still useful.

[nwf]

Well, it looks like we now (again) have tons of conflicting files. Is it worth dusting this off for merge or would it just languish again?

[arichardson]

Well, it looks like we now (again) have tons of conflicting files. Is it worth dusting this off for merge or would it just languish again?

I think it would be worthwhile, but I can't guarantee it will be merged :(

[jordancarlin]

Well, it looks like we now (again) have tons of conflicting files. Is it worth dusting this off for merge or would it just languish again?

I think it would be worthwhile, but I can't guarantee it will be merged :(

We will eventually need to support E, and I haven’t seen any other proposals for how to do that, so it sort of seems like something along these lines is necessary. Even without that aspect, the additional type safety seems like a good thing and is a direction the model is generally moving in (see the recent virtual/physical address new types). So I’d be in favor of it. If you’re concerned about doing the work only for it not to get merged, maybe we can hold off and discuss it at the next weekly meeting to see if we can come to some sort of consensus on if we want to go through with this.

[nwf]

To be clear, I am not adamant that this PR merge, and if someone has a better proposal, please, go for it. But the lack of structured support for E has bitten CHERIoT already, in that our currently in-tree "throw an exception on invalid register access" approach is subtly wrong (because the model does not model instructions with transactions and sail's sequential/monadic behavior is such that state effects survive thrown exceptions, so the CHERIoT model can, for example, write to a CSR before trapping on a GPR access) and more proper fixes are unpleasant, holographic, and eternal divergences from the upstream model, such as changing all arms of the en-/de-coding definition to have additional 0 @.