diff options
| -rw-r--r-- | src/lem_interp/sail_impl_base.lem | 75 |
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 |