Skip to content

Commit

Permalink
Introduce load-capability generation traps
Browse files Browse the repository at this point in the history
  • Loading branch information
@nwf-msr
nwf-msr committed Nov 12, 2020
1 parent 202a7b2 commit d949a83
Show file tree
Hide file tree
Showing 4 changed files with 99 additions and 22 deletions.
55 changes: 41 additions & 14 deletions src/cheri_insts.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1372,11 +1372,25 @@ function handle_load_cap_via_cap(cd, auth_idx, auth_val, vaddrBits) = {
let c = mem_read_cap(addr, aq, rl, false);
match c {
MemValue(v) => {
let cr = if ptw_info.ptw_lc == PTW_LC_CLEAR
then {v with tag = false} /* strip the tag */
else {v with tag = v.tag & auth_val.permit_load_cap};
C(cd) = cr;
RETIRE_SUCCESS
match ptw_info.ptw_lc {
PTW_LC_OK => {
C(cd) = { v with tag = v.tag & auth_val.permit_load_cap };
RETIRE_SUCCESS
},
PTW_LC_CLEAR => {
C(cd) = { v with tag = false };
RETIRE_SUCCESS
},
PTW_LC_TRAP => {
if v.tag then {
handle_mem_exception(vaddrBits, E_Extension(EXC_LOAD_CAP_PAGE_FAULT));
RETIRE_FAIL
} else {
C(cd) = v;
RETIRE_SUCCESS
}
}
}
},
MemException(e) => {handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
}
Expand Down Expand Up @@ -1603,15 +1617,28 @@ if not(auth_val.tag) then {
let c = mem_read_cap(addr, aq, rl, false);
match c {
MemValue(v) => {
let cr = if ptw_info.ptw_lc == PTW_LC_CLEAR
then {v with tag = false} /* strip the tag */
else {
/* the Sail model currently reserves virtual addresses */
load_reservation(addr);
{v with tag = v.tag & auth_val.permit_load_cap}
};
C(cd) = cr;
RETIRE_SUCCESS
match ptw_info.ptw_lc {
PTW_LC_OK => {
load_reservation(addr);
C(cd) = { v with tag = v.tag & auth_val.permit_load_cap };
RETIRE_SUCCESS
},
PTW_LC_CLEAR => {
load_reservation(addr);
C(cd) = { v with tag = false };
RETIRE_SUCCESS
},
PTW_LC_TRAP => {
if v.tag then {
handle_mem_exception(vaddrBits, E_Extension(EXC_LOAD_CAP_PAGE_FAULT));
RETIRE_FAIL
} else {
load_reservation(addr);
C(cd) = v;
RETIRE_SUCCESS
}
}
}
},
MemException(e) => {handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
}
Expand Down
50 changes: 44 additions & 6 deletions src/cheri_pte.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,22 +31,39 @@ bitfield PTE_Bits : pteAttribs = {
* state cached and then observe a CW=1 CD=1 PTE, no PTE write is necessary.
* On the other hand, if CW=0 is observed, the store operation must trap.
*
* The intended semantics for capability loads are as follows.
*
* CR CR_Mod CR_Gen Action
*
* 0 0 0 Capability loads strip tags
* 0 1 0 Capability loads trap (on set tag)
* 0 X 1 [Reserved]
*
* 1 0 0 Capability loads succeed: no traps or tag clearing
* 1 0 1 [Reserved]
* 1 1 G Capability loads trap if G mismatches sccsr.gclg[su],
* where the compared bit is keyed off of this PTE's U.
*
* SV32: There are no extension bits available, so we hard-code the result to
* CW=1 CR=1 CD=1.
* CW=1 CR=1 CD=1 CR_Mod=0 CR_Gen=0
*/
type extPte = bits(10)

bitfield Ext_PTE_Bits : extPte = {
CapWrite : 9, /* Permit capability stores */
CapRead : 8, /* Permit capability loads */
CapDirty : 7, /* Capability Dirty flag */
CapRead_Mod : 6, /* Modify capability load prohibition; see above table */
CapRead_Gen : 5, /* When load-cap gens. are in use, the "local" gen. bit */
}

/*
* CapWrite = 1,
* CapRead = 1,
* CapDirty = 1,
* bits 0 .. 6 = 0
* CapRead_Mod = 0,
* CapRead_Gen = 0,
* bits 0 .. 4 = 0
*/
let default_sv32_ext_pte : extPte = 0b1110000000

Expand All @@ -57,7 +74,10 @@ function isPTEPtr(p : pteAttribs, ext : extPte) -> bool = {

function isInvalidPTE(p : pteAttribs, ext : extPte) -> bool = {
let a = Mk_PTE_Bits(p);
a.V() == 0b0 | (a.W() == 0b1 & a.R() == 0b0)
let e = Mk_Ext_PTE_Bits(ext);
a.V() == 0b0 | (a.W() == 0b1 & a.R() == 0b0) |
(e.CapRead() == 0b0 & e.CapRead_Gen() == 0b1) |
(e.CapRead() == 0b1 & e.CapRead_Gen() == 0b1 & e.CapRead_Mod() == 0b0)
}

union PTE_Check = {
Expand All @@ -73,6 +93,25 @@ function checkPTEPermission_SC(e, ext_ptw) = {
else PTE_Check_Failure(ext_ptw, EPTWF_CAP_ERR)
}

/*
* Assuming we're allowed to load from this page, modulate our cap response
*/
val checkPTEPermission_LC : (PTE_Bits, Ext_PTE_Bits, ext_ptw) -> PTE_Check effect { escape, rreg }
function checkPTEPermission_LC(p, e, ext_ptw) =
match (e.CapRead(), e.CapRead_Mod(), e.CapRead_Gen()) {
(0b0, 0b0, 0b0) => PTE_Check_Success(ext_ptw_lc_join(ext_ptw, PTW_LC_CLEAR)), /* Clear tag for "unmodified" no-LC case */
(0b0, 0b1, 0b0) => PTE_Check_Success(ext_ptw_lc_join(ext_ptw, PTW_LC_TRAP)), /* Trap on tag load for "modified" no-LC case */
(0b0, _ , 0b1) => internal_error("Bad PTE not caught by isInvalidPTE"),
(0b1, 0b0, 0b0) => PTE_Check_Success(ext_ptw_lc_join(ext_ptw, PTW_LC_OK)), /* Unmodified LC case: go ahead */
(0b1, 0b0, 0b1) => internal_error("Bad PTE not caught by isInvalidPTE"),
(0b1, 0b1, lclg) => {
/* Compare local CLG against the pte.U-selected, not mode-selected, global CLG bit */
let gclg : bits(1) = if p.U() == 0b1 then sccsr.gclgu() else sccsr.gclgs();
let ptwl = if lclg == gclg then PTW_LC_OK else PTW_LC_TRAP;
PTE_Check_Success(ext_ptw_lc_join(ext_ptw, ptwl))
}
}

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 = {
/*
* Although in many cases MXR doesn't make sense for capabilities, we honour
Expand Down Expand Up @@ -123,7 +162,6 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
};

/* Load side */
let ptw_lc = if e.CapRead() == 0b1 then PTW_LC_OK else PTW_LC_CLEAR;
let res : PTE_Check = match res {
PTE_Check_Failure(_, _) => res,
PTE_Check_Success(ext_ptw) => match ac {
Expand All @@ -132,8 +170,8 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
Write(_) => res,
ReadWrite(Data, _) => res,

Read(Cap) => PTE_Check_Success(ext_ptw_lc_join(ext_ptw, ptw_lc)),
ReadWrite(Cap, _) => PTE_Check_Success(ext_ptw_lc_join(ext_ptw, ptw_lc))
Read(Cap) => checkPTEPermission_LC(p, e, ext_ptw),
ReadWrite(Cap, _) => checkPTEPermission_LC(p, e, ext_ptw)
}
};

Expand Down
12 changes: 10 additions & 2 deletions src/cheri_riscv_types.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,10 @@ enum ext_ptw_lc = {
PTW_LC_OK,

/* PTE settings require clearing tags */
PTW_LC_CLEAR
PTW_LC_CLEAR,

/* PTE settings require us to trap */
PTW_LC_TRAP
}

struct ext_ptw = {
Expand All @@ -21,7 +24,12 @@ function ext_ptw_lc_join(e : ext_ptw, l : ext_ptw_lc) -> ext_ptw =
{ e with ptw_lc =
match l {
PTW_LC_OK => e.ptw_lc,
PTW_LC_CLEAR => l
PTW_LC_CLEAR => match e.ptw_lc {
PTW_LC_OK => PTW_LC_CLEAR,
PTW_LC_CLEAR => PTW_LC_CLEAR,
PTW_LC_TRAP => PTW_LC_TRAP
},
PTW_LC_TRAP => PTW_LC_TRAP
}
}

Expand Down
4 changes: 4 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, /* Global Cap Load Gen bit for User pages */
gclgs : 2, /* Global Cap Load Gen bit for System (not User) pages */
d : 1, /* dirty */
e : 0 /* enable */
}
Expand All @@ -23,6 +25,8 @@ function legalize_ccsr(c : ccsr, v : xlenbits) -> ccsr = {
let v = Mk_ccsr(v);
let c = update_cap_idx(c, v.cap_idx());
let c = update_cause(c, v.cause());
let c = update_gclgu(c, v.gclgu());
let c = update_gclgs(c, v.gclgs());
/* For now these bits are not really supported so hardwired to true */
let c = update_d(c, 0b1);
let c = update_e(c, 0b1);
Expand Down

0 comments on commit d949a83

Please sign in to comment.