Skip to content

Commit

Permalink
Move CHERI PTE traps to their own vectors
Browse files Browse the repository at this point in the history 
Rather than riding through the generic 0x1C vector.  This removes
CapEx_CapLoadGen and CapEx_MMUNoStoreCap
  • Loading branch information
@nwf
nwf committed Jun 17, 2020
1 parent 554eb6f commit 5cea27f
Show file tree
Hide file tree
Showing 3 changed files with 54 additions and 28 deletions.
24 changes: 13 additions & 11 deletions src/cheri_insts.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -900,7 +900,7 @@ function clause execute (CLoadCap(rd, cs, is_unsigned, width)) =

union load_cap_ptw_ext_result = {
LCPE_OK : Capability,
LCPE_Exn : CapEx
LCPE_Exn : ExceptionType
}

val handle_load_cap_ptw_ext : (Capability, bool, ext_ptw_lcm) -> load_cap_ptw_ext_result
Expand All @@ -910,7 +910,7 @@ function handle_load_cap_ptw_ext (v, vialc, ptw_info) =
else match ptw_info {
PTW_LCM_OK => LCPE_OK({v with tag = v.tag & vialc}),
PTW_LCM_CLR => LCPE_OK({v with tag = false}),
PTW_LCM_TRAP => LCPE_Exn(CapEx_CapLoadGen)
PTW_LCM_TRAP => LCPE_Exn(E_Extension(EXC_CHERI_MMU_LOAD_CAP))
}

