diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 1 | ||||
| -rw-r--r-- | src/lem_interp/sail_impl_base.lem | 26 |
2 files changed, 27 insertions, 0 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index d35653c9..a39f3f3a 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -535,6 +535,7 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | "Barrier_DSB_ST" -> Barrier_DSB_ST | "Barrier_DSB_LD" -> Barrier_DSB_LD | "Barrier_ISB" -> Barrier_ISB + | "Barrier_MIPS_SYNC" -> Barrier_MIPS_SYNC end) | Interp.V_ctor (Id_aux (Id "IK_mem_read") _) _ _ (Interp.V_ctor (Id_aux (Id r) _) _ _ _) -> diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index e29b3391..7ede9aa6 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -402,6 +402,8 @@ type barrier_kind = (* AArch64 barriers *) | Barrier_DMB | Barrier_DMB_ST | Barrier_DMB_LD | Barrier_DSB | Barrier_DSB_ST | Barrier_DSB_LD | Barrier_ISB + (* MIPS barriers *) + | Barrier_MIPS_SYNC type instruction_kind = | IK_barrier of barrier_kind @@ -627,6 +629,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 = | (Barrier_Sync, Barrier_DSB_ST) -> LT | (Barrier_Sync, Barrier_DSB_LD) -> LT | (Barrier_Sync, Barrier_ISB) -> LT + | (Barrier_Sync, Barrier_MIPS_SYNC) -> LT | (Barrier_LwSync, Barrier_Sync) -> GT | (Barrier_LwSync, Barrier_LwSync) -> EQ @@ -639,6 +642,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 = | (Barrier_LwSync, Barrier_DSB_ST) -> LT | (Barrier_LwSync, Barrier_DSB_LD) -> LT | (Barrier_LwSync, Barrier_ISB) -> LT + | (Barrier_LwSync, Barrier_MIPS_SYNC) -> LT | (Barrier_Eieio, Barrier_Sync) -> GT | (Barrier_Eieio, Barrier_LwSync) -> GT @@ -651,6 +655,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 = | (Barrier_Eieio, Barrier_DSB_ST) -> LT | (Barrier_Eieio, Barrier_DSB_LD) -> LT | (Barrier_Eieio, Barrier_ISB) -> LT + | (Barrier_Eieio, Barrier_MIPS_SYNC) -> LT | (Barrier_Isync, Barrier_Sync) -> GT | (Barrier_Isync, Barrier_LwSync) -> GT @@ -663,6 +668,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 = | (Barrier_Isync, Barrier_DSB_ST) -> LT | (Barrier_Isync, Barrier_DSB_LD) -> LT | (Barrier_Isync, Barrier_ISB) -> LT + | (Barrier_Isync, Barrier_MIPS_SYNC) -> LT | (Barrier_DMB, Barrier_Sync) -> GT | (Barrier_DMB, Barrier_LwSync) -> GT @@ -675,6 +681,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 = | (Barrier_DMB, Barrier_DSB_ST) -> LT | (Barrier_DMB, Barrier_DSB_LD) -> LT | (Barrier_DMB, Barrier_ISB) -> LT + | (Barrier_DMB, Barrier_MIPS_SYNC) -> LT | (Barrier_DMB_ST, Barrier_Sync) -> GT | (Barrier_DMB_ST, Barrier_LwSync) -> GT @@ -687,6 +694,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 = | (Barrier_DMB_ST, Barrier_DSB_ST) -> LT | (Barrier_DMB_ST, Barrier_DSB_LD) -> LT | (Barrier_DMB_ST, Barrier_ISB) -> LT + | (Barrier_DMB_ST, Barrier_MIPS_SYNC) -> LT | (Barrier_DMB_LD, Barrier_Sync) -> GT | (Barrier_DMB_LD, Barrier_LwSync) -> GT @@ -699,6 +707,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 = | (Barrier_DMB_LD, Barrier_DSB_ST) -> LT | (Barrier_DMB_LD, Barrier_DSB_LD) -> LT | (Barrier_DMB_LD, Barrier_ISB) -> LT + | (Barrier_DMB_LD, Barrier_MIPS_SYNC) -> LT | (Barrier_DSB, Barrier_Sync) -> GT | (Barrier_DSB, Barrier_LwSync) -> GT @@ -711,6 +720,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 = | (Barrier_DSB, Barrier_DSB_ST) -> LT | (Barrier_DSB, Barrier_DSB_LD) -> LT | (Barrier_DSB, Barrier_ISB) -> LT + | (Barrier_DSB, Barrier_MIPS_SYNC) -> LT | (Barrier_DSB_ST, Barrier_Sync) -> GT | (Barrier_DSB_ST, Barrier_LwSync) -> GT @@ -723,6 +733,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 = | (Barrier_DSB_ST, Barrier_DSB_ST) -> EQ | (Barrier_DSB_ST, Barrier_DSB_LD) -> LT | (Barrier_DSB_ST, Barrier_ISB) -> LT + | (Barrier_DSB_ST, Barrier_MIPS_SYNC) -> LT | (Barrier_DSB_LD, Barrier_Sync) -> GT | (Barrier_DSB_LD, Barrier_LwSync) -> GT @@ -735,6 +746,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 = | (Barrier_DSB_LD, Barrier_DSB_ST) -> GT | (Barrier_DSB_LD, Barrier_DSB_LD) -> EQ | (Barrier_DSB_LD, Barrier_ISB) -> LT + | (Barrier_DSB_LD, Barrier_MIPS_SYNC) -> LT | (Barrier_ISB, Barrier_Sync) -> GT | (Barrier_ISB, Barrier_LwSync) -> GT @@ -747,6 +759,20 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 = | (Barrier_ISB, Barrier_DSB_ST) -> GT | (Barrier_ISB, Barrier_DSB_LD) -> GT | (Barrier_ISB, Barrier_ISB) -> EQ + | (Barrier_ISB, Barrier_MIPS_SYNC) -> LT + + | (Barrier_ISB, Barrier_Sync) -> GT + | (Barrier_ISB, Barrier_LwSync) -> GT + | (Barrier_ISB, Barrier_Eieio) -> GT + | (Barrier_ISB, Barrier_Isync) -> GT + | (Barrier_ISB, Barrier_DMB) -> GT + | (Barrier_ISB, Barrier_DMB_ST) -> GT + | (Barrier_ISB, Barrier_DMB_LD) -> GT + | (Barrier_ISB, Barrier_DSB) -> GT + | (Barrier_ISB, Barrier_DSB_ST) -> GT + | (Barrier_ISB, Barrier_DSB_LD) -> GT + | (Barrier_ISB, Barrier_ISB) -> GT + | (Barrier_ISB, Barrier_MIPS_SYNC) -> EQ end let inline {ocaml} barrier_kindCompare = defaultCompare |