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.lem75
1 files changed, 66 insertions, 9 deletions
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 60c7bf0b..b4f92ec9 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -367,7 +367,7 @@ end
type read_kind =
(* common reads *)
- Read_plain
+ | Read_plain
| Read_tag | Read_tag_reserve (*For reading the tag of tagged memory*)
(* Power reads *)
| Read_reserve
@@ -378,6 +378,7 @@ instance (Show read_kind)
let show = function
| Read_plain -> "Read_plain"
| Read_tag -> "Read_tag"
+ | Read_tag_reserve -> "Read_tag_reserve"
| Read_reserve -> "Read_reserve"
| Read_acquire -> "Read_acquire"
| Read_exclusive -> "Read_exclusive"
@@ -388,7 +389,7 @@ end
type write_kind =
(* common writes *)
- Write_plain
+ | Write_plain
| Write_tag | Write_tag_conditional (*For writing the tag of tagged memory*)
(* Power writes *)
| Write_conditional
@@ -446,6 +447,8 @@ let ~{ocaml} read_kindCompare rk1 rk2 =
| (Read_plain, Read_exclusive) -> LT
| (Read_plain, Read_exclusive_acquire) -> LT
| (Read_plain, Read_stream) -> LT
+ | (Read_plain, Read_tag) -> LT
+ | (Read_plain, Read_tag_reserve) -> LT
| (Read_reserve, Read_plain) -> GT
| (Read_reserve, Read_reserve) -> EQ
@@ -453,6 +456,8 @@ let ~{ocaml} read_kindCompare rk1 rk2 =
| (Read_reserve, Read_exclusive) -> LT
| (Read_reserve, Read_exclusive_acquire) -> LT
| (Read_reserve, Read_stream) -> LT
+ | (Read_reserve, Read_tag) -> LT
+ | (Read_reserve, Read_tag_reserve) -> LT
| (Read_acquire, Read_plain) -> GT
| (Read_acquire, Read_reserve) -> GT
@@ -460,6 +465,8 @@ let ~{ocaml} read_kindCompare rk1 rk2 =
| (Read_acquire, Read_exclusive) -> LT
| (Read_acquire, Read_exclusive_acquire) -> LT
| (Read_acquire, Read_stream) -> LT
+ | (Read_acquire, Read_tag) -> LT
+ | (Read_acquire, Read_tag_reserve) -> LT
| (Read_exclusive, Read_plain) -> GT
| (Read_exclusive, Read_reserve) -> GT
@@ -467,6 +474,8 @@ let ~{ocaml} read_kindCompare rk1 rk2 =
| (Read_exclusive, Read_exclusive) -> EQ
| (Read_exclusive, Read_exclusive_acquire) -> LT
| (Read_exclusive, Read_stream) -> LT
+ | (Read_exclusive, Read_tag) -> LT
+ | (Read_exclusive, Read_tag_reserve) -> LT
| (Read_exclusive_acquire, Read_plain) -> GT
| (Read_exclusive_acquire, Read_reserve) -> GT
@@ -474,6 +483,8 @@ let ~{ocaml} read_kindCompare rk1 rk2 =
| (Read_exclusive_acquire, Read_exclusive) -> GT
| (Read_exclusive_acquire, Read_exclusive_acquire) -> EQ
| (Read_exclusive_acquire, Read_stream) -> GT
+ | (Read_exclusive_acquire, Read_tag) -> LT
+ | (Read_exclusive_acquire, Read_tag_reserve) -> LT
| (Read_stream, Read_plain) -> GT
| (Read_stream, Read_reserve) -> GT
@@ -481,6 +492,26 @@ let ~{ocaml} read_kindCompare rk1 rk2 =
| (Read_stream, Read_exclusive) -> GT
| (Read_stream, Read_exclusive_acquire) -> GT
| (Read_stream, Read_stream) -> EQ
+ | (Read_stream, Read_tag) -> LT
+ | (Read_stream, Read_tag_reserve) -> LT
+
+ | (Read_tag, Read_plain) -> GT
+ | (Read_tag, Read_reserve) -> GT
+ | (Read_tag, Read_acquire) -> GT
+ | (Read_tag, Read_exclusive) -> GT
+ | (Read_tag, Read_exclusive_acquire) -> GT
+ | (Read_tag, Read_stream) -> GT
+ | (Read_tag, Read_tag) -> EQ
+ | (Read_tag, Read_tag_reserve) -> LT
+
+ | (Read_tag_reserve, Read_plain) -> GT
+ | (Read_tag_reserve, Read_reserve) -> GT
+ | (Read_tag_reserve, Read_acquire) -> GT
+ | (Read_tag_reserve, Read_exclusive) -> GT
+ | (Read_tag_reserve, Read_exclusive_acquire) -> GT
+ | (Read_tag_reserve, Read_stream) -> GT
+ | (Read_tag_reserve, Read_tag) -> GT
+ | (Read_tag_reserve, Read_tag_reserve) -> EQ
end
let inline {ocaml} read_kindCompare = defaultCompare
@@ -509,30 +540,56 @@ let ~{ocaml} write_kindCompare wk1 wk2 =
| (Write_plain, Write_release) -> LT
| (Write_plain, Write_exclusive) -> LT
| (Write_plain, Write_exclusive_release) -> LT
+ | (Write_plain, Write_tag) -> LT
+ | (Write_plain, Write_tag_conditional) -> 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_conditional, Write_tag) -> LT
+ | (Write_conditional, Write_tag_conditional) -> 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_release, Write_tag) -> LT
+ | (Write_release, Write_tag_conditional) -> 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, Write_tag) -> LT
+ | (Write_exclusive, Write_tag_conditional) -> 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
+ | (Write_exclusive_release, Write_tag) -> LT
+ | (Write_exclusive_release, Write_tag_conditional) -> LT
+
+ | (Write_tag, Write_plain) -> GT
+ | (Write_tag, Write_conditional) -> GT
+ | (Write_tag, Write_release) -> GT
+ | (Write_tag, Write_exclusive) -> GT
+ | (Write_tag, Write_exclusive_release) -> GT
+ | (Write_tag, Write_tag) -> EQ
+ | (Write_tag, Write_tag_conditional) -> LT
+
+ | (Write_tag_conditional, Write_plain) -> GT
+ | (Write_tag_conditional, Write_conditional) -> GT
+ | (Write_tag_conditional, Write_release) -> GT
+ | (Write_tag_conditional, Write_exclusive) -> GT
+ | (Write_tag_conditional, Write_exclusive_release) -> GT
+ | (Write_tag_conditional, Write_tag) -> GT
+ | (Write_tag_conditional, Write_tag_conditional) -> EQ
end
let inline {ocaml} write_kindCompare = defaultCompare
@@ -607,7 +664,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 =
| (DMB, Sync) -> GT
| (DMB, LwSync) -> GT
| (DMB, Eieio) -> GT
- | (DMB, ISync) -> GT
+ | (DMB, Isync) -> GT
| (DMB, DMB) -> EQ
| (DMB, DMB_ST) -> LT
| (DMB, DMB_LD) -> LT
@@ -619,7 +676,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 =
| (DMB_ST, Sync) -> GT
| (DMB_ST, LwSync) -> GT
| (DMB_ST, Eieio) -> GT
- | (DMB_ST, ISync) -> GT
+ | (DMB_ST, Isync) -> GT
| (DMB_ST, DMB) -> GT
| (DMB_ST, DMB_ST) -> EQ
| (DMB_ST, DMB_LD) -> LT
@@ -631,7 +688,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 =
| (DMB_LD, Sync) -> GT
| (DMB_LD, LwSync) -> GT
| (DMB_LD, Eieio) -> GT
- | (DMB_LD, ISync) -> GT
+ | (DMB_LD, Isync) -> GT
| (DMB_LD, DMB) -> GT
| (DMB_LD, DMB_ST) -> GT
| (DMB_LD, DMB_LD) -> EQ
@@ -643,7 +700,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 =
| (DSB, Sync) -> GT
| (DSB, LwSync) -> GT
| (DSB, Eieio) -> GT
- | (DSB, ISync) -> GT
+ | (DSB, Isync) -> GT
| (DSB, DMB) -> GT
| (DSB, DMB_ST) -> GT
| (DSB, DMB_LD) -> GT
@@ -655,7 +712,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 =
| (DSB_ST, Sync) -> GT
| (DSB_ST, LwSync) -> GT
| (DSB_ST, Eieio) -> GT
- | (DSB_ST, ISync) -> GT
+ | (DSB_ST, Isync) -> GT
| (DSB_ST, DMB) -> GT
| (DSB_ST, DMB_ST) -> GT
| (DSB_ST, DMB_LD) -> GT
@@ -667,7 +724,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 =
| (DSB_LD, Sync) -> GT
| (DSB_LD, LwSync) -> GT
| (DSB_LD, Eieio) -> GT
- | (DSB_LD, ISync) -> GT
+ | (DSB_LD, Isync) -> GT
| (DSB_LD, DMB) -> GT
| (DSB_LD, DMB_ST) -> GT
| (DSB_LD, DMB_LD) -> GT
@@ -679,7 +736,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 =
| (ISB, Sync) -> GT
| (ISB, LwSync) -> GT
| (ISB, Eieio) -> GT
- | (ISB, ISync) -> GT
+ | (ISB, Isync) -> GT
| (ISB, DMB) -> GT
| (ISB, DMB_ST) -> GT
| (ISB, DMB_LD) -> GT
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 15:23:47 +0000