Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/cheri_addr_checks.sail
Original file line number Diff line number Diff line change
Expand Up @@ -182,7 +182,7 @@ type ext_data_addr_error = (CapEx, capreg_idx)
function ext_data_get_addr(base_reg : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : word_width)
-> Ext_DataAddr_Check(ext_data_addr_error) = {

let auth_val = C(base_reg);
let auth_val = cheri_load_store_base_from_regidx(base_reg);
let newAddr = auth_val.address + offset;
let auth_idx = 0b0 @ base_reg;

Expand Down
4 changes: 2 additions & 2 deletions src/cheri_insts.sail
Original file line number Diff line number Diff line change
Expand Up @@ -856,7 +856,7 @@ union clause ast = LoadCapImm : (regidx, regidx, bits(12))
*/
function clause execute LoadCapImm(cd, cs1, imm) = {
let offset : xlenbits = sign_extend(imm);
let auth_val = C(cs1);
let auth_val = cheri_load_store_base_from_regidx(cs1);
let vaddrBits = auth_val.address + offset;
if not(auth_val.tag) then {
handle_cheri_reg_exception(CapEx_TagViolation, cs1);
Expand Down Expand Up @@ -950,7 +950,7 @@ union clause ast = StoreCapImm : (regidx, regidx, bits(12))
*/
function clause execute StoreCapImm(cs2, cs1, imm) = {
let offset : xlenbits = sign_extend(imm);
let auth_val = C(cs1);
let auth_val = cheri_load_store_base_from_regidx(cs1);
let vaddrBits = auth_val.address + offset;
let cs2_val = C(cs2);
if not(auth_val.tag) then {
Expand Down
13 changes: 13 additions & 0 deletions src/cheri_regs.sail
Original file line number Diff line number Diff line change
Expand Up @@ -123,6 +123,19 @@ function wC_bits(r: bits(5), v: regtype) -> unit = wC(unsigned(r), v)

overload C = {rC_bits, wC_bits, rC, wC}

function cheri_load_store_base_from_regidx(r : regidx) -> Capability =
if r != zreg
then C(r)
else if PCC.access_system_regs /* XXX: pcc_access_system_regs is later */
then MTDC /*
* XXX: would be mscratch in RISC-V CHERI standard, which is
* ASR-gated for reads and writes like our MTDC SCR.
*/
else PCC /*
* XXX: would be mtidc in RISC-V CHERI standard, but all our
* SCRs are ASR write-gated, so PCC might be an OK stand-in?
*/

val ext_init_regs : unit -> unit
function ext_init_regs () = {
PCC = root_cap_exe;
Expand Down