Closed mndstrmr closed 11 months ago
Since the PCC address is not stored anywhere (note that this is not the same as PC)
Can you clarify that? This has traditionally been true on all CHERI systems and I'm not sure how we changed that.
Sure.
Looking at the Sail for CJALR (for example) we see that nextPC and nextPCC are updated separately.
cs1_val.address + off
cs1_val
Looking at the step
function in the Sail, nextPCC.address
is not later updated to the PC - instead in tick_pc
, PCC
becomes nextPCC
and PC
becomes nextPC
.
To me this is neat, since it leaves no questions about the bounds of the PCC
- they stay the same until an exception or a CJALR
- there is no need to test for representability.
As for not needing to remember PCC.address
, the Sail only keeps it around to decompress the bounds again - but in CherIoT-ibex you already have the decompressed bounds stored, so you don't need to remember PCC.address
.
@mndstrmr You are absolutely right that top_cor/base_cor == 0 can't be right all the time. However in this case (pcc_full_cap), top_cor and base_cor are actually never used (since we really only need the expanded top/base and exp to convert between pcc and reg_cap).
The reason I still want a separate structure type for pcc_cap is really try to save a few flops (which may not work out too well) and not having to worry about keeping the cor values consistent all the time. The conversion to/from full_cap is still causing too much confusion though, so likely going to have to clean it up further.
Ah, you are totally right - I should have spotted that. Turns out a check we had in place was a bit too strong. Relaxing it works and everything still proves.
Thanks!
Currently the PCC is stored as a
pcc_cap_t
in the CSR block. This means it does not have cached top_cor and base_cor. When the PCC is converted to afull_cap_t
, instead of computingtop_cor
andbase_cor
thepcc2fullcap
function currently just sets them both to zero.Forgive me if I am wrong, but that seems like it cannot be right.
Since the PCC address is not stored anywhere (note that this is not the same as PC), the
top_cor
andbase_cor
fields (as well astop33
andbase32
) must instead be stored with the PCC. The stored PCC could therefore be afull_cap_t
andpcc_cap_t
could be removed from CherIoT-ibex altogether.