diff options
| -rw-r--r-- | cheri/cheri_prelude_128.sail | 8 | ||||
| -rw-r--r-- | mips/run_embed.ml | 2 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.ml | 27 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf_cheri128.ml | 2 |
4 files changed, 23 insertions, 16 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 diff --git a/mips/run_embed.ml b/mips/run_embed.ml index 463caffd..9dd063b1 100644 --- a/mips/run_embed.ml +++ b/mips/run_embed.ml @@ -250,7 +250,7 @@ module CHERI128_model : ISA_model = struct let start_addr = (to_vec_dec_big (bi64, big_int_of_string "0x9000000040000000")) in set_register Cheri128_embed._nextPC start_addr; set_register_field_bit Cheri128_embed._CP0Status "BEV" Vone; - let initial_cap_val_int = big_int_of_string "0x1fffe0000000800000000000000000000" in (* hex((0x80000 << 64) + (0x7fff << 113) + (1 << 128)) *) + let initial_cap_val_int = big_int_of_string "0x1fffe6000000100000000000000000000" in (* hex((0x10000 << 64) + (48 << 105) + (0x7fff << 113) + (1 << 128)) T=0x10000 E=48 perms=0x7fff tag=1 *) let initial_cap_vec = to_vec_dec ((bi129), initial_cap_val_int) in set_register Cheri128_embed._PCC initial_cap_vec; set_register Cheri128_embed._nextPCC initial_cap_vec; 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")); |