Skip to content

Commit ea3b0cd

Browse files
nwfnwf
committed
Move CHERI PTE traps to their own vectors
Rather than riding through the generic 0x1C vector. This removes CapEx_CapLoadGen and CapEx_MMUNoStoreCap
1 parent 6aa50fb commit ea3b0cd

File tree

3 files changed

+54
-28
lines changed

3 files changed

+54
-28
lines changed

‎src/cheri_insts.sail

+13-11
Original file line numberDiff line numberDiff line change
@@ -944,7 +944,7 @@ function clause execute (CLoadCap(rd, cs, is_unsigned, width)) =
944944

945945
union load_cap_ptw_ext_result = {
946946
LCPE_OK : Capability,
947-
LCPE_Exn : CapEx
947+
LCPE_Exn : ExceptionType
948948
}
949949

950950
val handle_load_cap_ptw_ext : (Capability, bool, ext_ptw_lcm) -> load_cap_ptw_ext_result
@@ -954,7 +954,7 @@ function handle_load_cap_ptw_ext (v, vialc, ptw_info) =
954954
else match ptw_info {
955955
PTW_LCM_OK => LCPE_OK({v with tag = v.tag & vialc}),
956956
PTW_LCM_CLR => LCPE_OK({v with tag = false}),
957-
PTW_LCM_TRAP => LCPE_Exn(CapEx_CapLoadGen)
957+
PTW_LCM_TRAP => LCPE_Exn(E_Extension(EXC_CHERI_MMU_LOAD_CAP))
958958
}
959959

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

