From 32b264ab027cb43af40414f81272327b38132068 Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Fri, 22 Oct 2021 14:56:19 +0100 Subject: [PATCH 1/5] Catch up with upstream sail-riscv Pull up to https://github.com/riscv/sail-riscv/commit/2265a2576fac6d555cfc5f850f78e79c2da56312 Some upstream changes apply to files in this repository as well: - Following along with https://github.com/riscv/sail-riscv/commit/b1db5b944b42062d063343db8e2efd05e5889b21 add ext_check_phys_mem_read and ext_check_phys_mem_write implementations. - Following along with https://github.com/riscv/sail-riscv/commit/9b38e33c766c7c0397b9d51bf91544db391be670 always use riscv_flen_D.sail rather than riscv_flen_F.sail on RV32. - Following along with https://github.com/riscv/sail-riscv/commit/ffea7a39c32a210a446379aeda0eabcec4918ed6 use -fcommon in C_FLAGS. --- Makefile | 6 ++---- sail-riscv | 2 +- src/cheri_addr_checks.sail | 6 ++++++ 3 files changed, 9 insertions(+), 5 deletions(-) diff --git a/Makefile b/Makefile index 037448e3..54c214e7 100644 --- a/Makefile +++ b/Makefile @@ -12,15 +12,13 @@ SAIL_RISCV_MODEL_DIR=$(SAIL_RISCV_DIR)/model SAIL_CHERI_MODEL_DIR=src SAIL_RV32_XLEN := $(SAIL_RISCV_MODEL_DIR)/riscv_xlen32.sail -SAIL_RV32_FLEN := $(SAIL_RISCV_MODEL_DIR)/riscv_flen_F.sail CHERI_CAP_RV32_IMPL := cheri_prelude_64.sail SAIL_RV64_XLEN := $(SAIL_RISCV_MODEL_DIR)/riscv_xlen64.sail -SAIL_RV64_FLEN := $(SAIL_RISCV_MODEL_DIR)/riscv_flen_D.sail CHERI_CAP_RV64_IMPL := cheri_prelude_128.sail SAIL_XLEN = $(SAIL_$(ARCH)_XLEN) -SAIL_FLEN = $(SAIL_$(ARCH)_FLEN) +SAIL_FLEN = $(SAIL_RISCV_MODEL_DIR)/riscv_flen_D.sail CHERI_CAP_IMPL = $(CHERI_CAP_$(ARCH)_IMPL) @@ -191,7 +189,7 @@ GMP_LIBS := $(shell pkg-config --libs gmp || echo -lgmp) ZLIB_FLAGS = $(shell pkg-config --cflags zlib) ZLIB_LIBS = $(shell pkg-config --libs zlib) -C_FLAGS = -I $(SAIL_LIB_DIR) -I $(SAIL_RISCV_DIR)/c_emulator $(GMP_FLAGS) $(ZLIB_FLAGS) $(SOFTFLOAT_FLAGS) +C_FLAGS = -I $(SAIL_LIB_DIR) -I $(SAIL_RISCV_DIR)/c_emulator $(GMP_FLAGS) $(ZLIB_FLAGS) $(SOFTFLOAT_FLAGS) -fcommon C_LIBS = $(GMP_LIBS) $(ZLIB_LIBS) $(SOFTFLOAT_LIBS) ifneq (,$(SAILCOV)) diff --git a/sail-riscv b/sail-riscv index 60776f92..2265a257 160000 --- a/sail-riscv +++ b/sail-riscv @@ -1 +1 @@ -Subproject commit 60776f92c2f3e6ca02e1f40e27645a51ad1266af +Subproject commit 2265a2576fac6d555cfc5f850f78e79c2da56312 diff --git a/src/cheri_addr_checks.sail b/src/cheri_addr_checks.sail index 3797f5be..49280b84 100644 --- a/src/cheri_addr_checks.sail +++ b/src/cheri_addr_checks.sail @@ -212,6 +212,12 @@ function ext_handle_data_check_error(err : ext_data_addr_error) -> unit = { handle_cheri_cap_exception(capEx, regnum) } +/* Default implementations of these hooks permit all accesses. */ +function ext_check_phys_mem_read (access_type, paddr, size, aquire, release, reserved, read_meta) = + Ext_PhysAddr_OK() + +function ext_check_phys_mem_write(write_kind, paddr, size, data, metadata) = + Ext_PhysAddr_OK() /* Is XRET from given mode permitted by extension? */ function ext_check_xret_priv (p : Privilege) : Privilege -> bool = From b7a0edbb542161b225fc3c801eb8e29dc6d08a51 Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Thu, 12 Nov 2020 00:29:17 +0000 Subject: [PATCH 2/5] Add a fast-cap-dirty PTE behavior The cap-store instructions now look at the data being stored to decide whether they issue Write(Cap) or Write(Data) requests on "the bus". This allows the PTW logic (and update_PTE_Bits) in particular to not fast-cap-dirty a page that's being targeted by the store of an untagged capability. This is not, however, viable for AMOCAS and so additional changes may be required if we are to avoid considering AMOCAS as always capability-dirtying. Co-authored-by: Jessica Clarke --- src/cheri_pte.sail | 45 ++++++++++++++++++++++++++++++++++++++------- 1 file changed, 38 insertions(+), 7 deletions(-) diff --git a/src/cheri_pte.sail b/src/cheri_pte.sail index 223e4b93..49b3c6d6 100644 --- a/src/cheri_pte.sail +++ b/src/cheri_pte.sail @@ -78,23 +78,39 @@ bitfield PTE_Bits : pteAttribs = { /* * Reserved PTE bits used by extensions on RV64. * - * There are no such bits on RV32/SV32, so we hard-code both CapWrite=1 - * and CapRead=1 (i.e., there is no ability to disable capability loads - * from or stores to pages in the SV32 MMU). + * For capability store the behaviors are as follows. + * + * CW CD Action + * + * 0 X Trap on tagged capability store + * 1 0 CAS the PTE to CW=1, CD=1 (i.e., set both bits) or trap + * 1 1 Permit tagged capability store + * + * The CW/CD pair is akin to Sv{32,48,...}'s W/D bits. + * + * The CW=1 CD=0 behavior is described as a CAS (and not an AMO OR) of the PTE + * to close race conditions, much as with W and D. Should the TLB have this + * 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. + * + * SV32: There are no extension bits available, so we hard-code the result to + * CW=1 CR=1 CD=1. */ type extPte = bits(10) bitfield Ext_PTE_Bits : extPte = { CapWrite : 9, /* Permit capability stores */ CapRead : 8, /* Permit capability loads */ + CapDirty : 7, /* Capability Dirty flag */ } /* * CapWrite = 1, * CapRead = 1, - * bits 0 .. 7 = 0 + * CapDirty = 1, + * bits 0 .. 6 = 0 */ -let default_sv32_ext_pte : extPte = 0b1100000000 +let default_sv32_ext_pte : extPte = 0b1110000000 function isPTEPtr(p : pteAttribs, ext : extPte) -> bool = { let a = Mk_PTE_Bits(p); @@ -176,9 +192,24 @@ function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type), ext : ex // accessed bit let update_a = p.A() == 0b0; - if update_d | update_a then { + let pte_ext = Mk_Ext_PTE_Bits(ext); + + // store cap bits + let update_cd = pte_ext.CapWrite() == 0b1 & + pte_ext.CapDirty() == 0b0 & + (match a { + Execute() => false, + Read(_) => false, + Write(Cap) => true, + Write(Data) => false, + ReadWrite(_, Cap) => true, + ReadWrite(_, Data) => false + }); + + if update_d | update_a | update_cd then { let np = update_A(p, 0b1); let np = if update_d then update_D(np, 0b1) else np; - Some(np, ext) + let npte_ext = if update_cd then update_CapDirty(pte_ext, 0b1) else pte_ext; + Some(np, npte_ext.bits()) } else None() } From b41f871b74e5dcc6fe77dd745cc9f9093ccb1a95 Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Thu, 12 Nov 2020 00:29:17 +0000 Subject: [PATCH 3/5] Refactor checkPTEPermission Use Either-monadic style Eliminate ext_ptw_sc / PTW_SC_* as we now simply test the error cases in priority order, so there's no need to explicitly pass this information forward in checkPTEPermission. ext_ptw_lc / PTW_LC_* persist as the extended PTW information is analysed by instructions. Co-authored-by: Jessica Clarke --- src/cheri_pte.sail | 62 ++++++++++++++++++++++++++------------ src/cheri_riscv_types.sail | 22 ++------------ 2 files changed, 44 insertions(+), 40 deletions(-) diff --git a/src/cheri_pte.sail b/src/cheri_pte.sail index 49b3c6d6..d9ce9757 100644 --- a/src/cheri_pte.sail +++ b/src/cheri_pte.sail @@ -127,6 +127,14 @@ union PTE_Check = { PTE_Check_Failure : (ext_ptw, ext_ptw_fail) } +/* Gate Cap-transporting stores on the CapWrite PTE bit */ +val checkPTEPermission_SC : (Ext_PTE_Bits, ext_ptw) -> PTE_Check +function checkPTEPermission_SC(e, ext_ptw) = { + if e.CapWrite() == 0b1 + then PTE_Check_Success(ext_ptw) + else PTE_Check_Failure(ext_ptw, EPTWF_CAP_ERR) +} + 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 @@ -140,7 +148,7 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, * * 3. It's simpler to implement yet still safe (LC is unaffected by MXR). */ - let base_succ : bool = + let succ : bool = match (ac, priv) { (Read(_), User) => p.U() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr)), (Write(_), User) => p.U() == 0b1 & p.W() == 0b1, @@ -155,29 +163,43 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, (_, Machine) => internal_error("m-mode mem perm check") }; + let res = + if succ + then PTE_Check_Success(ext_ptw) + else PTE_Check_Failure(ext_ptw, EPTWF_NO_PERM); + let e = Mk_Ext_PTE_Bits(ext); + + /* Store side */ + let res : PTE_Check = match res { + PTE_Check_Failure(_, _) => res, + PTE_Check_Success(ext_ptw) => match ac { + Execute() => res, + Read(_) => res, + Write(Data) => res, + ReadWrite(_, Data) => res, + + Write(Cap) => checkPTEPermission_SC(e, ext_ptw), + ReadWrite(_, Cap) => checkPTEPermission_SC(e, ext_ptw) + } + }; + + /* Load side */ let ptw_lc = if e.CapRead() == 0b1 then PTW_LC_OK else PTW_LC_CLEAR; - let ptw_sc = if e.CapWrite() == 0b1 then PTW_SC_OK else PTW_SC_TRAP; - let (succ, ext_ptw') : (bool, ext_ptw) = - match (base_succ, ac) { - /* Base translation exceptions take priority over CHERI exceptions */ - (false, _) => (false, init_ext_ptw), - - (true, Read(Cap)) => (true, ext_ptw_lc_join(ext_ptw, ptw_lc)), - (true, Write(Cap)) => (true, ext_ptw_sc_join(ext_ptw, ptw_sc)), - (true, ReadWrite(Data, Cap)) => (true, ext_ptw_sc_join(ext_ptw, ptw_sc)), - (true, ReadWrite(Cap, Data)) => (true, ext_ptw_lc_join(ext_ptw, ptw_lc)), - (true, ReadWrite(Cap, Cap)) => (true, ext_ptw_sc_join(ext_ptw_lc_join(ext_ptw, ptw_lc), ptw_sc)), - - (true, Read(Data)) => (true, ext_ptw), - (true, Write(Data)) => (true, ext_ptw), - (true, ReadWrite(Data, Data)) => (true, ext_ptw), - (true, Execute()) => (true, ext_ptw) + let res : PTE_Check = match res { + PTE_Check_Failure(_, _) => res, + PTE_Check_Success(ext_ptw) => match ac { + Execute() => res, + Read(Data) => res, + 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)) + } }; - if succ - then PTE_Check_Success(ext_ptw') - else PTE_Check_Failure(ext_ptw', if ext_ptw'.ptw_sc == PTW_SC_TRAP then EPTWF_CAP_ERR else EPTWF_NO_PERM) + res } function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type), ext : extPte) -> option((PTE_Bits, extPte)) = { diff --git a/src/cheri_riscv_types.sail b/src/cheri_riscv_types.sail index b6d1e245..cc56ddea 100644 --- a/src/cheri_riscv_types.sail +++ b/src/cheri_riscv_types.sail @@ -75,17 +75,8 @@ enum ext_ptw_lc = { PTW_LC_CLEAR } -enum ext_ptw_sc = { - /* Tag stores are permitted */ - PTW_SC_OK, - - /* Tag-asserting stores trap */ - PTW_SC_TRAP -} - struct ext_ptw = { - ptw_lc : ext_ptw_lc, - ptw_sc : ext_ptw_sc + ptw_lc : ext_ptw_lc } function ext_ptw_lc_join(e : ext_ptw, l : ext_ptw_lc) -> ext_ptw = @@ -96,18 +87,9 @@ function ext_ptw_lc_join(e : ext_ptw, l : ext_ptw_lc) -> ext_ptw = } } -function ext_ptw_sc_join(e : ext_ptw, s : ext_ptw_sc) -> ext_ptw = - { e with ptw_sc = - match s { - PTW_SC_OK => e.ptw_sc, - PTW_SC_TRAP => s - } - } - /* initial value of the PTW accumulator */ let init_ext_ptw : ext_ptw = struct { - ptw_lc = PTW_LC_OK, - ptw_sc = PTW_SC_OK + ptw_lc = PTW_LC_OK } /* Address translation failures */ From 3c71c959c95b6f8a3fd9d1694f25a10733e991d9 Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Thu, 3 Dec 2020 14:39:26 +0000 Subject: [PATCH 4/5] xccsr: pass legalizer the privilege level --- src/cheri_sys_regs.sail | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/src/cheri_sys_regs.sail b/src/cheri_sys_regs.sail index e46841d1..1a00087b 100644 --- a/src/cheri_sys_regs.sail +++ b/src/cheri_sys_regs.sail @@ -75,11 +75,8 @@ register uccsr : ccsr /* access to CCSRs */ -// for now, use a single privilege-independent legalizer -function legalize_ccsr(c : ccsr, v : xlenbits) -> ccsr = { +function legalize_ccsr(csrp : Privilege, c : ccsr, v : xlenbits) -> ccsr = { // write only the defined bits, leaving the other bits untouched - // Technically, WPRI does not need a legalizer, since software is - // assumed to legalize; so we could remove this function. let v = Mk_ccsr(v); /* For now these bits are not really supported so hardwired to true */ let c = update_d(c, 0b1); @@ -96,9 +93,9 @@ function clause ext_read_CSR (0x8C0) = Some(uccsr.bits()) function clause ext_read_CSR (0x9C0) = Some(sccsr.bits()) function clause ext_read_CSR (0xBC0) = Some(mccsr.bits()) -function clause ext_write_CSR (0x8C0, value) = { uccsr = legalize_ccsr(uccsr, value); Some(uccsr.bits()) } -function clause ext_write_CSR (0x9C0, value) = { sccsr = legalize_ccsr(sccsr, value); Some(sccsr.bits()) } -function clause ext_write_CSR (0xBC0, value) = { mccsr = legalize_ccsr(mccsr, value); Some(mccsr.bits()) } +function clause ext_write_CSR (0x8C0, value) = { uccsr = legalize_ccsr(User, uccsr, value); Some(uccsr.bits()) } +function clause ext_write_CSR (0x9C0, value) = { sccsr = legalize_ccsr(Supervisor, sccsr, value); Some(sccsr.bits()) } +function clause ext_write_CSR (0xBC0, value) = { mccsr = legalize_ccsr(Machine, mccsr, value); Some(mccsr.bits()) } function clause ext_is_CSR_defined (0x8C0, p) = haveUsrMode() // uccsr function clause ext_is_CSR_defined (0x9C0, p) = haveSupMode() & (p == Machine | p == Supervisor) // sccsr From 12f4a73642c36ba08eb41eed2ebcaa602887d8cb Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Thu, 12 Nov 2020 00:29:18 +0000 Subject: [PATCH 5/5] Introduce load-capability generation traps Co-authored-by: Jessica Clarke --- src/cheri_insts.sail | 55 +++++++++++++++++++++++++--------- src/cheri_pte.sail | 60 +++++++++++++++++++++++++++++++------- src/cheri_riscv_types.sail | 12 ++++++-- src/cheri_sys_regs.sail | 16 ++++++++++ 4 files changed, 117 insertions(+), 26 deletions(-) diff --git a/src/cheri_insts.sail b/src/cheri_insts.sail index 29b3f036..9810699a 100644 --- a/src/cheri_insts.sail +++ b/src/cheri_insts.sail @@ -1498,11 +1498,25 @@ function handle_load_cap_via_cap(cd, auth_idx, auth_val, vaddrBits) = { let c = mem_read_cap(addr, aq, 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 } } @@ -1727,15 +1741,28 @@ if not(auth_val.tag) then { let c = mem_read_cap(addr, aq, 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 } } diff --git a/src/cheri_pte.sail b/src/cheri_pte.sail index d9ce9757..bfb2e104 100644 --- a/src/cheri_pte.sail +++ b/src/cheri_pte.sail @@ -93,8 +93,22 @@ 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. * - * SV32: There are no extension bits available, so we hard-code the result to - * CW=1 CR=1 CD=1. + * The intended semantics for capability loads are as follows. + * + * CR CRT CRG 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 [ms]ccsr.[su]gclg, where + * the compared bit is keyed off of this PTE's U. sccsr is + * used if the machine has Supervisor mode, otherwise mccsr. + * + * Sv32: There are no extension bits available, so we hard-code the result to + * CW=1 CR=1 CD=1 CRT=0 CRG=0 */ type extPte = bits(10) @@ -102,13 +116,17 @@ bitfield Ext_PTE_Bits : extPte = { CapWrite : 9, /* Permit capability stores */ CapRead : 8, /* Permit capability loads */ CapDirty : 7, /* Capability Dirty flag */ + CapReadTrap : 6, /* Trap on capability loads; see above table */ + CapReadGen : 5, /* When load-cap gens. are in use, the "local" gen. bit */ } /* - * CapWrite = 1, - * CapRead = 1, - * CapDirty = 1, - * bits 0 .. 6 = 0 + * CapWrite = 1, + * CapRead = 1, + * CapDirty = 1, + * CapReadTrap = 0, + * CapReadGen = 0, + * bits 0 .. 4 = 0 */ let default_sv32_ext_pte : extPte = 0b1110000000 @@ -119,7 +137,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.CapReadGen() == 0b1) | + (e.CapRead() == 0b1 & e.CapReadGen() == 0b1 & e.CapReadTrap() == 0b0) } union PTE_Check = { @@ -135,6 +156,26 @@ 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.CapReadTrap(), e.CapReadGen()) { + (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 ccsr = if haveSupMode() then sccsr else mccsr; + let gclg : bits(1) = if p.U() == 0b1 then ccsr.ugclg() else ccsr.sgclg(); + 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 @@ -185,7 +226,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 { @@ -194,8 +234,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) } }; diff --git a/src/cheri_riscv_types.sail b/src/cheri_riscv_types.sail index cc56ddea..c5ece7fc 100644 --- a/src/cheri_riscv_types.sail +++ b/src/cheri_riscv_types.sail @@ -72,7 +72,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 = { @@ -83,7 +86,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 } } diff --git a/src/cheri_sys_regs.sail b/src/cheri_sys_regs.sail index 1a00087b..5dcb6510 100644 --- a/src/cheri_sys_regs.sail +++ b/src/cheri_sys_regs.sail @@ -65,6 +65,8 @@ /* Capability control csr */ bitfield ccsr : xlenbits = { + ugclg : 3, /* Global Cap Load Gen bit for User pages */ + sgclg : 2, /* Global Cap Load Gen bit for System (not User) pages */ d : 1, /* dirty */ e : 0 /* enable */ } @@ -78,6 +80,20 @@ register uccsr : ccsr function legalize_ccsr(csrp : Privilege, c : ccsr, v : xlenbits) -> ccsr = { // write only the defined bits, leaving the other bits untouched let v = Mk_ccsr(v); + + let c : ccsr = match csrp { + User => { + // No bits defined for uccsr + c + }, + _ => { + // GCLG bits defined for both m- and s-ccsr + let c = update_ugclg(c, v.ugclg()); + let c = update_sgclg(c, v.sgclg()); + c + } + }; + /* For now these bits are not really supported so hardwired to true */ let c = update_d(c, 0b1); let c = update_e(c, 0b1);