the interpreter/shallow expects little-endian memory-values

3 files changed, 78 insertions, 62 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 8c80b1c1..03de0123 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -54,21 +54,21 @@ open import Interp_interface
 val intern_reg_value : register_value -> Interp.value
 val intern_mem_value : interp_mode -> direction -> memory_value -> Interp.value
 val extern_reg_value : reg_name -> Interp.value -> register_value
-val extern_mem_value : interp_mode -> Interp.value -> (memory_value * maybe (list reg_name))
+val extern_with_track: forall 'a. interp_mode -> (Interp.value -> 'a) -> Interp.value -> ('a * maybe (list reg_name))
+val extern_vector_value: Interp.value -> list byte_lifted
+val extern_mem_value :   Interp.value -> memory_value
 val extern_reg : Interp.reg_form -> maybe (nat * nat) -> reg_name
 
 let make_interpreter_mode eager_eval tracking_values = 
   <| Interp.eager_eval = eager_eval; Interp.track_values = tracking_values; Interp.track_lmem = false|>;;
 
-let make_mode eager_eval tracking_values endian = 
-  <|internal_mode = make_interpreter_mode eager_eval tracking_values;
-    endian = endian|>;;
-let make_mode_exhaustive endian = 
-  <| internal_mode = <| Interp.eager_eval = true; Interp.track_values = true; Interp.track_lmem = true|>;
-     endian = endian |>;;
+let make_mode eager_eval tracking_values =
+  <|internal_mode = make_interpreter_mode eager_eval tracking_values|>;;
+let make_mode_exhaustive =
+  <| internal_mode = <| Interp.eager_eval = true; Interp.track_values = true; Interp.track_lmem = true|> |>;;
 let tracking_dependencies mode = mode.internal_mode.Interp.track_values
-let make_eager_mode mode = <| mode with internal_mode = <|mode.internal_mode with Interp.eager_eval = true |> |>;;
-let make_default_mode _ = <|internal_mode = make_interpreter_mode false false; endian = E_big_endian|>;;
+let make_eager_mode mode = <| internal_mode = <|mode.internal_mode with Interp.eager_eval = true |> |>;;
+let make_default_mode = fun () -> <|internal_mode = make_interpreter_mode false false|>;;
 
 let bitl_to_ibit = function 
   | Bitl_zero -> (Interp.V_lit (L_aux L_zero Interp_ast.Unknown)) 
@@ -156,11 +156,12 @@ let intern_reg_value v = match v with
   | _ -> Interp.V_vector v.rv_start_internal (intern_direction v.rv_dir) (bitls_to_ibits v.rv_bits)
 end
 
-let intern_mem_value mode direction v = 
-  let v = if mode.endian = E_big_endian then v else List.reverse v in
-  let bits = (List.concatMap (fun (Byte_lifted bits) -> bitls_to_ibits bits) v) in
+let intern_mem_value mode direction v =
+  List.reverse v (* match little endian representation *)
+  $> List.concatMap (fun (Byte_lifted bits) -> bitls_to_ibits bits)
+  $> fun bits ->
   let direction = intern_direction direction in
-  Interp.V_vector (if Interp.is_inc(direction) then 0 else (List.length(bits) -1)) direction bits
+  Interp.V_vector (if Interp.is_inc direction then 0 else (List.length bits) -1) direction bits
 
 let intern_ifield_value direction v =
   let bits = bits_to_ibits v in
@@ -239,22 +240,27 @@ let rec extern_reg_value reg_name v =
          rv_start_internal = internal_start |>
 end 
 
-let rec extern_mem_value mode v = match v with
-  | Interp.V_track v regs -> 
-    let (external_v,_) = extern_mem_value mode v in
-    (external_v,
-     if mode.internal_mode.Interp.track_values 
+let extern_with_track mode f = function
+  | Interp.V_track v regs ->
+    (f v,
+     if mode.internal_mode.Interp.track_values
      then (Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList regs)))
      else Nothing)
-  | Interp.V_vector fst inc bits -> 
-    let bytes = to_bytes (bitls_from_ibits bits) in 
-    if mode.endian = E_big_endian 
-    then (bytes, Nothing)
-    else (List.reverse bytes, Nothing)
-  | Interp.V_vector_sparse fst stop inc bits default ->
-    extern_mem_value mode (Interp_lib.fill_in_sparse v)
-  | _ -> Assert_extra.failwith ("extern_mem_value received non-externable value " ^ (Interp.string_of_value v))
-end 
+  | v -> (f v, Nothing)
+  end
+
+let rec extern_vector_value v = match v with
+  | Interp.V_vector _fst _inc bits ->
+    bitls_from_ibits bits
+    $> to_bytes
+  | Interp.V_vector_sparse _fst _stop _inc _bits _default ->
+    Interp_lib.fill_in_sparse v
+    $> extern_vector_value
+  | _ -> Assert_extra.failwith ("extern_vector_value received non-externable value " ^ (Interp.string_of_value v))
+end
+
+let rec extern_mem_value v = List.reverse (extern_vector_value v)
+
 
 let rec extern_ifield_value i_name field_name v ftyp = match (v,ftyp) with
   | (Interp.V_track v regs,_) -> extern_ifield_value i_name field_name v ftyp