986986
if ~(load_cap_data_dep_trap) & vialc & lcav == PTW_LCM_TRAP then {
987987
/* If we're not permitted to do tag-dependent traps, trap now */
988-
handle_cheri_cap_exception(CapEx_CapLoadGen, cs); RETIRE_FAIL
988+
handle_mem_exception(vaddrBits, E_Extension(EXC_CHERI_MMU_LOAD_CAP));
989+
RETIRE_FAIL
989990
} else {
990991
let c = mem_read_cap(addr, aq, rl, false);
991992
match c {
992993
MemValue(v) => {
993994
match handle_load_cap_ptw_ext(v, vialc, lcav) {
994995
LCPE_OK(v') => { writeCapReg(rd, v'); RETIRE_SUCCESS },
995-
LCPE_Exn(e) => { handle_cheri_cap_exception(e, cs); RETIRE_FAIL }
996+
LCPE_Exn(e) => { handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
996997
}
997998
},
998999
MemException(e) => {handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
@@ -1090,14 +1091,15 @@ if not(cap_val.tag) then {
10901091

10911092
if ~(load_cap_data_dep_trap) & vialc & lcav == PTW_LCM_TRAP then {
10921093
/* If we're not permitted to do tag-dependent traps, trap now */
1093-
handle_cheri_cap_exception(CapEx_CapLoadGen, cs); RETIRE_FAIL
1094+
handle_mem_exception(vaddrBits, E_Extension(EXC_CHERI_MMU_LOAD_CAP));
1095+
RETIRE_FAIL
10941096
} else {
10951097
let c = mem_read_cap(addr, aq, rl, false);
10961098
match c {
10971099
MemValue(v) => {
10981100
match handle_load_cap_ptw_ext(v, vialc, lcav) {
10991101
LCPE_OK(v') => { load_reservation(addr); writeCapReg(cd, v'); RETIRE_SUCCESS },
1100-
LCPE_Exn(e) => { handle_cheri_cap_exception(e, cs); RETIRE_FAIL }
1102+
LCPE_Exn(e) => { handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
11011103
}
11021104
},
11031105
MemException(e) => {handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
@@ -1248,16 +1250,16 @@ function handle_store_cap_via_cap(rs, cs, cap_val, vaddrBits) = {
12481250
handle_mem_exception(vaddrBits, E_SAMO_Addr_Align());
12491251
RETIRE_FAIL
12501252
} else match translateAddr(vaddrBits, Write(if rs_val.tag then Cap else Data)) {
1251-
TR_Failure(E_Extension(EXC_CHERI_VMEM_STORE_CAP), _) => {
1252-
handle_cheri_cap_exception(CapEx_MMUNoStoreCap, cs);
1253+
TR_Failure(E_Extension(EXC_CHERI_MMU_STORE_CAP), _) => {
1254+
handle_mem_exception(vaddrBits, E_Extension(EXC_CHERI_MMU_STORE_CAP));
12531255
RETIRE_FAIL
12541256
},
12551257
TR_Failure(E_Extension(_), _) => { internal_error("unexpected cheri exception for cap store") },
12561258
TR_Failure(e, _) => { handle_mem_exception(vaddrBits, e); RETIRE_FAIL },
12571259
TR_Address(addr, caveats) => {
12581260
match (caveats.ptw_sc_mod, rs_val.tag) {
12591261
(PTW_SCM_TRAP, true) => {
1260-
handle_cheri_cap_exception(CapEx_MMUNoStoreCap, cs);
1262+
handle_mem_exception(vaddrBits, E_Extension(EXC_CHERI_MMU_STORE_CAP));
12611263
RETIRE_FAIL
12621264
},
12631265
_ => {
@@ -1405,15 +1407,15 @@ function handle_store_cond_cap_via_cap(cs2, cs, cap_val, vaddrBits) = {
14051407
} else {
14061408
match translateAddr(vaddrBits, Write(if cs2_val.tag then Cap else Data)) {
14071409
TR_Failure(E_Extension(EXC_CHERI_VMEM_STORE_CAP), _) => {
1408-
handle_cheri_cap_exception(CapEx_MMUNoStoreCap, cs);
1410+
handle_mem_exception(vaddrBits, E_Extension(EXC_CHERI_MMU_STORE_CAP));
14091411
RETIRE_FAIL
14101412
},
14111413
TR_Failure(E_Extension(_), _) => { internal_error("unexpected cheri exception for cap store") },
14121414
TR_Failure(e, _) => { handle_mem_exception(vaddrBits, e); RETIRE_FAIL },
14131415
TR_Address(addr, caveats) => {
14141416
match (caveats.ptw_sc_mod, cs2_val.tag) {
14151417
(PTW_SCM_TRAP, true) => {
1416-
handle_cheri_cap_exception(CapEx_MMUNoStoreCap, cs);
1418+
handle_mem_exception(vaddrBits, E_Extension(EXC_CHERI_MMU_STORE_CAP));
14171419
RETIRE_FAIL
14181420
},
14191421
_ => {

‎src/cheri_riscv_types.sail

+37-8
Original file line numberDiff line numberDiff line change
@@ -61,28 +61,57 @@ let init_ext_ptw : ext_ptw = struct {
6161
ptw_sc_mod = PTW_SCM_OK
6262
}
6363

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

6777
/* CHERI exception extensions */
6878

69-
enum ext_exc_type = {EXC_CHERI, EXC_CHERI_VMEM_LOAD_CAP, EXC_CHERI_VMEM_STORE_CAP}
79+
enum ext_exc_type = {
80+
EXC_CHERI,
81+
EXC_CHERI_MMU_LOAD_CAP,
82+
EXC_CHERI_MMU_STORE_CAP
83+
}
7084

7185
/* CHERI translation of PTW errors into exception annotations */
7286
function ext_translate_exception(e : ext_ptw_error) -> ext_exc_type =
7387
match e {
74-
AT_LOAD_CAP_ERR => EXC_CHERI_VMEM_LOAD_CAP,
75-
AT_STORE_CAP_ERR => EXC_CHERI_VMEM_STORE_CAP
88+
AT_LOAD_CAP_ERR => EXC_CHERI_MMU_LOAD_CAP,
89+
AT_STORE_CAP_ERR => EXC_CHERI_MMU_STORE_CAP
7690
}
7791

7892
/* CHERI conversion of extension exceptions to bits */
7993
val ext_exc_type_to_bits : ext_exc_type -> exc_code
80-
function ext_exc_type_to_bits(e) = 0x1C
94+
function ext_exc_type_to_bits(e) =
95+
match e {
96+
EXC_CHERI_MMU_LOAD_CAP => 0x1A,
97+
EXC_CHERI_MMU_STORE_CAP => 0x1B,
98+
_ => 0x1C
99+
}
81100

82101
/* CHERI conversion of extension exceptions to integers */
83102
val num_of_ext_exc_type : ext_exc_type -> {'n, (0 <= 'n < xlen). int('n)}
84-
function num_of_ext_exc_type(e) = 28
103+
function num_of_ext_exc_type(e) =
104+
match e {
105+
EXC_CHERI_MMU_LOAD_CAP => 26,
106+
EXC_CHERI_MMU_STORE_CAP => 27,
107+
_ => 28
108+
}
85109

86110
/* CHERI conversion of extension exceptions to strings */
87111
val ext_exc_type_to_str : ext_exc_type -> string
88-
function ext_exc_type_to_str(e) = "cheri-exception"
112+
function ext_exc_type_to_str(e) =
113+
match e {
114+
EXC_CHERI_MMU_LOAD_CAP => "cheri-mmu-cap-load",
115+
EXC_CHERI_MMU_STORE_CAP => "cheri-mmu-cap-store",
116+
_ => "cheri-exception"
117+
}

‎src/cheri_types.sail

+4-9
Original file line numberDiff line numberDiff line change
@@ -65,7 +65,6 @@ enum CapEx = {
6565
CapEx_ReturnTrap,
6666
CapEx_TSSUnderFlow,
6767
CapEx_UserDefViolation,
68-
CapEx_MMUNoStoreCap,
6968
CapEx_InexactBounds,
7069
CapEx_UnalignedBase,
7170
CapEx_GlobalViolation,
@@ -80,8 +79,7 @@ enum CapEx = {
8079
CapEx_PermitCCallViolation,
8180
CapEx_AccessCCallIDCViolation,
8281
CapEx_PermitUnsealViolation,
83-
CapEx_PermitSetCIDViolation,
84-
CapEx_CapLoadGen
82+
CapEx_PermitSetCIDViolation
8583
}
8684

8785
function CapExCode(ex) : CapEx -> bits(5) =
@@ -95,7 +93,7 @@ function CapExCode(ex) : CapEx -> bits(5) =
9593
CapEx_ReturnTrap => 0b00110,
9694
CapEx_TSSUnderFlow => 0b00111,
9795
CapEx_UserDefViolation => 0b01000,
98-
CapEx_MMUNoStoreCap => 0b01001,
96+
/* 0b01001 unused; was CapEx_MMUNoStoreCap */
9997
CapEx_InexactBounds => 0b01010,
10098
CapEx_UnalignedBase => 0b01011,
10199
CapEx_GlobalViolation => 0b10000,
@@ -110,8 +108,7 @@ function CapExCode(ex) : CapEx -> bits(5) =
110108
CapEx_PermitCCallViolation => 0b11001,
111109
CapEx_AccessCCallIDCViolation => 0b11010,
112110
CapEx_PermitUnsealViolation => 0b11011,
113-
CapEx_PermitSetCIDViolation => 0b11100,
114-
CapEx_CapLoadGen => 0b11101
111+
CapEx_PermitSetCIDViolation => 0b11100
115112
}
116113

117114
function string_of_capex (ex) : CapEx -> string =
@@ -125,7 +122,6 @@ function string_of_capex (ex) : CapEx -> string =
125122
CapEx_ReturnTrap => "ReturnTrap" ,
126123
CapEx_TSSUnderFlow => "TSSUnderFlow" ,
127124
CapEx_UserDefViolation => "UserDefViolation" ,
128-
CapEx_MMUNoStoreCap => "MMUNoStoreCap" ,
129125
CapEx_InexactBounds => "InexactBounds" ,
130126
CapEx_UnalignedBase => "UnalignedBounds" ,
131127
CapEx_GlobalViolation => "GlobalViolation" ,
@@ -140,8 +136,7 @@ function string_of_capex (ex) : CapEx -> string =
140136
CapEx_PermitCCallViolation => "PermitCCallViolation" ,
141137
CapEx_AccessCCallIDCViolation => "AccessCCallIDCViolation" ,
142138
CapEx_PermitUnsealViolation => "PermitUnsealViolation" ,
143-
CapEx_PermitSetCIDViolation => "PermitSetCIDViolation" ,
144-
CapEx_CapLoadGen => "CapLoadGen"
139+
CapEx_PermitSetCIDViolation => "PermitSetCIDViolation"
145140
}
146141

147142
type capreg_idx = bits(6)

0 commit comments

Comments
 (0)