diff options
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 61 | ||||
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 20 |
2 files changed, 54 insertions, 27 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 08aa04a7..14745763 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -5,7 +5,7 @@ open import Interp_interface open import Pervasives val intern_value : value -> Interp.value -val extern_value : bool -> Interp.value -> value +val extern_value : interp_mode -> bool -> Interp.value -> (value * maybe (list reg_name)) val extern_reg : Interp.reg_form -> maybe (integer * integer) -> reg_name let build_context defs = Interp.to_top_env defs @@ -28,20 +28,27 @@ let intern_value v = match v with | Unknown -> Interp.V_unknown end -let extern_value for_mem v = match v with - | Interp.V_vector _ true bits -> - if for_mem - then Bytevector (to_bytes (from_bits bits)) - else Bitvector (from_bits bits) - | _ -> Unknown -end - let extern_reg r slice = match (r,slice) with | (Interp.Reg (Id_aux (Id x) _) _,Nothing) -> Reg x | (Interp.Reg (Id_aux (Id x) _) _,Just(i1,i2)) -> Reg_slice x (i1,i2) | (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_single i) _),Nothing) -> Reg_field x y (i,i) end +let extern_value mode for_mem v = match v with + | Interp.V_vector _ true bits -> + if for_mem + then (Bytevector (to_bytes (from_bits bits)), Nothing) + else (Bitvector (from_bits bits), Nothing) + | Interp.V_track (Interp.V_vector _ true bits) regs -> + if for_mem + then (Bytevector (to_bytes (from_bits bits)), + if (mode.Interp.track_values) + then (Just (List.map (fun r -> extern_reg r Nothing) regs)) + else Nothing) + else (Bitvector (from_bits bits), Nothing) + | _ -> (Unknown,Nothing) +end + let initial_instruction_state top_level main arg = let (e_arg,env) = Interp.to_exp <| Interp.eager_eval = true; Interp.track_values = false |> Interp.eenv (intern_value arg) in Interp.Thunk_frame (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) [e_arg]) (Interp_ast.Unknown, Nothing)) top_level Interp.eenv Interp.emem @@ -50,13 +57,14 @@ let initial_instruction_state top_level main arg = let external_functions = Interp_lib.function_map -type mem_function = (string * (maybe read_kind * maybe write_kind * Interp.value -> value)) +type mem_function = (string * + (maybe read_kind * maybe write_kind * (interp_mode -> Interp.value -> (value * (maybe (list reg_name)))))) (*List of memory functions; needs to be expanded with all of the memory functions needed for PPCMem. Should probably be expanded into a parameter to mode as with above *) let memory_functions = - [ ("MEM", (Just(Interp.Read_plain), Just(Interp.Write_plain), (fun v -> extern_value true v))); + [ ("MEM", (Just(Interp.Read_plain), Just(Interp.Write_plain), (fun mode v -> extern_value mode true v))); ] let rec interp_to_outcome mode thunk = @@ -65,16 +73,27 @@ let rec interp_to_outcome mode thunk = | Interp.Error l msg -> Error msg (*Todo, add the l information the string format*) | Interp.Action a next_state -> match a with - | Interp.Read_reg reg_form slice -> Read_reg (extern_reg reg_form slice) (fun v -> Interp.add_answer_to_stack next_state (intern_value v)) - | Interp.Write_reg reg_form slice value -> Write_reg (extern_reg reg_form slice) (extern_value false value) next_state + | Interp.Read_reg reg_form slice -> + Read_reg (extern_reg reg_form slice) + (fun v -> + let v = (intern_value v) in + let v = if mode.Interp.track_values then (Interp.V_track v [reg_form]) else v in + Interp.add_answer_to_stack next_state v) + | Interp.Write_reg reg_form slice value -> + let (v,_) = extern_value mode false value in Write_reg (extern_reg reg_form slice) v next_state | Interp.Read_mem (Id_aux (Id i) _) value slice -> match List.lookup i memory_functions with - | (Just (Just read_k,_,f)) -> Read_mem read_k (f value) (fun v -> Interp.add_answer_to_stack next_state (intern_value v)) + | (Just (Just read_k,_,f)) -> + let (location, tracking) = (f mode value) in + Read_mem read_k location tracking (fun v -> Interp.add_answer_to_stack next_state (intern_value v)) | _ -> Error ("Memory " ^ i ^ " function with read kind not found") end | Interp.Write_mem (Id_aux (Id i) _) loc_val slice write_val -> match List.lookup i memory_functions with - | (Just (_,Just write_k,f)) -> Write_mem write_k (f loc_val) (extern_value true write_val) (fun b -> next_state) + | (Just (_,Just write_k,f)) -> + let (location, tracking) = (f mode loc_val) in + let (value, val_tracking) = (extern_value mode true write_val) in + Write_mem write_k location tracking value val_tracking (fun b -> next_state) | _ -> Error ("Memory " ^ i ^ " function with write kind not found") end | Interp.Barrier (Id_aux (Id i) _) lval -> @@ -86,7 +105,7 @@ let rec interp_to_outcome mode thunk = match List.lookup i external_functions with | Nothing -> Error ("External function not available " ^ i) | Just f -> interp_to_outcome mode (fun _ -> Interp.resume mode next_state (Just (f value))) end - | Interp.Step l _ _ -> Internal next_state + | Interp.Step l _ _ -> Internal (fun _ -> "Function state to string not implemented yet") next_state end end @@ -100,11 +119,11 @@ let rec ie_loop mode i_state = (E_read_reg reg)::(ie_loop mode (i_state_fun Unknown)) | Write_reg reg value i_state-> (E_write_reg reg value)::(ie_loop mode i_state) - | Read_mem read_k loc i_state_fun -> - (E_read_mem read_k loc)::(ie_loop mode (i_state_fun Unknown)) - | Write_mem write_k loc value i_state_fun -> - (E_write_mem write_k loc value)::(ie_loop mode (i_state_fun true)) - | Internal next -> (ie_loop mode next) + | Read_mem read_k loc tracking i_state_fun -> + (E_read_mem read_k loc tracking)::(ie_loop mode (i_state_fun Unknown)) + | Write_mem write_k loc l_track value v_track i_state_fun -> + (E_write_mem write_k loc l_track value v_track)::(ie_loop mode (i_state_fun true)) + | Internal _ next -> (ie_loop mode next) end ;; let interp_exhaustive i_state = diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index f74a70db..a1ddef88 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -1,4 +1,5 @@ import Interp +open import Pervasives open import Num type read_kind = Interp.read_kind @@ -24,19 +25,26 @@ type reg_name = | Reg_f_slice of string * string * slice * slice (* Same as above but only accessing second slice of the field *) type outcome = -| Read_mem of read_kind * value * (value -> instruction_state) -| Write_mem of write_kind * value * value * (bool -> instruction_state) +(* Request to read memory, value is location to read followed by registers that location depended on when mode.track_values *) +| Read_mem of read_kind * value * maybe (list reg_name) * (value -> instruction_state) +(* Request to write memory, first value and dependent registers is location, second is the value to write *) +| Write_mem of write_kind * value * maybe (list reg_name) * value * maybe (list reg_name) * (bool -> instruction_state) +(* Request a memory barrier *) | Barrier of barrier_kind * instruction_state +(* Request to read register, will track dependency when mode.track_values *) | Read_reg of reg_name * (value -> instruction_state) +(* Request to write register *) | Write_reg of reg_name * value * instruction_state +(* List of instruciton states to be run in parrallel, any order permitted *) | Nondet_choice of list instruction_state * instruction_state -| Internal of instruction_state +(* Stop for incremental stepping, function can be used to display function call data *) +| Internal of (unit -> string) * instruction_state | Done | Error of string type event = -| E_read_mem of read_kind * value -| E_write_mem of write_kind * value * value +| E_read_mem of read_kind * value * maybe (list reg_name) +| E_write_mem of write_kind * value * maybe (list reg_name) * value * maybe (list reg_name) | E_barrier of barrier_kind | E_read_reg of reg_name | E_write_reg of reg_name * value @@ -47,7 +55,7 @@ type event = val build_context : Interp_ast.defs Interp.tannot -> context val initial_instruction_state : context -> string -> value -> instruction_state -type interp_mode = <| eager_eval : bool |> +type interp_mode = Interp.interp_mode val interp : interp_mode -> instruction_state -> outcome val interp_exhaustive : instruction_state -> list event |