Skip to content

Commit

Permalink
Introduce capability load generation traps
Browse files Browse the repository at this point in the history
  • Loading branch information
@nwf
nwf committed May 15, 2020
1 parent 7a308ef commit d14889f
Show file tree
Hide file tree
Showing 5 changed files with 100 additions and 40 deletions.
33 changes: 19 additions & 14 deletions src/cheri_insts.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -882,6 +882,17 @@ function clause execute (CLoadCap(rd, cs, is_unsigned, width)) =
handle_load_data_via_cap(rd, 0b0 @ cs, cap_val, vaddr, is_unsigned, width)
}

val handle_load_cap_ptw_ext : (Capability, bool, ext_ptw) -> option(Capability)
function handle_load_cap_ptw_ext (v, vialc, ptw_info) =
if v.tag == false
then Some(v)
else match ptw_info {
PTW_CAP_OK => Some({v with tag = v.tag & vialc}),
PTW_LOAD_CAP_CLR => Some({v with tag = false}),
PTW_LOAD_CAP_TRAP => None(),
PTW_STORE_CAP_ERR => internal_error("PTW store fault on load path")
}

val handle_load_cap_via_cap : (regidx, capreg_idx, Capability, xlenbits) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
function handle_load_cap_via_cap(rd, cs, cap_val, vaddrBits) = {
let aq : bool = false;
Expand All @@ -908,11 +919,10 @@ function handle_load_cap_via_cap(rd, cs, cap_val, vaddrBits) = {
let c = mem_read_cap(addr, aq, rl, false);
match c {
MemValue(v) => {
let cr = if ptw_info == PTW_LOAD_CAP_ERR
then {v with tag = false} /* strip the tag */
else {v with tag = v.tag & cap_val.permit_load_cap};
writeCapReg(rd, cr);
RETIRE_SUCCESS
match handle_load_cap_ptw_ext(v, cap_val.permit_load_cap, ptw_info) {
Some(v') => { writeCapReg(rd, v'); RETIRE_SUCCESS },
None() => { handle_cheri_cap_exception(CapEx_CapLoadGen, cs); RETIRE_FAIL }
}
},
MemException(e) => {handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
}
Expand Down Expand Up @@ -1006,15 +1016,10 @@ if not(cap_val.tag) then {
let c = mem_read_cap(addr, aq, rl, false);
match c {
MemValue(v) => {
let cr = if ptw_info == PTW_LOAD_CAP_ERR
then {v with tag = false} /* strip the tag */
else {
/* the Sail model currently reserves virtual addresses */
load_reservation(addr);
{v with tag = v.tag & cap_val.permit_load_cap}
};
writeCapReg(cd, cr);
RETIRE_SUCCESS
match handle_load_cap_ptw_ext(v, cap_val.permit_load_cap, ptw_info) {
Some(v') => { load_reservation(addr); writeCapReg(cd, v'); RETIRE_SUCCESS },
None() => { handle_cheri_cap_exception(CapEx_CapLoadGen, cs); RETIRE_FAIL }
}
},
MemException(e) => {handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
}
Expand Down
58 changes: 45 additions & 13 deletions src/cheri_pte.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,12 +15,29 @@ bitfield PTE_Bits : pteAttribs = {

/* Reserved PTE bits could be used by extensions on RV64. There are
* no such available bits on RV32, so these bits will be zeros on RV32.
*
* XXX Because these bits are 0 on RV32, do we want to use inverted polarity,
* so that 0 is the *enabled* form?
*
* The intended semantics for LoadCap* are:
*
* LC LC_Mod LC_CLG Action
* 0 0 0 Capability loads always strip tags
* 0 [other values] [Reserved]
*
* 1 0 0 Capability loads always succeed without tag stripping
* 1 0 1 Capability loads always trap
* 1 1 G Capability loads trap if G mismatches sccsr.gclg[su],
* where the compared bit is keyed off of this PTE's U.
*
*/
type extPte = bits(10)

bitfield Ext_PTE_Bits : extPte = {
LoadCap : 9,
StoreCap : 8,
LoadCap_Mod : 7,
LoadCap_CLG : 6,
}

function isPTEPtr(p : pteAttribs, ext : extPte) -> bool = {
Expand All @@ -41,6 +58,26 @@ union PTE_Check = {
function to_pte_check(b : bool) -> (bool, pte_check) =
(b, PTE_CAP_OK)

/*
* Assuming we're allowed to load from this page, modulate our cap response
*/
val checkPTEPermission_LC : (PTE_Bits, Ext_PTE_Bits) -> pte_check effect {rreg}
function checkPTEPermission_LC(p, e) =
if e.LoadCap() == 0b0
then PTE_LOAD_CAP_CLR
else if e.LoadCap_Mod() == 0b0
then { /* With LoadCap_Mod off, CLG modulates the behavior directly */
if e.LoadCap_CLG() == 0b0
then PTE_CAP_OK
else PTE_LOAD_CAP_TRAP
}
else { /* With LoadCap_Mod on, use CLG as such */
let gclg : bits(1) = if p.U() == 0b1 then sccsr.gclgu() else sccsr.gclgs();
if e.LoadCap_CLG() == gclg
then PTE_CAP_OK
else PTE_LOAD_CAP_TRAP
}

function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits, ext : extPte, ext_ptw : ext_ptw) -> PTE_Check = {
let (succ, pte_chk) : (bool, pte_check) =
match (ac, priv) {
Expand All @@ -58,12 +95,7 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
if p.U() == 0b1 & p.R() == 0b1
then {
let e = Mk_Ext_PTE_Bits(ext);
if e.LoadCap() == 0b1
then (true, PTE_CAP_OK)
else {
/* Allow the address translation to proceed, but mark for tag stripping */
(true, PTE_LOAD_CAP_ERR)
}
(true, checkPTEPermission_LC(p, e))
}
else (false, PTE_CAP_OK)
},
Expand All @@ -84,23 +116,22 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
(ReadWrite(Cap), User) => { if p.U() == 0b1 & p.R() == 0b1 & p.W() == 0b1
then {
let e = Mk_Ext_PTE_Bits(ext);
if e.StoreCap() == 0b1 & e.LoadCap() == 0b1
let lcm = checkPTEPermission_LC(p, e);
if e.StoreCap() == 0b1 & lcm == PTE_CAP_OK
then (true, PTE_CAP_OK)
else if e.StoreCap() == 0b0
/* return a failure since we should cause an exception */
then (false, PTE_STORE_CAP_ERR)
/* return a success since the translation should proceed */
else (true, PTE_LOAD_CAP_ERR)
else (true, lcm)
}
else (false, PTE_CAP_OK)
},

(Read(Cap), Supervisor) => { if (p.U() == 0b0 | do_sum) & p.R() == 0b1
then {
let e = Mk_Ext_PTE_Bits(ext);
if e.LoadCap() == 0b1
then (true, PTE_CAP_OK)
else (true, PTE_LOAD_CAP_ERR)
(true, checkPTEPermission_LC(p, e))
}
else (false, PTE_CAP_OK)
},
Expand All @@ -118,13 +149,14 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
(ReadWrite(Cap), Supervisor) => { let e = Mk_Ext_PTE_Bits(ext);
if (p.U() == 0b0 | do_sum) & p.R() == 0b1 & p.W() == 0b1
then {
if e.StoreCap() == 0b1 & e.LoadCap() == 0b1
let lcm = checkPTEPermission_LC(p, e);
if e.StoreCap() == 0b1 & lcm == PTE_CAP_OK
then (true, PTE_CAP_OK)
else if e.StoreCap() == 0b0
/* return a failure since we should cause an exception */
then (false, PTE_STORE_CAP_ERR)
/* return a success since the translation should proceed */
else (true, PTE_LOAD_CAP_ERR)
else (true, lcm)
}
else (false, PTE_CAP_OK)
},
Expand Down
38 changes: 28 additions & 10 deletions src/cheri_riscv_types.sail
View file
Original file line number Diff line number Diff line change
@@ -1,26 +1,44 @@
/* Extension for CHERI PTE checks */
enum pte_check = {PTE_CAP_OK, PTE_LOAD_CAP_ERR, PTE_STORE_CAP_ERR}
enum pte_check = {
PTE_CAP_OK,
PTE_LOAD_CAP_TRAP,
PTE_LOAD_CAP_CLR,
PTE_STORE_CAP_ERR
}

/* Extension for CHERI page-table-walks */

enum ext_ptw = {PTW_CAP_OK, PTW_LOAD_CAP_ERR, PTW_STORE_CAP_ERR}
enum ext_ptw = {
PTW_CAP_OK,
PTW_LOAD_CAP_TRAP,
PTW_LOAD_CAP_CLR,
PTW_STORE_CAP_ERR
}

let init_ext_ptw : ext_ptw = PTW_CAP_OK /* initial value of the PTW accumulator */

/* Default accumulation of PTE check extensions into PTW accumulator */
function ext_accum_ptw_result(ptw : ext_ptw, pte : pte_check) -> ext_ptw =
match (ptw, pte) {
(PTW_CAP_OK, PTE_CAP_OK) => PTW_CAP_OK,
(PTW_CAP_OK, PTE_LOAD_CAP_ERR) => PTW_LOAD_CAP_ERR,
(PTW_CAP_OK, PTE_STORE_CAP_ERR) => PTW_STORE_CAP_ERR,
(PTW_CAP_OK, PTE_CAP_OK) => PTW_CAP_OK,
(PTW_CAP_OK, PTE_LOAD_CAP_TRAP) => PTW_LOAD_CAP_TRAP,
(PTW_CAP_OK, PTE_LOAD_CAP_CLR) => PTW_LOAD_CAP_CLR,
(PTW_CAP_OK, PTE_STORE_CAP_ERR) => PTW_STORE_CAP_ERR,

/*
* CHECK ME: The below prioritizes store exceptions over load modifiers,
* and prefers load traps from permission to load traps from CLG to load
* clearing.
*/

/* CHECK ME: The below prioritizes store exceptions over load tag stripping. */
(PTW_LOAD_CAP_CLR, PTE_STORE_CAP_ERR) => PTW_STORE_CAP_ERR,
(PTW_LOAD_CAP_CLR, PTE_STORE_CAP_TRAP) => PTW_LOAD_CAP_TRAP,
(PTW_LOAD_CAP_CLR, _) => PTW_LOAD_CAP_CLR,

(PTW_LOAD_CAP_ERR, PTE_CAP_OK) => PTW_LOAD_CAP_ERR,
(PTW_LOAD_CAP_ERR, PTE_LOAD_CAP_ERR) => PTW_LOAD_CAP_ERR,
(PTW_LOAD_CAP_ERR, PTE_STORE_CAP_ERR) => PTW_STORE_CAP_ERR,
(PTW_LOAD_CAP_TRAP, PTE_STORE_CAP_ERR) => PTW_STORE_CAP_ERR,
(PTW_LOAD_CAP_TRAP, _) => PTW_LOAD_CAP_TRAP,

(PTW_STORE_CAP_ERR, _ ) => PTW_STORE_CAP_ERR
(PTW_STORE_CAP_ERR, _ ) => PTW_STORE_CAP_ERR
}

/* Address translation errors */
Expand Down
2 changes: 2 additions & 0 deletions src/cheri_sys_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,8 @@
bitfield ccsr : xlenbits = {
cap_idx : 15 .. 10,
cause : 9 .. 5, /* cap cause */
gclgu : 3,
gclgs : 2,
d : 1, /* dirty */
e : 0 /* enable */
}
Expand Down
9 changes: 6 additions & 3 deletions src/cheri_types.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,8 @@ enum CapEx = {
CapEx_PermitCCallViolation,
CapEx_AccessCCallIDCViolation,
CapEx_PermitUnsealViolation,
CapEx_PermitSetCIDViolation
CapEx_PermitSetCIDViolation,
CapEx_CapLoadGen
}

function CapExCode(ex) : CapEx -> bits(5) =
Expand Down Expand Up @@ -108,7 +109,8 @@ function CapExCode(ex) : CapEx -> bits(5) =
CapEx_PermitCCallViolation => 0b11001,
CapEx_AccessCCallIDCViolation => 0b11010,
CapEx_PermitUnsealViolation => 0b11011,
CapEx_PermitSetCIDViolation => 0b11100
CapEx_PermitSetCIDViolation => 0b11100,
CapEx_CapLoadGen => 0b11101
}

function string_of_capex (ex) : CapEx -> string =
Expand Down Expand Up @@ -137,7 +139,8 @@ function string_of_capex (ex) : CapEx -> string =
CapEx_PermitCCallViolation => "PermitCCallViolation" ,
CapEx_AccessCCallIDCViolation => "AccessCCallIDCViolation" ,
CapEx_PermitUnsealViolation => "PermitUnsealViolation" ,
CapEx_PermitSetCIDViolation => "PermitSetCIDViolation"
CapEx_PermitSetCIDViolation => "PermitSetCIDViolation" ,
CapEx_CapLoadGen => "CapLoadGen"
}

type capreg_idx = bits(6)
Expand Down

0 comments on commit d14889f

Please sign in to comment.