MTVEC legalisation

[mndstrmr]

According to the Sail, MTCC (called mtvec in CherIoT-ibex) must be legalised before it is stored. This means:

1. If the new MTVEC.MODE is not 0 or 1 the old MTVEC.MODE should instead be used: mtvec_d_combi[1]? {mtvec_d_combi[31:2], mtvec_q[1:0]}:mtvec_d_combi
2. The stored capability therefore needs to be set_addressed with the new modified address: full2regcap(set_address(reg2fullcap(cheri_csr_wcap_i, cheri_csr_wdata_i), <corrected address>, 0, 0))
3. MTVEC should have its tag cleared if it is sealed

None of these are currently done in CherIoT-ibex.

Note: Some legalisation is made in cheri_ex which I think is correct for MEPCC, but not for MTVEC. I think it might have been me who suggested one could just mask away a bit of MTVEC/MTCC but I don't think that I was correct.

[kliuMsft]

Good catch - will add to RTL. I would probably fix it in cheri_ex (where the main EX and set_address logic resides). I believe the current_address in this case would be {mvtec_d_combi[31:2], 2'b00}?

[rmn30]

It would certainly simplify things if we don't support vectored mode and we don't need it for cheriot-rtos because the first thing we do for every interrupt or exception is save some register context, which can be shared between different causes.

[rmn30]

However by clearing the bits you might make the capability unrepresentable so would need to check that.

[kliuMsft]

Ok this is indeed more painful than I first thought.. Say we allow 2'b00 and 2'b01 in the address LSB bits, now we need to decide which one we legalize the cap to, and I don't see either way quite works. 2'b00 makes sense since that's the vector address we actually will use. However if we allow reading back 2'b01 (which we should), then we have a problem. Maybe we could solve it by legalizing on readback, but it has to be pain to use since the address won't be aligned.

For now I can probably just force it to use direct mode in CHERIoT mode, so the actual vector address will match the 32-bit address value read from SCR. Any better suggestions?

[kliuMsft]

RTL changes made in commit ba458ab.

[rmn30]

So if we write a cap to MTCC with address[0]==1 and read it back then address[0] will be unset? This could be a monotonicity violation because if we write a cap with base==address and address[0]==1 then clearing the bottom bit will take the address out of representable range. The simplest solution would be to clear the tag if MTCC is written with 'address[1:0]!=0'.

[kliuMsft]

What RTL is doing now is to force the address[1:0] to be 2'b00 and do a set_address check on the new address. So LSB will readback as 2'b00 too. RTL is not clearing tag if the new address is out of bounds on writing MTCC, however if MTCC becomes PCC then the if_stage will compare fetch address with bounds.

[rmn30]

do a set_address check on the new address

What does this do? Does it clear the tag if the new address is oob / not representable?

RTL is not clearing tag if the new address is out of bounds on writing MTCC

It sounds like this would allow any code running with the access_system_registers permission to violate capability monotonicity by writing MTCC and then reading it back with a different address? This isn't such a big deal as only a very limited amount of very trusted code has that permission but it would be nice to avoid having this caveat to the global ISA invariant.

[mndstrmr]

Just been revisiting this. In cheri_ex.sv, when running a MTCC/MEPCC CSR write the adjusted address is not actually being output in csr_wdata_o which instead still receives rf_rdata_a. Setting csr_wdata_o = set_address_comb.taddr1 seems to fix things.

I need to run the full checks, but otherwise the fix looks to be correct and at least maintains the necessary invariants.

[mndstrmr]

The Sail should also be updated to reflect that only direct mode is supported, specifically in legalize_tvec in riscv_sys_regs.sail, TV_Vector should be removed as a supported mode.

[kliuMsft]

Per cheriot sail PR #37, mtvec legalization is simplified (tag removal when checks fail) and we now only allow mtvec[1:0] == 2'b00 in cheriot mode. RTL commit d95804c incorporated this change.

[mndstrmr]

Thanks, and apologies for the (admittedly quite long) delay (again).

The fix is mostly correct, but in the case that the address is changing the top_cor and base_cor bits need updating.

With that fix the successful case for CSpecialRW verifies.

[kliuMsft]

No problem - thanks for picking this up.

This is interesting - I guess we are changing the address[1:0] bits, assuming the source cap has its address[1:0] != 00. So technically we should recompute the correction values, even if the tags is cleared? I didn't do that since I was under the impression that this is a don't care.. @rmn30, does sail update the corrections in this case?

[mndstrmr]

Even if the tag is cleared (meaning there are no implications for memory operations) a CGetBase or CGetTop instruction will still give the wrong result. They are not specified to only be meaningful if the tag is set.

[kliuMsft]

True, I should be asking whether it's really necessary to force mtvec's address[1:0] to 00 in this case, since otherwise there is no need to recompute the corrections.

[kliuMsft]

I have updated RTL to match sail behavior (commit 863f9dc).

[mndstrmr]

This proves, thanks!