diff options
| author | Shaked Flur | 2017-05-24 16:19:27 +0100 |
|---|---|---|
| committer | Shaked Flur | 2017-05-24 16:19:27 +0100 |
| commit | 9cffd54c6170f8a5cdcc6e54cb9077b62bf6a284 (patch) | |
| tree | 3c94e563409844e8685714cbe331748c9ddd0fe6 /src/lem_interp/interp_interface.lem | |
| parent | fffcaaa390eaf03db689d0f108cc00653a41885d (diff) | |
added the exmem effect for AArch64 store-exclusive
Diffstat (limited to 'src/lem_interp/interp_interface.lem')
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 3ef6abb8..77572de9 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -185,11 +185,13 @@ type memory_write = MW of write_kind * memory_parameter_transformer * (maybe (in 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 excl_res_t = ER of maybe (instruction_state -> bool -> instruction_state) +and excl_res = maybe (string * excl_res_t) (* 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_writes * memory_write_eas * memory_write_vals * barriers * excl_res * external_functions (* An instruction in flight *) and instruction_state = IState of interpreter_state * context @@ -204,6 +206,9 @@ type outcome = | Write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name) * (bool -> instruction_state) +(* Request the result of store-exclusive *) +| Excl_res of (bool -> instruction_state) + (* Tell the system a write is imminent, at address lifted tainted by register list, of size nat *) | Write_ea of write_kind * address_lifted * nat * maybe (list reg_name) * instruction_state @@ -248,7 +253,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_writes -> memory_write_eas -> memory_write_vals -> barriers -> excl_res -> 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 *) |