summaryrefslogtreecommitdiff
path: root/src/lem_interp
diff options
context:
space:
mode:
Diffstat (limited to 'src/lem_interp')
-rw-r--r--src/lem_interp/interp_inter_imp.lem48
-rw-r--r--src/lem_interp/run_with_elf.ml10
-rw-r--r--src/lem_interp/run_with_elf_cheri.ml14
-rw-r--r--src/lem_interp/run_with_elf_cheri128.ml14
-rw-r--r--src/lem_interp/sail_impl_base.lem101
-rw-r--r--src/lem_interp/sail_instr_kinds.lem266
6 files changed, 120 insertions, 333 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 563da2e5..74e43a8f 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -573,13 +573,11 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
| Interp_ast.V_ctor (Id_aux (Id "DIAFP_reg") _) _ _ reg -> DIA_register (reg_to_reg_name reg)
| _ -> failwith "Register footprint analysis did not return dia of expected type" end in
let nia_to_nia = function
- | Interp_ast.V_ctor (Id_aux (Id "NIAFP_successor") _) _ _ _-> NIA_successor
+ | Interp_ast.V_ctor (Id_aux (Id "NIAFP_successor") _) _ _ _ -> NIA_successor
| Interp_ast.V_ctor (Id_aux (Id "NIAFP_concrete_address") _) _ _ address ->
NIA_concrete_address (get_addr address)
- | Interp_ast.V_ctor (Id_aux (Id "NIAFP_LR") _) _ _ _ -> NIA_LR
- | Interp_ast.V_ctor (Id_aux (Id "NIAFP_CTR") _) _ _ _ -> NIA_CTR
- | Interp_ast.V_ctor (Id_aux (Id "NIAFP_register") _) _ _ reg ->
- NIA_register (reg_to_reg_name reg)
+ | Interp_ast.V_ctor (Id_aux (Id "NIAFP_indirect_address") _) _ _ _ ->
+ NIA_indirect_address
| _ -> failwith "Register footprint analysis did not return nia of expected type" end in
let readk_to_readk = function
| "Read_plain" -> Read_plain
@@ -636,8 +634,8 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
(Interp_ast.V_tuple [(Interp_ast.V_ctor (Id_aux (Id readk) _) _ _ _) ;
(Interp_ast.V_ctor (Id_aux (Id writek) _) _ _ _)]) ->
IK_mem_rmw(readk_to_readk readk, writek_to_writek writek)
- | Interp_ast.V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ _ ->
- IK_cond_branch
+ | Interp_ast.V_ctor (Id_aux (Id "IK_branch") _) _ _ _ ->
+ IK_branch
| Interp_ast.V_ctor (Id_aux (Id "IK_simple") _) _ _ _ ->
IK_simple
| _ -> failwith "Analysis returned unexpected instruction kind"
@@ -1159,7 +1157,7 @@ let rr_interp_exhaustive mode i_state events =
*)
-let instruction_kind_of_event : event -> maybe instruction_kind = function
+let instruction_kind_of_event nia_reg : event -> maybe instruction_kind = function
(* this is a hack to avoid adding special events for AArch64 transactional-memory *)
| E_read_reg (Reg "TMStartEffect" 63 64 D_decreasing) -> Just (IK_trans Transaction_start)
| E_write_reg (Reg "TMAbortEffect" 63 64 D_decreasing) _ -> Just (IK_trans Transaction_abort)
@@ -1175,7 +1173,9 @@ let instruction_kind_of_event : event -> maybe instruction_kind = function
| E_barrier bk -> Just (IK_barrier bk)
| E_footprint -> Nothing
| E_read_reg _ -> Nothing
- | E_write_reg _ _ -> Nothing
+ | E_write_reg reg _ ->
+ if register_base_name reg = register_base_name nia_reg then Just IK_branch
+ else Nothing
| E_error s -> failwith ("instruction_kind_of_event error: "^s)
| E_escape -> Nothing (*failwith ("instruction_kind_of_event escape")*)
end
@@ -1254,8 +1254,8 @@ let interp_instruction_analysis
(interp_exhaustive : ((list (reg_name * register_value)) -> list event))
instruction
nia_reg
- (nias_function : (list (maybe address) -> list reg_name -> list nia))
- ism environment =
+ (nias_function : (list (maybe address) -> list nia))
+ ism environment =
let es = interp_exhaustive environment in
@@ -1265,19 +1265,15 @@ let interp_instruction_analysis
let regs_feeding_address = List.concatMap regs_feeding_memory_access_address_of_event es in
let nia_address = List.mapMaybe (nia_address_of_event nia_reg) es in
-
- let nias = nias_function nia_address regs_in in
+ let nias = nias_function nia_address in
let dia = DIA_none in (* FIX THIS! *)
-
let inst_kind =
- match List.mapMaybe instruction_kind_of_event es with
- | [] -> if List.length nias > 1 then IK_cond_branch else IK_simple
+ match List.mapMaybe (instruction_kind_of_event nia_reg) es with
+ | [] -> IK_simple
+ | inst_kind :: [] -> inst_kind
| inst_kind :: inst_kinds ->
- let () = ensure (List.length nias > 1 --> inst_kind = IK_cond_branch)
- "multiple NIAs must be IK_cond_branch" in
-
if forall (inst_kind' MEM inst_kinds). inst_kind' = inst_kind then
inst_kind
@@ -1288,19 +1284,9 @@ let interp_instruction_analysis
| IK_mem_write _ -> true
| IK_mem_rmw _ -> false
| IK_barrier _ -> false
- | IK_cond_branch -> false
+ | IK_branch -> false
| IK_trans _ -> false
| IK_simple -> false
- end) &&
- (exists (inst_kind' MEM (inst_kind :: inst_kinds)).
- match inst_kind' with
- | IK_mem_read _ -> true
- | _ -> false
- end) &&
- (exists (inst_kind' MEM (inst_kind :: inst_kinds)).
- match inst_kind' with
- | IK_mem_write _ -> true
- | _ -> false
end)
then
match
@@ -1357,7 +1343,7 @@ let interp_compare_analyses
interp_exhaustive
(instruction : Interp_ast.value)
nia_reg
- (nias_function : (list (maybe address) -> list reg_name -> list nia))
+ (nias_function : (list (maybe address) -> list nia))
ism
environment
analysis_function
diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml
index bb56c8a9..0dadc007 100644
--- a/src/lem_interp/run_with_elf.ml
+++ b/src/lem_interp/run_with_elf.ml
@@ -736,11 +736,11 @@ let initial_system_state_of_elf_file name =
initial_stack_and_reg_data_of_MIPS_elf_file e_entry !data_mem in
(Mips.defs,
- (Mips_extras.read_memory_functions,
- Mips_extras.memory_writes,
- Mips_extras.memory_eas,
- Mips_extras.memory_vals,
- Mips_extras.barrier_functions),
+ (Mips_extras.mips_read_memory_functions,
+ Mips_extras.mips_memory_writes,
+ Mips_extras.mips_memory_eas,
+ Mips_extras.mips_memory_vals,
+ Mips_extras.mips_barrier_functions),
[],
MIPS,
D_decreasing,
diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml
index 3d187aa9..2bf84e2d 100644
--- a/src/lem_interp/run_with_elf_cheri.ml
+++ b/src/lem_interp/run_with_elf_cheri.ml
@@ -405,13 +405,13 @@ let initial_system_state_of_elf_file name =
initial_stack_and_reg_data_of_MIPS_elf_file e_entry !data_mem in
(Cheri.defs,
- (Mips_extras.read_memory_functions,
- Mips_extras.read_memory_tagged_functions,
- Mips_extras.memory_writes,
- Mips_extras.memory_eas,
- Mips_extras.memory_vals,
- Mips_extras.memory_vals_tagged,
- Mips_extras.barrier_functions),
+ (Mips_extras.mips_read_memory_functions,
+ Mips_extras.mips_read_memory_tagged_functions,
+ Mips_extras.mips_memory_writes,
+ Mips_extras.mips_memory_eas,
+ Mips_extras.mips_memory_vals,
+ Mips_extras.mips_memory_vals_tagged,
+ Mips_extras.mips_barrier_functions),
[],
MIPS,
D_decreasing,
diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml
index 6b12ebbb..e4d91c41 100644
--- a/src/lem_interp/run_with_elf_cheri128.ml
+++ b/src/lem_interp/run_with_elf_cheri128.ml
@@ -405,13 +405,13 @@ let initial_system_state_of_elf_file name =
initial_stack_and_reg_data_of_MIPS_elf_file e_entry !data_mem in
(Cheri128.defs,
- (Mips_extras.read_memory_functions,
- Mips_extras.read_memory_tagged_functions,
- Mips_extras.memory_writes,
- Mips_extras.memory_eas,
- Mips_extras.memory_vals,
- Mips_extras.memory_vals_tagged,
- Mips_extras.barrier_functions),
+ (Mips_extras.mips_read_memory_functions,
+ Mips_extras.mips_read_memory_tagged_functions,
+ Mips_extras.mips_memory_writes,
+ Mips_extras.mips_memory_eas,
+ Mips_extras.mips_memory_vals,
+ Mips_extras.mips_memory_vals_tagged,
+ Mips_extras.mips_barrier_functions),
[],
MIPS,
D_decreasing,
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index f029b952..39ba0b5c 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -148,65 +148,20 @@ type opcode = Opcode of list byte (* of length 4 *)
(** typeclass instantiations *)
-let ~{ocaml} bitCompare (b1:bit) (b2:bit) =
- match (b1,b2) with
- | (Bitc_zero, Bitc_zero) -> EQ
- | (Bitc_one, Bitc_one) -> EQ
- | (Bitc_zero, _) -> LT
- | (_,_) -> GT
+instance (EnumerationType bit)
+ let toNat = function
+ | Bitc_zero -> 0
+ | Bitc_one -> 1
end
-let inline {ocaml} bitCompare = defaultCompare
-
-let ~{ocaml} bitLess b1 b2 = bitCompare b1 b2 = LT
-let ~{ocaml} bitLessEq b1 b2 = bitCompare b1 b2 <> GT
-let ~{ocaml} bitGreater b1 b2 = bitCompare b1 b2 = GT
-let ~{ocaml} bitGreaterEq b1 b2 = bitCompare b1 b2 <> LT
-
-let inline {ocaml} bitLess = defaultLess
-let inline {ocaml} bitLessEq = defaultLessEq
-let inline {ocaml} bitGreater = defaultGreater
-let inline {ocaml} bitGreaterEq = defaultGreaterEq
-
-instance (Ord bit)
- let compare = bitCompare
- let (<) = bitLess
- let (<=) = bitLessEq
- let (>) = bitGreater
- let (>=) = bitGreaterEq
end
-let ~{ocaml} bit_liftedCompare (bl1:bit_lifted) (bl2:bit_lifted) =
- match (bl1,bl2) with
- | (Bitl_zero, Bitl_zero) -> EQ
- | (Bitl_zero,_) -> LT
- | (Bitl_one, Bitl_zero) -> GT
- | (Bitl_one, Bitl_one) -> EQ
- | (Bitl_one, _) -> LT
- | (Bitl_undef,Bitl_zero) -> GT
- | (Bitl_undef,Bitl_one) -> GT
- | (Bitl_undef,Bitl_undef) -> EQ
- | (Bitl_undef,_) -> LT
- | (Bitl_unknown,Bitl_unknown) -> EQ
- | (Bitl_unknown,_) -> GT
+instance (EnumerationType bit_lifted)
+ let toNat = function
+ | Bitl_zero -> 0
+ | Bitl_one -> 1
+ | Bitl_undef -> 2
+ | Bitl_unknown -> 3
end
-let inline {ocaml} bit_liftedCompare = defaultCompare
-
-let ~{ocaml} bit_liftedLess b1 b2 = bit_liftedCompare b1 b2 = LT
-let ~{ocaml} bit_liftedLessEq b1 b2 = bit_liftedCompare b1 b2 <> GT
-let ~{ocaml} bit_liftedGreater b1 b2 = bit_liftedCompare b1 b2 = GT
-let ~{ocaml} bit_liftedGreaterEq b1 b2 = bit_liftedCompare b1 b2 <> LT
-
-let inline {ocaml} bit_liftedLess = defaultLess
-let inline {ocaml} bit_liftedLessEq = defaultLessEq
-let inline {ocaml} bit_liftedGreater = defaultGreater
-let inline {ocaml} bit_liftedGreaterEq = defaultGreaterEq
-
-instance (Ord bit_lifted)
- let compare = bit_liftedCompare
- let (<) = bit_liftedLess
- let (<=) = bit_liftedLessEq
- let (>) = bit_liftedGreater
- let (>=) = bit_liftedGreaterEq
end
let ~{ocaml} byte_liftedCompare (Byte_lifted b1) (Byte_lifted b2) = compare b1 b2
@@ -251,6 +206,10 @@ instance (Ord byte)
let (>=) = byteGreaterEq
end
+
+
+
+
let ~{ocaml} opcodeCompare (Opcode o1) (Opcode o2) =
compare o1 o2
let {ocaml} opcodeCompare = defaultCompare
@@ -1078,32 +1037,18 @@ end
type nia =
| NIA_successor
| NIA_concrete_address of address
- | NIA_LR (* "LR0:61 || 0b00" in Power pseudocode *)
- | NIA_CTR (* "CTR0:61 || 0b00" in Power pseudocode *)
- | NIA_register of reg_name (* the address will be in a register,
- corresponds to AArch64 BLR, BR, RET
- instructions *)
+ | NIA_indirect_address
let niaCompare n1 n2 = match (n1,n2) with
| (NIA_successor, NIA_successor) -> EQ
| (NIA_successor, _) -> LT
- | (NIA_concrete_address _, NIA_successor) -> GT
+ | (_, NIA_successor) -> GT
| (NIA_concrete_address a1, NIA_concrete_address a2) -> compare a1 a2
| (NIA_concrete_address _, _) -> LT
- | (NIA_LR, NIA_successor) -> GT
- | (NIA_LR, NIA_concrete_address _) -> GT
- | (NIA_LR, NIA_LR) -> EQ
- | (NIA_LR, _) -> LT
- | (NIA_CTR, NIA_successor) -> GT
- | (NIA_CTR, NIA_concrete_address _) -> GT
- | (NIA_CTR, NIA_LR) -> GT
- | (NIA_CTR, NIA_CTR) -> EQ
- | (NIA_CTR, NIA_register _) -> LT
- | (NIA_register _, NIA_successor) -> GT
- | (NIA_register _, NIA_concrete_address _) -> GT
- | (NIA_register _, NIA_LR) -> GT
- | (NIA_register _, NIA_CTR) -> GT
- | (NIA_register r1, NIA_register r2) -> compare r1 r2
+ | (_, NIA_concrete_address _) -> GT
+ | (NIA_indirect_address, NIA_indirect_address) -> EQ
+ (* | (NIA_indirect_address, _) -> LT
+ | (_, NIA_indirect_address) -> GT *)
end
instance (Ord nia)
@@ -1115,11 +1060,9 @@ instance (Ord nia)
end
let stringFromNia = function
- | NIA_successor -> "NIA_successor"
+ | NIA_successor -> "NIA_successor"
| NIA_concrete_address a -> "NIA_concrete_address " ^ show a
- | NIA_LR -> "NIA_LR"
- | NIA_CTR -> "NIA_CTR"
- | NIA_register r -> "NIA_register " ^ show r
+ | NIA_indirect_address -> "NIA_indirect_address"
end
instance (Show nia)
diff --git a/src/lem_interp/sail_instr_kinds.lem b/src/lem_interp/sail_instr_kinds.lem
index 89ff67b2..d8a2c0c0 100644
--- a/src/lem_interp/sail_instr_kinds.lem
+++ b/src/lem_interp/sail_instr_kinds.lem
@@ -50,6 +50,27 @@
open import Pervasives_extra
+
+class ( EnumerationType 'a )
+ val toNat : 'a -> nat
+end
+
+
+val enumeration_typeCompare : forall 'a. EnumerationType 'a => 'a -> 'a -> ordering
+let ~{ocaml} enumeration_typeCompare e1 e2 =
+ compare (toNat e1) (toNat e2)
+let inline {ocaml} enumeration_typeCompare = defaultCompare
+
+
+default_instance forall 'a. EnumerationType 'a => (Ord 'a)
+ let compare = enumeration_typeCompare
+ let (<) r1 r2 = (enumeration_typeCompare r1 r2) = LT
+ let (<=) r1 r2 = (enumeration_typeCompare r1 r2) <> GT
+ let (>) r1 r2 = (enumeration_typeCompare r1 r2) = GT
+ let (>=) r1 r2 = (enumeration_typeCompare r1 r2) <> LT
+end
+
+
(* Data structures for building up instructions *)
(* careful: changes in the read/write/barrier kinds have to be
@@ -177,10 +198,9 @@ type instruction_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_branch (* this includes conditional-branch (multiple nias, none of which is NIA_indirect_address),
+ indirect/computed-branch (single nia of kind NIA_indirect_address)
+ and branch/jump (single nia of kind NIA_concrete_address) *)
| IK_trans of trans_kind
| IK_simple
@@ -188,80 +208,16 @@ type instruction_kind =
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_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"
+ | IK_mem_rmw (r, w) -> "IK_mem_rmw " ^ (show r) ^ " " ^ (show w)
+ | IK_branch -> "IK_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 read_is_exclusive = function
| Read_plain -> false
| Read_reserve -> true
@@ -277,63 +233,46 @@ let read_is_exclusive = function
| Read_X86_locked -> true
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
+instance (EnumerationType read_kind)
+ let toNat = function
+ | Read_plain -> 0
+ | Read_reserve -> 1
+ | Read_acquire -> 2
+ | Read_exclusive -> 3
+ | Read_exclusive_acquire -> 4
+ | Read_stream -> 5
+ | Read_RISCV_acquire -> 6
+ | Read_RISCV_strong_acquire -> 7
+ | Read_RISCV_reserved -> 8
+ | Read_RISCV_reserved_acquire -> 9
+ | Read_RISCV_reserved_strong_acquire -> 10
+ | Read_X86_locked -> 11
+ end
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
+instance (EnumerationType write_kind)
+ let toNat = function
+ | Write_plain -> 0
+ | Write_conditional -> 1
+ | Write_release -> 2
+ | Write_exclusive -> 3
+ | Write_exclusive_release -> 4
+ | Write_RISCV_release -> 5
+ | Write_RISCV_strong_release -> 6
+ | Write_RISCV_conditional -> 7
+ | Write_RISCV_conditional_release -> 8
+ | Write_RISCV_conditional_strong_release -> 9
+ | Write_X86_locked -> 10
+ end
end
-(* Barrier comparison that uses less memory in Isabelle/HOL *)
-let ~{ocaml} barrier_number = function
- | Barrier_Sync -> (0 : natural)
+instance (EnumerationType barrier_kind)
+ let toNat = function
+ | Barrier_Sync -> 0
| Barrier_LwSync -> 1
- | Barrier_Eieio -> 2
+ | Barrier_Eieio ->2
| Barrier_Isync -> 3
| Barrier_DMB -> 4
| Barrier_DMB_ST -> 5
@@ -352,85 +291,4 @@ let ~{ocaml} barrier_number = function
| 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 19:02:11 +0000