diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 8 | ||||
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 4 | ||||
| -rw-r--r-- | src/lem_interp/printing_functions.mli | 1 | ||||
| -rw-r--r-- | src/lem_interp/run_interp_model.ml | 68 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf.ml | 7 |
5 files changed, 52 insertions, 36 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index d65814f3..c5690a5e 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -491,7 +491,7 @@ let rec interp_to_outcome mode context thunk = Read_mem read_k (Address_lifted location address_int) length tracking (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") + | _ -> Error ("Memory function " ^ i ^ " not found") end , lm) | Interp.Write_mem (Id_aux (Id i) _) loc_val slice write_val -> (match List.lookup i mem_writes with @@ -509,7 +509,7 @@ let rec interp_to_outcome mode context thunk = | Nothing -> (IState (Interp.add_answer_to_stack next_state Interp.unitv) context) | Just return_bool -> return_bool (IState next_state context) b end) else Error "Memory address on write is not 64 bits" - | _ -> Error ("Memory " ^ i ^ " function with write kind not found") + | _ -> Error ("Memory function " ^ i ^ " not found") end , lm) | Interp.Write_ea (Id_aux (Id i) _) loc_val -> (match List.lookup i mem_write_eas with @@ -521,7 +521,7 @@ let rec interp_to_outcome mode context thunk = | _ -> Nothing end in Write_ea write_k (Address_lifted location address_int) length tracking (IState next_state context) else Error "Memory address for write is not 64 bits" - | _ -> Error ("Memory " ^ i ^ " function to signal impending write, not found") end, lm) + | _ -> Error ("Memory function " ^ i ^ " to signal impending write, not found") end, lm) | Interp.Write_memv (Id_aux (Id i) _) write_val -> (match List.lookup i mem_write_vals with | (Just (MV return)) -> @@ -534,7 +534,7 @@ let rec interp_to_outcome mode context thunk = match return with | Nothing -> (IState (Interp.add_answer_to_stack next_state Interp.unitv) context) | Just return_bool -> return_bool (IState next_state context) b end) - | _ -> Error ("Memory " ^ i ^ " function with write value kind not found") end, lm) + | _ -> Error ("Memory function " ^ i ^ " not found") end, lm) | Interp.Barrier (Id_aux (Id i) _) lval -> (match List.lookup i barriers with | Just barrier -> diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index e5489bd5..6fe999c9 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -394,6 +394,7 @@ end type read_kind = (* common reads *) Read_plain + | Read_tag (*For reading the tag of tagged memory*) (* Power reads *) | Read_reserve (* AArch64 reads *) @@ -401,7 +402,8 @@ type read_kind = type write_kind = (* common writes *) - Write_plain + Write_plain + | Write_tag (*For writing the tag of tagged memory*) (* Power writes *) | Write_conditional (* AArch64 writes *) diff --git a/src/lem_interp/printing_functions.mli b/src/lem_interp/printing_functions.mli index 2b792ebb..c7747b50 100644 --- a/src/lem_interp/printing_functions.mli +++ b/src/lem_interp/printing_functions.mli @@ -67,3 +67,4 @@ val logfile_memory_value_to_string : end_flag -> memory_value -> string val logfile_address_to_string : address -> string val byte_list_to_string : byte list -> string +val bit_lifted_to_string : bit_lifted -> string diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml index 0bd3015a..706ab5ac 100644 --- a/src/lem_interp/run_interp_model.ml +++ b/src/lem_interp/run_interp_model.ml @@ -43,11 +43,10 @@ module Mem = struct type t = num let compare v1 v2 = compare v1 v2 end) -(* let find idx m = - let v = find idx m in - v - let add key valu m = - add key valu m*) + let find idx m = + if mem idx m + then find idx m + else List.hd(memory_value_unknown 1) let to_string loc v = sprintf "[%s] -> %s" (to_string loc) @@ -106,46 +105,56 @@ let combine_slices (start, stop) (inner_start,inner_stop) = let unit_lit = (L_aux(L_unit,Interp_ast.Unknown)) -let rec perform_action ((reg, mem) as env) = function +let rec perform_action ((reg, mem, tagmem) as env) = function (* registers *) | Read_reg0(Reg0(id,_,_,_), _) -> (Some(Reg.find id reg), env) | Read_reg0(Reg_slice(id, _, _, range), _) | Read_reg0(Reg_field(id, _, _, _, range), _) -> (Some(slice (Reg.find id reg) range), env) | Read_reg0(Reg_f_slice(id, _,_,_, range, mini_range), _) -> (Some(slice (slice (Reg.find id reg) range) mini_range),env) - | Write_reg0(Reg0(id,_,_,_), value, _) -> (None, (Reg.add id value reg,mem)) + | Write_reg0(Reg0(id,_,_,_), value, _) -> (None, (Reg.add id value reg,mem,tagmem)) | Write_reg0((Reg_slice(id,_,_,range) as reg_n),value, _) | Write_reg0((Reg_field(id,_,_,_,range) as reg_n),value,_)-> let old_val = Reg.find id reg in let new_val = fupdate_slice reg_n old_val value range in - (None, (Reg.add id new_val reg, mem)) + (None, (Reg.add id new_val reg, mem,tagmem)) | Write_reg0((Reg_f_slice(id,_,_,_,range,mini_range) as reg_n),value,_) -> let old_val = Reg.find id reg in let new_val = fupdate_slice reg_n old_val value (combine_slices range mini_range) in - (None,(Reg.add id new_val reg,mem)) - | Read_mem0(_,location, length, _,_) -> + (None,(Reg.add id new_val reg,mem,tagmem)) + | Read_mem0(kind,location, length, _,_) -> let address = match address_of_address_lifted location with | Some a -> a | None -> assert false (*TODO remember how to report an error *)in - let naddress = integer_of_address address in - let rec reading (n : num) length = - if length = 0 - then [] - else (Mem.find n mem)::(reading (add n big_num_unit) (length - 1)) in - (Some (register_value_of_memory_value (reading naddress length) !default_order), env) - | Write_mem0(_,location, length, _, bytes,_,_) -> + let naddress = integer_of_address address in + (match kind with + | Read_tag -> + (Some (register_value_of_memory_value [(Mem.find naddress tagmem)] !default_order), env) + | _ -> + let rec reading (n : num) length = + if length = 0 + then [] + else (Mem.find n mem)::(reading (add n big_num_unit) (length - 1)) in + (Some (register_value_of_memory_value (reading naddress length) !default_order), env)) + | Write_mem0(kind,location, length, _, bytes,_,_) -> let address = match address_of_address_lifted location with | Some a -> a | None -> assert false (*TODO remember how to report an error *)in - let naddress = integer_of_address address in - let rec writing location length bytes mem = - if length = 0 - then mem - else match bytes with - | [] -> mem - | b::bytes -> - writing (add location big_num_unit) (length - 1) bytes (Mem.add location b mem) in - (None,(reg,writing naddress length bytes mem)) + let naddress = integer_of_address address in + (match kind with + | Write_tag -> + (match bytes with + | [b] -> (None,(reg,mem,Mem.add naddress b tagmem)) + | _ -> assert false) + | _ -> + let rec writing location length bytes mem = + if length = 0 + then mem + else match bytes with + | [] -> mem + | b::bytes -> + writing (add location big_num_unit) (length - 1) bytes (Mem.add location b mem) in + (None,(reg,writing naddress length bytes mem,tagmem))) | _ -> (None, env) ;; @@ -170,6 +179,7 @@ let run (istate : instruction_state) reg mem + tagmem eager_eval track_dependencies mode @@ -186,7 +196,7 @@ let run mem print content of memory exh run interpreter exhaustively with unknown and print events quit exit interpreter" in - let rec interact mode ((reg, mem) as env) stack = + let rec interact mode ((reg, mem, tagmem) as env) stack = flush_all(); let command = Pervasives.read_line () in let command' = if command = "" then mode_to_string mode else command in @@ -350,9 +360,9 @@ let run (Pretty_interp.pp_exp top_env Printing_functions.red top_exp); try Printexc.record_backtrace true; - loop mode (reg, mem) (Interp_inter_imp.interp0 imode istate) + loop mode (reg, mem,tagmem) (Interp_inter_imp.interp0 imode istate) with e -> let trace = Printexc.get_backtrace () in interactf "%s: %s %s\n%s\n" (grey name) (red "interpretor error") (Printexc.to_string e) trace; - (false, mode, !track_dependencies, (reg, mem)) + (false, mode, !track_dependencies, (reg, mem, tagmem)) ;; diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml index c971550d..75ed3b33 100644 --- a/src/lem_interp/run_with_elf.ml +++ b/src/lem_interp/run_with_elf.ml @@ -23,6 +23,7 @@ let hex_to_big_int s = big_int_of_int64 (Int64.of_string s) ;; let data_mem = (ref Mem.empty : (memory_byte Run_interp_model.Mem.t) ref) ;; let prog_mem = (ref Mem.empty : (memory_byte Run_interp_model.Mem.t) ref) ;; +let tag_mem = (ref Mem.empty : (memory_byte Run_interp_model.Mem.t) ref);; let reg = ref Reg.empty ;; let add_mem byte addr mem = @@ -529,6 +530,7 @@ let initial_system_state_of_elf_file name = begin prog_mem := Mem.empty; data_mem := Mem.empty; + tag_mem := Mem.empty; load_memory_segments segments; (* debugf "prog_mem\n"; @@ -956,11 +958,12 @@ let rec fde_loop count context model mode track_dependencies opcode addr_trans = else begin set_next_instruction_address model; - match Run_interp_model.run istate !reg !prog_mem !eager_eval track_dependencies mode "execute" with + match Run_interp_model.run istate !reg !prog_mem !tag_mem !eager_eval track_dependencies mode "execute" with | false, _,_, _ -> errorf "FAILURE\n"; exit 1 - | true, mode, track_dependencies, (my_reg, my_mem) -> + | true, mode, track_dependencies, (my_reg, my_mem, my_tags) -> reg := my_reg; prog_mem := my_mem; + tag_mem := my_tags; let opcode = fetch_instruction_opcode_and_update_ia model addr_trans in fde_loop (count + 1) context model (Some mode) (ref track_dependencies) opcode addr_trans end |