CJALR otype decompression

[mndstrmr]

The Sail has this large condition for CJALR:

if not (cs1_val.tag) then {
  handle_cheri_reg_exception(CapEx_TagViolation, cs1);
  RETIRE_FAIL
} else if (isCapSealed(cs1_val) & imm != zeros()) |
          not ((cd == zreg & cs1 == ra & isCapBackwardSentry(cs1_val)) |
               (cd == zreg & cs1 != ra & (not(isCapSealed(cs1_val)) | isCapForwardInheritSentry(cs1_val))) |
               (cd != zreg & (not(isCapSealed(cs1_val)) | isCapForwardInheritSentry(cs1_val))) |
               (cd == ra & (not(isCapSealed(cs1_val)) | isCapForwardSentry(cs1_val)))) then {
  handle_cheri_reg_exception(CapEx_SealViolation, cs1);
  RETIRE_FAIL
} else if not (cs1_val.permit_execute) then {

These otype checks (e.g. isCapForwardSentry) compare the otype of a Sail Capability with some constants. Sail stores the otype of a Capability in its decompressed (4 bit) form.

In cheriot-ibex the same constants are used to do a comparison on the compressed (3 bit) form:

cs1_otype_0  =  (rf_fullcap_a.otype == 3'h0);
cs1_otype_1  =  (rf_fullcap_a.otype == 3'h1);
cs1_otype_45 = (rf_fullcap_a.otype == 3'h4) || (rf_fullcap_a.otype == 3'h5);
cs1_otype_23 = (rf_fullcap_a.otype == 3'h2) || (rf_fullcap_a.otype == 3'h3);

This leads to an issue where if the capability is not executable and sealed, none of the above should match (but will) since its otype is instead {1'b1, rf_fullcap_a.otype}, since the decompression scheme for otypes is the following:

let otype = (if isExe | c.cotype == 0b000 then 0b0 else 0b1) @ c.cotype;

Changing cheriot-ibex to first decompress the otype fixes the issue. Since the capability is not executable we will fail the next check anyway, so there is no security issue (the CJALR will fail if it should and not if it shouldn't, it just may report different reasons - i.e. a different mtval).

[rmn30]

That certainly sounds like a bug but will await confirmation from @kliuMsft . Good find!

[marnovandermaas]

Looks like it's an exception priority issue, so not a huge problem but definitely nice to fix to match with the Sail definition.

[kliuMsft]

This is indeed an exception priority issue (bug causing MTVAL to be encoded as permission violation instead of seal violation). Commit cf1a0f7 should fix issue, please verify. Thanks!

[mndstrmr]

Fix is correct, thanks.