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.lem88
-rw-r--r--src/lem_interp/interp_interface.lem10
-rw-r--r--src/lem_interp/run_with_elf.ml10
3 files changed, 82 insertions, 26 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 53603fae..d1e1672e 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -14,18 +14,18 @@ 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_reg : Interp.reg_form -> maybe (nat * nat) -> reg_name
-let make_interp_mode eager_eval tracking_values =
+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_interp_mode eager_eval tracking_values;
+ <|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 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_interp_mode false false; endian = E_big_endian|>;;
+let make_default_mode _ = <|internal_mode = make_interpreter_mode false false; endian = E_big_endian|>;;
let bitl_to_ibit = function
| Bitl_zero -> (Interp.V_lit (L_aux L_zero Interp_ast.Unknown))
@@ -243,42 +243,50 @@ let update_reg_value_slice reg_name v start stop v2 =
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_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)
+ | [arg] -> let (e,_) = Interp.to_exp (make_interpreter_mode true false) Interp.eenv (intern_reg_value arg) in [e]
+ | args -> List.map fst (List.map (Interp.to_exp (make_interpreter_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 "istate top level") Interp.Top
-type interp_value_helper_mode = Ivh_decode | Ivh_unsupported | Ivh_illegal
+type interp_value_helper_mode = Ivh_translate | Ivh_decode | Ivh_unsupported | Ivh_illegal
-let rec interp_to_value_helper arg ivh_mode err_str instr direction thunk =
+let rec interp_to_value_helper arg ivh_mode err_str instr direction thunk =
+ let errk_str = match ivh_mode with
+ | Ivh_translate -> "translate"
+ | Ivh_decode -> "decode"
+ | Ivh_unsupported -> "supported_instructions"
+ | Ivh_illegal -> "illegal instruction" end in
match thunk() with
| (Interp.Value value,_,_) ->
(match value with
| Interp.V_ctor (Id_aux (Id "Some") _) _ _ vinstr -> (Just vinstr,Nothing)
| Interp.V_ctor (Id_aux (Id "None") _) _ _ _ ->
- match ivh_mode with
+ (match ivh_mode with
| Ivh_decode -> (Nothing, Just (Not_an_instruction_error arg))
| Ivh_illegal -> (Nothing, Just (Not_an_instruction_error arg))
| Ivh_unsupported -> (Nothing, Just (Unsupported_instruction_error instr))
- end end)
+ end)
+ | Interp.V_tuple [v1;v2] ->
+ (match ivh_mode with
+ | Ivh_translate -> (Just value,Nothing)
+ | _ -> (Nothing, Just (Internal_error ("Found a tuple for this " ^ errk_str))) end)
+ end)
| (Interp.Error l msg,_,_) -> (Nothing, Just (Internal_error msg))
| (Interp.Action (Interp.Call_extern i value) stack,_,_) ->
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 ivh_mode err_str instr direction
- (fun _ -> Interp.resume (make_interp_mode true false) stack (Just (f value)))
+ (fun _ -> Interp.resume (make_interpreter_mode true false) stack (Just (f value)))
end
| (Interp.Action (Interp.Exit ((E_aux e _) as exp)) stack,_,_) ->
match e with
- (*| E_id (Id_aux (Id "unsupported_instruction") _) -> (Nothing,Just (Unsupported_instruction_error instr))
- | E_id (Id_aux (Id "no_matching_pattern") _) -> (Nothing,Just (Not_an_instruction_error arg))*)
| E_lit (L_aux (L_string str) _) -> (Nothing, Just (Internal_error ("Exit called with message: " ^ str)))
| E_id (Id_aux (Id i) _) ->
- (match (Interp.resume (make_interp_mode true false) (Interp.set_in_context stack exp) Nothing) with
+ (match (Interp.resume (make_interpreter_mode true false) (Interp.set_in_context stack exp) Nothing) with
| (Interp.Value (Interp.V_lit (L_aux (L_string str) _)),_,_) ->
- (Nothing, Just (Internal_error ("Exit called when decoding "^err_str ^" with message: " ^ str)))
+ (Nothing, Just (Internal_error ("Exit called when processing "^err_str ^" with message: " ^ str)))
| _ -> (Nothing, Just (Internal_error ("Exit called with unrecognized expression bound to an id " ^ i))) end)
| _ -> (Nothing, Just (Internal_error "Exit called with unrecognized expression"))
end
@@ -286,18 +294,18 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction thunk =
let rname = match r with
| Interp.Reg (Id_aux (Id i) _) _ _ -> i
| Interp.SubReg (Id_aux (Id i) _) (Interp.Reg (Id_aux (Id i2) _) _ _) _ -> i2 ^ "." ^ i end in
- (Nothing, Just (Internal_error ("Register read of "^ rname^" request in a decode of " ^ err_str)))
+ (Nothing, Just (Internal_error ("Register read of "^ rname^" request in a " ^ errk_str ^ " of " ^ err_str)))
| (Interp.Action (Interp.Write_reg _ _ _) _,_,_) ->
- (Nothing, Just (Internal_error "Register write request in a decode"))
+ (Nothing, Just (Internal_error ("Register write request in a " ^ errk_str)))
| (Interp.Action (Interp.Read_mem _ _ _) _,_,_) ->
- (Nothing, Just (Internal_error "Read memory request in a decode"))
+ (Nothing, Just (Internal_error ("Read memory request in a " ^ errk_str)))
| (Interp.Action (Interp.Write_mem _ _ _ _) _,_,_) ->
- (Nothing, Just (Internal_error "Write memory request in a decode"))
+ (Nothing, Just (Internal_error ("Write memory request in a " ^ errk_str)))
| (Interp.Action (Interp.Write_ea _ _) _,_,_) ->
- (Nothing, Just (Internal_error "Write ea request in a decode"))
+ (Nothing, Just (Internal_error ("Write ea request in a " ^ errk_str)))
| (Interp.Action (Interp.Write_memv _ _) _,_,_) ->
- (Nothing, Just (Internal_error "Write memory value request in a decode"))
- | _ -> (Nothing, Just (Internal_error "Non expected action in a decode"))
+ (Nothing, Just (Internal_error ("Write memory value request in a " ^ errk_str)))
+ | _ -> (Nothing, Just (Internal_error ("Non expected action in a " ^ errk_str)))
end
let call_external_functions direction outcome =
@@ -315,6 +323,40 @@ let build_context defs reads writes write_eas write_vals barriers externs =
Context context (if Interp.is_inc(dir) then D_increasing else D_decreasing) reads writes write_eas write_vals barriers externs end
+let translate_address top_level end_flag thunk_name address =
+ let (Address bytes i) = address in
+ let mode = make_mode true false end_flag 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
+ let val_str = Interp.string_of_value intern_val in
+ let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in
+ let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
+ let (address,error) = interp_to_value_helper (Opcode bytes) Ivh_translate val_str ("",[],[]) internal_direction
+ (fun _ -> Interp.resume
+ int_mode
+ (Interp.Thunk_frame
+ (E_aux (E_app (Id_aux (Id thunk_name) Interp_ast.Unknown) [arg]) (Interp_ast.Unknown, Nothing))
+ top_env Interp.eenv (Interp.emem "translate top level") Interp.Top) Nothing) in
+ match (address,error) with
+ | (Just addr, _) ->
+ (match addr with
+ | Interp.V_tuple[Interp.V_ctor (Id_aux (Id "Some") _) _ _ v;
+ Interp.V_ctor (Id_aux (Id "Some") _) _ _ (Interp.V_lit (L_aux (L_num n) _))] ->
+ let (mem_v,_) = extern_mem_value mode v in
+ ((address_of_memory_value end_flag mem_v), Just n)
+ | Interp.V_tuple[Interp.V_ctor (Id_aux (Id "Some") _) _ _ v;
+ Interp.V_ctor (Id_aux (Id "None") _) _ _ _] ->
+ let (mem_v,_) = extern_mem_value mode v in
+ ((address_of_memory_value end_flag mem_v), Nothing)
+ | Interp.V_tuple[Interp.V_ctor (Id_aux (Id "None") _) _ _ _;
+ Interp.V_ctor (Id_aux (Id "Some") _) _ _ (Interp.V_lit (L_aux (L_num n) _))] ->
+ (Nothing, Just n)
+ | _ -> (Nothing,Nothing) end)
+ | (Nothing, Just err) -> (Nothing,Nothing)
+end
+
+
let rec find_instruction i = function
| [] -> Nothing
| Instruction_extractor.Skipped::instrs -> find_instruction i instrs
@@ -334,7 +376,7 @@ end
let decode_to_istate top_level value =
- let mode = make_interp_mode true false in
+ let mode = make_interpreter_mode true false in
let (Context ((Interp.Env _ instructions _ _ _ _ _ _) as top_env) direction _ _ _ _ _ _) = top_level in
let intern_val = intern_opcode direction value in
let val_str = Interp.string_of_value intern_val in
@@ -393,7 +435,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_interp_mode true false in
+ let mode = make_interpreter_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
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index d333873b..e5489bd5 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -1137,7 +1137,7 @@ let clear_low_order_bits_of_address a =
end
end
-val translate_address : string -> address -> maybe address * maybe nat
+val translate_address : context -> end_flag -> string -> address -> maybe address * maybe nat
val byte_list_of_memory_value : end_flag -> memory_value -> maybe (list byte)
let byte_list_of_memory_value endian mv =
@@ -1219,7 +1219,7 @@ let address_of_address_lifted (al:address_lifted): maybe address =
| Just bs -> Just (Address bs i)
end
| _ -> Nothing
- end
+end
val address_of_register_value : register_value -> maybe address
(* returning Nothing iff the register value is not 64 bits wide, or contains Bitl_undef or Bitl_unknown *)
@@ -1270,6 +1270,12 @@ let byte_list_of_address (a:address) : list byte =
| Address bs _ -> bs
end
+val memory_value_of_address : end_flag -> address -> memory_value
+let memory_value_of_address endian addr =
+ match addr with
+ | Address bs _ -> List.map byte_lifted_of_byte (if endian = E_big_endian then bs else List.reverse bs)
+ end
+
val byte_list_of_opcode : opcode -> list byte
let byte_list_of_opcode (opc:opcode) : list byte =
match opc with
diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml
index 4f99fa64..6324f193 100644
--- a/src/lem_interp/run_with_elf.ml
+++ b/src/lem_interp/run_with_elf.ml
@@ -968,6 +968,15 @@ let run () =
startaddr,
startaddr_internal), pp_symbol_map) = initial_system_state_of_elf_file !file in
+ let context = build_context isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_externs in
+ (*NOTE: this is likely MIPS specific, so should probably pull from initial_system_state info on to translate or not,
+ endian mode, and translate function name
+ *)
+ let addr_trans = translate_address context E_big_endian "translate_address" in
+ let startaddr,startaddr_internal = match addr_trans startaddr_internal with
+ | Some a, _ -> integer_of_address a, a
+ | None, _ -> failwith "Address translation failed in some way"
+ in
let initial_opcode = Opcode (List.map (fun b -> match b with
| Some b -> b
| None -> errorf "A byte in opcode contained unknown or undef"; exit 1)
@@ -976,7 +985,6 @@ let run () =
Mem.find (add1 startaddr) !prog_mem;
Mem.find (add1 (add1 startaddr)) !prog_mem;
Mem.find (add1 (add1 (add1 startaddr))) !prog_mem])) in
- let context = build_context isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_externs in
reg := Reg.add "PC" (register_value_of_address startaddr_internal model_reg_d ) !reg;
(* entry point: unit -> unit fde *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 21:09:28 +0000