Extend mode and external memory functions with endian flag

2 files changed, 40 insertions, 29 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 26a44539..0ecd6fe7 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -8,16 +8,20 @@ open import Assert_extra
 
 
 val intern_reg_value : register_value -> Interp.value
-val intern_mem_value : direction -> memory_value -> Interp.value
+val intern_mem_value : interp_mode -> direction -> memory_value -> Interp.value
 val extern_reg_value : Interp.i_direction -> maybe nat -> Interp.value -> register_value
 val extern_mem_value : interp_mode -> Interp.value -> (memory_value * maybe (list reg_name))
 val extern_reg : Interp.reg_form -> maybe (nat * nat) -> reg_name
 
+let make_interp_mode eager_eval tracking_values = <| Interp.eager_eval = eager_eval; Interp.track_values = tracking_values|>;;
 
-let make_mode eager_eval tracking_values = <| Interp.eager_eval = eager_eval; Interp.track_values = tracking_values |>;;
-let tracking_dependencies mode = mode.Interp.track_values
-let make_eager_mode mode = <| mode with Interp.eager_eval = true |>;;
-let make_default_mode _ = <| Interp.eager_eval = false; Interp.track_values = false |>;;
+let make_mode eager_eval tracking_values endian = 
+  <|internal_mode = make_interp_mode eager_eval tracking_values;
+    endian = endian|>;;
+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 = <| Interp.eager_eval = false; Interp.track_values = false |>;
+                            endian = E_big_endian|>;;
 
 let bitl_to_ibit = function 
   | Bitl_zero -> (Interp.V_lit (L_aux L_zero Interp_ast.Unknown)) 
@@ -101,7 +105,8 @@ 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 direction v = 
+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 direction = intern_direction direction in
   Interp.V_vector (if Interp.is_inc(direction) then 0 else (List.length(bits) -1)) direction bits
@@ -187,8 +192,12 @@ 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.Interp.track_values then (Just (List.map (fun r -> extern_reg r Nothing) regs)) else Nothing)
-  | Interp.V_vector fst inc bits -> (to_bytes (bitls_from_ibits bits), Nothing)
+     if mode.internal_mode.Interp.track_values then (Just (List.map (fun r -> extern_reg r Nothing) 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))
@@ -272,8 +281,8 @@ let coerce_Bitvector_of_Bytevector (v: value) : value =
 let initial_instruction_state top_level main args = 
   let e_args = match args with
     | [] -> [E_aux (E_lit (L_aux L_unit Interp_ast.Unknown)) (Interp_ast.Unknown,Nothing)]
-    | [arg] -> let (e,_) = Interp.to_exp (make_mode true false) Interp.eenv (intern_reg_value arg) in [e]
-    | args -> List.map fst (List.map (Interp.to_exp (make_mode true false) Interp.eenv)
+    | [arg] -> let (e,_) = Interp.to_exp (make_interp_mode true false) Interp.eenv (intern_reg_value arg) in [e]
+    | args -> List.map fst (List.map (Interp.to_exp (make_interp_mode true false) Interp.eenv)
 			      (List.map intern_reg_value args)) end in
   Interp.Thunk_frame (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) e_args) (Interp_ast.Unknown, Nothing)) 
     top_level Interp.eenv Interp.emem Interp.Top
@@ -287,7 +296,7 @@ let rec interp_to_value_helper arg instr direction thunk =
       match List.lookup i (Interp_lib.library_functions direction) with
 	| Nothing -> (Nothing, Just (Internal_error ("External function not available " ^ i)))
 	| Just f  -> 
-          interp_to_value_helper arg instr direction (fun _ -> Interp.resume (make_mode true false) stack (Just (f value)))
+          interp_to_value_helper arg instr direction (fun _ -> Interp.resume (make_interp_mode true false) stack (Just (f value)))
       end 
     | Interp.Action (Interp.Exit (E_aux e _)) _ ->
       match e with
@@ -330,13 +339,13 @@ let migrate_typ = function
 end
 
 let decode_to_istate top_level value = 
