diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp.lem | 1 | ||||
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 61 | ||||
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 6 | ||||
| -rw-r--r-- | src/lem_interp/sail_impl_base.lem | 307 |
4 files changed, 191 insertions, 184 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index cbde6e8b..cdfde00b 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -14,6 +14,7 @@ open import Instruction_extractor type tannot = Interp_utilities.tannot + val debug_print : string -> unit declare ocaml target_rep function debug_print s = `Printf.eprintf` "%s" s diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 340904f2..dad84a5c 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -524,17 +524,17 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | Interp.V_ctor (Id_aux (Id "IK_barrier") _) _ _ (Interp.V_ctor (Id_aux (Id b) _) _ _ _) -> IK_barrier (match b with - | "Barrier_Sync" -> Sync - | "Barrier_LwSync" -> LwSync - | "Barrier_Eieio" -> Eieio - | "Barrier_Isync" -> Isync - | "Barrier_DMB" -> DMB - | "Barrier_DMB_ST" -> DMB_ST - | "Barrier_DMB_LD" -> DMB_LD - | "Barrier_DSB" -> DSB - | "Barrier_DSB_ST" -> DSB_ST - | "Barrier_DSB_LD" -> DSB_LD - | "Barrier_ISB" -> ISB + | "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 end) | Interp.V_ctor (Id_aux (Id "IK_mem_read") _) _ _ (Interp.V_ctor (Id_aux (Id r) _) _ _ _) -> @@ -620,7 +620,7 @@ let interp_value_to_instr_external top_level instr = end -let decode_to_istate top_level registers value = +let decode_to_instruction top_level registers value : instruction_or_decode_error = let mode = make_interpreter_mode true false in let (Context ((Interp.Env _ instructions _ _ _ _ _ _) as top_env) direction _ _ _ _ _ _) = top_level in let intern_val = intern_opcode direction value in @@ -637,7 +637,6 @@ let decode_to_istate top_level registers value = match (instr_decoded_error) with | Ivh_value instr -> let instr_external = interp_value_to_instr_external top_level instr in - let (arg,_) = Interp.to_exp mode Interp.eenv instr in let (instr_decoded_error,events) = interp_to_value_helper (Just value) Ivh_unsupported val_str instr_external internal_direction registers [] false @@ -648,27 +647,29 @@ let decode_to_istate top_level registers value = (Interp_ast.Unknown, Nothing)) top_env Interp.eenv (Interp.emem "decode second top level") Interp.Top) Nothing) in match (instr_decoded_error) with - | Ivh_value instr -> - (*let (arg,_) = Interp.to_exp mode Interp.eenv instr in*) - Instr instr_external - (IState (Interp.Thunk_frame - (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown,Nothing)) - top_env Interp.eenv (Interp.emem "execute") Interp.Top) - top_level) + | Ivh_value instr -> IDE_instr instr_external instr | Ivh_value_after_exn v -> Assert_extra.failwith "supported_instructions called exit, so support will be needed for that now" - | Ivh_error err -> Decode_error err + | Ivh_error err -> IDE_decode_error err end | Ivh_value_after_exn _ -> - Assert_extra.failwith ("Decode of " ^ val_str ^ " called exit.") - | Ivh_error err -> Decode_error err + Assert_extra.failwith ("Decode of " ^ val_str ^ " called exit.") + | Ivh_error err -> IDE_decode_error err end -let decode_to_instruction (top_level:context) registers (value:opcode) : instruction_or_decode_error = - match decode_to_istate top_level registers value with - | Instr inst is -> IDE_instr inst - | Decode_error de -> IDE_decode_error de +let decode_to_istate (top_level:context) registers (value:opcode) : i_state_or_error = + let (Context top_env _ _ _ _ _ _ _) = top_level in + match decode_to_instruction top_level registers value with + | IDE_instr instr instrv -> + let mode = make_interpreter_mode true false in + let (arg,_) = Interp.to_exp mode Interp.eenv instrv in + Instr instr + (IState (Interp.Thunk_frame + (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown,Nothing)) + top_env Interp.eenv (Interp.emem "execute") Interp.Top) + top_level) + | IDE_decode_error de -> Decode_error de end @@ -840,8 +841,8 @@ let interp mode (IState interp_state context) = | (o,_) -> o end -val state_to_outcome_s : forall 'v. interp_mode -> instruction_state -> Sail_impl_base.outcome_s instruction_state unit unit -val outcome_to_outcome : interp_mode -> Interp_interface.outcome -> Sail_impl_base.outcome instruction_state unit unit +val state_to_outcome_s : forall 'v. interp_mode -> instruction_state -> Sail_impl_base.outcome_s instruction_state unit +val outcome_to_outcome : interp_mode -> Interp_interface.outcome -> Sail_impl_base.outcome instruction_state unit let rec outcome_to_outcome mode = function | Interp_interface.Read_mem rk addr size _ k -> Sail_impl_base.Read_mem (rk,addr,size) (fun v -> state_to_outcome_s mode (k v)) @@ -862,7 +863,7 @@ let rec outcome_to_outcome mode = function | Interp_interface.Nondet_choice _ _ -> failwith "Nondet_choice not supported yet" | Interp_interface.Escape maybestate _ -> - Sail_impl_base.Escape (Maybe.map (state_to_outcome_s mode) maybestate) + Sail_impl_base.Escape Nothing (Maybe.map (state_to_outcome_s mode) maybestate) | Interp_interface.Fail maybestring -> Sail_impl_base.Fail maybestring | Interp_interface.Internal maybestring maybeprint state -> diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index cf8c51a2..a648b437 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -156,6 +156,10 @@ val build_context : specification -> memory_reads -> memory_writes -> memory_wri val initial_instruction_state : context -> string -> list register_value -> instruction_state (* string is a function name, list of value are the parameters to that function *) +type instruction_or_decode_error = + | IDE_instr of instruction * Interp.value + | IDE_decode_error of decode_error + (** propose to remove the following type and use the above instead *) type i_state_or_error = | Instr of instruction * instruction_state @@ -198,4 +202,4 @@ val instruction_analysis : -> maybe (list (reg_name * register_value)) -> instruction -> (list reg_name * list reg_name * list reg_name * list nia * dia * instruction_kind) -val initial_outcome_s_of_instruction : context -> interp_mode -> instruction -> Sail_impl_base.outcome_s instruction_state string unit +val initial_outcome_s_of_instruction : context -> interp_mode -> instruction -> Sail_impl_base.outcome_s instruction_state unit diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 4587004f..81d84dec 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -398,9 +398,10 @@ type write_kind = type barrier_kind = (* Power barriers *) - Sync | LwSync | Eieio | Isync + Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync (* AArch64 barriers *) - | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB + | Barrier_DMB | Barrier_DMB_ST | Barrier_DMB_LD | Barrier_DSB + | Barrier_DSB_ST | Barrier_DSB_LD | Barrier_ISB type instruction_kind = | IK_barrier of barrier_kind @@ -414,30 +415,30 @@ they just have particular nias (and will be IK_simple *) | IK_simple (* the address_lifted types should go away here and be replaced by address *) -type outcome 's 'e 'a = +type outcome 's 'a = (* Request to read memory, value is location to read, integer is size to read, followed by registers that were used in computing that size *) - | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> outcome_s 's 'e 'a) + | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> outcome_s 's 'a) (* Tell the system a write is imminent, at address lifted, of size nat *) - | Write_ea of (write_kind * address_lifted * nat) * outcome_s 's 'e 'a + | Write_ea of (write_kind * address_lifted * nat) * outcome_s 's 'a (* Request to write memory at last signalled address. Memory value should be 8 times the size given in ea signal *) - | Write_memv of memory_value * (bool -> outcome_s 's 'e 'a) + | Write_memv of memory_value * (bool -> outcome_s 's 'a) (* Request a memory barrier *) - | Barrier of barrier_kind * outcome_s 's 'e 'a + | Barrier of barrier_kind * outcome_s 's 'a (* Tell the system to dynamically recalculate dependency footprint *) - | Footprint of outcome_s 's 'e 'a + | Footprint of outcome_s 's 'a (* Request to read register, will track dependency when mode.track_values *) - | Read_reg of reg_name * (register_value -> outcome_s 's 'e 'a) + | Read_reg of reg_name * (register_value -> outcome_s 's 'a) (* Request to write register *) - | Write_reg of (reg_name * register_value) * (outcome_s 's 'e 'a) - | Escape of maybe (outcome_s 's 'e 'e) + | Write_reg of (reg_name * register_value) * (outcome_s 's 'a) + | Escape of maybe string * maybe (outcome_s 's unit) (*Result of a failed assert with possible error message to report*) | Fail of maybe string - | Internal of (maybe string * maybe (unit -> string)) * outcome_s 's 'e 'a + | Internal of (maybe string * maybe (unit -> string)) * outcome_s 's 'a | Done of 'a | Error of string - and outcome_s 's 'e 'a = outcome 's 'e 'a * maybe 's + and outcome_s 's 'a = outcome 's 'a * maybe 's let ~{ocaml} read_kindCompare rk1 rk2 = match (rk1, rk2) with @@ -613,137 +614,137 @@ end let ~{ocaml} barrier_kindCompare bk1 bk2 = match (bk1, bk2) with - | (Sync, Sync) -> EQ - | (Sync, LwSync) -> LT - | (Sync, Eieio) -> LT - | (Sync, Isync) -> LT - | (Sync, DMB) -> LT - | (Sync, DMB_ST) -> LT - | (Sync, DMB_LD) -> LT - | (Sync, DSB) -> LT - | (Sync, DSB_ST) -> LT - | (Sync, DSB_LD) -> LT - | (Sync, ISB) -> LT - - | (LwSync, Sync) -> GT - | (LwSync, LwSync) -> EQ - | (LwSync, Eieio) -> LT - | (LwSync, Isync) -> LT - | (LwSync, DMB) -> LT - | (LwSync, DMB_ST) -> LT - | (LwSync, DMB_LD) -> LT - | (LwSync, DSB) -> LT - | (LwSync, DSB_ST) -> LT - | (LwSync, DSB_LD) -> LT - | (LwSync, ISB) -> LT - - | (Eieio, Sync) -> GT - | (Eieio, LwSync) -> GT - | (Eieio, Eieio) -> EQ - | (Eieio, Isync) -> LT - | (Eieio, DMB) -> LT - | (Eieio, DMB_ST) -> LT - | (Eieio, DMB_LD) -> LT - | (Eieio, DSB) -> LT - | (Eieio, DSB_ST) -> LT - | (Eieio, DSB_LD) -> LT - | (Eieio, ISB) -> LT - - | (Isync, Sync) -> GT - | (Isync, LwSync) -> GT - | (Isync, Eieio) -> GT - | (Isync, Isync) -> EQ - | (Isync, DMB) -> LT - | (Isync, DMB_ST) -> LT - | (Isync, DMB_LD) -> LT - | (Isync, DSB) -> LT - | (Isync, DSB_ST) -> LT - | (Isync, DSB_LD) -> LT - | (Isync, ISB) -> LT - - | (DMB, Sync) -> GT - | (DMB, LwSync) -> GT - | (DMB, Eieio) -> GT - | (DMB, Isync) -> GT - | (DMB, DMB) -> EQ - | (DMB, DMB_ST) -> LT - | (DMB, DMB_LD) -> LT - | (DMB, DSB) -> LT - | (DMB, DSB_ST) -> LT - | (DMB, DSB_LD) -> LT - | (DMB, ISB) -> LT - - | (DMB_ST, Sync) -> GT - | (DMB_ST, LwSync) -> GT - | (DMB_ST, Eieio) -> GT - | (DMB_ST, Isync) -> GT - | (DMB_ST, DMB) -> GT - | (DMB_ST, DMB_ST) -> EQ - | (DMB_ST, DMB_LD) -> LT - | (DMB_ST, DSB) -> LT - | (DMB_ST, DSB_ST) -> LT - | (DMB_ST, DSB_LD) -> LT - | (DMB_ST, ISB) -> LT - - | (DMB_LD, Sync) -> GT - | (DMB_LD, LwSync) -> GT - | (DMB_LD, Eieio) -> GT - | (DMB_LD, Isync) -> GT - | (DMB_LD, DMB) -> GT - | (DMB_LD, DMB_ST) -> GT - | (DMB_LD, DMB_LD) -> EQ - | (DMB_LD, DSB) -> LT - | (DMB_LD, DSB_ST) -> LT - | (DMB_LD, DSB_LD) -> LT - | (DMB_LD, ISB) -> LT - - | (DSB, Sync) -> GT - | (DSB, LwSync) -> GT - | (DSB, Eieio) -> GT - | (DSB, Isync) -> GT - | (DSB, DMB) -> GT - | (DSB, DMB_ST) -> GT - | (DSB, DMB_LD) -> GT - | (DSB, DSB) -> EQ - | (DSB, DSB_ST) -> LT - | (DSB, DSB_LD) -> LT - | (DSB, ISB) -> LT - - | (DSB_ST, Sync) -> GT - | (DSB_ST, LwSync) -> GT - | (DSB_ST, Eieio) -> GT - | (DSB_ST, Isync) -> GT - | (DSB_ST, DMB) -> GT - | (DSB_ST, DMB_ST) -> GT - | (DSB_ST, DMB_LD) -> GT - | (DSB_ST, DSB) -> GT - | (DSB_ST, DSB_ST) -> EQ - | (DSB_ST, DSB_LD) -> LT - | (DSB_ST, ISB) -> LT - - | (DSB_LD, Sync) -> GT - | (DSB_LD, LwSync) -> GT - | (DSB_LD, Eieio) -> GT - | (DSB_LD, Isync) -> GT - | (DSB_LD, DMB) -> GT - | (DSB_LD, DMB_ST) -> GT - | (DSB_LD, DMB_LD) -> GT - | (DSB_LD, DSB) -> GT - | (DSB_LD, DSB_ST) -> GT - | (DSB_LD, DSB_LD) -> EQ - | (DSB_LD, ISB) -> LT + | (Barrier_Sync, Barrier_Sync) -> EQ + | (Barrier_Sync, Barrier_LwSync) -> LT + | (Barrier_Sync, Barrier_Eieio) -> LT + | (Barrier_Sync, Barrier_Isync) -> LT + | (Barrier_Sync, Barrier_DMB) -> LT + | (Barrier_Sync, Barrier_DMB_ST) -> LT + | (Barrier_Sync, Barrier_DMB_LD) -> LT + | (Barrier_Sync, Barrier_DSB) -> LT + | (Barrier_Sync, Barrier_DSB_ST) -> LT + | (Barrier_Sync, Barrier_DSB_LD) -> LT + | (Barrier_Sync, Barrier_ISB) -> LT + + | (Barrier_LwSync, Barrier_Sync) -> GT + | (Barrier_LwSync, Barrier_LwSync) -> EQ + | (Barrier_LwSync, Barrier_Eieio) -> LT + | (Barrier_LwSync, Barrier_Isync) -> LT + | (Barrier_LwSync, Barrier_DMB) -> LT + | (Barrier_LwSync, Barrier_DMB_ST) -> LT + | (Barrier_LwSync, Barrier_DMB_LD) -> LT + | (Barrier_LwSync, Barrier_DSB) -> LT + | (Barrier_LwSync, Barrier_DSB_ST) -> LT + | (Barrier_LwSync, Barrier_DSB_LD) -> LT + | (Barrier_LwSync, Barrier_ISB) -> LT + + | (Barrier_Eieio, Barrier_Sync) -> GT + | (Barrier_Eieio, Barrier_LwSync) -> GT + | (Barrier_Eieio, Barrier_Eieio) -> EQ + | (Barrier_Eieio, Barrier_Isync) -> LT + | (Barrier_Eieio, Barrier_DMB) -> LT + | (Barrier_Eieio, Barrier_DMB_ST) -> LT + | (Barrier_Eieio, Barrier_DMB_LD) -> LT + | (Barrier_Eieio, Barrier_DSB) -> LT + | (Barrier_Eieio, Barrier_DSB_ST) -> LT + | (Barrier_Eieio, Barrier_DSB_LD) -> LT + | (Barrier_Eieio, Barrier_ISB) -> LT + + | (Barrier_Isync, Barrier_Sync) -> GT + | (Barrier_Isync, Barrier_LwSync) -> GT + | (Barrier_Isync, Barrier_Eieio) -> GT + | (Barrier_Isync, Barrier_Isync) -> EQ + | (Barrier_Isync, Barrier_DMB) -> LT + | (Barrier_Isync, Barrier_DMB_ST) -> LT + | (Barrier_Isync, Barrier_DMB_LD) -> LT + | (Barrier_Isync, Barrier_DSB) -> LT + | (Barrier_Isync, Barrier_DSB_ST) -> LT + | (Barrier_Isync, Barrier_DSB_LD) -> LT + | (Barrier_Isync, Barrier_ISB) -> LT + + | (Barrier_DMB, Barrier_Sync) -> GT + | (Barrier_DMB, Barrier_LwSync) -> GT + | (Barrier_DMB, Barrier_Eieio) -> GT + | (Barrier_DMB, Barrier_Isync) -> GT + | (Barrier_DMB, Barrier_DMB) -> EQ + | (Barrier_DMB, Barrier_DMB_ST) -> LT + | (Barrier_DMB, Barrier_DMB_LD) -> LT + | (Barrier_DMB, Barrier_DSB) -> LT + | (Barrier_DMB, Barrier_DSB_ST) -> LT + | (Barrier_DMB, Barrier_DSB_LD) -> LT + | (Barrier_DMB, Barrier_ISB) -> LT + + | (Barrier_DMB_ST, Barrier_Sync) -> GT + | (Barrier_DMB_ST, Barrier_LwSync) -> GT + | (Barrier_DMB_ST, Barrier_Eieio) -> GT + | (Barrier_DMB_ST, Barrier_Isync) -> GT + | (Barrier_DMB_ST, Barrier_DMB) -> GT + | (Barrier_DMB_ST, Barrier_DMB_ST) -> EQ + | (Barrier_DMB_ST, Barrier_DMB_LD) -> LT + | (Barrier_DMB_ST, Barrier_DSB) -> LT + | (Barrier_DMB_ST, Barrier_DSB_ST) -> LT + | (Barrier_DMB_ST, Barrier_DSB_LD) -> LT + | (Barrier_DMB_ST, Barrier_ISB) -> LT + + | (Barrier_DMB_LD, Barrier_Sync) -> GT + | (Barrier_DMB_LD, Barrier_LwSync) -> GT + | (Barrier_DMB_LD, Barrier_Eieio) -> GT + | (Barrier_DMB_LD, Barrier_Isync) -> GT + | (Barrier_DMB_LD, Barrier_DMB) -> GT + | (Barrier_DMB_LD, Barrier_DMB_ST) -> GT + | (Barrier_DMB_LD, Barrier_DMB_LD) -> EQ + | (Barrier_DMB_LD, Barrier_DSB) -> LT + | (Barrier_DMB_LD, Barrier_DSB_ST) -> LT + | (Barrier_DMB_LD, Barrier_DSB_LD) -> LT + | (Barrier_DMB_LD, Barrier_ISB) -> LT + + | (Barrier_DSB, Barrier_Sync) -> GT + | (Barrier_DSB, Barrier_LwSync) -> GT + | (Barrier_DSB, Barrier_Eieio) -> GT + | (Barrier_DSB, Barrier_Isync) -> GT + | (Barrier_DSB, Barrier_DMB) -> GT + | (Barrier_DSB, Barrier_DMB_ST) -> GT + | (Barrier_DSB, Barrier_DMB_LD) -> GT + | (Barrier_DSB, Barrier_DSB) -> EQ + | (Barrier_DSB, Barrier_DSB_ST) -> LT + | (Barrier_DSB, Barrier_DSB_LD) -> LT + | (Barrier_DSB, Barrier_ISB) -> LT + + | (Barrier_DSB_ST, Barrier_Sync) -> GT + | (Barrier_DSB_ST, Barrier_LwSync) -> GT + | (Barrier_DSB_ST, Barrier_Eieio) -> GT + | (Barrier_DSB_ST, Barrier_Isync) -> GT + | (Barrier_DSB_ST, Barrier_DMB) -> GT + | (Barrier_DSB_ST, Barrier_DMB_ST) -> GT + | (Barrier_DSB_ST, Barrier_DMB_LD) -> GT + | (Barrier_DSB_ST, Barrier_DSB) -> GT + | (Barrier_DSB_ST, Barrier_DSB_ST) -> EQ + | (Barrier_DSB_ST, Barrier_DSB_LD) -> LT + | (Barrier_DSB_ST, Barrier_ISB) -> LT + + | (Barrier_DSB_LD, Barrier_Sync) -> GT + | (Barrier_DSB_LD, Barrier_LwSync) -> GT + | (Barrier_DSB_LD, Barrier_Eieio) -> GT + | (Barrier_DSB_LD, Barrier_Isync) -> GT + | (Barrier_DSB_LD, Barrier_DMB) -> GT + | (Barrier_DSB_LD, Barrier_DMB_ST) -> GT + | (Barrier_DSB_LD, Barrier_DMB_LD) -> GT + | (Barrier_DSB_LD, Barrier_DSB) -> GT + | (Barrier_DSB_LD, Barrier_DSB_ST) -> GT + | (Barrier_DSB_LD, Barrier_DSB_LD) -> EQ + | (Barrier_DSB_LD, Barrier_ISB) -> LT - | (ISB, Sync) -> GT - | (ISB, LwSync) -> GT - | (ISB, Eieio) -> GT - | (ISB, Isync) -> GT - | (ISB, DMB) -> GT - | (ISB, DMB_ST) -> GT - | (ISB, DMB_LD) -> GT - | (ISB, DSB) -> GT - | (ISB, DSB_ST) -> GT - | (ISB, DSB_LD) -> GT - | (ISB, ISB) -> EQ + | (Barrier_ISB, Barrier_Sync) -> GT + | (Barrier_ISB, Barrier_LwSync) -> GT + | (Barrier_ISB, Barrier_Eieio) -> GT + | (Barrier_ISB, Barrier_Isync) -> GT + | (Barrier_ISB, Barrier_DMB) -> GT + | (Barrier_ISB, Barrier_DMB_ST) -> GT + | (Barrier_ISB, Barrier_DMB_LD) -> GT + | (Barrier_ISB, Barrier_DSB) -> GT + | (Barrier_ISB, Barrier_DSB_ST) -> GT + | (Barrier_ISB, Barrier_DSB_LD) -> GT + | (Barrier_ISB, Barrier_ISB) -> EQ end let inline {ocaml} barrier_kindCompare = defaultCompare @@ -820,16 +821,6 @@ let inline ~{coq} instructionEqual = unsafe_structural_equality let {coq} instructionInequal i1 i2 = not (instructionEqual i1 i2) let inline ~{coq} instructionInequal = unsafe_structural_inequality -type decode_error = - | Unsupported_instruction_error of instruction - | Not_an_instruction_error of opcode - | Internal_error of string - -type instruction_or_decode_error = - | IDE_instr of instruction - | IDE_decode_error of decode_error - - (** operations and coercions on basic values *) val word8_to_bitls : word8 -> list bit_lifted @@ -1364,3 +1355,13 @@ end type v_kind = Bitv | Bytev + + +type decode_error = + | Unsupported_instruction_error of instruction + | Not_an_instruction_error of opcode + | Internal_error of string + + + + |