diff --git a/src/cheri_cap_common.sail b/src/cheri_cap_common.sail index 2484800..8f8d00b 100644 --- a/src/cheri_cap_common.sail +++ b/src/cheri_cap_common.sail @@ -614,16 +614,27 @@ function isCapForwardControlSentry(cap) = } /*! - * Returns true if the given capability has one of the backward sentry otypes, otherwise false. + * Returns true if the given capability has one of the IRQ-setting backward sentry otypes, otherwise false. */ -val isCapBackwardSentry : Capability -> bool -function isCapBackwardSentry(cap) = +val isCapBackwardNoninheritingSentry : Capability -> bool +function isCapBackwardNoninheritingSentry(cap) = match unsigned(cap.otype) { otype if otype == otype_sentry_bid => true, otype if otype == otype_sentry_bie => true, _ => false } +/*! + * Returns true iff the given capability is an IRQ-inheriting backward sentry. + */ +val isCapBackwardInheritingSentry : Capability -> bool +function isCapBackwardInheritingSentry(cap) = + match unsigned(cap.otype) { + otype if otype == otype_sentry_b => true, + _ => false + } + + /*! * Returns true if the given capability has one of the forward interrupt-inherited sentry otype, otherwise false. */ diff --git a/src/cheri_insts.sail b/src/cheri_insts.sail index 79a8053..fbeadf3 100644 --- a/src/cheri_insts.sail +++ b/src/cheri_insts.sail @@ -122,8 +122,8 @@ function clause execute(CJAL(imm, cd)) = { let sentry_type = if mstatus.MIE() == 0b1 then otype_sentry_bie else otype_sentry_bid; C(cd) = sealCap(linkCap, to_bits(cap_otype_width, sentry_type)); } else { - /* Generate an unsealed return capability. */ - C(cd) = linkCap; + /* Generate an IRQ-inheriting return capability. */ + C(cd) = sealCap(linkCap, to_bits(cap_otype_width, otype_sentry_b)); }; nextPC = newPC; @@ -168,8 +168,11 @@ function clause execute(CJALR(imm, cs1, cd)) = { 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))) | + not ((cd == zreg & cs1 == ra & isCapBackwardNoninheritingSentry(cs1_val)) | + (cd == zreg & cs1 != ra & + (not(isCapSealed(cs1_val)) | + isCapBackwardInheritingSentry(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); @@ -195,9 +198,10 @@ function clause execute(CJALR(imm, cs1, cd)) = { } else { /* * Generate an unsealed return capability. From the conditions above, it - * must be the case that cs1 is unsealed or a forward inheriting sentry. + * must be the case that cs1 is unsealed or an inheriting sentry (either + * forward or backward). */ - C(cd) = linkCap; + C(cd) = sealCap(linkCap, to_bits(cap_otype_width, otype_sentry_b)); }; nextPC = newPC; diff --git a/src/cheri_types.sail b/src/cheri_types.sail index f1cb81d..906df7a 100644 --- a/src/cheri_types.sail +++ b/src/cheri_types.sail @@ -66,6 +66,7 @@ let otype_sentry_id = 2 /* sentry disabling interrupts */ let otype_sentry_ie = 3 /* sentry enabling interrupts */ let otype_sentry_bid = 4 /* backward sentry disabling interrupts */ let otype_sentry_bie = 5 /* backward sentry enabling interrupts */ +let otype_sentry_b = 6 /* backward sentry inheriting */ enum CPtrCmpOp = { CEQ,