From 29182cd14e228529b3e26ef901e927bde8d27345 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Tue, 24 Oct 2017 15:44:10 +0100
Subject: 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.

---
 src/gen_lib/sail_values.ml              | 27 +++++++++++++++++----------
 src/lem_interp/run_with_elf_cheri128.ml |  2 +-
 2 files changed, 18 insertions(+), 11 deletions(-)

(limited to 'src')

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)
diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml
index 3ad507bc..f4f319ea 100644
--- a/src/lem_interp/run_with_elf_cheri128.ml
+++ b/src/lem_interp/run_with_elf_cheri128.ml
@@ -665,7 +665,7 @@ let cheri_register_data_all = mips_register_data_all @ [
 
 let initial_stack_and_reg_data_of_MIPS_elf_file e_entry all_data_memory =
   let initial_stack_data = [] in 
-  let initial_cap_val_int = Nat_big_num.of_string "0x1fffe0000000800000000000000000000" in (* hex((0x80000 << 64) + (0x7fff << 113) + (1 << 128)) *)
+  let initial_cap_val_int = Nat_big_num.of_string "0x1fffe6000000100000000000000000000" in (* hex((0x10000 << 64) + (48 << 105) + (0x7fff << 113) + (1 << 128)) T=0x10000 E=48 perms=0x7fff tag=1 *)
   let initial_cap_val_reg = Sail_impl_base.register_value_of_integer 129 128 D_decreasing  initial_cap_val_int in
   let initial_register_abi_data : (string * Sail_impl_base.register_value) list = [
     ("CP0Status", Sail_impl_base.register_value_of_integer 32 31 D_decreasing (Nat_big_num.of_string "0x00400000"));
-- 
cgit v1.2.3