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 = 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 223e4b93..bfb2e104 100644 --- a/src/cheri_pte.sail +++ b/src/cheri_pte.sail @@ -78,23 +78,57 @@ 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. + * + * 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) 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, - * bits 0 .. 7 = 0 + * CapWrite = 1, + * CapRead = 1, + * CapDirty = 1, + * CapReadTrap = 0, + * CapReadGen = 0, + * bits 0 .. 4 = 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); @@ -103,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 = { @@ -111,6 +148,34 @@ 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) +} + +/* + * 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 @@ -124,7 +189,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, @@ -139,29 +204,42 @@ 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); - 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) + + /* 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) + } }; - 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) + /* Load side */ + 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) => checkPTEPermission_LC(p, e, ext_ptw), + ReadWrite(Cap, _) => checkPTEPermission_LC(p, e, ext_ptw) + } + }; + + res } function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type), ext : extPte) -> option((PTE_Bits, extPte)) = { @@ -176,9 +254,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() } diff --git a/src/cheri_riscv_types.sail b/src/cheri_riscv_types.sail index b6d1e245..c5ece7fc 100644 --- a/src/cheri_riscv_types.sail +++ b/src/cheri_riscv_types.sail @@ -72,42 +72,32 @@ enum ext_ptw_lc = { PTW_LC_OK, /* PTE settings require clearing tags */ - PTW_LC_CLEAR -} - -enum ext_ptw_sc = { - /* Tag stores are permitted */ - PTW_SC_OK, + PTW_LC_CLEAR, - /* Tag-asserting stores trap */ - PTW_SC_TRAP + /* PTE settings require us to trap */ + PTW_LC_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 = { e with ptw_lc = match l { PTW_LC_OK => e.ptw_lc, - PTW_LC_CLEAR => l - } - } - -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 + 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 } } /* 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 */ diff --git a/src/cheri_sys_regs.sail b/src/cheri_sys_regs.sail index e46841d1..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 */ } @@ -75,12 +77,23 @@ 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); + + 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); @@ -96,9 +109,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