mstatus cleanup

[radimkrcmar]

This series started by noticing that we use SXL in RV32 mode, which results in very ugly accessors for mstatus. The code around mstatus can be improved by changing the architecture (XLEN) detection.

There is (should be) no functional change.

[arichardson]

Thanks for this change, I haven't had a detailed look at it yet but it seems some of the changes conflict with https://github.com/riscv/sail-riscv/pull/652/files which will most likely be merged soon.

@Timmmm could you take a look and see which one is better or if we want both changes?

[radimkrcmar]

The pull request also expands the status to bits(64) and explicitly copies the fields, so I can drop 4 patches. I will rebase when it lands and add 2 patches to clean up its handling of SXL/UXL and SD.

[radimkrcmar]

I rebased on top of #652 and noticed a bug in it, so this isn't just a cleanup anymore, but introduces a software observable change.

[Timmmm]

Ah what's the bug? Can we fix that quickly in another PR?

[radimkrcmar]

The patch fixing it is dc3e3c0. In short, mstatush contains 0b01 in SXL and UXL fields instead of required 0b00.

To fix it quickly, we could replace the SXL/UXL bits with zeros in mstatush accessors, but I don't think we have to rush, because software should ignore those WPRI bits.

[jrtc27]

They're also supposed to be 0 if the corresponding privilege mode isn't implemented

[radimkrcmar]

They're also supposed to be 0 if the corresponding privilege mode isn't implemented

Good point. I didn't really want to change any software-visible behavior in this PR, so I'll add the extensionEnabled in another PR.

[radimkrcmar]

I noticed that I didn't commit my last change, so the reset patch was only correct if mstatus was pre-initialized with zeros... It makes no difference, because we have to zero WPRI, but it's still not a good practice.
The force push just removes the last patch, because it would conflict with the reset PR (#597) anyway.

[github-actions]

Test Results

392 tests  ±0   392 ✅ ±0   1m 19s ⏱️ -1s
  1 suites ±0     0 💤 ±0 
  1 files   ±0     0 ❌ ±0 

Results for commit 27f6296. ± Comparison against base commit 8ca0ac0.

♻️ This comment has been updated with latest results.

[Timmmm]

LGTM but I think this could be split into several basically independent PRs which would make it a lot easier to review (and give us nicer history). E.g.

PR 1:
sys_regs: rename cur_Architecture to cur_architecture
types: simplify architecture return type
types: turn architecture into a mapping

PR 2:
insts_base: ignore architecture in SFENCE_VMA

PR 3:
sys_regs: fix RV32 detection in cur_architecture
sys_regs: remove SXL and UXL accessors

PR 4:
sys_regs: compute mstatus and sstatus SD bit on CSR read

PR 5 (these could also be separate PRs but that's probably overkill):
sys_regs: fix SXL and UXL fields in RV32 mstatush
sys_regs: legalize UXL and SXL mstatus fields

Sorry I know it's a bit of a pain! Especially because Github doesn't really support the stacked patch development workflow...

I'll hold off on #597 until all these are merged.

[radimkrcmar]

LGTM but I think this could be split into several basically independent PRs which would make it a lot easier to review (and give us nicer history). E.g.

Will do, although history will be the same. Please don't tell me you want to squash all the patches. :)

Sorry I know it's a bit of a pain! Especially because Github doesn't really support the stacked patch development workflow...

No worries, this will be quick and easy compared to all the reshuffling I already did.

Especially because Github doesn't really support the stacked patch development workflow...

I think Github supports it (Git alone does), both rebase and merge-commit PR resolution should get you the desired result if you merge the PRs in order.

I'll hold off on #597 until all these are merged.

I would actually prefer to have that one merged first.
It will allow me to end up with cleaner code and more other PRs can depend on it.

[arichardson]

LGTM but I think this could be split into several basically independent PRs which would make it a lot easier to review (and give us nicer history). E.g.

Will do, although history will be the same. Please don't tell me you want to squash all the patches. :)

I agree that in cases where the history is nice and clean we should use rebase or merge instead of squash

[Timmmm]

Please don't tell me you want to squash all the patches. :)

Nope!

I think Github supports it (Git alone does), both rebase and merge-commit PR resolution should get you the desired result if you merge the PRs in order.

Yeah I mean it doesn't really have a concept of saying "this PR depends on this other PR, so don't show that one". Apparently some source hosting systems do support that (Gerrit maybe?)

I would actually prefer to have that one merged first.

Ok! I'll fix the initial SXL/UXL for RV32 in that one at least.

[radimkrcmar]

Yeah I mean it doesn't really have a concept of saying "this PR depends on this other PR, so don't show that one". Apparently some source hosting systems do support that (Gerrit maybe?)

Right, Github just compares the two branches. We would have to work around that by using a range on commits, e.g. https://github.com/riscv/sail-riscv/pull/683/files/cf121a0..ddd0c7f

[radimkrcmar]

I tried to remove the assert(xlen >= 64) in the RV64 match, but Sail didn't compile with this hunk, nor with

let arch = if xlen >= 64 then architecture(mstatus[SXL]) else RV32;

Type error:
riscv_vmem.sail:187.24-28:
187 |        Mk_Satp64(satp)[Mode]
    |                        ^--^
    | Identifier Mode is unbound
    | 
    | Caused by riscv_vmem.sail:187.18-22:
    | 187 |        Mk_Satp64(satp)[Mode]
    |     |                  ^--^ checking function argument has type bitvector(64)
    |     | Failed to prove constraint: 32 == 64

Am I missing some better way to provide this constraint?

Thanks.

[Timmmm]

Does it work if you change it to if xlen < 64 then RV32 else ...?

[Timmmm]

Oh wait I can't read... Never mind.

[Alasdair]

The constraints mostly flow lexically, i.e. from the condition in the if down into the branches. The type-checker isn't smart enough to understand that arch == RV64 implies that branch in a previous if was taken, it's a bit too indirect.

You can use an assert that's always true at runtime just to assert a fact to the type system. Sometimes it's better to do that than to try to re-write the logic.