From 55235837d2e89291324d9b92e737c23220511fbc Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Wed, 29 Mar 2017 16:55:22 +0100 Subject: change reqiured to work with little endian interpreter. --- cheri/cheri_insts.sail | 4 ++-- cheri/cheri_prelude_common.sail | 12 ++++++------ mips/mips_insts.sail | 2 +- mips/mips_prelude.sail | 13 ++++++++++++- mips/mips_wrappers.sail | 4 ++-- src/lem_interp/run_with_elf.ml | 2 +- src/lem_interp/run_with_elf_cheri.ml | 2 +- src/lem_interp/run_with_elf_cheri128.ml | 2 +- 8 files changed, 26 insertions(+), 15 deletions(-) diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail index 5882ec77..e40e684a 100644 --- a/cheri/cheri_insts.sail +++ b/cheri/cheri_insts.sail @@ -797,10 +797,10 @@ function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) = { CP0LLBit := 0b1; CP0LLAddr := pAddr; - MEMr_reserve(pAddr, widthBytes); + MEMr_reserve_wrapper(pAddr, widthBytes); } else - MEMr(pAddr, widthBytes); + MEMr_wrapper(pAddr, widthBytes); if (signext) then wGPR(rd) := EXTS(memResult) else diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail index 84161e95..95a81657 100644 --- a/cheri/cheri_prelude_common.sail +++ b/cheri/cheri_prelude_common.sail @@ -228,28 +228,28 @@ function (bool, bit[cap_size_t * 8]) MEMr_tagged ((bit[64]) addr) = { (* assumes addr is cap. aligned *) let ((bit[8]) tag : mem) = (MEMr_tag (addr, cap_size)) in - (tag[0], mem) + (tag[0], reverse_endianness(mem)) } function (bool, bit[cap_size_t * 8]) MEMr_tagged_reserve ((bit[64]) addr) = { (* assumes addr is cap. aligned *) let ((bit[8]) tag : mem) = (MEMr_tag_reserve (addr, cap_size)) in - (tag[0], mem) + (tag[0], reverse_endianness(mem)) } function unit MEMw_tagged((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) = { (* assumes addr is cap. aligned *) MEMea_tag(addr, cap_size); - MEMval_tag(addr, cap_size, 0b0000000 : [tag] : data); + MEMval_tag(addr, cap_size, 0b0000000 : [tag] : reverse_endianness(data)); } function bool MEMw_tagged_conditional((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) = { (* assumes addr is cap. aligned *) MEMea_tag_conditional(addr, cap_size); - MEMval_tag_conditional(addr, cap_size, 0b0000000 : [tag] : data); + MEMval_tag_conditional(addr, cap_size, 0b0000000 : [tag] : reverse_endianness(data)); } function (bit[64]) align((bit[64]) addr, (nat) alignment) = @@ -269,14 +269,14 @@ function unit effect {wmem} MEMw_wrapper(addr, size, data) = should probably be done in memory model. *) TAGw(align(addr, cap_size), 0x00); MEMea(addr,size); - MEMval(addr, size, data); + MEMval(addr, size, reverse_endianness(data)); } function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) = { (* On cheri non-capability writes must clear the corresponding tag*) MEMea_conditional(addr, size); - success := MEMval_conditional(addr,size,data); + success := MEMval_conditional(addr,size,reverse_endianness(data)); if (success) then (* XXX as above TAGw is vestigal and must die *) TAGw(align(addr, cap_size), 0x00); diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail index 07ded875..285d3011 100644 --- a/mips/mips_insts.sail +++ b/mips/mips_insts.sail @@ -1129,7 +1129,7 @@ function clause execute (Load(width, signed, linked, base, rt, offset)) = { CP0LLBit := 0b1; CP0LLAddr := pAddr; - MEMr_reserve(pAddr, wordWidthBytes(width)); + MEMr_reserve_wrapper(pAddr, wordWidthBytes(width)); } else MEMr_wrapper(pAddr, wordWidthBytes(width)); diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail index 3643d211..22e2f138 100644 --- a/mips/mips_prelude.sail +++ b/mips/mips_prelude.sail @@ -574,6 +574,14 @@ function (bool) isAddressAligned (addr, (WordType) wordType) = let a = unsigned(addr) in ((a quot alignment_width) == (a + wordWidthBytes(wordType) - 1) quot alignment_width) +val forall Nat 'W. bit[8 * 'W] -> bit[8 * 'W] effect pure reverse_endianness +function rec forall Nat 'W . bit[8 * 'W] reverse_endianness ((bit[8 * 'W]) value) = +{ + (nat) width := length(value); + if width <= 8 then value + else value[7..0] : reverse_endianness(value[(width - 1) .. 8]) +} + function forall Nat 'n. (bit[8 * 'n]) effect { rmem } MEMr_wrapper ((bit[64]) addr, ([:'n:]) size) = if (addr == 0x000000007f000000) then { @@ -586,4 +594,7 @@ function forall Nat 'n. (bit[8 * 'n]) effect { rmem } MEMr_wrapper ((bit[64]) ad else if (addr == 0x000000007f000004) then mask(0x000000000004ffff) (* Always plenty of write space available and jtag activity *) else - MEMr(addr, size) + reverse_endianness(MEMr(addr, size)) (* MEMr assumes little endian *) + +function forall Nat 'n. (bit[8 * 'n]) effect { rmem } MEMr_reserve_wrapper ((bit[64]) addr , ([:'n:]) size) = + reverse_endianness(MEMr_reserve(addr, size)) diff --git a/mips/mips_wrappers.sail b/mips/mips_wrappers.sail index 357aa9dd..b70853f0 100644 --- a/mips/mips_wrappers.sail +++ b/mips/mips_wrappers.sail @@ -42,13 +42,13 @@ function unit effect {wmem} MEMw_wrapper(addr, size, data) = UART_WRITTEN := 1; } else { MEMea(addr, size); - MEMval(addr, size, data); + MEMval(addr, size, reverse_endianness(data)); } function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) = { MEMea_conditional(addr, size); - MEMval_conditional(addr, size, data) + MEMval_conditional(addr, size, reverse_endianness(data)) } function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) = diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml index 813bef3a..3538dd44 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_big_endian "TranslateAddress" in + let addr_trans = translate_address context E_little_endian "TranslateAddress" 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 d58a6bd0..a0f2a951 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_big_endian "TranslateAddress" in + let addr_trans = translate_address context E_little_endian "TranslateAddress" 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 37685233..01e9bd2d 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_big_endian "TranslateAddress" in + let addr_trans = translate_address context E_little_endian "TranslateAddress" 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; -- cgit v1.2.3