diff --git a/CHERICC_Fat.bsv b/CHERICC_Fat.bsv index ace1807..14ba193 100644 --- a/CHERICC_Fat.bsv +++ b/CHERICC_Fat.bsv @@ -278,6 +278,11 @@ function BoundsInfo#(CapAddrW) getBoundsInfoFat (CapFat cap, TempFields tf) Bit #(fullW) topBitsFull = zeroExtend (topBits) << exp; Bit #(fullW) repBoundBitsFull = zeroExtend (repBoundBits) << exp; + // other helper values + CapAddr capAddr0 = 0; + CapAddrPlus1 addrSpaceTop = {1'b1, capAddr0}; + Bool alwaysRep = exp >= resetExp - 2; + // shared +1 and -1/~0 shifted by exponent Bit #(upperW) allOnesExpShifted = ~0 << exp; let mask = allOnesExpShifted; @@ -341,22 +346,34 @@ function BoundsInfo#(CapAddrW) getBoundsInfoFat (CapFat cap, TempFields tf) ////////////////////////////////////////////////////////////////////////////// // Use the "lo" region upper bits of the address, append implied zeroes in the - // lower bits, and or in the representable bound bits + // lower bits, and or in the representable bound bit. + // Saturate to zero when in the "always representable" case, + // i.e. exp >= resetExp - 2. CapAddr repBase = - truncate ({addrUpperLo, lowerZeroes} | repBoundBitsFull); + alwaysRep ? capAddr0 + : truncate ({addrUpperLo, lowerZeroes} | repBoundBitsFull); // compute repTop ////////////////////////////////////////////////////////////////////////////// // Use the "hi" region upper bits of the address, append implied zeroes in the // lower bits, and or in the representable bound bits - CapAddrPlus1 repTop = {addrUpperHi, lowerZeroes} | repBoundBitsFull; + // Saturate to 1 and all zeroes when in the "always representable" case, + // i.e. exp >= resetExp - 2. + CapAddrPlus1 repTop = + alwaysRep ? addrSpaceTop + : {addrUpperHi, lowerZeroes} | repBoundBitsFull; // compute repLength ////////////////////////////////////////////////////////////////////////////// CapAddrPlus1 repLength = {oneExpShifted, lowerZeroes}; + // compute split of representable space + ////////////////////////////////////////////////////////////////////////////// + + Bool repSplit = alwaysRep ? False : ! unpack (reduceOr (addrUpperHi)); + // return populated BoundsInfo structure ////////////////////////////////////////////////////////////////////////////// @@ -365,7 +382,8 @@ function BoundsInfo#(CapAddrW) getBoundsInfoFat (CapFat cap, TempFields tf) , length: length , repBase: repBase , repTop: repTop - , repLength: repLength }; + , repLength: repLength + , repSplit: repSplit }; endfunction function CapAddr getBotFat(CapFat cap, TempFields tf); diff --git a/CHERICap.bsv b/CHERICap.bsv index 684b34f..791060a 100644 --- a/CHERICap.bsv +++ b/CHERICap.bsv @@ -84,6 +84,7 @@ typedef struct { Bit #(addrW) repBase; Bit #(TAdd #(addrW, 1)) repTop; Bit #(TAdd #(addrW, 1)) repLength; + Bool repSplit; } BoundsInfo #(numeric type addrW) deriving (Bits, Eq, FShow); // helper types and functions @@ -272,13 +273,18 @@ typeclass CHERICap #( type capT // type of the CHERICap capability // Get the representable length function Bit #(TAdd #(addrW, 1)) getRepLength (capT cap) = getBoundsInfo(cap).repLength; + // Check if the capapbility's representable region is split (i.e. wrapping the + // address space) + function Bool isRepSplit (capT cap) = getBoundsInfo(cap).repSplit; // Assertion that the capability's address is between its representable // base and top - function Bool isInRepBounds (capT cap, Bool isRepTopIncluded) = - belongsToRange ( zeroExtend (getAddr (cap)) - , zeroExtend (getRepBase (cap)) - , getRepTop (cap) - , isRepTopIncluded ); + function Bool isInRepBounds (capT cap); + let addr = getAddr (cap); + let bInfo = getBoundsInfo (cap); + let okLo = addr >= bInfo.repBase; + let okHi = zeroExtend (addr) < bInfo.repTop; + return (okLo && okHi) || (bInfo.repSplit && (okLo != okHi)); + endfunction // Check the alignment of the base, giving least significant 2 bits. function Bit #(2) getBaseAlignment (capT cap) = getBoundsInfo (cap).base[1:0];