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, 17 insertions, 10 deletions

diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml
index d160e84a..213acea1 100644
--- a/src/gen_lib/sail_values.ml
+++ b/src/gen_lib/sail_values.ml
@@ -889,18 +889,25 @@ let shift_op_vec_int op (l,r) =
     let len = Array.length array in
     (match op with
      | "<<" ->
-       let left = Array.sub array r (len - r) in
-       let right = Array.make r Vzero in
-       let result = Array.append left right in
-       Vvector(result, start, ord)
+       if (r <= len) then
+         let left = Array.sub array r (len - r) in
+         let right = Array.make r Vzero in
+         let result = Array.append left right in
+         Vvector(result, start, ord)
+       else
+         Vvector(Array.make len Vzero, start, ord)
      | ">>" ->
-       let left = Array.make r Vzero in
-       let right = Array.sub array 0 (len - r) in
-       let result = Array.append left right in
-       Vvector(result, start, ord)
+       if (r <= len) then
+         let left = Array.make r Vzero in
+         let right = Array.sub array 0 (len - r) in
+         let result = Array.append left right in
+         Vvector(result, start, ord)
+       else
+         Vvector(Array.make len Vzero, start, ord)
      | "<<<" ->
-       let left = Array.sub array r (len - r) in
-       let right = Array.sub array 0 r in
+       let rmod = r mod len in
+       let left = Array.sub array rmod (len - rmod) in
+       let right = Array.sub array 0 rmod in
        let result = Array.append left right in
        Vvector(result, start, ord)
      | _ -> assert false)