diff options
| author | Robert Norton | 2017-10-31 16:09:46 +0000 |
|---|---|---|
| committer | Robert Norton | 2017-10-31 16:09:46 +0000 |
| commit | a35692d69681683c2bffe7c824ad230b88679ed9 (patch) | |
| tree | 2b0962eb00a62c581a5eced904fa6451687cc382 /src | |
| parent | b41ee79485e155f67099b007650d73f449db1961 (diff) | |
cheri: throw an exception if there is an attempt to access C26/IDC in the delay slot of a ccall selector 1 call.
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/run_with_elf_cheri.ml | 2 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf_cheri128.ml | 2 |
2 files changed, 4 insertions, 0 deletions
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 *) |