val handle_load_cap_via_cap : (regidx, capreg_idx, Capability, xlenbits) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
Expand Down Expand Up @@ -941,14 +941,15 @@ function handle_load_cap_via_cap(rd, cs, cap_val, vaddrBits) = {

if ~(load_cap_data_dep_trap) & vialc & lcav == PTW_LCM_TRAP then {
/* If we're not permitted to do tag-dependent traps, trap now */
handle_cheri_cap_exception(CapEx_CapLoadGen, cs); RETIRE_FAIL
handle_mem_exception(vaddrBits, E_Extension(EXC_CHERI_MMU_LOAD_CAP));
RETIRE_FAIL
} else {
let c = mem_read_cap(addr, aq, rl, false);
match c {
MemValue(v) => {
match handle_load_cap_ptw_ext(v, vialc, lcav) {
LCPE_OK(v') => { writeCapReg(rd, v'); RETIRE_SUCCESS },
LCPE_Exn(e) => { handle_cheri_cap_exception(e, cs); RETIRE_FAIL }
LCPE_Exn(e) => { handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
}
},
MemException(e) => {handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
Expand Down Expand Up @@ -1046,14 +1047,15 @@ if not(cap_val.tag) then {

if ~(load_cap_data_dep_trap) & vialc & lcav == PTW_LCM_TRAP then {
/* If we're not permitted to do tag-dependent traps, trap now */
handle_cheri_cap_exception(CapEx_CapLoadGen, cs); RETIRE_FAIL
handle_mem_exception(vaddrBits, E_Extension(EXC_CHERI_MMU_LOAD_CAP));
RETIRE_FAIL
} else {
let c = mem_read_cap(addr, aq, rl, false);
match c {
MemValue(v) => {
match handle_load_cap_ptw_ext(v, vialc, lcav) {
LCPE_OK(v') => { load_reservation(addr); writeCapReg(cd, v'); RETIRE_SUCCESS },
LCPE_Exn(e) => { handle_cheri_cap_exception(e, cs); RETIRE_FAIL }
LCPE_Exn(e) => { handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
}
},
MemException(e) => {handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
Expand Down Expand Up @@ -1204,16 +1206,16 @@ function handle_store_cap_via_cap(rs, cs, cap_val, vaddrBits) = {
handle_mem_exception(vaddrBits, E_SAMO_Addr_Align());
RETIRE_FAIL
} else match translateAddr(vaddrBits, Write(if rs_val.tag then Cap else Data)) {
TR_Failure(E_Extension(EXC_CHERI_VMEM_STORE_CAP), _) => {
handle_cheri_cap_exception(CapEx_MMUNoStoreCap, cs);
TR_Failure(E_Extension(EXC_CHERI_MMU_STORE_CAP), _) => {
handle_mem_exception(vaddrBits, E_Extension(EXC_CHERI_MMU_STORE_CAP));
RETIRE_FAIL
},
TR_Failure(E_Extension(_), _) => { internal_error("unexpected cheri exception for cap store") },
TR_Failure(e, _) => { handle_mem_exception(vaddrBits, e); RETIRE_FAIL },
TR_Address(addr, caveats) => {
match (caveats.ptw_sc_mod, rs_val.tag) {
(PTW_SCM_TRAP, true) => {
handle_cheri_cap_exception(CapEx_MMUNoStoreCap, cs);
handle_mem_exception(vaddrBits, E_Extension(EXC_CHERI_MMU_STORE_CAP));
RETIRE_FAIL
},
_ => {
Expand Down Expand Up @@ -1361,15 +1363,15 @@ function handle_store_cond_cap_via_cap(cs2, cs, cap_val, vaddrBits) = {
} else {
match translateAddr(vaddrBits, Write(if cs2_val.tag then Cap else Data)) {
TR_Failure(E_Extension(EXC_CHERI_VMEM_STORE_CAP), _) => {
handle_cheri_cap_exception(CapEx_MMUNoStoreCap, cs);
handle_mem_exception(vaddrBits, E_Extension(EXC_CHERI_MMU_STORE_CAP));
RETIRE_FAIL
},
TR_Failure(E_Extension(_), _) => { internal_error("unexpected cheri exception for cap store") },
TR_Failure(e, _) => { handle_mem_exception(vaddrBits, e); RETIRE_FAIL },
TR_Address(addr, caveats) => {
match (caveats.ptw_sc_mod, cs2_val.tag) {
(PTW_SCM_TRAP, true) => {
handle_cheri_cap_exception(CapEx_MMUNoStoreCap, cs);
handle_mem_exception(vaddrBits, E_Extension(EXC_CHERI_MMU_STORE_CAP));
RETIRE_FAIL
},
_ => {
Expand Down
45 changes: 37 additions & 8 deletions src/cheri_riscv_types.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,28 +61,57 @@ let init_ext_ptw : ext_ptw = struct {
ptw_sc_mod = PTW_SCM_OK
}

/* Address translation errors */
enum ext_ptw_error = {AT_LOAD_CAP_ERR, AT_STORE_CAP_ERR}
/*
* Address translation errors
*
* For CHERI, these are defined but not used at present: our PTE extensions
* are defined here in a data-dependent way. In some eventuality, perhaps
* we'll have this kind of data-independence as well, so it doesn't hurt to
* keep the symbols around.
*/
enum ext_ptw_error = {
AT_LOAD_CAP_ERR,
AT_STORE_CAP_ERR
}

/* CHERI exception extensions */

enum ext_exc_type = {EXC_CHERI, EXC_CHERI_VMEM_LOAD_CAP, EXC_CHERI_VMEM_STORE_CAP}
enum ext_exc_type = {
EXC_CHERI,
EXC_CHERI_MMU_LOAD_CAP,
EXC_CHERI_MMU_STORE_CAP
}

/* CHERI translation of PTW errors into exception annotations */
function ext_translate_exception(e : ext_ptw_error) -> ext_exc_type =
match e {
AT_LOAD_CAP_ERR => EXC_CHERI_VMEM_LOAD_CAP,
AT_STORE_CAP_ERR => EXC_CHERI_VMEM_STORE_CAP
AT_LOAD_CAP_ERR => EXC_CHERI_MMU_LOAD_CAP,
AT_STORE_CAP_ERR => EXC_CHERI_MMU_STORE_CAP
}

/* CHERI conversion of extension exceptions to bits */
val ext_exc_type_to_bits : ext_exc_type -> exc_code
function ext_exc_type_to_bits(e) = 0x1C
function ext_exc_type_to_bits(e) =
match e {
EXC_CHERI_MMU_LOAD_CAP => 0x1A,
EXC_CHERI_MMU_STORE_CAP => 0x1B,
_ => 0x1C
}

/* CHERI conversion of extension exceptions to integers */
val num_of_ext_exc_type : ext_exc_type -> {'n, (0 <= 'n < xlen). int('n)}
function num_of_ext_exc_type(e) = 28
function num_of_ext_exc_type(e) =
match e {
EXC_CHERI_MMU_LOAD_CAP => 26,
EXC_CHERI_MMU_STORE_CAP => 27,
_ => 28
}

/* CHERI conversion of extension exceptions to strings */
val ext_exc_type_to_str : ext_exc_type -> string
function ext_exc_type_to_str(e) = "cheri-exception"
function ext_exc_type_to_str(e) =
match e {
EXC_CHERI_MMU_LOAD_CAP => "cheri-mmu-cap-load",
EXC_CHERI_MMU_STORE_CAP => "cheri-mmu-cap-store",
_ => "cheri-exception"
}
13 changes: 4 additions & 9 deletions src/cheri_types.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,6 @@ enum CapEx = {
CapEx_ReturnTrap,
CapEx_TSSUnderFlow,
CapEx_UserDefViolation,
CapEx_MMUNoStoreCap,
CapEx_InexactBounds,
CapEx_UnalignedBase,
CapEx_GlobalViolation,
Expand All @@ -79,8 +78,7 @@ enum CapEx = {
CapEx_PermitCCallViolation,
CapEx_AccessCCallIDCViolation,
CapEx_PermitUnsealViolation,
CapEx_PermitSetCIDViolation,
CapEx_CapLoadGen
CapEx_PermitSetCIDViolation
}

function CapExCode(ex) : CapEx -> bits(5) =
Expand All @@ -94,7 +92,7 @@ function CapExCode(ex) : CapEx -> bits(5) =
CapEx_ReturnTrap => 0b00110,
CapEx_TSSUnderFlow => 0b00111,
CapEx_UserDefViolation => 0b01000,
CapEx_MMUNoStoreCap => 0b01001,
/* 0b01001 unused; was CapEx_MMUNoStoreCap */
CapEx_InexactBounds => 0b01010,
CapEx_UnalignedBase => 0b01011,
CapEx_GlobalViolation => 0b10000,
Expand All @@ -109,8 +107,7 @@ function CapExCode(ex) : CapEx -> bits(5) =
CapEx_PermitCCallViolation => 0b11001,
CapEx_AccessCCallIDCViolation => 0b11010,
CapEx_PermitUnsealViolation => 0b11011,
CapEx_PermitSetCIDViolation => 0b11100,
CapEx_CapLoadGen => 0b11101
CapEx_PermitSetCIDViolation => 0b11100
}

function string_of_capex (ex) : CapEx -> string =
Expand All @@ -124,7 +121,6 @@ function string_of_capex (ex) : CapEx -> string =
CapEx_ReturnTrap => "ReturnTrap" ,
CapEx_TSSUnderFlow => "TSSUnderFlow" ,
CapEx_UserDefViolation => "UserDefViolation" ,
CapEx_MMUNoStoreCap => "MMUNoStoreCap" ,
CapEx_InexactBounds => "InexactBounds" ,
CapEx_UnalignedBase => "UnalignedBounds" ,
CapEx_GlobalViolation => "GlobalViolation" ,
Expand All @@ -139,8 +135,7 @@ function string_of_capex (ex) : CapEx -> string =
CapEx_PermitCCallViolation => "PermitCCallViolation" ,
CapEx_AccessCCallIDCViolation => "AccessCCallIDCViolation" ,
CapEx_PermitUnsealViolation => "PermitUnsealViolation" ,
CapEx_PermitSetCIDViolation => "PermitSetCIDViolation" ,
CapEx_CapLoadGen => "CapLoadGen"
CapEx_PermitSetCIDViolation => "PermitSetCIDViolation"
}

type capreg_idx = bits(6)
Expand Down

0 comments on commit 5cea27f

Please sign in to comment.