diff options
| -rw-r--r-- | cheri/cheri_prelude_128.sail | 10 | ||||
| -rw-r--r-- | cheri/cheri_prelude_common.sail | 8 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf_cheri128.ml | 2 |
3 files changed, 12 insertions, 8 deletions
diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail index a96949a5..348bfc43 100644 --- a/cheri/cheri_prelude_128.sail +++ b/cheri/cheri_prelude_128.sail @@ -105,7 +105,7 @@ function CapStruct capRegToCapStruct((CapReg) c) = permit_execute = c[114]; global = c[113]; reserved = c[112..111]; - E = c[110..105]; + E = c[110..105] ^ 0b110000; sealed = s; B = B; T = T; @@ -132,7 +132,7 @@ function (bit[128]) capStructToMemBits((CapStruct) cap) = ( cap.uperms : getCapHardPerms(cap) : cap.reserved - : cap.E + : (cap.E ^ 0b110000) (* XXX brackets required otherwise sail interpreter error *) : [cap.sealed] : b : t @@ -155,7 +155,7 @@ function (bit[31]) getCapPerms((CapStruct) cap) = function CapStruct setCapPerms((CapStruct) cap, (bit[31]) perms) = { cap with uperms = perms[18..15]; -(* perm_reserved11_14 = (cap.perm_reserved11_14 & (perms[14..11]));*) + (* 14..11 reserved -- ignore *) access_system_regs = perms[10]; perm_reserved9 = perms[9]; perm_reserved8 = perms[8]; @@ -184,7 +184,7 @@ function int a_top_correction((bit[20]) a_mid, (bit[20]) R, (bit[20]) bound) = } function bit[64] getCapBase((CapStruct) c) = - let ([|63|]) E = unsigned(c.E) in + let ([|63|]) E = min(unsigned(c.E), 45) in let (bool) s = c.sealed in let (bit[20]) B = c.B in let (bit[64]) a = c.address in @@ -196,7 +196,7 @@ function bit[64] getCapBase((CapStruct) c) = base << E function bit[65] getCapTop((CapStruct) c) = - let ([|63|]) E = unsigned(c.E) in + let ([|63|]) E = min(unsigned(c.E), 45) in let (bool) s = c.sealed in let (bit[20]) B = c.B in let (bit[20]) T = c.T in diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail index 7530c9cc..5d88c43a 100644 --- a/cheri/cheri_prelude_common.sail +++ b/cheri/cheri_prelude_common.sail @@ -171,9 +171,13 @@ register CapCauseReg CapCause function forall Type 'o . 'o SignalException ((Exception) ex) = { + let pc = (bit[64]) PC in (* XXX Cast forces read of register. Sail bug? *) let pcc = capRegToCapStruct(PCC) in - let (success, epcc) = setCapOffset(pcc, PC) in - C31 := capStructToCapReg(epcc); + let (success, epcc) = setCapOffset(pcc, pc) in + if (success) then + C31 := capStructToCapReg(epcc) + else + C31 := capStructToCapReg(int_to_cap(pc)); (* XXX what if not success? *) nextPCC := C29; (* KCC *) delayedPCC := C29; (* always write delayedPCC together whether PCC so diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml index 99a6e681..bfffb562 100644 --- a/src/lem_interp/run_with_elf_cheri128.ml +++ b/src/lem_interp/run_with_elf_cheri128.ml @@ -623,7 +623,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 "0x1fffe5a00000800000000000000000000" in (* hex((0x80000 << 64) + (45 << 105) + (0x7fff << 113) + (1 << 128)) *) + let initial_cap_val_int = Nat_big_num.of_string "0x1fffe0000000800000000000000000000" in (* hex((0x80000 << 64) + (0x7fff << 113) + (1 << 128)) *) 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")); |