From 81f5025366c727af105b597207ce93a0ea0e2cba Mon Sep 17 00:00:00 2001 From: jon Date: Wed, 3 Jun 2020 11:09:19 +0100 Subject: [PATCH] Make setOffset precise. --- CHERICC_Fat.bsv | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/CHERICC_Fat.bsv b/CHERICC_Fat.bsv index 836056a..c4e839f 100644 --- a/CHERICC_Fat.bsv +++ b/CHERICC_Fat.bsv @@ -623,15 +623,17 @@ function VnD#(CapFat) incOffsetFat(CapFat cap, LCapAddress pointer, Bit#(CapAddr // Select the appropriate toBounds value Bit#(MW) toBounds = (setOffset) ? toBounds_A : toBounds_B; Bit#(MW) toBoundsM1 = (setOffset) ? toBoundsM1_A : toBoundsM1_B; + Bool addrAtRepBound = !setOffset && (repBoundBits == cap.addrBits); // Implement the inLimit test Bool inLimits = False; if (posInc) begin // For a positive or null increment - inLimits = offsetBits < toBoundsM1; + // SetOffset is offsetting against base, which has 0 in the lower bits, so we don't need to be conservative. + inLimits = (setOffset) ? offsetBits <= toBoundsM1 : offsetBits < toBoundsM1; end else begin // For a negative increment - inLimits = (offsetBits >= toBounds) && (repBoundBits != cap.addrBits); + inLimits = (offsetBits >= toBounds) && !addrAtRepBound; end // Complete representable bounds check