From 1bb77b31f84946f036c0b7e37245809bbdb82def Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Thu, 18 Jul 2019 10:13:10 +0100 Subject: Support DMB/DSB domains --- src/lem_interp/interp_inter_imp.lem | 63 +------------ src/lem_interp/sail2_instr_kinds.lem | 175 +++++++++++++++++++++-------------- 2 files changed, 109 insertions(+), 129 deletions(-) (limited to 'src/lem_interp') diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 74e43a8f..3413494e 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -579,74 +579,13 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | Interp_ast.V_ctor (Id_aux (Id "NIAFP_indirect_address") _) _ _ _ -> NIA_indirect_address | _ -> failwith "Register footprint analysis did not return nia of expected type" end in - let readk_to_readk = function - | "Read_plain" -> Read_plain - | "Read_reserve" -> Read_reserve - | "Read_acquire" -> Read_acquire - | "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 - | "Write_conditional" -> Write_conditional - | "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") _) _ _ - (Interp_ast.V_ctor (Id_aux (Id b) _) _ _ _) -> - IK_barrier (match b with - | "Barrier_Sync" -> Barrier_Sync - | "Barrier_LwSync" -> Barrier_LwSync - | "Barrier_Eieio" -> Barrier_Eieio - | "Barrier_Isync" -> Barrier_Isync - | "Barrier_DMB" -> Barrier_DMB - | "Barrier_DMB_ST" -> Barrier_DMB_ST - | "Barrier_DMB_LD" -> Barrier_DMB_LD - | "Barrier_DSB" -> Barrier_DSB - | "Barrier_DSB_ST" -> Barrier_DSB_ST - | "Barrier_DSB_LD" -> Barrier_DSB_LD - | "Barrier_ISB" -> Barrier_ISB - | "Barrier_MIPS_SYNC" -> Barrier_MIPS_SYNC - | "Barrier_x86_MFENCE" -> Barrier_x86_MFENCE - end) - | Interp_ast.V_ctor (Id_aux (Id "IK_mem_read") _) _ _ - (Interp_ast.V_ctor (Id_aux (Id r) _) _ _ _) -> - IK_mem_read(readk_to_readk r) - | Interp_ast.V_ctor (Id_aux (Id "IK_mem_write") _) _ _ - (Interp_ast.V_ctor (Id_aux (Id w) _) _ _ _) -> - IK_mem_write(writek_to_writek w) - | Interp_ast.V_ctor (Id_aux (Id "IK_mem_rmw") _) _ _ - (Interp_ast.V_tuple [(Interp_ast.V_ctor (Id_aux (Id readk) _) _ _ _) ; - (Interp_ast.V_ctor (Id_aux (Id writek) _) _ _ _)]) -> - IK_mem_rmw(readk_to_readk readk, writek_to_writek writek) - | Interp_ast.V_ctor (Id_aux (Id "IK_branch") _) _ _ _ -> - IK_branch - | Interp_ast.V_ctor (Id_aux (Id "IK_simple") _) _ _ _ -> - IK_simple - | _ -> failwith "Analysis returned unexpected instruction kind" - end in let (regs1,regs2,regs3,nias,dia,ik) = (List.map reg_to_reg_name regs1, List.map reg_to_reg_name regs2, List.map reg_to_reg_name regs3, List.map nia_to_nia nias, dia_to_dia dia, - ik_to_ik ik) in + fromInterpValue ik) in ((regs1,regs2,regs3,nias,dia,ik), events) | _ -> Assert_extra.failwith "Analysis did not return a four-tuple of lists" end) | Ivh_value_after_exn _ -> Assert_extra.failwith "Instruction analysis failed" diff --git a/src/lem_interp/sail2_instr_kinds.lem b/src/lem_interp/sail2_instr_kinds.lem index bd3a3eb7..f3cdfbc9 100644 --- a/src/lem_interp/sail2_instr_kinds.lem +++ b/src/lem_interp/sail2_instr_kinds.lem @@ -136,58 +136,86 @@ instance (Show write_kind) end end +type a64_barrier_domain = + A64_FullShare + | A64_InnerShare + | A64_OuterShare + | A64_NonShare + +type a64_barrier_type = + A64_barrier_all + | A64_barrier_LD + | A64_barrier_ST + type barrier_kind = (* Power barriers *) - Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync + Barrier_Sync of unit | Barrier_LwSync of unit | Barrier_Eieio of unit | Barrier_Isync of unit (* AArch64 barriers *) - | Barrier_DMB | Barrier_DMB_ST | Barrier_DMB_LD | Barrier_DSB - | Barrier_DSB_ST | Barrier_DSB_LD | Barrier_ISB - | Barrier_TM_COMMIT + | Barrier_DMB of (a64_barrier_domain * a64_barrier_type) + | Barrier_DSB of (a64_barrier_domain * a64_barrier_type) + | Barrier_ISB of unit + | Barrier_TM_COMMIT of unit (* MIPS barriers *) - | Barrier_MIPS_SYNC + | Barrier_MIPS_SYNC of unit (* RISC-V barriers *) - | Barrier_RISCV_rw_rw - | Barrier_RISCV_r_rw - | Barrier_RISCV_r_r - | Barrier_RISCV_rw_w - | Barrier_RISCV_w_w - | Barrier_RISCV_w_rw - | Barrier_RISCV_rw_r - | Barrier_RISCV_r_w - | Barrier_RISCV_w_r - | Barrier_RISCV_tso - | Barrier_RISCV_i + | Barrier_RISCV_rw_rw of unit + | Barrier_RISCV_r_rw of unit + | Barrier_RISCV_r_r of unit + | Barrier_RISCV_rw_w of unit + | Barrier_RISCV_w_w of unit + | Barrier_RISCV_w_rw of unit + | Barrier_RISCV_rw_r of unit + | Barrier_RISCV_r_w of unit + | Barrier_RISCV_w_r of unit + | Barrier_RISCV_tso of unit + | Barrier_RISCV_i of unit (* X86 *) - | Barrier_x86_MFENCE + | Barrier_x86_MFENCE of unit +let string_a64_barrier_domain = function + | A64_FullShare -> "A64_FullShare" + | A64_InnerShare -> "A64_InnerShare" + | A64_OuterShare -> "A64_OuterShare" + | A64_NonShare -> "A64_NonShare" +end + +instance (Show a64_barrier_domain) + let show = string_a64_barrier_domain +end + +let string_a64_barrier_type = function + | A64_barrier_all -> "A64_barrier_all" + | A64_barrier_LD -> "A64_barrier_LD" + | A64_barrier_ST -> "A64_barrier_ST" +end + +instance (Show a64_barrier_type) + let show = string_a64_barrier_type +end instance (Show barrier_kind) let show = function - | Barrier_Sync -> "Barrier_Sync" - | Barrier_LwSync -> "Barrier_LwSync" - | Barrier_Eieio -> "Barrier_Eieio" - | Barrier_Isync -> "Barrier_Isync" - | Barrier_DMB -> "Barrier_DMB" - | Barrier_DMB_ST -> "Barrier_DMB_ST" - | Barrier_DMB_LD -> "Barrier_DMB_LD" - | Barrier_DSB -> "Barrier_DSB" - | Barrier_DSB_ST -> "Barrier_DSB_ST" - | Barrier_DSB_LD -> "Barrier_DSB_LD" - | Barrier_ISB -> "Barrier_ISB" - | Barrier_TM_COMMIT -> "Barrier_TM_COMMIT" - | Barrier_MIPS_SYNC -> "Barrier_MIPS_SYNC" - | Barrier_RISCV_rw_rw -> "Barrier_RISCV_rw_rw" - | Barrier_RISCV_r_rw -> "Barrier_RISCV_r_rw" - | Barrier_RISCV_r_r -> "Barrier_RISCV_r_r" - | Barrier_RISCV_rw_w -> "Barrier_RISCV_rw_w" - | Barrier_RISCV_w_w -> "Barrier_RISCV_w_w" - | Barrier_RISCV_w_rw -> "Barrier_RISCV_w_rw" - | Barrier_RISCV_rw_r -> "Barrier_RISCV_rw_r" - | Barrier_RISCV_r_w -> "Barrier_RISCV_r_w" - | Barrier_RISCV_w_r -> "Barrier_RISCV_w_r" - | Barrier_RISCV_tso -> "Barrier_RISCV_tso" - | Barrier_RISCV_i -> "Barrier_RISCV_i" - | Barrier_x86_MFENCE -> "Barrier_x86_MFENCE" + | Barrier_Sync () -> "Barrier_Sync" + | Barrier_LwSync () -> "Barrier_LwSync" + | Barrier_Eieio () -> "Barrier_Eieio" + | Barrier_Isync () -> "Barrier_Isync" + | Barrier_DMB (dom,typ) -> "Barrier_DMB (" ^ (show dom) ^ ", " ^ (show typ) ^ ")" + | Barrier_DSB (dom,typ) -> "Barrier_DSB (" ^ (show dom) ^ ", " ^ (show typ) ^ ")" + | Barrier_ISB () -> "Barrier_ISB" + | Barrier_TM_COMMIT () -> "Barrier_TM_COMMIT" + | Barrier_MIPS_SYNC () -> "Barrier_MIPS_SYNC" + | Barrier_RISCV_rw_rw () -> "Barrier_RISCV_rw_rw" + | Barrier_RISCV_r_rw () -> "Barrier_RISCV_r_rw" + | Barrier_RISCV_r_r () -> "Barrier_RISCV_r_r" + | Barrier_RISCV_rw_w () -> "Barrier_RISCV_rw_w" + | Barrier_RISCV_w_w () -> "Barrier_RISCV_w_w" + | Barrier_RISCV_w_rw () -> "Barrier_RISCV_w_rw" + | Barrier_RISCV_rw_r () -> "Barrier_RISCV_rw_r" + | Barrier_RISCV_r_w () -> "Barrier_RISCV_r_w" + | Barrier_RISCV_w_r () -> "Barrier_RISCV_w_r" + | Barrier_RISCV_tso () -> "Barrier_RISCV_tso" + | Barrier_RISCV_i () -> "Barrier_RISCV_i" + | Barrier_x86_MFENCE () -> "Barrier_x86_MFENCE" end end @@ -304,32 +332,45 @@ instance (EnumerationType write_kind) end end +instance (EnumerationType a64_barrier_domain) + let toNat = function + | A64_FullShare -> 0 + | A64_InnerShare -> 1 + | A64_OuterShare -> 2 + | A64_NonShare -> 3 + end +end + +instance (EnumerationType a64_barrier_type) + let toNat = function + | A64_barrier_all -> 0 + | A64_barrier_LD -> 1 + | A64_barrier_ST -> 2 + end +end + instance (EnumerationType barrier_kind) let toNat = function - | Barrier_Sync -> 0 - | Barrier_LwSync -> 1 - | Barrier_Eieio ->2 - | Barrier_Isync -> 3 - | Barrier_DMB -> 4 - | Barrier_DMB_ST -> 5 - | Barrier_DMB_LD -> 6 - | Barrier_DSB -> 7 - | Barrier_DSB_ST -> 8 - | Barrier_DSB_LD -> 9 - | Barrier_ISB -> 10 - | Barrier_TM_COMMIT -> 11 - | Barrier_MIPS_SYNC -> 12 - | Barrier_RISCV_rw_rw -> 13 - | Barrier_RISCV_r_rw -> 14 - | Barrier_RISCV_r_r -> 15 - | Barrier_RISCV_rw_w -> 16 - | Barrier_RISCV_w_w -> 17 - | Barrier_RISCV_w_rw -> 18 - | Barrier_RISCV_rw_r -> 19 - | Barrier_RISCV_r_w -> 20 - | Barrier_RISCV_w_r -> 21 - | Barrier_RISCV_tso -> 22 - | Barrier_RISCV_i -> 23 - | Barrier_x86_MFENCE -> 24 + | Barrier_Sync () -> 0 + | Barrier_LwSync () -> 1 + | Barrier_Eieio () -> 2 + | Barrier_Isync () -> 3 + | Barrier_DMB (dom,typ) -> 4 + (toNat dom) + (4 * (toNat typ)) (* 4-15 *) + | Barrier_DSB (dom,typ) -> 16 + (toNat dom) + (4 * (toNat typ)) (* 16-27 *) + | Barrier_ISB () -> 28 + | Barrier_TM_COMMIT () -> 29 + | Barrier_MIPS_SYNC () -> 30 + | Barrier_RISCV_rw_rw () -> 31 + | Barrier_RISCV_r_rw () -> 32 + | Barrier_RISCV_r_r () -> 33 + | Barrier_RISCV_rw_w () -> 34 + | Barrier_RISCV_w_w () -> 35 + | Barrier_RISCV_w_rw () -> 36 + | Barrier_RISCV_rw_r () -> 37 + | Barrier_RISCV_r_w () -> 38 + | Barrier_RISCV_w_r () -> 39 + | Barrier_RISCV_tso () -> 40 + | Barrier_RISCV_i () -> 41 + | Barrier_x86_MFENCE () -> 42 end end -- cgit v1.2.3