Skip to content

Commit c94e70d

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

File tree

4 files changed

+110
-23
lines changed

4 files changed

+110
-23
lines changed

‎src/cheri_insts.sail

Lines changed: 41 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1495,11 +1495,25 @@ function handle_load_cap_via_cap(cd, auth_idx, auth_val, vaddrBits) = {
14951495
let c = mem_read_cap(addr, aq, aq & rl, false);
14961496
match c {
14971497
MemValue(v) => {
1498-
let cr = if ptw_info.ptw_lc == PTW_LC_CLEAR
1499-
then {v with tag = false} /* strip the tag */
1500-
else {v with tag = v.tag & auth_val.permit_load_cap};
1501-
C(cd) = cr;
1502-
RETIRE_SUCCESS
1498+
match ptw_info.ptw_lc {
1499+
PTW_LC_OK => {
1500+
C(cd) = { v with tag = v.tag & auth_val.permit_load_cap };
1501+
RETIRE_SUCCESS
1502+
},
1503+
PTW_LC_CLEAR => {
1504+
C(cd) = { v with tag = false };
1505+
RETIRE_SUCCESS
1506+
},
1507+
PTW_LC_TRAP => {
1508+
if v.tag then {
1509+
handle_mem_exception(vaddrBits, E_Extension(EXC_LOAD_CAP_PAGE_FAULT));
1510+
RETIRE_FAIL
1511+
} else {
1512+
C(cd) = v;
1513+
RETIRE_SUCCESS
1514+
}
1515+
}
1516+
}
15031517
},
15041518
MemException(e) => {handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
15051519
}
@@ -1724,15 +1738,28 @@ if not(auth_val.tag) then {
17241738
let c = mem_read_cap(addr, aq, aq & rl, false);
17251739
match c {
17261740
MemValue(v) => {
1727-
let cr = if ptw_info.ptw_lc == PTW_LC_CLEAR
1728-
then {v with tag = false} /* strip the tag */
1729-
else {
1730-
/* the Sail model currently reserves virtual addresses */
1731-
load_reservation(addr);
1732-
{v with tag = v.tag & auth_val.permit_load_cap}
1733-
};
1734-
C(cd) = cr;
1735-
RETIRE_SUCCESS
1741+
match ptw_info.ptw_lc {
1742+
PTW_LC_OK => {
1743+
load_reservation(addr);
1744+
C(cd) = { v with tag = v.tag & auth_val.permit_load_cap };
1745+
RETIRE_SUCCESS
1746+
},
1747+
PTW_LC_CLEAR => {
1748+
load_reservation(addr);
1749+
C(cd) = { v with tag = false };
1750+
RETIRE_SUCCESS
1751+
},
1752+
PTW_LC_TRAP => {
1753+
if v.tag then {
1754+
handle_mem_exception(vaddrBits, E_Extension(EXC_LOAD_CAP_PAGE_FAULT));
1755+
RETIRE_FAIL
1756+
} else {
1757+
load_reservation(addr);
1758+
C(cd) = v;
1759+
RETIRE_SUCCESS
1760+
}
1761+
}
1762+
}
17361763
},
17371764
MemException(e) => {handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
17381765
}

‎src/cheri_pte.sail

Lines changed: 45 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -93,22 +93,39 @@ 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 CR_Trap CR_Gen 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 sccsr.[su]gclg,
107+
* where the compared bit is keyed off of this PTE's U.
108+
*
109+
* Sv32: There are no extension bits available, so we hard-code the result to
110+
* CW=1 CR=1 CD=1 CR_Trap=0 CR_Gen=0
98111
*/
99112
type extPte = bits(10)
100113

101114
bitfield Ext_PTE_Bits : extPte = {
102115
CapWrite : 9, /* Permit capability stores */
103116
CapRead : 8, /* Permit capability loads */
104117
CapDirty : 7, /* Capability Dirty flag */
118+
CapRead_Trap : 6, /* Trap on capability loads; see above table */
119+
CapRead_Gen : 5, /* When load-cap gens. are in use, the "local" gen. bit */
105120
}
106121

107122
/*
108123
* CapWrite = 1,
109124
* CapRead = 1,
110125
* CapDirty = 1,
111-
* bits 0 .. 6 = 0
126+
* CapRead_Trap = 0,
127+
* CapRead_Gen = 0,
128+
* bits 0 .. 4 = 0
112129
*/
113130
let default_sv32_ext_pte : extPte = 0b1110000000
114131

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

120137
function isInvalidPTE(p : pteAttribs, ext : extPte) -> bool = {
121138
let a = Mk_PTE_Bits(p);
122-
a.V() == 0b0 | (a.W() == 0b1 & a.R() == 0b0)
139+
let e = Mk_Ext_PTE_Bits(ext);
140+
a.V() == 0b0 | (a.W() == 0b1 & a.R() == 0b0) |
141+
(e.CapRead() == 0b0 & e.CapRead_Gen() == 0b1) |
142+
(e.CapRead() == 0b1 & e.CapRead_Gen() == 0b1 & e.CapRead_Trap() == 0b0)
123143
}
124144

125145
union PTE_Check = {
@@ -135,6 +155,25 @@ function checkPTEPermission_SC(e, ext_ptw) = {
135155
else PTE_Check_Failure(ext_ptw, EPTWF_CAP_ERR)
136156
}
137157

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

187226
/* Load side */
188-
let ptw_lc = if e.CapRead() == 0b1 then PTW_LC_OK else PTW_LC_CLEAR;
189227
let res : PTE_Check = match res {
190228
PTE_Check_Failure(_, _) => res,
191229
PTE_Check_Success(ext_ptw) => match ac {
@@ -194,8 +232,8 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
194232
Write(_) => res,
195233
ReadWrite(Data, _) => res,
196234

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))
235+
Read(Cap) => checkPTEPermission_LC(p, e, ext_ptw),
236+
ReadWrite(Cap, _) => checkPTEPermission_LC(p, e, ext_ptw)
199237
}
200238
};
201239

‎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: 14 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,18 @@ function legalize_ccsr(csrp : Privilege, c : ccsr, v : xlenbits) -> ccsr = {
7880
// write only the defined bits, leaving the other bits untouched
7981
let v = Mk_ccsr(v);
8082

83+
let c : ccsr = match csrp {
84+
User => {
85+
// No bits defined for uccsr
86+
c
87+
},
88+
_ => {
89+
let c = update_ugclg(c, v.ugclg());
90+
let c = update_sgclg(c, v.sgclg());
91+
c
92+
}
93+
};
94+
8195
/* For now these bits are not really supported so hardwired to true */
8296
let c = update_d(c, 0b1);
8397
let c = update_e(c, 0b1);

0 commit comments

Comments
 (0)