diff options
Diffstat (limited to 'src/lem_interp/interp_interface.lem')
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 3ef6abb8..fce5b14f 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -179,17 +179,21 @@ type memory_parameter_transformer = interp_mode -> Interp.value -> (memory_value type optional_memory_transformer = interp_mode -> Interp.value -> maybe memory_value type memory_read = MR of read_kind * memory_parameter_transformer type memory_reads = list (string * memory_read) +type memory_read_tagged = MRT of read_kind * memory_parameter_transformer +type memory_read_taggeds = list (string * memory_read_tagged) 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 optional_memory_transformer * (maybe (instruction_state -> bool -> instruction_state)) and memory_write_vals = list (string * memory_write_val) +and memory_write_val_tagged = MVT of optional_memory_transformer * (maybe (instruction_state -> bool -> instruction_state)) +and memory_write_vals_tagged = list (string * memory_write_val_tagged) (* Definition information needed to run an instruction *) and context = Context of Interp.top_level * direction * - memory_reads * memory_writes * memory_write_eas * memory_write_vals * barriers * external_functions + memory_reads * memory_read_taggeds * memory_writes * memory_write_eas * memory_write_vals * memory_write_vals_tagged * barriers * external_functions (* An instruction in flight *) and instruction_state = IState of interpreter_state * context @@ -199,6 +203,7 @@ type outcome = (* Request to read N bytes at address *) (* The register list, used when mode.track_values, is those that the address depended on *) | Read_mem of read_kind * address_lifted * nat * maybe (list reg_name) * (memory_value -> instruction_state) +| Read_mem_tagged of read_kind * address_lifted * nat * maybe (list reg_name) * ((bit_lifted * memory_value) -> instruction_state) (* Request to write memory *) | Write_mem of write_kind * address_lifted * nat * maybe (list reg_name) @@ -209,6 +214,7 @@ type outcome = (* Request to write memory at last signaled address. Memory value should be 8* the size given in Write_ea *) | Write_memv of maybe address_lifted * memory_value * maybe (list reg_name) * (bool -> instruction_state) +| Write_memv_tagged of maybe address_lifted * (bit_lifted * memory_value) * maybe (list reg_name) * (bool -> instruction_state) (* Request a memory barrier *) | Barrier of barrier_kind * instruction_state @@ -248,7 +254,7 @@ type outcome = (* Functions to build up the initial state for interpretation *) -val build_context : specification -> memory_reads -> memory_writes -> memory_write_eas -> memory_write_vals -> barriers -> external_functions -> context +val build_context : specification -> memory_reads -> memory_read_taggeds-> memory_writes -> memory_write_eas -> memory_write_vals -> memory_write_vals_tagged -> 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 *) |