diff options
| author | Robert Norton | 2017-10-09 16:38:03 +0100 |
|---|---|---|
| committer | Robert Norton | 2017-10-09 16:38:03 +0100 |
| commit | 93dfd61038583eac852e5e3ea66c46817a610bbe (patch) | |
| tree | 60d76226ef8ff0e23d18997b618466320d9ab0fa /src/lem_interp | |
| parent | 97b808681f951a962cdb3c087d79aee5556a7089 (diff) | |
add translations for missing read/write kinds.
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 1c993ba0..8199f271 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -578,6 +578,12 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | "Read_exclusive" -> Read_exclusive | "Read_exclusive_acquire" -> Read_exclusive_acquire | "Read_stream" -> Read_stream + | "Read_RISCV_acquire" -> Read_RISCV_acquire + | "Read_RISCV_strong_acquire" -> Read_RISCV_strong_acquire + | "Read_RISCV_reserved" -> Read_RISCV_reserved + | "Read_RISCV_reserved_acquire" -> Read_RISCV_reserved_acquire + | "Read_RISCV_reserved_strong_acquire" -> Read_RISCV_reserved_strong_acquire + | "Read_X86_locked" -> Read_X86_locked | r -> failwith ("unknown read kind: " ^ r) end in let writek_to_writek = function | "Write_plain" -> Write_plain @@ -585,6 +591,12 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | "Write_release" -> Write_release | "Write_exclusive" -> Write_exclusive | "Write_exclusive_release" -> Write_exclusive_release + | "Write_RISCV_release" -> Write_RISCV_release + | "Write_RISCV_strong_release" -> Write_RISCV_strong_release + | "Write_RISCV_conditional" -> Write_RISCV_conditional + | "Write_RISCV_conditional_release" -> Write_RISCV_conditional_release + | "Write_RISCV_conditional_strong_release" -> Write_RISCV_conditional_strong_release + | "Write_X86_locked" -> Write_X86_locked | w -> failwith ("unknown write kind: " ^ w) end in let ik_to_ik = function | Interp_ast.V_ctor (Id_aux (Id "IK_barrier") _) _ _ |