diff options
| -rw-r--r-- | cheri/cheri_prelude_common.sail | 4 | ||||
| -rw-r--r-- | mips/mips_wrappers.sail | 4 | ||||
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 3 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf.ml | 2 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf_cheri.ml | 2 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf_cheri128.ml | 2 |
6 files changed, 8 insertions, 9 deletions
diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail index 92e4f508..dd2ec99c 100644 --- a/cheri/cheri_prelude_common.sail +++ b/cheri/cheri_prelude_common.sail @@ -309,7 +309,7 @@ function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordTy (bit[64]) vAddr; (* XXX vAddr not truncated because top <= 2^64 and size > 0 *) } -function (bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) = { +function (bit[64]) TranslatePC ((bit[64]) vAddr) = { incrementCP0Count(); let pcc = capRegToCapStruct(PCC) in let base = getCapBase(pcc) in @@ -320,7 +320,7 @@ function (bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType else if ((absPC + 4) > top) then (raise_c2_exception_noreg(CapEx_LengthViolation)) else - TLBTranslate((bit[64]) absPC, accessType) (* XXX assert absPC never gets truncated due to above check and top <= 2^64 for valid caps *) + TLBTranslate((bit[64]) absPC, Instruction) (* XXX assert absPC never gets truncated due to above check and top <= 2^64 for valid caps *) } function unit checkCP2usable () = diff --git a/mips/mips_wrappers.sail b/mips/mips_wrappers.sail index b70853f0..b46e35be 100644 --- a/mips/mips_wrappers.sail +++ b/mips/mips_wrappers.sail @@ -54,12 +54,12 @@ function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) = function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) = addr -function (bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) = { +function (bit[64]) TranslatePC ((bit[64]) vAddr) = { incrementCP0Count(); if (vAddr[1..0] != 0b00) then (* bad PC alignment *) (SignalExceptionBadAddr(AdEL, vAddr)) else - TLBTranslate(vAddr, accessType) + TLBTranslate(vAddr, Instruction) } let have_cp2 = false diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index aad7418d..63dd0d76 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -466,8 +466,7 @@ let translate_address top_level end_flag thunk_name registers address = (fun _ -> Interp.resume int_mode (Interp.Thunk_frame - (E_aux (E_app (Id_aux (Id thunk_name) Interp_ast.Unknown) - [arg;E_aux (E_lit (L_aux (L_num 0) Interp_ast.Unknown)) (Interp_ast.Unknown,Nothing)]) + (E_aux (E_app (Id_aux (Id thunk_name) Interp_ast.Unknown) [arg]) (Interp_ast.Unknown, Nothing)) top_env Interp.eenv (Interp.emem "translate top level") Interp.Top) Nothing) in match (address_error) with diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml index 3538dd44..6ce5d5e8 100644 --- a/src/lem_interp/run_with_elf.ml +++ b/src/lem_interp/run_with_elf.ml @@ -1296,7 +1296,7 @@ let run () = (*NOTE: this is likely MIPS specific, so should probably pull from initial_system_state info on to translate or not, endian mode, and translate function name *) - let addr_trans = translate_address context E_little_endian "TranslateAddress" in + let addr_trans = translate_address context E_little_endian "TranslatePC" in if String.length(!raw_file) != 0 then load_raw_file prog_mem (Nat_big_num.of_int !raw_at) (open_in_bin !raw_file); reg := Reg.add "PC" (register_value_of_address startaddr_internal model_reg_d ) !reg; diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml index a0f2a951..546fe6c8 100644 --- a/src/lem_interp/run_with_elf_cheri.ml +++ b/src/lem_interp/run_with_elf_cheri.ml @@ -1388,7 +1388,7 @@ let run () = (*NOTE: this is likely MIPS specific, so should probably pull from initial_system_state info on to translate or not, endian mode, and translate function name *) - let addr_trans = translate_address context E_little_endian "TranslateAddress" in + let addr_trans = translate_address context E_little_endian "TranslatePC" in if String.length(!raw_file) != 0 then load_raw_file prog_mem (Nat_big_num.of_int !raw_at) (open_in_bin !raw_file); reg := Reg.add "PC" (register_value_of_address startaddr_internal model_reg_d ) !reg; diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml index 01e9bd2d..4c881b04 100644 --- a/src/lem_interp/run_with_elf_cheri128.ml +++ b/src/lem_interp/run_with_elf_cheri128.ml @@ -1388,7 +1388,7 @@ let run () = (*NOTE: this is likely MIPS specific, so should probably pull from initial_system_state info on to translate or not, endian mode, and translate function name *) - let addr_trans = translate_address context E_little_endian "TranslateAddress" in + let addr_trans = translate_address context E_little_endian "TranslatePC" in if String.length(!raw_file) != 0 then load_raw_file prog_mem (Nat_big_num.of_int !raw_at) (open_in_bin !raw_file); reg := Reg.add "PC" (register_value_of_address startaddr_internal model_reg_d ) !reg; |