Add an implementation of the proposed CRelocate instruction

src/cheri_cap_common.sail

@@ -549,14 +549,66 @@ function capToString (cap) = {
   concat_str(BitStr(getCapBaseBits(cap)),
   concat_str(" length:", len_str)))))))))))))
 }
-function getRepresentableAlignmentMask(len) : xlenbits -> xlenbits = {
-  let (exact, c) = setCapBounds(default_cap, to_bits(sizeof(xlen), 0), 0b0 @ len);
+
+function getBoundsAlignmentMask(c) : Capability -> xlenbits = {
   let e = min(unsigned(c.E), cap_max_E);
   let e' = if c.internal_E then e + internal_E_take_bits else 0;
   ones(sizeof(xlen)-e') @ zeros(e')
 }
 
+function getRepresentableAlignmentMask(len) : xlenbits -> xlenbits = {
+  let (exact, c) = setCapBounds(default_cap, to_bits(sizeof(xlen), 0), 0b0 @ len);
+  getBoundsAlignmentMask(c)
+}
+
 function getRepresentableLength(len) : xlenbits -> xlenbits = {
   let m = getRepresentableAlignmentMask(len);
   (len + ~(m)) & m
 }
+
+function relocateCap(cap, offset) : (Capability, CapAddrBits) -> (bool, Capability) = {
+  let E = min(cap_max_E, unsigned(cap.E));
+  let a : CapAddrBits = cap.address;
+  let a_mid = truncate(a >> E, cap_mantissa_width);
+  let a3 = truncate(a >> (E + cap_mantissa_width - 3), 3);
+  let B3 = truncateLSB(cap.B, 3);
+  let R3 = B3 - 0b001; /* wraps */
+  let aHi = if a3 <_u R3 then 1 else 0;
+  let bHi = if B3 <_u R3 then 1 else 0;
+  let correction_base = bHi - aHi;
+
+  Aoffset : CapAddrBits = offset;
+  if cap.internal_E then {
+    Aoffset[E + internal_E_take_bits - 1..0] = zeros();
+  };
+
+  let BToffset : bits(cap_mantissa_width) = truncate(Aoffset >> E, cap_mantissa_width);
+
+  newB = cap.B + BToffset;
+  newT = cap.T + BToffset;
+  if E > cap_max_E - 2 then {
+    let msbs = E - (cap_max_E - 2);
+    let lsbs = cap_mantissa_width - msbs;
+    let BLsbsCarry = if newB[lsbs - 1..0] <_u cap.B[lsbs - 1..0] then 0b11 else 0b00;
+    let BTuncarry = truncate(BLsbsCarry @ zeros(lsbs), cap_mantissa_width);
+    newB = newB + BTuncarry;
+    newT = newT + BTuncarry;
+  };
+
+  let new_a_mid = truncate((a + Aoffset) >> E, cap_mantissa_width);
+  let newA3 = truncate((a + Aoffset) >> (E + cap_mantissa_width - 3), 3);
+  let newB3 = truncateLSB(newB, 3);
+  let newR3 = newB3 - 0b001;
+  let newAHi = if newA3 <_u newR3 then 1 else 0;
+  let newBHi = if newB3 <_u newR3 then 1 else 0;
+  let new_correction_base = newBHi - newAHi;
+  let Acorrection = to_bits(cap_addr_width, correction_base - new_correction_base);
+  let Acarry = if new_a_mid <_u a_mid then 1 else 0;
+  let Bcarry = if newB <_u cap.B then 1 else 0;
+  Aoffset = Aoffset + ((Acorrection + Bcarry - Acarry) << (E + cap_mantissa_width));
+  let newA = a + Aoffset;
+
+  let lostSignificant = Aoffset != offset;
+  let newCap = {cap with B = newB, T = newT, address = newA};
+  (lostSignificant, newCap)
+}

src/cheri_insts.sail

@@ -854,6 +854,39 @@ function clause execute (CFromPtr(cd, cs1, rs2)) = {
   }
 }
 
