Add builtin for reversing endianness

5 files changed, 17 insertions, 4 deletions

diff --git a/lib/ocaml_rts/sail_lib.ml b/lib/ocaml_rts/sail_lib.ml
index c550b2ce..20d3e281 100644
--- a/lib/ocaml_rts/sail_lib.ml
+++ b/lib/ocaml_rts/sail_lib.ml
@@ -376,6 +376,10 @@ let read_ram (addr_size, data_size, hex_ram, addr) =
   in
   read_byte data_size
 
+let rec reverse_endianness bits =
+  if List.length bits <= 8 then bits else
+  reverse_endianness (drop 8 bits) @ (take 8 bits)
+
 (* FIXME: Casts can't be externed *)
 let zcast_unit_vec x = [x]
 
diff --git a/lib/prelude.sail b/lib/prelude.sail
index b7403057..8cc1b86d 100644
--- a/lib/prelude.sail
+++ b/lib/prelude.sail
@@ -126,6 +126,9 @@ val extern forall Num 'n, Num 'l, Order 'ord. vector<'n,'l,'ord,bit> -> list<bit
 (* MSB *)
 val forall Num 'n, Num 'm, Order 'ord. vector<'n, 'm, 'ord, bit> -> bit effect pure most_significant
 
+(* Endianness *)
+val extern forall Num 'n, Num 'm, Order 'ord. vector<'n, 8 * 'm, 'ord, bit> -> vector<'n, 8 * 'm, 'ord, bit> effect pure reverse_endianness
+
 (* List functions *)
 
 val extern forall Type 'a. (int, list<'a>) -> list<'a> effect pure list_take
diff --git a/mips_new_tc/mips_prelude.sail b/mips_new_tc/mips_prelude.sail
index 128c63d8..c026c85f 100644
--- a/mips_new_tc/mips_prelude.sail
+++ b/mips_new_tc/mips_prelude.sail
@@ -577,7 +577,7 @@ function (bool) isAddressAligned ((bit[64]) addr, (WordType) wordType) =
   let a = unsigned(addr) in
   ((a quot alignment_width) == (a + wordWidthBytes(wordType) - 1) quot alignment_width)
 
-val forall Nat 'W, 'W >= 1. ([:'W:], bit[8 * 'W]) -> bit[8 * 'W] effect pure reverse_endianness'
+(*val forall Nat 'W, 'W >= 1. ([:'W:], bit[8 * 'W]) -> bit[8 * 'W] effect pure reverse_endianness'
 
 function rec forall Nat 'W, 'W >= 1. bit[8 * 'W] reverse_endianness' (w, value) =
 {
@@ -592,7 +592,7 @@ val forall Nat 'W, 'W >= 1. bit[8 * 'W] -> bit[8 * 'W] effect pure reverse_endia
 function rec forall Nat 'W, 'W >= 1. bit[8 * 'W] reverse_endianness ((bit[8 * 'W]) value) =
 {
     reverse_endianness'(sizeof 'W, value)
-}
+}*)
 
 function forall Nat 'n, 1 <= 'n, 'n <= 8. (bit[8 * 'n]) effect { rmem } MEMr_wrapper ((bit[64]) addr, ([:'n:]) size) =
     if (addr == 0x000000007f000000) then
diff --git a/mips_new_tc/mips_wrappers.sail b/mips_new_tc/mips_wrappers.sail
index c5eb6cf4..70033977 100644
--- a/mips_new_tc/mips_wrappers.sail
+++ b/mips_new_tc/mips_wrappers.sail
@@ -38,7 +38,7 @@
 val forall Nat 'n, 'n >= 1, 'n <= 8. (bit[64], [:'n:], bit[8 * 'n]) -> unit effect {eamem, wmv, wreg} MEMw_wrapper
 
 function unit MEMw_wrapper((bit[64]) addr, ([:'n:]) size, (bit[8 * 'n]) data) =
-    let ledata = reverse_endianness'(sizeof 'n, data) in
+    let ledata = reverse_endianness(data) in
     if (addr == 0x000000007f000000) then
       {
         UART_WDATA   := ledata[7..0];
@@ -53,7 +53,7 @@ val forall Nat 'n, 'n >= 1, 'n <= 8. (bit[64], [:'n:], bit[8 * 'n]) -> bool effe
 function bool MEMw_conditional_wrapper(addr, size, data) =
     {
       MEMea_conditional(addr, size);
-      MEMval_conditional(addr, size, reverse_endianness'(sizeof 'n, data))
+      MEMval_conditional(addr, size, reverse_endianness(data))
     }
 
 function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) =
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 96886199..bd18cf81 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -450,6 +450,12 @@ let address_of_bitv v =
   let bytes = bytes_of_bitv v in
   address_of_byte_list bytes
 
+let rec reverse_endianness_bl bits =
+  if List.length bits <= 8 then bits else
+    list_append(reverse_endianness_bl(list_drop(8, bits)), list_take(8, bits))
+
+val reverse_endianness : forall 'a. Bitvector 'a => 'a -> 'a
+let reverse_endianness v = of_bits (reverse_endianness_bl (bits_of v))
 
 
 (*** Registers *)