change reqiured to work with little endian interpreter.

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;