diff options
Diffstat (limited to 'src/lem_interp/sail_impl_base.lem')
| -rw-r--r-- | src/lem_interp/sail_impl_base.lem | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 76ac1797..3f38f521 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -398,6 +398,18 @@ type write_kind = (* AArch64 writes *) | Write_release | Write_exclusive | Write_exclusive_release +instance (Show write_kind) + let show = function + | Write_plain -> "Write_plain" + | Write_tag -> "Write_tag" + | Write_tag_conditional -> "Write_tag_conditional" + | Write_conditional -> "Write_conditional" + | Write_release -> "Write_release" + | Write_exclusive -> "Write_exclusive" + | Write_exclusive_release -> "Write_exclusive_release" + end +end + type barrier_kind = (* Power barriers *) Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync @@ -407,6 +419,23 @@ type barrier_kind = (* MIPS barriers *) | Barrier_MIPS_SYNC +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_MIPS_SYNC -> "Barrier_MIPS_SYNC" + end +end + type instruction_kind = | IK_barrier of barrier_kind | IK_mem_read of read_kind @@ -419,6 +448,18 @@ they just have particular nias (and will be IK_simple *) | IK_simple +instance (Show instruction_kind) + let show = function + | IK_barrier barrier_kind -> "IK_barrier " ^ (show barrier_kind) + | IK_mem_read read_kind -> "IK_mem_read " ^ (show read_kind) + | IK_mem_write write_kind -> "IK_mem_write " ^ (show write_kind) + | IK_cond_branch -> "IK_cond_branch" + | IK_simple -> "IK_simple" + end +end + + + let ~{ocaml} read_kindCompare rk1 rk2 = match (rk1, rk2) with | (Read_plain, Read_plain) -> EQ |