From 69acf1091525333d8a9495c2bb9858319573c8bd Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Thu, 6 May 2021 19:46:01 +0100 Subject: [PATCH] Indirect sentries, Load-PCC flavor --- src/cheri_cap_common.sail | 4 ++ src/cheri_insts.sail | 91 ++++++++++++++++++++++++++++++++++++++- src/cheri_types.sail | 1 + 3 files changed, 95 insertions(+), 1 deletion(-) diff --git a/src/cheri_cap_common.sail b/src/cheri_cap_common.sail index 7c55003a..82484a7e 100644 --- a/src/cheri_cap_common.sail +++ b/src/cheri_cap_common.sail @@ -416,6 +416,10 @@ function isCapSealed(cap) = signed(cap.otype) != otype_unsealed val hasReservedOType : Capability -> bool function hasReservedOType(cap) = unsigned(cap.otype) > cap_max_otype +function isCapSentryOrIsentry(cap) : Capability -> bool = + let sotype = signed(cap.otype) in + (sotype == otype_sentry) | (sotype == otype_isentry_pcc) + function sealCap(cap, otyp) : (Capability, bits(cap_otype_width)) -> Capability = {cap with otype=otyp} diff --git a/src/cheri_insts.sail b/src/cheri_insts.sail index 20261476..1a43c22b 100644 --- a/src/cheri_insts.sail +++ b/src/cheri_insts.sail @@ -933,7 +933,7 @@ function clause execute (CBuildCap(cd, cs1, cs2)) = { RETIRE_FAIL } else { assert(exact, "CBuildCap: setCapBounds was not exact"); /* base and top came from cs2 originally so will be exact */ - let cd5 = if signed(cs2_val.otype) == otype_sentry then sealCap(cd4, to_bits(cap_otype_width, otype_sentry)) else cd4; + let cd5 = if isCapSentryOrIsentry(cs2_val) then sealCap(cd4, cs2_val.otype) else cd4; C(cd) = cd5; RETIRE_SUCCESS } @@ -1695,6 +1695,89 @@ function clause execute (CLoadTags(rd, cs1)) = { } } +/* + * Indirect sentries. + * + * At the risk of becoming CISC, the invocation instructions load, unseal, and + * transfer control. They depend on helpers above for most of those tasks. + */ + +union clause ast = CSealL : (regidx, regidx) +/*! + * Capability register *cd* is replaced with capability register *cs1* and + * sealed as an indirect, points-to-PCC sentry + * + * ## Exceptions + * + * An exception is raised if: + * - *cs1*.**tag** is not set. + * - *cs1* is sealed. + * - *cs1*.**perms** does not grant both **Permit_Load** and + * **Permit_Load_Capability**. + */ +function clause execute (CSealL(cd, cs1)) = { + let cs1_val = C(cs1); + if not (cs1_val.tag) then { + handle_cheri_reg_exception(CapEx_TagViolation, cs1); + RETIRE_FAIL + } else if (isCapSealed(cs1_val)) then { + handle_cheri_reg_exception(CapEx_SealViolation, cs1); + RETIRE_FAIL + } else if not (cs1_val.permit_load) then { + handle_cheri_reg_exception(CapEx_PermitLoadViolation, cs1); + RETIRE_FAIL + } else if not (cs1_val.permit_load_cap) then { + handle_cheri_reg_exception(CapEx_PermitLoadCapViolation, cs1); + RETIRE_FAIL + } else { + C(cd) = sealCap(cs1_val, to_bits(cap_otype_width, otype_isentry_pcc)); + RETIRE_SUCCESS + } +} + +union clause ast = CInvokeLAL : (regidx, regidx) +/*! + * Jump through an indirect, points-to-PCC sentry capability held in + * capability register cs. + */ +function clause execute (CInvokeLAL(cd, cs)) = { + let cs_val = C(cs); + + if not (cs_val.tag) then { + handle_cheri_reg_exception(CapEx_TagViolation, cs); + RETIRE_FAIL + } else if not (isCapSealed(cs_val)) | + signed(cs_val.otype) != otype_isentry_pcc then { + handle_cheri_reg_exception(CapEx_SealViolation, cs); + RETIRE_FAIL + } else { + let idc = unsealCap(cs_val); + let idcaddr = cs_val.address; + + if not (idc.permit_load) | not (idc.permit_load_cap) then { + handle_cheri_reg_exception(CapEx_PermitLoadViolation, cs); + RETIRE_FAIL + } else if not(inCapBounds(idc, idcaddr, cap_size)) then { + handle_cheri_reg_exception(CapEx_LengthViolation, cs); + RETIRE_FAIL + } else if not(is_aligned_addr(idcaddr, cap_size)) then { + handle_mem_exception(idcaddr, E_Load_Addr_Align()); + RETIRE_FAIL + } else { + match load_cap_via_cap(0b0 @ cs, cs_val, idcaddr, false, false) { + None() => RETIRE_FAIL, + Some(_,v) => match cjalr_worker(cd, cs, v, zeros()) { + RETIRE_FAIL => RETIRE_FAIL, + RETIRE_SUCCESS => { + C(31) = idc; + RETIRE_SUCCESS + } + } + } + } + } +} + /* avoid platform checks for reservation address misalignment */ function check_res_misaligned(vaddr : xlenbits, width : word_width) -> bool = match width { @@ -2376,6 +2459,9 @@ mapping clause encdec = JALR_PCC(rd, rs1) if (haveXcheri()) <-> 0b1111111 @ 0b mapping clause encdec = CLoadTags(rd, cs1) if (haveXcheri()) <-> 0b1111111 @ 0b10010 @ cs1 @ 0b000 @ rd @ 0b1011011 if (haveXcheri()) +mapping clause encdec = CSealL(cd, cs1) if (haveXcheri()) <-> 0b1111111 @ 0b11000 @ cs1 @ 0b000 @ cd @ 0b1011011 if (haveXcheri()) +mapping clause encdec = CInvokeLAL(cd, cs1) if (haveXcheri()) <-> 0b1111111 @ 0b11001 @ cs1 @ 0b000 @ cd @ 0b1011011 if (haveXcheri()) + mapping clause encdec = CRRL(rd, rs1) if (haveXcheri()) <-> 0b1111111 @ 0b01000 @ rs1 @ 0b000 @ rd @ 0b1011011 if (haveXcheri()) mapping clause encdec = CRAM(rd, rs1) if (haveXcheri()) <-> 0b1111111 @ 0b01001 @ rs1 @ 0b000 @ rd @ 0b1011011 if (haveXcheri()) @@ -2403,6 +2489,9 @@ mapping clause assembly = JALR_PCC(rd, rs1) <-> "jalr.pcc" ^ spc() ^ reg_ mapping clause assembly = CLoadTags(rd, cs1) <-> "cloadtags" ^ spc() ^ reg_name(rd) ^ sep() ^ "(" ^ cap_reg_name(cs1) ^ ")" +mapping clause assembly = CSealL(rd, cs1) <-> "cseall" ^ spc() ^ reg_name(rd) ^ sep() ^ "(" ^ cap_reg_name(cs1) ^ ")" +mapping clause assembly = CInvokeLAL(rd, cs1) <-> "cinvokelal" ^ spc() ^ reg_name(rd) ^ sep() ^ "(" ^ cap_reg_name(cs1) ^ ")" + mapping clause assembly = CRRL(rd, rs1) <-> "crrl" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) mapping clause assembly = CRAM(rd, rs1) <-> "cram" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) diff --git a/src/cheri_types.sail b/src/cheri_types.sail index 2ae8f5f0..e89cad10 100644 --- a/src/cheri_types.sail +++ b/src/cheri_types.sail @@ -63,6 +63,7 @@ let reserved_otypes = 4 let otype_unsealed = -1 let otype_sentry = -2 /* Sealed erstwhile or prospective PCC */ +let otype_isentry_pcc = -3 /* Sealed erstwhile IDC pointing at PCC */ enum CPtrCmpOp = { CEQ,