summaryrefslogtreecommitdiff
path: root/src/lem_interp
diff options
context:
space:
mode:
Diffstat (limited to 'src/lem_interp')
-rw-r--r--src/lem_interp/interp_inter_imp.lem53
-rw-r--r--src/lem_interp/interp_interface.lem16
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 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 12:03:43 +0000