Sealed PCC instruction fetch

[mndstrmr]

According to the Sail, instruction fetch is to fail if the PCC is sealed:

val ext_fetch_check_pc : (xlenbits, xlenbits) -> Ext_FetchAddr_Check(ext_fetch_addr_error)
function ext_fetch_check_pc(start_pc, pc) = {
  if   start_pc == pc
  then {
    // ...
    if isCapSealed(PCC)
    then    Ext_FetchAddr_Error(CapEx_SealViolation)
    // ...
    else    Ext_FetchAddr_OK(pc)
  } else {
    // ...
  }
}

This is not done in CherIoT-ibex. Specifically the term is_cap_sealed(pcc_fullcap_i) should be included in the set of error cases for cheri_acc_vio in the IF stage.

[kliuMsft]

ok - I will add this check. Thanks.

[rmn30]

This does beg the question of how it is possible to end up with a sealed PCC? cj[al]r should trap if the destination is sealed with a non-sentry type so that leaves only two possibilities:

1. mret after installing a sealed mepcc
2. exception or interrupt with a sealed mtcc

The ISA says that writing a sealed capability to either of these SCRs should clear the tag bit because they both contain WARL bits (mepc[0] and mtvec[1:0]) that would need to be cleared, which could violate the immutability of sealed capabilities. Therefore the check on instruction fetch is probably redundant -- I left it in as a precaution.

[mndstrmr]

You are correct, it was the mret from mepcc case. The legalisation check is done incorrectly in CherIoT-ibex: Specifically the tag of MEPCC was not being cleared when the writing capability was sealed at it is in the Sail.

We didn't spot that because we were treating MEPCC writes differently to other CSR writes due to MEPCC being legalised on load instead of store in the Sail. We were planning on coming back to it but I guess this issue found it first.

[kliuMsft]

Checking for sealed PCC is added to RTL in commit ba458ab.

[rmn30]

What happens if you write a sealed capability to MEPCC and then read it back? What if you do this with address[0]=1?

[kliuMsft]

@rmn30 Right now we are not doing anything special for sealed caps when writing to mepcc or mtcc. So the write will go through and the resulting SCR would remain sealed but adjusted to an aligned address. What would be the desired behavior?

[kliuMsft]

See comments in #10. we now explicitly clear tag of mepcc at cpecialw time if either execution permission is cleared or sealed.

[mndstrmr]

Seems correct, thanks.