the interpreter/shallow expects little-endian memory-values

1 files changed, 34 insertions, 23 deletions

diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 6f1a052b..76d6c993 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -94,17 +94,13 @@ type memory_byte = byte_lifted (* of length 8 *) (*MSB first everywhere*)
 
 type memory_value = list memory_byte
 (* the list is of length >=1 *)
-(* for both big-endian (Power) and little-endian (ARM), the head of the
-     list is the byte stored at the lowest address *)
-(* for big-endian Power the head of the list is the most-significant
-   byte, in both the interpreter and machineDef* code. *)
-(* For little-endian ARM, the head of the list is the
-   least-significant byte in machineDef* code and the
-   most-significant byte in interpreter code, with the switch over
-   (a list-reverse) being done just inside the interpreter interface*)
-(* In other words, in the machineDef* code the lowest-address byte is first,
-   and in the interpreter code the most-significant byte is first *)
-
+(* the head of the list is the byte stored at the lowest address;
+when calling a Sail function with a wmv effect, the list significant 8
+bits of the bit vector passed to the function will be interpreted as
+the lowest address byte; similarly, when calling a Sail function with
+rmem effect, the lowest address byte will be placed in the list
+significant 8 bits of the bit vector returned by the function; this
+behaviour is consistent with little-endian. *)
 
 
 (* not sure which of these is more handy yet *)
@@ -941,6 +937,13 @@ val memory_value_undef : nat (*the number of bytes*) -> memory_value
 let memory_value_undef (width:nat) : memory_value = 
   List.replicate width byte_lifted_undef 
 
+val match_endianness : forall 'a. end_flag -> list 'a -> list 'a
+let match_endianness endian l =
+  match endian with
+  | E_little_endian -> l
+  | E_big_endian    -> List.reverse l
+  end
+
 (* lengths *)  
 
 val memory_value_length : memory_value -> nat
@@ -1104,6 +1107,12 @@ let address_of_byte_list bs =
   if List.length bs <> 8 then failwith "address_of_byte_list given list not of length 8" else 
   Address bs (integer_of_byte_list bs)
 
+let address_of_byte_lifted_list bls =
+  match maybe_all (List.map byte_of_byte_lifted bls) with
+  | Nothing -> Nothing
+  | Just bs -> Just (address_of_byte_list bs)
+  end
+
 (* operations on addresses *)
 
 val add_address_nat : address -> nat -> address 
@@ -1127,22 +1136,23 @@ let clear_low_order_bits_of_address a =
 
 
 val byte_list_of_memory_value : end_flag -> memory_value -> maybe (list byte)
-let byte_list_of_memory_value endian mv = 
-  let mv = if endian = E_big_endian then mv else List.reverse mv in
-  maybe_all (List.map byte_of_memory_byte mv)
-    
+let byte_list_of_memory_value endian mv =
+  match_endianness endian mv
+  $> List.map byte_of_memory_byte
+  $> maybe_all
+
 
-val integer_of_memory_value : end_flag -> memory_value -> maybe integer 
-let integer_of_memory_value endian (mv:memory_value):maybe integer = 
+val integer_of_memory_value : end_flag -> memory_value -> maybe integer
+let integer_of_memory_value endian (mv:memory_value):maybe integer =
   match byte_list_of_memory_value endian mv with
   | Just bs -> Just (integer_of_byte_list bs)
   | Nothing -> Nothing 
   end
 
-val memory_value_of_integer : end_flag  -> nat -> integer -> memory_value 
+val memory_value_of_integer : end_flag  -> nat -> integer -> memory_value
 let memory_value_of_integer endian (len:nat) (i:integer):memory_value =
-  let mv = List.map (byte_lifted_of_byte) (byte_list_of_integer len i) in
-  if endian = E_big_endian then mv else List.reverse mv
+  List.map byte_lifted_of_byte (byte_list_of_integer len i)
+  $> match_endianness endian
 
 
 val integer_of_register_value : register_value -> maybe integer 
@@ -1221,7 +1231,7 @@ let address_of_register_value (rv:register_value) : maybe address =
       end
   end
 
-let address_of_memory_value (endian: end_flag) (mv:memory_value) : maybe address = 
+let address_of_memory_value (endian: end_flag) (mv:memory_value) : maybe address =
   match byte_list_of_memory_value endian mv with
   | Nothing -> Nothing
   | Just bs -> 
@@ -1247,14 +1257,15 @@ let int_of_memory_byte (mb:memory_byte) : int =
 
 val memory_value_of_address_lifted : end_flag -> address_lifted -> memory_value
 let memory_value_of_address_lifted endian (Address_lifted bs _ :address_lifted) =
-  if endian = E_big_endian then bs else List.reverse bs
+  match_endianness endian bs
 
 val byte_list_of_address : address -> list byte
 let byte_list_of_address (Address bs _) : list byte = bs
 
 val memory_value_of_address : end_flag -> address -> memory_value
 let memory_value_of_address endian (Address bs _) =
-  List.map byte_lifted_of_byte (if endian = E_big_endian then bs else List.reverse bs)
+  match_endianness endian bs
+  $> List.map byte_lifted_of_byte
 
 val byte_list_of_opcode : opcode -> list byte
 let byte_list_of_opcode (Opcode bs) : list byte = bs