summaryrefslogtreecommitdiff
path: root/src/lem_interp/sail_impl_base.lem
diff options
context:
space:
mode:
Diffstat (limited to 'src/lem_interp/sail_impl_base.lem')
-rw-r--r--src/lem_interp/sail_impl_base.lem373
1 files changed, 5 insertions, 368 deletions
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 219677ac..f029b952 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -49,7 +49,7 @@
(*========================================================================*)
open import Pervasives_extra
-
+open import Sail_instr_kinds
class ( EnumerationType 'a )
@@ -478,373 +478,10 @@ end
(* Data structures for building up instructions *)
-(* careful: changes in the read/write/barrier kinds have to be
- reflected in deep_shallow_convert *)
-type read_kind =
- (* common reads *)
- | Read_plain
- (* Power reads *)
- | Read_reserve
- (* AArch64 reads *)
- | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream
- (* RISC-V reads *)
- | Read_RISCV_acquire | Read_RISCV_strong_acquire
- | Read_RISCV_reserved | Read_RISCV_reserved_acquire
- | Read_RISCV_reserved_strong_acquire
- (* x86 reads *)
- | Read_X86_locked (* the read part of a lock'd instruction (rmw) *)
-
-instance (Show read_kind)
- let show = 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"
- end
-end
-
-type write_kind =
- (* common writes *)
- | Write_plain
- (* Power writes *)
- | Write_conditional
- (* AArch64 writes *)
- | Write_release | Write_exclusive | Write_exclusive_release
- (* RISC-V *)
- | Write_RISCV_release | Write_RISCV_strong_release
- | Write_RISCV_conditional | Write_RISCV_conditional_release
- | Write_RISCV_conditional_strong_release
- (* x86 writes *)
- | Write_X86_locked (* the write part of a lock'd instruction (rmw) *)
-
-instance (Show write_kind)
- let show = 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"
- end
-end
-
-type barrier_kind =
- (* Power barriers *)
- Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync
- (* AArch64 barriers *)
- | Barrier_DMB | Barrier_DMB_ST | Barrier_DMB_LD | Barrier_DSB
- | Barrier_DSB_ST | Barrier_DSB_LD | Barrier_ISB
- | Barrier_TM_COMMIT
- (* MIPS barriers *)
- | Barrier_MIPS_SYNC
- (* 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_i
- (* X86 *)
- | Barrier_x86_MFENCE
-
-
-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_i -> "Barrier_RISCV_i"
- | Barrier_x86_MFENCE -> "Barrier_x86_MFENCE"
- end
-end
-
-type trans_kind =
- (* AArch64 *)
- | Transaction_start | Transaction_commit | Transaction_abort
-
-instance (Show trans_kind)
- let show = function
- | Transaction_start -> "Transaction_start"
- | Transaction_commit -> "Transaction_commit"
- | Transaction_abort -> "Transaction_abort"
- end
-end
-
-type instruction_kind =
- | IK_barrier of barrier_kind
- | IK_mem_read of read_kind
- | IK_mem_write of write_kind
- | IK_mem_rmw of (read_kind * write_kind)
- | IK_cond_branch
- (* unconditional branches are not distinguished in the instruction_kind;
- they just have particular nias (and will be IK_simple *)
- (* | IK_uncond_branch *)
- | IK_trans of trans_kind
- | 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_trans trans_kind -> "IK_trans " ^ (show trans_kind)
- | IK_simple -> "IK_simple"
- end
-end
-
-
-
-let ~{ocaml} read_kindCompare rk1 rk2 =
- match (rk1, rk2) with
- | (Read_plain, Read_plain) -> EQ
- | (Read_plain, Read_reserve) -> LT
- | (Read_plain, Read_acquire) -> LT
- | (Read_plain, Read_exclusive) -> LT
- | (Read_plain, Read_exclusive_acquire) -> LT
- | (Read_plain, Read_stream) -> LT
-
- | (Read_reserve, Read_plain) -> GT
- | (Read_reserve, Read_reserve) -> EQ
- | (Read_reserve, Read_acquire) -> LT
- | (Read_reserve, Read_exclusive) -> LT
- | (Read_reserve, Read_exclusive_acquire) -> LT
- | (Read_reserve, Read_stream) -> LT
-
- | (Read_acquire, Read_plain) -> GT
- | (Read_acquire, Read_reserve) -> GT
- | (Read_acquire, Read_acquire) -> EQ
- | (Read_acquire, Read_exclusive) -> LT
- | (Read_acquire, Read_exclusive_acquire) -> LT
- | (Read_acquire, Read_stream) -> LT
-
- | (Read_exclusive, Read_plain) -> GT
- | (Read_exclusive, Read_reserve) -> GT
- | (Read_exclusive, Read_acquire) -> GT
- | (Read_exclusive, Read_exclusive) -> EQ
- | (Read_exclusive, Read_exclusive_acquire) -> LT
- | (Read_exclusive, Read_stream) -> LT
-
- | (Read_exclusive_acquire, Read_plain) -> GT
- | (Read_exclusive_acquire, Read_reserve) -> GT
- | (Read_exclusive_acquire, Read_acquire) -> GT
- | (Read_exclusive_acquire, Read_exclusive) -> GT
- | (Read_exclusive_acquire, Read_exclusive_acquire) -> EQ
- | (Read_exclusive_acquire, Read_stream) -> GT
-
- | (Read_stream, Read_plain) -> GT
- | (Read_stream, Read_reserve) -> GT
- | (Read_stream, Read_acquire) -> GT
- | (Read_stream, Read_exclusive) -> GT
- | (Read_stream, Read_exclusive_acquire) -> GT
- | (Read_stream, Read_stream) -> EQ
-end
-let inline {ocaml} read_kindCompare = defaultCompare
-
-let ~{ocaml} read_kindLess b1 b2 = read_kindCompare b1 b2 = LT
-let ~{ocaml} read_kindLessEq b1 b2 = read_kindCompare b1 b2 <> GT
-let ~{ocaml} read_kindGreater b1 b2 = read_kindCompare b1 b2 = GT
-let ~{ocaml} read_kindGreaterEq b1 b2 = read_kindCompare b1 b2 <> LT
-
-let inline {ocaml} read_kindLess = defaultLess
-let inline {ocaml} read_kindLessEq = defaultLessEq
-let inline {ocaml} read_kindGreater = defaultGreater
-let inline {ocaml} read_kindGreaterEq = defaultGreaterEq
-
-instance (Ord read_kind)
- let compare = read_kindCompare
- let (<) = read_kindLess
- let (<=) = read_kindLessEq
- let (>) = read_kindGreater
- let (>=) = read_kindGreaterEq
-end
-
-let ~{ocaml} write_kindCompare wk1 wk2 =
- match (wk1, wk2) with
- | (Write_plain, Write_plain) -> EQ
- | (Write_plain, Write_conditional) -> LT
- | (Write_plain, Write_release) -> LT
- | (Write_plain, Write_exclusive) -> LT
- | (Write_plain, Write_exclusive_release) -> LT
-
- | (Write_conditional, Write_plain) -> GT
- | (Write_conditional, Write_conditional) -> EQ
- | (Write_conditional, Write_release) -> LT
- | (Write_conditional, Write_exclusive) -> LT
- | (Write_conditional, Write_exclusive_release) -> LT
-
- | (Write_release, Write_plain) -> GT
- | (Write_release, Write_conditional) -> GT
- | (Write_release, Write_release) -> EQ
- | (Write_release, Write_exclusive) -> LT
- | (Write_release, Write_exclusive_release) -> LT
-
- | (Write_exclusive, Write_plain) -> GT
- | (Write_exclusive, Write_conditional) -> GT
- | (Write_exclusive, Write_release) -> GT
- | (Write_exclusive, Write_exclusive) -> EQ
- | (Write_exclusive, Write_exclusive_release) -> LT
-
- | (Write_exclusive_release, Write_plain) -> GT
- | (Write_exclusive_release, Write_conditional) -> GT
- | (Write_exclusive_release, Write_release) -> GT
- | (Write_exclusive_release, Write_exclusive) -> GT
- | (Write_exclusive_release, Write_exclusive_release) -> EQ
-end
-let inline {ocaml} write_kindCompare = defaultCompare
-
-let ~{ocaml} write_kindLess b1 b2 = write_kindCompare b1 b2 = LT
-let ~{ocaml} write_kindLessEq b1 b2 = write_kindCompare b1 b2 <> GT
-let ~{ocaml} write_kindGreater b1 b2 = write_kindCompare b1 b2 = GT
-let ~{ocaml} write_kindGreaterEq b1 b2 = write_kindCompare b1 b2 <> LT
-
-let inline {ocaml} write_kindLess = defaultLess
-let inline {ocaml} write_kindLessEq = defaultLessEq
-let inline {ocaml} write_kindGreater = defaultGreater
-let inline {ocaml} write_kindGreaterEq = defaultGreaterEq
-
-instance (Ord write_kind)
- let compare = write_kindCompare
- let (<) = write_kindLess
- let (<=) = write_kindLessEq
- let (>) = write_kindGreater
- let (>=) = write_kindGreaterEq
-end
-
-(* Barrier comparison that uses less memory in Isabelle/HOL *)
-let ~{ocaml} barrier_number = function
- | Barrier_Sync -> (0 : natural)
- | 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_i -> 18
- | Barrier_x86_MFENCE -> 19
- end
-
-let ~{ocaml} barrier_kindCompare bk1 bk2 =
- let n1 = barrier_number bk1 in
- let n2 = barrier_number bk2 in
- if n1 < n2 then LT
- else if n1 = n2 then EQ
- else GT
-let inline {ocaml} barrier_kindCompare = defaultCompare
-
-(*let ~{ocaml} barrier_kindCompare bk1 bk2 =
- match (bk1, bk2) with
- | (Barrier_Sync, Barrier_Sync) -> EQ
- | (Barrier_Sync, _) -> LT
- | (_, Barrier_Sync) -> GT
-
- | (Barrier_LwSync, Barrier_LwSync) -> EQ
- | (Barrier_LwSync, _) -> LT
- | (_, Barrier_LwSync) -> GT
-
- | (Barrier_Eieio, Barrier_Eieio) -> EQ
- | (Barrier_Eieio, _) -> LT
- | (_, Barrier_Eieio) -> GT
-
- | (Barrier_Isync, Barrier_Isync) -> EQ
- | (Barrier_Isync, _) -> LT
- | (_, Barrier_Isync) -> GT
-
- | (Barrier_DMB, Barrier_DMB) -> EQ
- | (Barrier_DMB, _) -> LT
- | (_, Barrier_DMB) -> GT
-
- | (Barrier_DMB_ST, Barrier_DMB_ST) -> EQ
- | (Barrier_DMB_ST, _) -> LT
- | (_, Barrier_DMB_ST) -> GT
-
- | (Barrier_DMB_LD, Barrier_DMB_LD) -> EQ
- | (Barrier_DMB_LD, _) -> LT
- | (_, Barrier_DMB_LD) -> GT
-
- | (Barrier_DSB, Barrier_DSB) -> EQ
- | (Barrier_DSB, _) -> LT
- | (_, Barrier_DSB) -> GT
-
- | (Barrier_DSB_ST, Barrier_DSB_ST) -> EQ
- | (Barrier_DSB_ST, _) -> LT
- | (_, Barrier_DSB_ST) -> GT
-
- | (Barrier_DSB_LD, Barrier_DSB_LD) -> EQ
- | (Barrier_DSB_LD, _) -> LT
- | (_, Barrier_DSB_LD) -> GT
-
- | (Barrier_ISB, Barrier_ISB) -> EQ
- | (Barrier_ISB, _) -> LT
- | (_, Barrier_ISB) -> GT
-
- | (Barrier_TM_COMMIT, Barrier_TM_COMMIT) -> EQ
- | (Barrier_TM_COMMIT, _) -> LT
- | (_, Barrier_TM_COMMIT) -> GT
-
- | (Barrier_MIPS_SYNC, Barrier_MIPS_SYNC) -> EQ
- (* | (Barrier_MIPS_SYNC, _) -> LT
- | (_, Barrier_MIPS_SYNC) -> GT *)
-
- end*)
-
-let ~{ocaml} barrier_kindLess b1 b2 = barrier_kindCompare b1 b2 = LT
-let ~{ocaml} barrier_kindLessEq b1 b2 = barrier_kindCompare b1 b2 <> GT
-let ~{ocaml} barrier_kindGreater b1 b2 = barrier_kindCompare b1 b2 = GT
-let ~{ocaml} barrier_kindGreaterEq b1 b2 = barrier_kindCompare b1 b2 <> LT
-
-let inline {ocaml} barrier_kindLess = defaultLess
-let inline {ocaml} barrier_kindLessEq = defaultLessEq
-let inline {ocaml} barrier_kindGreater = defaultGreater
-let inline {ocaml} barrier_kindGreaterEq = defaultGreaterEq
-
-instance (Ord barrier_kind)
- let compare = barrier_kindCompare
- let (<) = barrier_kindLess
- let (<=) = barrier_kindLessEq
- let (>) = barrier_kindGreater
- let (>=) = barrier_kindGreaterEq
-end
+(* read_kind, write_kind, barrier_kind, trans_kind and instruction_kind have
+ been moved to sail_instr_kinds.lem. This removes the dependency of the
+ shallow embedding on the rest of sail_impl_base.lem, and helps avoid name
+ clashes between the different monad types. *)
type event =
| E_read_mem of read_kind * address_lifted * nat * maybe (list reg_name)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 09:59:04 +0000