diff options
| author | Peter Sewell | 2017-01-25 15:01:27 +0000 |
|---|---|---|
| committer | Peter Sewell | 2017-01-25 15:01:27 +0000 |
| commit | b357733fefdbbbdd4efa56c8b3ddc6bcbeca4c28 (patch) | |
| tree | 8b5417d74da0c0d1280eceb8fcef4af71a5250bf /src/lem_interp/sail_impl_base.lem | |
| parent | c588e96bd15572d929d2f957b2a9b2ac86814c0a (diff) | |
| parent | 2968c83f019b6945ac06a6faf8aaf518e92bdc29 (diff) | |
Merge branch 'master' of bitbucket.org:Peter_Sewell/sail
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 |