diff options
| -rw-r--r-- | cheri/cheri_insts.sail | 1 | ||||
| -rw-r--r-- | cheri/cheri_prelude_common.sail | 12 | ||||
| -rw-r--r-- | mips/run_embed.ml | 10 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf_cheri.ml | 2 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf_cheri128.ml | 2 |
5 files changed, 23 insertions, 4 deletions
diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail index 50399785..5687a275 100644 --- a/cheri/cheri_insts.sail +++ b/cheri/cheri_insts.sail @@ -1060,6 +1060,7 @@ function clause execute (CCall(cs, cb, 0b00000000001)) = (* selector=1 *) delayedPC := (bit[64]) (getCapOffset(cs_val)); delayedPCC := csUnsealed; branchPending := true; + inCCallDelay := true; C26 := capStructToCapReg({cb_val with sealed=false; otype=0; diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail index dcb56d01..fa36decb 100644 --- a/cheri/cheri_prelude_common.sail +++ b/cheri/cheri_prelude_common.sail @@ -35,6 +35,7 @@ register CapReg PCC register CapReg nextPCC register CapReg delayedPCC +register (bit[1]) inCCallDelay register CapReg C00 (* aka default data capability, DDC *) register CapReg C01 register CapReg C02 @@ -105,6 +106,7 @@ typedef CapEx = enumerate { CapEx_PermitSealViolation; CapEx_AccessSystemRegsViolation; CapEx_PermitCCallViolation; + CapEx_AccessCCallIDCViolation; } typedef CPtrCmpOp = enumerate { @@ -148,6 +150,7 @@ function (bit[8]) CapExCode((CapEx) ex) = case CapEx_PermitSealViolation -> 0x17 case CapEx_AccessSystemRegsViolation -> 0x18 case CapEx_PermitCCallViolation -> 0x19 + case CapEx_AccessCCallIDCViolation -> 0x1a } typedef CapCauseReg = register bits [15:0] { @@ -194,7 +197,11 @@ function forall Type 'o . 'o raise_c2_exception8((CapEx) capEx, (bit[8]) regnum) } function forall Type 'o . 'o raise_c2_exception((CapEx) capEx, (regno) regnum) = - raise_c2_exception8(capEx, 0b000 : regnum) + let reg8 = 0b000 : regnum in + if ((capEx == CapEx_AccessSystemRegsViolation) & (regnum == 26 (* IDC *))) then + raise_c2_exception8(CapEx_AccessCCallIDCViolation, reg8) + else + raise_c2_exception8(capEx, reg8) function forall Type 'o . 'o raise_c2_exception_noreg((CapEx) capEx) = raise_c2_exception8(capEx, 0xff) @@ -203,7 +210,8 @@ function bool pcc_access_system_regs () = let pcc = capRegToCapStruct(PCC) in (pcc.access_system_regs) -function bool register_inaccessible((regno) r) = +function bool register_inaccessible((regno) r) = + if ((r == 26 (* IDC *)) & inCCallDelay) then true else let is_sys_reg = switch(r) { case 0b11011 -> true case 0b11100 -> true diff --git a/mips/run_embed.ml b/mips/run_embed.ml index 9dd063b1..1bb6d5f6 100644 --- a/mips/run_embed.ml +++ b/mips/run_embed.ml @@ -219,7 +219,10 @@ module CHERI_model : ISA_model = struct let pc_vaddr = unsigned_big(Cheri_embed._PC) in let npc_addr = add_int_big_int 4 pc_vaddr in let npc_vec = to_vec_dec_big (bi64, npc_addr) in - set_register Cheri_embed._nextPC npc_vec + begin + set_register Cheri_embed._nextPC npc_vec; + set_register Cheri_embed._inCCallDelay (to_vec_dec_int (1, 0)) + end let get_pc () = unsigned_big (Cheri_embed._PC) @@ -277,7 +280,10 @@ module CHERI128_model : ISA_model = struct let pc_vaddr = unsigned_big(Cheri128_embed._PC) in let npc_addr = add_int_big_int 4 pc_vaddr in let npc_vec = to_vec_dec_big (bi64, npc_addr) in - set_register Cheri128_embed._nextPC npc_vec + begin + set_register Cheri128_embed._nextPC npc_vec; + set_register Cheri128_embed._inCCallDelay (to_vec_dec_int (1, 0)) + end let get_pc () = unsigned_big (Cheri128_embed._PC) diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml index b879f702..b50cb01d 100644 --- a/src/lem_interp/run_with_elf_cheri.ml +++ b/src/lem_interp/run_with_elf_cheri.ml @@ -493,6 +493,7 @@ let mips_register_data_all = [ ("PC", (D_decreasing, 64, 63)); ("branchPending", (D_decreasing, 1, 0)); ("inBranchDelay", (D_decreasing, 1, 0)); + ("inCCallDelay", (D_decreasing, 1, 0)); ("delayedPC", (D_decreasing, 64, 63)); ("nextPC", (D_decreasing, 64, 63)); (* General purpose registers *) @@ -1072,6 +1073,7 @@ let set_next_instruction_address model = begin reg := Reg.add "nextPC" n_pc !reg; reg := Reg.add "inBranchDelay" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg; + reg := Reg.add "inCCallDelay" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg; end | (Some pc_val, Some 1) -> (* delay slot -- branch to delayed PC and clear branchPending *) diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml index f4f319ea..148b29ae 100644 --- a/src/lem_interp/run_with_elf_cheri128.ml +++ b/src/lem_interp/run_with_elf_cheri128.ml @@ -493,6 +493,7 @@ let mips_register_data_all = [ ("PC", (D_decreasing, 64, 63)); ("branchPending", (D_decreasing, 1, 0)); ("inBranchDelay", (D_decreasing, 1, 0)); + ("inCCallDelay", (D_decreasing, 1, 0)); ("delayedPC", (D_decreasing, 64, 63)); ("nextPC", (D_decreasing, 64, 63)); (* General purpose registers *) @@ -1072,6 +1073,7 @@ let set_next_instruction_address model = begin reg := Reg.add "nextPC" n_pc !reg; reg := Reg.add "inBranchDelay" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg; + reg := Reg.add "inCCallDelay" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg; end | (Some pc_val, Some 1) -> (* delay slot -- branch to delayed PC and clear branchPending *) |