+union clause ast = CRelocate : (regidx, regidx, regidx)
+/*!
+ * Capability register *cd* is set equal to capability register *cs1*, with the
+ * **tag** field cleared, and its **base** and **address* replaced with
+ * *cs1*.**base** $+$ *rs2* and *cs1*.**address** $+$ *rs2* respectively,
+ * subject to representability. If the resulting capability is not
+ * representable, the value of *rs2* as used for both calculations is
+ * truncated, and for out-of-bounds capabilities where the **address* is not
+ * representable with the requested **base** the **address** is further
+ * adjusted to yield the requested **base**.
+ *
+ * ## Notes
+ *
+ * This instruction is designed to accelerate relocating capabilities in
+ * position-independent code at load time which will then be given to
+ * [CBuildCap].
+ *
+ * Unlike instructions like [CIncOffset] where unrepresentable capabilities
+ * result in changing the **base** but keeping the **address**, this
+ * instruction instead keeps the **base** but changes the **address** in order
+ * to avoid introducing accidental aliasing for invalid requests where *rs2* is
+ * nevertheless sufficiently aligned.
+ */
+function clause execute(CRelocate(cd, cs1, rs2)) = {
+  let cs1_val = C(cs1);
+  let rs2_val = X(rs2);
+
+  let cd1      = invalidateCap(cs1_val);
+  let (_, cd2) = relocateCap(cd1, rs2_val);
+  C(cd) = cd2;
+  RETIRE_SUCCESS
+}
+
 union clause ast = CBuildCap : (regidx, regidx, regidx)
 /*!
  * Capability register *cd* is set equal to capability register *cs1* with its
@@ -2421,6 +2454,7 @@ mapping clause encdec = CSetBoundsExact(cd, cs1, rs2) if (haveXcheri()) <-> 0b00
 mapping clause encdec = CBuildCap(cd, cs1, cs2)   if (haveXcheri()) <-> 0b0011101 @ cs2 @ cs1 @ 0b000 @ cd @ 0b1011011 if (haveXcheri())
 mapping clause encdec = CCopyType(cd, cs1, cs2)   if (haveXcheri()) <-> 0b0011110 @ cs2 @ cs1 @ 0b000 @ cd @ 0b1011011 if (haveXcheri())
 mapping clause encdec = CCSeal(cd, cs1, cs2)      if (haveXcheri()) <-> 0b0011111 @ cs2 @ cs1 @ 0b000 @ cd @ 0b1011011 if (haveXcheri())
+mapping clause encdec = CRelocate(cd, cs1, rs2)   if (haveXcheri()) <-> 0b0010101 @ rs2 @ cs1 @ 0b000 @ cd @ 0b1011011 if (haveXcheri())
 
 mapping clause encdec = CToPtr(rd, cs1, cs2)      if (haveXcheri()) <-> 0b0010010 @ cs2 @ cs1 @ 0b000 @ rd @ 0b1011011 if (haveXcheri())
 mapping clause encdec = CFromPtr(cd, cs1, rs2)    if (haveXcheri()) <-> 0b0010011 @ rs2 @ cs1 @ 0b000 @ cd @ 0b1011011 if (haveXcheri())
@@ -2446,6 +2480,7 @@ mapping clause assembly = CSetBoundsExact(cd, cs1, rs2) <-> "csetboundsexact" ^
 mapping clause assembly = CBuildCap(cd, cs1, cs2) <-> "cbuildcap"   ^ spc() ^ cap_reg_name(cd) ^ sep() ^ cap_reg_name(cs1) ^ sep() ^ cap_reg_name(cs2)
 mapping clause assembly = CCopyType(cd, cs1, cs2) <-> "ccopytype"   ^ spc() ^ cap_reg_name(cd) ^ sep() ^ cap_reg_name(cs1) ^ sep() ^ cap_reg_name(cs2)
 mapping clause assembly = CCSeal(cd, cs1, cs2)    <-> "ccseal"      ^ spc() ^ cap_reg_name(cd) ^ sep() ^ cap_reg_name(cs1) ^ sep() ^ cap_reg_name(cs2)
+mapping clause assembly = CRelocate(cd, cs1, rs2) <-> "crelocate"   ^ spc() ^ cap_reg_name(cd) ^ sep() ^ cap_reg_name(cs1) ^ sep() ^ reg_name(rs2)
 
 mapping clause assembly = CToPtr(rd, cs1, cs2)    <-> "ctoptr"      ^ spc() ^ reg_name(rd) ^ sep() ^ cap_reg_name(cs1) ^ sep() ^ cap_reg_name(cs2)
 mapping clause assembly = CFromPtr(cd, cs1, rs2)  <-> "cfromptr"    ^ spc() ^ cap_reg_name(cd) ^ sep() ^ cap_reg_name(cs1) ^ sep() ^ reg_name(rs2)