diff options
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 14 | ||||
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 23 |
2 files changed, 27 insertions, 10 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 3877a08f..91fc4141 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -313,11 +313,11 @@ let call_external_functions direction outcome = | Just f -> Just (f value) end | _ -> Nothing end -let build_context defs reads writes barriers externs = +let build_context defs reads writes write_eas write_vals barriers externs = (*TODO add externs to to_top_env*) match Interp.to_top_env call_external_functions defs with | (_,((Interp.Env _ _ dir _ _ _ _ _) as context)) -> - Context context (if Interp.is_inc(dir) then D_increasing else D_decreasing) reads writes barriers externs end + Context context (if Interp.is_inc(dir) then D_increasing else D_decreasing) reads writes write_eas write_vals barriers externs end let rec find_instruction i = function @@ -339,7 +339,7 @@ end let decode_to_istate top_level value = let mode = make_interp_mode true false in - let (Context ((Interp.Env _ instructions _ _ _ _ _ _) as top_env) direction _ _ _ _) = top_level 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 @@ -396,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_interp_mode true false in - let (Context top_env direction _ _ _ _) = top_level in + let (Context top_env direction _ _ _ _ _ _) = top_level in let get_value (name,typ,v) = let vec = intern_ifield_value direction v in let v = match vec with @@ -420,7 +420,7 @@ let instruction_to_istate (top_level:context) (((name, parms, _) as instr):instr top_level) let rec interp_to_outcome mode context thunk = - let (Context _ direction mem_reads mem_writes barriers spec_externs) = context in + let (Context _ direction mem_reads mem_writes mem_write_eas mem_write_vals barriers spec_externs) = context in let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in match thunk () with | Interp.Value _ -> Done @@ -536,7 +536,7 @@ let reg_size = function end let rec ie_loop mode register_values (IState interp_state context) = - let (Context _ direction externs reads writes barriers) = context in + let (Context _ direction externs reads writes write_eas write_vals barriers) = context in let unknown_reg size = <| rv_bits = (List.replicate size Bitl_unknown); rv_start = 0; @@ -574,7 +574,7 @@ let interp_exhaustive register_values i_state = ie_loop mode register_values i_state let rec rr_ie_loop mode i_state = - let (IState _ (Context _ direction _ _ _ _)) = i_state in + let (IState _ (Context _ direction _ _ _ _ _ _)) = i_state in let unknown_reg size = <| rv_bits = (List.replicate size Bitl_unknown); rv_start = 0; diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index ce9cac1d..8db772c8 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -421,11 +421,17 @@ type barriers = list (string * barrier_kind) type memory_parameter_transformer = interp_mode -> Interp.value -> (memory_value * nat * maybe (list reg_name)) type memory_read = MR of read_kind * memory_parameter_transformer type memory_reads = list (string * memory_read) +type memory_write_ea = MEA of write_kind * memory_parameter_transformer +type memory_write_eas = list (string * memory_write_ea) type memory_write = MW of write_kind * memory_parameter_transformer * (maybe (instruction_state -> bool -> instruction_state)) and memory_writes = list (string * memory_write) +and memory_write_val = MV of maybe (instruction_state -> bool -> instruction_state) +and memory_write_vals = list (string * memory_write_val) (* Definition information needed to run an instruction *) -and context = Context of Interp.top_level * direction * memory_reads * memory_writes * barriers * external_functions +and context = + Context of Interp.top_level * direction * + memory_reads * memory_writes * memory_write_eas * memory_write_vals * barriers * external_functions (* An instruction in flight *) and instruction_state = IState of interpreter_state * context @@ -437,6 +443,10 @@ type outcome = | Read_mem of read_kind * address_lifted * nat * maybe (list reg_name) * (memory_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 * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name) * (bool -> instruction_state) +(* Tell the system a write is imminent, at address lifted tanted by register list, of size nat *) +| Write_ea of write_kind * address_lifted * nat * maybe (list reg_name) * instruction_state +(* Request to write memory at last signaled address. Memory value should be 8* the size given in ea signal *) +| Write_memv of memory_value * maybe (list reg_name) * (bool -> instruction_state) (* Request a memory barrier *) | Barrier of barrier_kind * instruction_state (* Tell the system to dynamically recalculate dependency footprint *) @@ -457,12 +467,14 @@ type outcome = type event = | E_read_mem of read_kind * address_lifted * nat * maybe (list reg_name) | E_write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name) +| E_write_ea of write_kind * address_lifted * nat * maybe (list reg_name) +| E_write_memv of memory_value * maybe (list reg_name) | E_barrier of barrier_kind | E_footprint | E_read_reg of reg_name | E_write_reg of reg_name * register_value | E_escape -| E_error of string (* Should not happen, but may if the symbolic evaluation doesn't work out*) +| E_error of string (* more explicit type classes to work around the occurrences of big_int in reg_name ::no longer necessary?*) @@ -742,6 +754,9 @@ let ~{ocaml} eventCompare e1 e2 = compare (rk1, (v1,i1,tr1)) (rk2,(v2, i2, tr2)) | (E_write_mem wk1 v1 i1 tr1 v1' tr1', E_write_mem wk2 v2 i2 tr2 v2' tr2') -> compare ((wk1,v1,i1),(tr1,v1',tr1')) ((wk2,v2,i2),(tr2,v2',tr2')) + | (E_write_ea wk1 a1 i1 tr1, E_write_ea wk2 a2 i2 tr2) -> + compare (wk1, (a1, i1, tr1)) (wk2, (a2, i2, tr2)) + | (E_write_memv mv1 tr1, E_write_memv mv2 tr2) -> compare (mv1,tr1) (mv2,tr2) | (E_barrier bk1, E_barrier bk2) -> compare bk1 bk2 | (E_read_reg r1, E_read_reg r2) -> compare r1 r2 | (E_write_reg r1 v1, E_write_reg r2 v2) -> compare (r1,v1) (r2,v2) @@ -749,6 +764,8 @@ let ~{ocaml} eventCompare e1 e2 = | (E_escape,E_escape) -> EQ | (E_read_mem _ _ _ _, _) -> LT | (E_write_mem _ _ _ _ _ _, _) -> LT + | (E_write_ea _ _ _ _, _) -> LT + | (E_write_memv _ _, _) -> LT | (E_barrier _, _) -> LT | (E_read_reg _, _) -> LT | (E_write_reg _ _, _) -> LT @@ -779,7 +796,7 @@ instance (SetType event) end (* Functions to build up the initial state for interpretation *) -val build_context : specification -> memory_reads -> memory_writes -> barriers -> external_functions -> context +val build_context : specification -> memory_reads -> memory_writes -> memory_write_eas -> memory_write_vals -> barriers -> external_functions -> context val initial_instruction_state : context -> string -> list register_value -> instruction_state (* string is a function name, list of value are the parameters to that function *) |