diff options
Diffstat (limited to 'src/lem_interp/interp_interface.lem')
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index a7049633..e821aae8 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -14,7 +14,7 @@ val tracking_dependencies : interp_mode -> bool (*Concrete types*) type read_kind = Read_plain | Read_reserve | Read_acquire type write_kind = Write_plain | Write_conditional | Write_release -type barrier_kind = Plain | Sync | LwSync | Eieio | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD +type barrier_kind = Sync | LwSync | Eieio | Isync | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB (* PS removed "plain" and added "Isync" and "ISB" *) type value = | Bitvector of list bool (* For register accesses *) @@ -36,9 +36,9 @@ type reg_name = type outcome = (* Request to read memory, value is location to read followed by registers that location depended on when mode.track_values *) -| Read_mem of read_kind * value * maybe (list reg_name) * (value -> instruction_state) +| Read_mem of read_kind * value * integer * maybe (list reg_name) * (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 * value * maybe (list reg_name) * value * maybe (list reg_name) * (bool -> instruction_state) +| Write_mem of write_kind * value * integer * maybe (list reg_name) * value * maybe (list reg_name) * (bool -> instruction_state) (* Request a memory barrier *) | Barrier of barrier_kind * instruction_state (* Request to read register, will track dependency when mode.track_values *) @@ -53,8 +53,8 @@ type outcome = | Error of string type event = -| E_read_mem of read_kind * value * maybe (list reg_name) -| E_write_mem of write_kind * value * maybe (list reg_name) * value * maybe (list reg_name) +| E_read_mem of read_kind * value * integer * maybe (list reg_name) +| E_write_mem of write_kind * value * integer * maybe (list reg_name) * value * maybe (list reg_name) | E_barrier of barrier_kind | E_read_reg of reg_name | E_write_reg of reg_name * value |