-  let mode = make_mode true false in
+  let mode = make_interp_mode true false in
   let (Context ((Interp.Env _ instructions _ _ _ _ _ _) as top_env) direction _ _ _ _) = top_level in
   let (arg,_) = Interp.to_exp mode Interp.eenv (intern_opcode direction value) in
   let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
   let (instr_decoded,error) = interp_to_value_helper value ("",[],[]) internal_direction
     (fun _ -> Interp.resume 
-      (make_mode true false) 
+      mode 
       (Interp.Thunk_frame 
 	 (E_aux (E_app (Id_aux (Id "decode") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown, Nothing)) 
 	 top_env Interp.eenv Interp.emem Interp.Top) Nothing) in
@@ -360,8 +369,8 @@ let decode_to_istate top_level value =
       let (arg,_) = Interp.to_exp mode Interp.eenv instr in
       let (instr_decoded,error) = interp_to_value_helper value instr_external internal_direction
 	(fun _ -> Interp.resume 
-	 (make_mode true false) 
-	 (Interp.Thunk_frame 
+	 mode
+	  (Interp.Thunk_frame 
 	 (E_aux (E_app (Id_aux (Id "supported_instructions") Interp_ast.Unknown) [arg]) 
 	    (Interp_ast.Unknown, Nothing)) 
 	 top_env Interp.eenv Interp.emem Interp.Top) Nothing) in
@@ -387,7 +396,7 @@ let decode_to_instruction (top_level:context) (value:opcode) : instruction_or_de
 
 val instruction_to_istate : context -> instruction -> instruction_state 
 let instruction_to_istate (top_level:context) (((name, parms, _) as instr):instruction) : instruction_state  = 
-  let mode = make_mode true false in
+  let mode = make_interp_mode true false in
   let (Context top_env direction _ _ _ _) = top_level in
   let get_value (name,typ,v) = 
     let vec = intern_ifield_value direction v in
@@ -423,7 +432,7 @@ let rec interp_to_outcome mode context thunk =
       Read_reg (extern_reg reg_form slice) 
                (fun v -> 
                  let v = (intern_reg_value v) in
-                 let v = if mode.Interp.track_values then (Interp.V_track v [reg_form]) else v in 
+                 let v = if mode.internal_mode.Interp.track_values then (Interp.V_track v [reg_form]) else v in 
                  IState (Interp.add_answer_to_stack next_state v) context)
     | Interp.Write_reg reg_form slice value ->
       let optional_start = 
@@ -439,7 +448,7 @@ let rec interp_to_outcome mode context thunk =
 	  | Just bs -> Just (integer_of_byte_list bs)
 	  | _ -> Nothing end in
           Read_mem read_k (Address_lifted location address_int) length tracking 
-	    (fun v -> IState (Interp.add_answer_to_stack next_state (intern_mem_value direction v)) context)
+	    (fun v -> IState (Interp.add_answer_to_stack next_state (intern_mem_value mode direction v)) context)
 	else Error ("Memory address on read is not 64 bits")
       | _ -> Error ("Memory " ^ i ^ " function with read kind not found")
       end
@@ -475,8 +484,8 @@ let rec interp_to_outcome mode context thunk =
       match List.lookup i ((Interp_lib.library_functions internal_direction) ++ spec_externs) with
       | Nothing -> Error ("External function not available " ^ i)
       | Just f  -> 
-        if (mode.Interp.eager_eval)
-        then interp_to_outcome mode context (fun _ -> Interp.resume mode next_state (Just (f value))) 
+        if (mode.internal_mode.Interp.eager_eval)
+        then interp_to_outcome mode context (fun _ -> Interp.resume mode.internal_mode next_state (Just (f value))) 
         else let new_v = f value in
              Internal (Just i) 
                       (Just (fun _ -> (Interp.string_of_value value) ^ "=>" ^ (Interp.string_of_value new_v)))
@@ -494,7 +503,7 @@ let rec interp_to_outcome mode context thunk =
   end 
 
 let interp mode (IState interp_state context) = 
-  interp_to_outcome mode context (fun _ -> Interp.resume mode interp_state Nothing)
+  interp_to_outcome mode context (fun _ -> Interp.resume mode.internal_mode interp_state Nothing)
 
 (*TODO: Only find some sub piece matches, need to look for field/slice sub pieces*)
 (*TODO immediate: this will be impacted by need to change slicing *)
@@ -564,7 +573,7 @@ let rec ie_loop mode register_values (IState interp_state context) =
      end ;;
   
 let interp_exhaustive register_values i_state = 
-  let mode = make_mode true true in
+  let mode = make_mode true true E_big_endian in
   ie_loop mode register_values i_state
 
 let rec rr_ie_loop mode i_state = 
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 374f633e..396f0f5c 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -30,11 +30,16 @@ end
 
 type word8 = nat (* bounded at a byte, for when lem supports it*)
 
+type end_flag =
+  | E_big_endian
+  | E_little_endian
+
 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 interp_mode = Interp.interp_mode (*Deem abstract*)
-val make_mode : bool -> bool -> interp_mode
+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
 val tracking_dependencies : interp_mode -> bool
 
 (** basic values *)
@@ -53,10 +58,6 @@ type direction =
   | D_increasing
   | D_decreasing
 
-type end_flag =
-  | E_big_endian
-  | E_little_endian
-
 type register_value = <| 
     rv_bits: list bit_lifted (* MSB first, smallest index number *); 
     rv_dir: direction; 
@@ -73,8 +74,9 @@ type instruction_field_value = list bit
 type byte = Byte of list bit (* of length 8 *)  (*MSB first everywhere*) 
 
 type address_lifted = Address_lifted of list byte_lifted (* of length 8 for 64bit machines*) * maybe integer
+(* for both values of end_flag, MSBy first *)
 
-type memory_byte = byte_lifted
+type memory_byte = byte_lifted (* of length 8 *) (*MSB first everywhere*)
 
 type memory_value = list memory_byte
 (* the list is of length >=1 *)