From e9b40edcc325bfe5a0e3566c61ee12a236c5ddf8 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 11 May 2017 14:54:32 +0100 Subject: Change types of MEMr_tag, MEMval_tag and co. so that tag is separate from data and invent rmemt and wmvt effects for them. Extend the interpreter context to include lists of tagged memory read and write functions. The memory model must round down the address to the nearest capability aligned address when reading/writing tags. Remove TAGw which is no longer needed as a result. --- src/lem_interp/interp_interface.lem | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) (limited to 'src/lem_interp/interp_interface.lem') 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 *) -- cgit v1.2.3