Skip to content

Commit 12f4a73

Browse files
nwf-msrjrtc27
nwf-msr
and
jrtc27
committed
Introduce load-capability generation traps
Co-authored-by: Jessica Clarke <[email protected]>
1 parent 3c71c95 commit 12f4a73

File tree

4 files changed

+117
-26
lines changed

4 files changed

+117
-26
lines changed

‎src/cheri_insts.sail

Lines changed: 41 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1498,11 +1498,25 @@ function handle_load_cap_via_cap(cd, auth_idx, auth_val, vaddrBits) = {
14981498
let c = mem_read_cap(addr, aq, aq & rl, false);
14991499
match c {
15001500
MemValue(v) => {
1501-
let cr = if ptw_info.ptw_lc == PTW_LC_CLEAR
1502-
then {v with tag = false} /* strip the tag */
1503-
else {v with tag = v.tag & auth_val.permit_load_cap};
1504-
C(cd) = cr;
1505-
RETIRE_SUCCESS
1501+
match ptw_info.ptw_lc {
1502+
PTW_LC_OK => {
1503+
C(cd) = { v with tag = v.tag & auth_val.permit_load_cap };
1504+
RETIRE_SUCCESS
1505+
},
1506+
PTW_LC_CLEAR => {
1507+
C(cd) = { v with tag = false };
1508+
RETIRE_SUCCESS
1509+
},
1510+
PTW_LC_TRAP => {
1511+
if v.tag then {
1512+
handle_mem_exception(vaddrBits, E_Extension(EXC_LOAD_CAP_PAGE_FAULT));
1513+
RETIRE_FAIL
1514+
} else {
1515+
C(cd) = v;
1516+
RETIRE_SUCCESS
1517+
}
1518+
}
1519+
}
15061520
},
15071521
MemException(e) => {handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
15081522
}
@@ -1727,15 +1741,28 @@ if not(auth_val.tag) then {
17271741
let c = mem_read_cap(addr, aq, aq & rl, false);
17281742
match c {
17291743
MemValue(v) => {
1730-
let cr = if ptw_info.ptw_lc == PTW_LC_CLEAR
1731-
then {v with tag = false} /* strip the tag */
1732-
else {
1733-
/* the Sail model currently reserves virtual addresses */
1734-
load_reservation(addr);
1735-
{v with tag = v.tag & auth_val.permit_load_cap}
1736-
};
1737-
C(cd) = cr;
1738-
RETIRE_SUCCESS
1744+
match ptw_info.ptw_lc {
1745+
PTW_LC_OK => {
1746+
load_reservation(addr);
1747+
C(cd) = { v with tag = v.tag & auth_val.permit_load_cap };
1748+
RETIRE_SUCCESS
1749+
},
1750+
PTW_LC_CLEAR => {
1751+
load_reservation(addr);
1752+
C(cd) = { v with tag = false };
1753+
RETIRE_SUCCESS
1754+
},
1755+
PTW_LC_TRAP => {
1756+
if v.tag then {
1757+
handle_mem_exception(vaddrBits, E_Extension(EXC_LOAD_CAP_PAGE_FAULT));
1758+
RETIRE_FAIL
1759+
} else {
1760+
load_reservation(addr);
1761+
C(cd) = v;
1762+
RETIRE_SUCCESS
1763+
}
1764+
}
1765+
}
17391766
},
17401767
MemException(e) => {handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
17411768
}

‎src/cheri_pte.sail

Lines changed: 50 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -93,22 +93,40 @@ bitfield PTE_Bits : pteAttribs = {
9393
* state cached and then observe a CW=1 CD=1 PTE, no PTE write is necessary.
9494
* On the other hand, if CW=0 is observed, the store operation must trap.
9595
*
96-
* SV32: There are no extension bits available, so we hard-code the result to
97-
* CW=1 CR=1 CD=1.
96+
* The intended semantics for capability loads are as follows.
97+
*
98+
* CR CRT CRG Action
99+
*
100+
* 0 0 0 Capability loads strip tags
101+
* 0 1 0 Capability loads trap (on set tag)
102+
* 0 X 1 [Reserved]
103+
*
104+
* 1 0 0 Capability loads succeed: no traps or tag clearing
105+
* 1 0 1 [Reserved]
106+
* 1 1 G Capability loads trap if G mismatches [ms]ccsr.[su]gclg, where
107+
* the compared bit is keyed off of this PTE's U. sccsr is
108+
* used if the machine has Supervisor mode, otherwise mccsr.
109+
*
110+
* Sv32: There are no extension bits available, so we hard-code the result to
111+
* CW=1 CR=1 CD=1 CRT=0 CRG=0
98112
*/
99113
type extPte = bits(10)
100114

101115
bitfield Ext_PTE_Bits : extPte = {
102116
CapWrite : 9, /* Permit capability stores */
103117
CapRead : 8, /* Permit capability loads */
104118
CapDirty : 7, /* Capability Dirty flag */
119+
CapReadTrap : 6, /* Trap on capability loads; see above table */
120+
CapReadGen : 5, /* When load-cap gens. are in use, the "local" gen. bit */
105121
}
106122

107123
/*
108-
* CapWrite = 1,
109-
* CapRead = 1,
110-
* CapDirty = 1,
111-
* bits 0 .. 6 = 0
124+
* CapWrite = 1,
125+
* CapRead = 1,
126+
* CapDirty = 1,
127+
* CapReadTrap = 0,
128+
* CapReadGen = 0,
129+
* bits 0 .. 4 = 0
112130
*/
113131
let default_sv32_ext_pte : extPte = 0b1110000000
114132

@@ -119,7 +137,10 @@ function isPTEPtr(p : pteAttribs, ext : extPte) -> bool = {
119137

120138
function isInvalidPTE(p : pteAttribs, ext : extPte) -> bool = {
121139
let a = Mk_PTE_Bits(p);
122-
a.V() == 0b0 | (a.W() == 0b1 & a.R() == 0b0)
140+
let e = Mk_Ext_PTE_Bits(ext);
141+
a.V() == 0b0 | (a.W() == 0b1 & a.R() == 0b0) |
142+
(e.CapRead() == 0b0 & e.CapReadGen() == 0b1) |
143+
(e.CapRead() == 0b1 & e.CapReadGen() == 0b1 & e.CapReadTrap() == 0b0)
123144
}
124145

125146
union PTE_Check = {
@@ -135,6 +156,26 @@ function checkPTEPermission_SC(e, ext_ptw) = {
135156
else PTE_Check_Failure(ext_ptw, EPTWF_CAP_ERR)
136157
}
137158

159+
/*
160+
* Assuming we're allowed to load from this page, modulate our cap response
161+
*/
162+
val checkPTEPermission_LC : (PTE_Bits, Ext_PTE_Bits, ext_ptw) -> PTE_Check effect { escape, rreg }
163+
function checkPTEPermission_LC(p, e, ext_ptw) =
164+
match (e.CapRead(), e.CapReadTrap(), e.CapReadGen()) {
165+
(0b0, 0b0, 0b0) => PTE_Check_Success(ext_ptw_lc_join(ext_ptw, PTW_LC_CLEAR)), /* Clear tag for "unmodified" no-LC case */
166+
(0b0, 0b1, 0b0) => PTE_Check_Success(ext_ptw_lc_join(ext_ptw, PTW_LC_TRAP)), /* Trap on tag load for "modified" no-LC case */
167+
(0b0, _ , 0b1) => internal_error("Bad PTE not caught by isInvalidPTE"),
168+
(0b1, 0b0, 0b0) => PTE_Check_Success(ext_ptw_lc_join(ext_ptw, PTW_LC_OK)), /* Unmodified LC case: go ahead */
169+
(0b1, 0b0, 0b1) => internal_error("Bad PTE not caught by isInvalidPTE"),
170+
(0b1, 0b1, lclg) => {
171+
/* Compare local CLG against the pte.U-selected, not mode-selected, global CLG bit */
172+
let ccsr = if haveSupMode() then sccsr else mccsr;
173+
let gclg : bits(1) = if p.U() == 0b1 then ccsr.ugclg() else ccsr.sgclg();
174+
let ptwl = if lclg == gclg then PTW_LC_OK else PTW_LC_TRAP;
175+
PTE_Check_Success(ext_ptw_lc_join(ext_ptw, ptwl))
176+
}
177+
}
178+
138179
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 = {
139180
/*
140181
* Although in many cases MXR doesn't make sense for capabilities, we honour
@@ -185,7 +226,6 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
185226
};
186227

187228
/* Load side */
188-
let ptw_lc = if e.CapRead() == 0b1 then PTW_LC_OK else PTW_LC_CLEAR;
189229
let res : PTE_Check = match res {
190230
PTE_Check_Failure(_, _) => res,
191231
PTE_Check_Success(ext_ptw) => match ac {
@@ -194,8 +234,8 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
194234
Write(_) => res,
195235
ReadWrite(Data, _) => res,
196236

197-
Read(Cap) => PTE_Check_Success(ext_ptw_lc_join(ext_ptw, ptw_lc)),
198-
ReadWrite(Cap, _) => PTE_Check_Success(ext_ptw_lc_join(ext_ptw, ptw_lc))
237+
Read(Cap) => checkPTEPermission_LC(p, e, ext_ptw),
238+
ReadWrite(Cap, _) => checkPTEPermission_LC(p, e, ext_ptw)
199239
}
200240
};
201241

‎src/cheri_riscv_types.sail

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,10 @@ enum ext_ptw_lc = {
7272
PTW_LC_OK,
7373

7474
/* PTE settings require clearing tags */
75-
PTW_LC_CLEAR
75+
PTW_LC_CLEAR,
76+
77+
/* PTE settings require us to trap */
78+
PTW_LC_TRAP
7679
}
7780

7881
struct ext_ptw = {
@@ -83,7 +86,12 @@ function ext_ptw_lc_join(e : ext_ptw, l : ext_ptw_lc) -> ext_ptw =
8386
{ e with ptw_lc =
8487
match l {
8588
PTW_LC_OK => e.ptw_lc,
86-
PTW_LC_CLEAR => l
89+
PTW_LC_CLEAR => match e.ptw_lc {
90+
PTW_LC_OK => PTW_LC_CLEAR,
91+
PTW_LC_CLEAR => PTW_LC_CLEAR,
92+
PTW_LC_TRAP => PTW_LC_TRAP
93+
},
94+
PTW_LC_TRAP => PTW_LC_TRAP
8795
}
8896
}
8997

‎src/cheri_sys_regs.sail

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -65,6 +65,8 @@
6565
/* Capability control csr */
6666

6767
bitfield ccsr : xlenbits = {
68+
ugclg : 3, /* Global Cap Load Gen bit for User pages */
69+
sgclg : 2, /* Global Cap Load Gen bit for System (not User) pages */
6870
d : 1, /* dirty */
6971
e : 0 /* enable */
7072
}
@@ -78,6 +80,20 @@ register uccsr : ccsr
7880
function legalize_ccsr(csrp : Privilege, c : ccsr, v : xlenbits) -> ccsr = {
7981
// write only the defined bits, leaving the other bits untouched
8082
let v = Mk_ccsr(v);
83+
84+
let c : ccsr = match csrp {
85+
User => {
86+
// No bits defined for uccsr
87+
c
88+
},
89+
_ => {
90+
// GCLG bits defined for both m- and s-ccsr
91+
let c = update_ugclg(c, v.ugclg());
92+
let c = update_sgclg(c, v.sgclg());
93+
c
94+
}
95+
};
96+
8197
/* For now these bits are not really supported so hardwired to true */
8298
let c = update_d(c, 0b1);
8399
let c = update_e(c, 0b1);

0 commit comments

Comments
 (0)