fix default cap value on cheri128 following previous changes -- E stored in registers is no longer xored with 48 so need to initialise it. Also use E and T values used by CHERI hw and adjust decoding functions appropriately. Fix shift functions for ocaml shallow embedding which failed to handle shifts greater than vector length.

1 files changed, 4 insertions, 4 deletions

diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail
index 9bc0e2d2..fbb4c21c 100644
--- a/cheri/cheri_prelude_128.sail
+++ b/cheri/cheri_prelude_128.sail
@@ -195,23 +195,23 @@ function [|-1:1|] a_top_correction((bit[20]) a_mid, (bit[20]) R, (bit[20]) bound
     }
 
 function uint64 getCapBase((CapStruct) c)  = 
-    let ([|45|])  E = min(unsigned(c.E), 45) in
+    let ([|48|])  E = min(unsigned(c.E), 48) in
     let (bit[20]) B = c.B in
     let (bit[65]) a = EXTZ(c.address) in
     let (bit[20]) R = B - 0x01000 in (* wraps *)
-    let (bit[20]) a_mid = a[(E + 19)..E] in
+    let (bit[20]) a_mid = mask(a >> E) in
     let correction = a_top_correction(a_mid, R, B) in
     let a_top = a >> (E+20) in
     let (bit[64]) base = EXTZ((a_top + correction) : B) << E in
     unsigned(base)
 
 function CapLen getCapTop ((CapStruct) c)  = 
-    let ([|45|])  E = min(unsigned(c.E), 45) in
+    let ([|48|])  E = min(unsigned(c.E), 48) in
     let (bit[20]) B = c.B in
     let (bit[20]) T = c.T in
     let (bit[65]) a = EXTZ(c.address)  in
     let (bit[20]) R = B - 0x01000 in (* wraps *)
-    let (bit[20]) a_mid = a[(E + 19)..E] in
+    let (bit[20]) a_mid = mask(a >> E) in
     let correction = a_top_correction(a_mid, R, T) in
     let a_top = a >> (E+20) in
     let (bit[65]) top1 = EXTZ((a_top + correction) : T) in