From 6f8e3fa503afd7f5d4f68be2f8af810703f0ffa6 Mon Sep 17 00:00:00 2001
From: Alexandre Joannou <aj443@cam.ac.uk>
Date: Thu, 28 Jan 2021 18:06:52 +0000
Subject: [PATCH] Fix setAddress representability bug spotted by Dapeng Gao
 (with jdw57 and pdr32)

---
 CHERICC_Fat.bsv | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/CHERICC_Fat.bsv b/CHERICC_Fat.bsv
index b5a60e8..2bc8c49 100644
--- a/CHERICC_Fat.bsv
+++ b/CHERICC_Fat.bsv
@@ -653,8 +653,9 @@ function VnD#(CapFat) setAddress(CapFat cap, CapAddr address, TempFields tf);
   Bool newAddrHi  = truncateLSB(ret.addrBits) < tf.repBoundTopBits;
   // Shift amount needed to look at only the bits above the mantissa.
   Exp toUpperBits = e + fromInteger(valueOf(MW));
-  CapAddr mask = -1 << toUpperBits;
-  CapAddr newAddrDiff = (cap.address&mask) - (address&mask);
+  CapAddrPlus1 mask = -1 << toUpperBits;
+  CapAddrPlus1 newAddrDiff =
+    (signExtend(cap.address)&mask) - (signExtend(address)&mask);
   // Assert that the bits above the mantissa are all equal.
   Bool inRepBounds = True;
   // If the difference between the upper bits of the new address and the