@@ -446,7 +452,7 @@ let build_context defs reads writes write_eas write_vals barriers externs =
 
 let translate_address top_level end_flag thunk_name registers address =
   let (Address bytes i) = address in
-  let mode = make_mode true false end_flag in
+  let mode = make_mode true false in
   let int_mode = mode.internal_mode in
   let (Context top_env direction _ _ _ _ _ _) = top_level in
   let intern_val = intern_mem_value mode direction (memory_value_of_address end_flag address) in
@@ -465,8 +471,7 @@ let translate_address top_level end_flag thunk_name registers address =
          top_env Interp.eenv (Interp.emem "translate top level") Interp.Top) Nothing) in
   match (address_error) with
   | Ivh_value addr ->
-    let (mem_v,_) = extern_mem_value mode addr in 
-    ((address_of_memory_value end_flag mem_v), events)
+    (address_of_byte_lifted_list (extern_vector_value addr), events)
   | Ivh_value_after_exn _ ->
     (Nothing, events)
   | Ivh_error err -> match err with
@@ -492,7 +497,7 @@ let intern_instruction direction (name,parms) =
     (Interp.V_tuple (List.map (value_of_instruction_param direction) parms))
 
 let instruction_analysis top_level end_flag thunk_name regn_to_reg_details registers instruction =
-  let mode = make_mode true false end_flag in
+  let mode = make_mode true false in
   let int_mode = mode.internal_mode in
   let (Context top_env direction _ _ _ _ _ _) = top_level in
   let intern_val = intern_instruction direction instruction in
@@ -540,7 +545,7 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
            Reg_field n start direction f (extern_slice direction start span)             
          | _ -> Assert_extra.failwith "Register footprint analysis did not return an element of the specified type" end
        in
-       let get_addr v = match address_of_memory_value end_flag (fst (extern_mem_value mode v)) with
+       let get_addr v = match address_of_byte_lifted_list (extern_vector_value v) with
          | Just addr -> addr
          | Nothing -> failwith "get_nia encountered invalid address" end in
        let dia_to_dia = function
@@ -783,7 +788,7 @@ let rec interp_to_outcome mode context thunk =
         (match List.lookup i mem_writes with
           | (Just (MW write_k f return)) -> 
             let (location, length, tracking) = (f mode loc_val) in
-            let (value, v_tracking) = (extern_mem_value mode write_val) in
+            let (value, v_tracking) = extern_with_track mode extern_mem_value write_val in
             if (List.length location) = 8
             then let address_int = match (maybe_all (List.map byte_of_byte_lifted location)) with
               | Just bs -> Just (integer_of_byte_list bs)
@@ -813,8 +818,8 @@ let rec interp_to_outcome mode context thunk =
             | (Just (MV parmf return)) -> 
               let (value, v_tracking) = 
                 match (Interp.detaint write_val) with
-                  | Interp.V_tuple[_;v] -> (extern_mem_value mode (Interp.retaint write_val v))
-                  | _ -> (extern_mem_value mode write_val) end in
+                  | Interp.V_tuple[_;v] -> extern_with_track mode extern_mem_value (Interp.retaint write_val v)
+                  | _ -> extern_with_track mode extern_mem_value write_val end in
                let location_opt = match parmf mode address_val with
                   | Nothing -> Nothing
                   | Just mv -> let address_int = match (maybe_all (List.map byte_of_byte_lifted mv)) with
@@ -967,7 +972,7 @@ let rec ie_loop mode register_values (IState interp_state context) =
   
 val interp_exhaustive : maybe (list (reg_name * register_value)) -> instruction_state -> list event
 let interp_exhaustive register_values i_state = 
-  let mode = make_mode_exhaustive E_big_endian in
+  let mode = make_mode_exhaustive in
   match ie_loop mode register_values i_state with
     | (events,_) -> events
 end
@@ -1294,7 +1299,7 @@ let interp_instruction_analysis
 
   (regs_in, regs_out, regs_feeding_address, nias, dia, inst_kind)
 
-let interp_handwritten_instruction_analysis context endianness instruction analysis_function reg_info environment = 
+let interp_handwritten_instruction_analysis context endianness instruction analysis_function reg_info environment =
   fst (instruction_analysis context endianness analysis_function
                             reg_info (Just environment) instruction)
 
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 3e94285c..3ef6abb8 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -164,8 +164,8 @@ type interpreter_state = Interp.stack (*Deem abstract*)
 (* Will come from a .lem file generated by Sail, bound to a 'defs' identifier *)
 type specification = Interp_ast.defs Interp.tannot (*Deem abstract*)
 type interpreter_mode = Interp.interp_mode (*Deem abstract*)
-type interp_mode = <| internal_mode: interpreter_mode; endian: end_flag |>
-val make_mode : (*eager*) bool -> (*tracking*) bool -> end_flag -> interp_mode
+type interp_mode = <| internal_mode: interpreter_mode |>
+val make_mode : (*eager*) bool -> (*tracking*) bool -> interp_mode
 val tracking_dependencies : interp_mode -> bool
 
 
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