From 5faa709ecd5253003a3a9397ec71a4c628a71f18 Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Thu, 3 Oct 2024 19:48:30 +0000 Subject: [PATCH] CSetBoundsRoundDown implementation FIXES https://github.com/CHERIoT-Platform/cheriot-sail/issues/72 --- src/cheri_insts.sail | 44 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) diff --git a/src/cheri_insts.sail b/src/cheri_insts.sail index 3a967df..798ccba 100644 --- a/src/cheri_insts.sail +++ b/src/cheri_insts.sail @@ -596,6 +596,48 @@ function clause execute (CSetBoundsExact(cd, cs1, rs2)) = { RETIRE_SUCCESS } +/* + * Count trailing zeros; this is in the upstream RISC-V model but our submodule + * isn't new enough for it to be there, too. + */ +val LowestSetBit : forall 'N, 0 < 'N . bits('N) -> int +function LowestSetBit x = { + foreach (i from 0 to (sizeof('N) - 1) by 1 in dec) + if [x[i]] == 0b1 then return(i) else (); + return sizeof('N); +} + +union clause ast = CSetBoundsRoundDown : (regidx, regidx, regidx) +/*! + * Capability register *cd* is set to capability register *cs1* with its + * **base** field replaced with *cs1*.**address** and its **length** field + * replaced with the maximum exactly representable value no larger than + * the value in the integer register *rs2*. + * + * ## Notes + * - The same caveat regarding the order of the bounds check applies as for + * [CSetBounds]. + */ +function clause execute (CSetBoundsRoundDown(cd, cs1, rs2)) = { + let cs1_val = C(cs1); + let rs2_val = X(rs2); + + let newBase = cs1_val.address; + let maxLen = sail_zero_extend(sail_ones(cap_mantissa_width), sizeof(xlen)) + << LowestSetBit(newBase); + let reqLen = X(rs2); + let newLen = if unsigned(reqLen) > unsigned(maxLen) then maxLen else reqLen; + let inBounds = inCapBounds(cs1_val, newBase, unsigned(newLen)); + + let inCap = clearTagIfSealed(cs1_val); + let (exact, newCap) = setCapBounds(inCap, newBase, newLen); + + assert(exact, "CSetBoundsRoundDown must always result in an exact cap"); + + C(cd) = clearTagIf(newCap, not(inBounds)); + RETIRE_SUCCESS +} + union clause ast = CClearTag : (regidx, regidx) /*! * Capability register *cd* is replaced with the contents of *cs1*, with @@ -980,6 +1022,7 @@ mapping clause encdec = CSetHigh(cd, cs1, rs2) if (haveXcheri()) <-> 0b001011 mapping clause encdec = CIncAddr(cd, cs1, rs2) if (haveXcheri()) <-> 0b0010001 @ rs2 @ cs1 @ 0b000 @ cd @ 0b1011011 if (haveXcheri()) mapping clause encdec = CSetBounds(cd, cs1, rs2) if (haveXcheri()) <-> 0b0001000 @ rs2 @ cs1 @ 0b000 @ cd @ 0b1011011 if (haveXcheri()) mapping clause encdec = CSetBoundsExact(cd, cs1, rs2) if (haveXcheri()) <-> 0b0001001 @ rs2 @ cs1 @ 0b000 @ cd @ 0b1011011 if (haveXcheri()) +mapping clause encdec = CSetBoundsRoundDown(cd, cs1, rs2) if (haveXcheri()) <-> 0b0001010 @ rs2 @ cs1 @ 0b000 @ cd @ 0b1011011 if (haveXcheri()) mapping clause encdec = CSub(rd, cs1, cs2) if (haveXcheri()) <-> 0b0010100 @ cs2 @ cs1 @ 0b000 @ rd @ 0b1011011 if (haveXcheri()) @@ -999,6 +1042,7 @@ mapping clause assembly = CSetHigh(cd, cs1, rs2) <-> "csethigh" ^ spc() ^ ca mapping clause assembly = CIncAddr(cd, cs1, rs2) <-> "cincaddr" ^ spc() ^ cap_reg_name(cd) ^ sep() ^ cap_reg_name(cs1) ^ sep() ^ reg_name(rs2) mapping clause assembly = CSetBounds(cd, cs1, rs2) <-> "csetbounds" ^ spc() ^ cap_reg_name(cd) ^ sep() ^ cap_reg_name(cs1) ^ sep() ^ reg_name(rs2) mapping clause assembly = CSetBoundsExact(cd, cs1, rs2) <-> "csetboundsexact" ^ spc() ^ cap_reg_name(cd) ^ sep() ^ cap_reg_name(cs1) ^ sep() ^ reg_name(rs2) +mapping clause assembly = CSetBoundsRoundDown(cd, cs1, rs2) <-> "csetboundsrounddown" ^ spc() ^ cap_reg_name(cd) ^ sep() ^ cap_reg_name(cs1) ^ sep() ^ reg_name(rs2) mapping clause assembly = CSub(rd, cs1, cs2) <-> "csub" ^ spc() ^ reg_name(rd) ^ sep() ^ cap_reg_name(cs1) ^ sep() ^ cap_reg_name(cs2)