diff options
| author | Christopher Pulte | 2016-09-09 13:30:10 +0100 |
|---|---|---|
| committer | Christopher Pulte | 2016-09-09 13:30:10 +0100 |
| commit | 70b8a25d893e8bec8ec05fe313c8e883fb3e8fbc (patch) | |
| tree | 31ee4579d3398e243607b67cd40edd788eeb6f06 /src/lem_interp/interp_interface.lem | |
| parent | c669e42539f4b26adc6458ed9293cc6469f87bc6 (diff) | |
update instruction_analysis to support nias and instruction kind
Diffstat (limited to 'src/lem_interp/interp_interface.lem')
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 2da9e060..5473e1a0 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -416,6 +416,17 @@ type barrier_kind = (* AArch64 barriers *) | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB +type instruction_kind = + | IK_barrier of barrier_kind + | IK_mem_read of read_kind + | IK_mem_write of write_kind +(* SS reinstating cond_branches +at present branches are not distinguished in the instruction_kind; +they just have particular nias (and will be IK_simple *) + | IK_cond_branch +(* | IK_uncond_branch *) + | IK_simple + (*Map between external functions as preceived from a Sail spec and the actual implementation of the function *) type external_functions = list (string * (Interp.value -> Interp.value)) @@ -1156,7 +1167,7 @@ val translate_address : val instruction_analysis : context -> end_flag -> string -> (string -> (nat * nat * direction * (nat * nat))) - -> maybe (list (reg_name * register_value)) -> instruction -> (list reg_name * list reg_name * list reg_name) + -> maybe (list (reg_name * register_value)) -> instruction -> (list reg_name * list reg_name * list reg_name * list address) val byte_list_of_memory_value : end_flag -> memory_value -> maybe (list byte) let byte_list_of_memory_value endian mv = |