diff options
Diffstat (limited to 'aarch64_small')
| -rw-r--r-- | aarch64_small/gen/herdtools_ast_to_shallow_ast.hgen | 12 | ||||
| -rw-r--r-- | aarch64_small/gen/herdtools_types_to_shallow_types.hgen | 142 | ||||
| -rw-r--r-- | aarch64_small/gen/shallow_ast_to_herdtools_ast.hgen | 10 | ||||
| -rw-r--r-- | aarch64_small/gen/shallow_types_to_herdtools_types.hgen | 148 |
4 files changed, 156 insertions, 156 deletions
diff --git a/aarch64_small/gen/herdtools_ast_to_shallow_ast.hgen b/aarch64_small/gen/herdtools_ast_to_shallow_ast.hgen index b8fe851c..2d0ac5e2 100644 --- a/aarch64_small/gen/herdtools_ast_to_shallow_ast.hgen +++ b/aarch64_small/gen/herdtools_ast_to_shallow_ast.hgen @@ -1,20 +1,20 @@ -| `AArch64Unallocated -> Unallocated +| `AArch64Unallocated -> Unallocated () | `AArch64TMStart t -> TMStart (translate_reg "t" t) -| `AArch64TMCommit -> TMCommit +| `AArch64TMCommit -> TMCommit () | `AArch64TMAbort (retry,reason) -> TMAbort - (translate_boolean "retry" retry, + (translate_bool "retry" retry, translate_bit5 "reason" reason) -| `AArch64TMTest -> TMTest +| `AArch64TMTest -> TMTest () | `AArch64ImplementationDefinedStopFetching -> - ImplementationDefinedStopFetching + ImplementationDefinedStopFetching () | `AArch64ImplementationDefinedThreadStart -> - ImplementationDefinedThreadStart + ImplementationDefinedThreadStart () | `AArch64ImplementationDefinedTestBeginEnd(isEnd) -> ImplementationDefinedTestBeginEnd diff --git a/aarch64_small/gen/herdtools_types_to_shallow_types.hgen b/aarch64_small/gen/herdtools_types_to_shallow_types.hgen index e14a37e3..6ca50f83 100644 --- a/aarch64_small/gen/herdtools_types_to_shallow_types.hgen +++ b/aarch64_small/gen/herdtools_types_to_shallow_types.hgen @@ -1,4 +1,4 @@ -open Sail_values +open Sail2_values let is_inc = false @@ -6,16 +6,16 @@ let translate_big_int bits (name : string) value = (name, Range0 (Some bits), IInt.bit_list_of_integer bits value) let translate_big_bit bits (name:string) value = - Sail_values.to_vec0 is_inc (Nat_big_num.of_int bits,value) + Sail2_values.bits_of_int (Nat_big_num.of_int bits) value let translate_int (size : int) (name:string) value = (Nat_big_num.of_int value) let translate_bits bits (name:string) value = - Sail_values.to_vec0 is_inc (Nat_big_num.of_int bits,Nat_big_num.of_int value) + Sail2_values.bits_of_int (Nat_big_num.of_int bits) (Nat_big_num.of_int value) let translate_bool _ = function - | true -> B1 - | false -> B0 + | true -> B10 + | false -> B00 let translate_reg_size name value = match value with @@ -59,95 +59,95 @@ let translate_range8_64 = translate_int 7 let translate_uinteger = translate_int 63 let translate_extendType _ = function - | ExtendType_UXTB -> ArmV8_embed_types.ExtendType_UXTB - | ExtendType_UXTH -> ArmV8_embed_types.ExtendType_UXTH - | ExtendType_UXTW -> ArmV8_embed_types.ExtendType_UXTW - | ExtendType_UXTX -> ArmV8_embed_types.ExtendType_UXTX - | ExtendType_SXTB -> ArmV8_embed_types.ExtendType_SXTB - | ExtendType_SXTH -> ArmV8_embed_types.ExtendType_SXTH - | ExtendType_SXTW -> ArmV8_embed_types.ExtendType_SXTW - | ExtendType_SXTX -> ArmV8_embed_types.ExtendType_SXTX + | ExtendType_UXTB -> ArmV8_types.ExtendType_UXTB + | ExtendType_UXTH -> ArmV8_types.ExtendType_UXTH + | ExtendType_UXTW -> ArmV8_types.ExtendType_UXTW + | ExtendType_UXTX -> ArmV8_types.ExtendType_UXTX + | ExtendType_SXTB -> ArmV8_types.ExtendType_SXTB + | ExtendType_SXTH -> ArmV8_types.ExtendType_SXTH + | ExtendType_SXTW -> ArmV8_types.ExtendType_SXTW + | ExtendType_SXTX -> ArmV8_types.ExtendType_SXTX let translate_shiftType _ = function - | ShiftType_LSL -> ArmV8_embed_types.ShiftType_LSL - | ShiftType_LSR -> ArmV8_embed_types.ShiftType_LSR - | ShiftType_ASR -> ArmV8_embed_types.ShiftType_ASR - | ShiftType_ROR -> ArmV8_embed_types.ShiftType_ROR + | ShiftType_LSL -> ArmV8_types.ShiftType_LSL + | ShiftType_LSR -> ArmV8_types.ShiftType_LSR + | ShiftType_ASR -> ArmV8_types.ShiftType_ASR + | ShiftType_ROR -> ArmV8_types.ShiftType_ROR let translate_logicalOp _ = function - | LogicalOp_AND -> ArmV8_embed_types.LogicalOp_AND - | LogicalOp_EOR -> ArmV8_embed_types.LogicalOp_EOR - | LogicalOp_ORR -> ArmV8_embed_types.LogicalOp_ORR + | LogicalOp_AND -> ArmV8_types.LogicalOp_AND + | LogicalOp_EOR -> ArmV8_types.LogicalOp_EOR + | LogicalOp_ORR -> ArmV8_types.LogicalOp_ORR let translate_branchType _ = function - | BranchType_CALL -> ArmV8_embed_types.BranchType_CALL - | BranchType_ERET -> ArmV8_embed_types.BranchType_ERET - | BranchType_DBGEXIT -> ArmV8_embed_types.BranchType_DBGEXIT - | BranchType_RET -> ArmV8_embed_types.BranchType_RET - | BranchType_JMP -> ArmV8_embed_types.BranchType_JMP - | BranchType_EXCEPTION -> ArmV8_embed_types.BranchType_EXCEPTION - | BranchType_UNKNOWN -> ArmV8_embed_types.BranchType_UNKNOWN + | BranchType_CALL -> ArmV8_types.BranchType_CALL + | BranchType_ERET -> ArmV8_types.BranchType_ERET + | BranchType_DBGEXIT -> ArmV8_types.BranchType_DBGEXIT + | BranchType_RET -> ArmV8_types.BranchType_RET + | BranchType_JMP -> ArmV8_types.BranchType_JMP + | BranchType_EXCEPTION -> ArmV8_types.BranchType_EXCEPTION + | BranchType_UNKNOWN -> ArmV8_types.BranchType_UNKNOWN let translate_countOp _ = function - | CountOp_CLZ -> ArmV8_embed_types.CountOp_CLZ - | CountOp_CLS -> ArmV8_embed_types.CountOp_CLS - | CountOp_CNT -> ArmV8_embed_types.CountOp_CNT + | CountOp_CLZ -> ArmV8_types.CountOp_CLZ + | CountOp_CLS -> ArmV8_types.CountOp_CLS + | CountOp_CNT -> ArmV8_types.CountOp_CNT let translate_memBarrierOp _ = function - | MemBarrierOp_DSB -> ArmV8_embed_types.MemBarrierOp_DSB - | MemBarrierOp_DMB -> ArmV8_embed_types.MemBarrierOp_DMB - | MemBarrierOp_ISB -> ArmV8_embed_types.MemBarrierOp_ISB + | MemBarrierOp_DSB -> ArmV8_types.MemBarrierOp_DSB + | MemBarrierOp_DMB -> ArmV8_types.MemBarrierOp_DMB + | MemBarrierOp_ISB -> ArmV8_types.MemBarrierOp_ISB let translate_mBReqDomain _ = function - | MBReqDomain_Nonshareable -> ArmV8_embed_types.MBReqDomain_Nonshareable - | MBReqDomain_InnerShareable -> ArmV8_embed_types.MBReqDomain_InnerShareable - | MBReqDomain_OuterShareable -> ArmV8_embed_types.MBReqDomain_OuterShareable - | MBReqDomain_FullSystem -> ArmV8_embed_types.MBReqDomain_FullSystem + | MBReqDomain_Nonshareable -> ArmV8_types.MBReqDomain_Nonshareable + | MBReqDomain_InnerShareable -> ArmV8_types.MBReqDomain_InnerShareable + | MBReqDomain_OuterShareable -> ArmV8_types.MBReqDomain_OuterShareable + | MBReqDomain_FullSystem -> ArmV8_types.MBReqDomain_FullSystem let translate_mBReqTypes _ = function - | MBReqTypes_Reads -> ArmV8_embed_types.MBReqTypes_Reads - | MBReqTypes_Writes -> ArmV8_embed_types.MBReqTypes_Writes - | MBReqTypes_All -> ArmV8_embed_types.MBReqTypes_All + | MBReqTypes_Reads -> ArmV8_types.MBReqTypes_Reads + | MBReqTypes_Writes -> ArmV8_types.MBReqTypes_Writes + | MBReqTypes_All -> ArmV8_types.MBReqTypes_All let translate_systemHintOp _ = function - | SystemHintOp_NOP -> ArmV8_embed_types.SystemHintOp_NOP - | SystemHintOp_YIELD -> ArmV8_embed_types.SystemHintOp_YIELD - | SystemHintOp_WFE -> ArmV8_embed_types.SystemHintOp_WFE - | SystemHintOp_WFI -> ArmV8_embed_types.SystemHintOp_WFI - | SystemHintOp_SEV -> ArmV8_embed_types.SystemHintOp_SEV - | SystemHintOp_SEVL -> ArmV8_embed_types.SystemHintOp_SEVL + | SystemHintOp_NOP -> ArmV8_types.SystemHintOp_NOP + | SystemHintOp_YIELD -> ArmV8_types.SystemHintOp_YIELD + | SystemHintOp_WFE -> ArmV8_types.SystemHintOp_WFE + | SystemHintOp_WFI -> ArmV8_types.SystemHintOp_WFI + | SystemHintOp_SEV -> ArmV8_types.SystemHintOp_SEV + | SystemHintOp_SEVL -> ArmV8_types.SystemHintOp_SEVL let translate_accType _ = function - | AccType_NORMAL -> ArmV8_embed_types.AccType_NORMAL - | AccType_VEC -> ArmV8_embed_types.AccType_VEC - | AccType_STREAM -> ArmV8_embed_types.AccType_STREAM - | AccType_VECSTREAM -> ArmV8_embed_types.AccType_VECSTREAM - | AccType_ATOMIC -> ArmV8_embed_types.AccType_ATOMIC - | AccType_ORDERED -> ArmV8_embed_types.AccType_ORDERED - | AccType_UNPRIV -> ArmV8_embed_types.AccType_UNPRIV - | AccType_IFETCH -> ArmV8_embed_types.AccType_IFETCH - | AccType_PTW -> ArmV8_embed_types.AccType_PTW - | AccType_DC -> ArmV8_embed_types.AccType_DC - | AccType_IC -> ArmV8_embed_types.AccType_IC - | AccType_AT -> ArmV8_embed_types.AccType_AT + | AccType_NORMAL -> ArmV8_types.AccType_NORMAL + | AccType_VEC -> ArmV8_types.AccType_VEC + | AccType_STREAM -> ArmV8_types.AccType_STREAM + | AccType_VECSTREAM -> ArmV8_types.AccType_VECSTREAM + | AccType_ATOMIC -> ArmV8_types.AccType_ATOMIC + | AccType_ORDERED -> ArmV8_types.AccType_ORDERED + | AccType_UNPRIV -> ArmV8_types.AccType_UNPRIV + | AccType_IFETCH -> ArmV8_types.AccType_IFETCH + | AccType_PTW -> ArmV8_types.AccType_PTW + | AccType_DC -> ArmV8_types.AccType_DC + | AccType_IC -> ArmV8_types.AccType_IC + | AccType_AT -> ArmV8_types.AccType_AT let translate_memOp _ = function - | MemOp_LOAD -> ArmV8_embed_types.MemOp_LOAD - | MemOp_STORE -> ArmV8_embed_types.MemOp_STORE - | MemOp_PREFETCH -> ArmV8_embed_types.MemOp_PREFETCH + | MemOp_LOAD -> ArmV8_types.MemOp_LOAD + | MemOp_STORE -> ArmV8_types.MemOp_STORE + | MemOp_PREFETCH -> ArmV8_types.MemOp_PREFETCH let translate_moveWideOp _ = function - | MoveWideOp_N -> ArmV8_embed_types.MoveWideOp_N - | MoveWideOp_Z -> ArmV8_embed_types.MoveWideOp_Z - | MoveWideOp_K -> ArmV8_embed_types.MoveWideOp_K + | MoveWideOp_N -> ArmV8_types.MoveWideOp_N + | MoveWideOp_Z -> ArmV8_types.MoveWideOp_Z + | MoveWideOp_K -> ArmV8_types.MoveWideOp_K let translate_revOp _ = function - | RevOp_RBIT -> ArmV8_embed_types.RevOp_RBIT - | RevOp_REV16 -> ArmV8_embed_types.RevOp_REV16 - | RevOp_REV32 -> ArmV8_embed_types.RevOp_REV32 - | RevOp_REV64 -> ArmV8_embed_types.RevOp_REV64 + | RevOp_RBIT -> ArmV8_types.RevOp_RBIT + | RevOp_REV16 -> ArmV8_types.RevOp_REV16 + | RevOp_REV32 -> ArmV8_types.RevOp_REV32 + | RevOp_REV64 -> ArmV8_types.RevOp_REV64 let translate_pSTATEField _ = function - | PSTATEField_DAIFSet -> ArmV8_embed_types.PSTATEField_DAIFSet - | PSTATEField_DAIFClr -> ArmV8_embed_types.PSTATEField_DAIFClr - | PSTATEField_SP -> ArmV8_embed_types.PSTATEField_SP + | PSTATEField_DAIFSet -> ArmV8_types.PSTATEField_DAIFSet + | PSTATEField_DAIFClr -> ArmV8_types.PSTATEField_DAIFClr + | PSTATEField_SP -> ArmV8_types.PSTATEField_SP diff --git a/aarch64_small/gen/shallow_ast_to_herdtools_ast.hgen b/aarch64_small/gen/shallow_ast_to_herdtools_ast.hgen index 55179a97..96b74b4f 100644 --- a/aarch64_small/gen/shallow_ast_to_herdtools_ast.hgen +++ b/aarch64_small/gen/shallow_ast_to_herdtools_ast.hgen @@ -1,20 +1,20 @@ -| Unallocated -> `AArch64Unallocated +| Unallocated () -> `AArch64Unallocated | TMStart t -> `AArch64TMStart (translate_out_regzr Set64 t) -| TMCommit -> `AArch64TMCommit +| TMCommit () -> `AArch64TMCommit | TMAbort (retry, reason) -> `AArch64TMAbort ( translate_out_bool retry, translate_out_bits reason) -| TMTest -> `AArch64TMTest +| TMTest () -> `AArch64TMTest -| ImplementationDefinedStopFetching -> +| ImplementationDefinedStopFetching () -> `AArch64ImplementationDefinedStopFetching -| ImplementationDefinedThreadStart -> +| ImplementationDefinedThreadStart () -> `AArch64ImplementationDefinedThreadStart | ImplementationDefinedTestBeginEnd (isEnd) -> diff --git a/aarch64_small/gen/shallow_types_to_herdtools_types.hgen b/aarch64_small/gen/shallow_types_to_herdtools_types.hgen index 771f52ac..a26879b4 100644 --- a/aarch64_small/gen/shallow_types_to_herdtools_types.hgen +++ b/aarch64_small/gen/shallow_types_to_herdtools_types.hgen @@ -1,17 +1,17 @@ -let translate_out_big_int_bits x = Sail_values.unsigned x +let translate_out_big_int_bits bits = (match Sail2_values.unsigned_of_bits bits with Some x -> x | None -> failwith "unsigned_of_bits returned None") -let translate_out_big_bit = Sail_values.unsigned +let translate_out_big_bit bits = (match Sail2_values.unsigned_of_bits bits with Some x -> x | None -> failwith "unsigned_of_bits returned None") -let translate_out_signed_big_bit = Sail_values.signed +let translate_out_signed_big_bit bits = (match Sail2_values.signed_of_bits bits with Some x -> x | None -> failwith "signed_of_bits returned None") let translate_out_int inst = (Nat_big_num.to_int inst) -let translate_out_bits bits = Nat_big_num.to_int (Sail_values.unsigned bits) +let translate_out_bits bits = Nat_big_num.to_int (match Sail2_values.unsigned_of_bits bits with Some x -> x | None -> failwith "unsigned_of_bits returned None") let translate_out_bool = function - | Sail_values.B1 -> true - | Sail_values.B0 -> false - | Sail_values.BU -> failwith "translate_out_bool Undef" + | Sail2_values.B10 -> true + | Sail2_values.B00 -> false + | Sail2_values.BU0 -> failwith "translate_out_bool Undef" let translate_out_enum (name,_,bits) = Nat_big_num.to_int (IInt.integer_of_bit_list bits) @@ -44,7 +44,7 @@ let translate_out_regzrbyext regsize extend_type reg = begin match extend_type end let translate_out_reg_size_bits bits = - match Nat_big_num.to_int (Sail_values.length bits) with + match (List.length bits) with | 32 -> R32Bits (translate_out_bits bits) | 64 -> R64Bits (translate_out_big_bit bits) | _ -> assert false @@ -58,97 +58,97 @@ let translate_out_data_size inst = | _ -> assert false let translate_out_extendType = function - | ArmV8_embed_types.ExtendType_UXTB -> ExtendType_UXTB - | ArmV8_embed_types.ExtendType_UXTH -> ExtendType_UXTH - | ArmV8_embed_types.ExtendType_UXTW -> ExtendType_UXTW - | ArmV8_embed_types.ExtendType_UXTX -> ExtendType_UXTX - | ArmV8_embed_types.ExtendType_SXTB -> ExtendType_SXTB - | ArmV8_embed_types.ExtendType_SXTH -> ExtendType_SXTH - | ArmV8_embed_types.ExtendType_SXTW -> ExtendType_SXTW - | ArmV8_embed_types.ExtendType_SXTX -> ExtendType_SXTX + | ArmV8_types.ExtendType_UXTB -> ExtendType_UXTB + | ArmV8_types.ExtendType_UXTH -> ExtendType_UXTH + | ArmV8_types.ExtendType_UXTW -> ExtendType_UXTW + | ArmV8_types.ExtendType_UXTX -> ExtendType_UXTX + | ArmV8_types.ExtendType_SXTB -> ExtendType_SXTB + | ArmV8_types.ExtendType_SXTH -> ExtendType_SXTH + | ArmV8_types.ExtendType_SXTW -> ExtendType_SXTW + | ArmV8_types.ExtendType_SXTX -> ExtendType_SXTX let translate_out_shiftType = function - | ArmV8_embed_types.ShiftType_LSL -> ShiftType_LSL - | ArmV8_embed_types.ShiftType_LSR -> ShiftType_LSR - | ArmV8_embed_types.ShiftType_ASR -> ShiftType_ASR - | ArmV8_embed_types.ShiftType_ROR -> ShiftType_ROR + | ArmV8_types.ShiftType_LSL -> ShiftType_LSL + | ArmV8_types.ShiftType_LSR -> ShiftType_LSR + | ArmV8_types.ShiftType_ASR -> ShiftType_ASR + | ArmV8_types.ShiftType_ROR -> ShiftType_ROR let translate_out_logicalOp = function - | ArmV8_embed_types.LogicalOp_AND -> LogicalOp_AND - | ArmV8_embed_types.LogicalOp_EOR -> LogicalOp_EOR - | ArmV8_embed_types.LogicalOp_ORR -> LogicalOp_ORR + | ArmV8_types.LogicalOp_AND -> LogicalOp_AND + | ArmV8_types.LogicalOp_EOR -> LogicalOp_EOR + | ArmV8_types.LogicalOp_ORR -> LogicalOp_ORR let translate_out_branchType = function - | ArmV8_embed_types.BranchType_CALL -> BranchType_CALL - | ArmV8_embed_types.BranchType_ERET -> BranchType_ERET - | ArmV8_embed_types.BranchType_DBGEXIT -> BranchType_DBGEXIT - | ArmV8_embed_types.BranchType_RET -> BranchType_RET - | ArmV8_embed_types.BranchType_JMP -> BranchType_JMP - | ArmV8_embed_types.BranchType_EXCEPTION -> BranchType_EXCEPTION - | ArmV8_embed_types.BranchType_UNKNOWN -> BranchType_UNKNOWN + | ArmV8_types.BranchType_CALL -> BranchType_CALL + | ArmV8_types.BranchType_ERET -> BranchType_ERET + | ArmV8_types.BranchType_DBGEXIT -> BranchType_DBGEXIT + | ArmV8_types.BranchType_RET -> BranchType_RET + | ArmV8_types.BranchType_JMP -> BranchType_JMP + | ArmV8_types.BranchType_EXCEPTION -> BranchType_EXCEPTION + | ArmV8_types.BranchType_UNKNOWN -> BranchType_UNKNOWN let translate_out_countOp = function - | ArmV8_embed_types.CountOp_CLZ -> CountOp_CLZ - | ArmV8_embed_types.CountOp_CLS -> CountOp_CLS - | ArmV8_embed_types.CountOp_CNT -> CountOp_CNT + | ArmV8_types.CountOp_CLZ -> CountOp_CLZ + | ArmV8_types.CountOp_CLS -> CountOp_CLS + | ArmV8_types.CountOp_CNT -> CountOp_CNT let translate_out_memBarrierOp = function - | ArmV8_embed_types.MemBarrierOp_DSB -> MemBarrierOp_DSB - | ArmV8_embed_types.MemBarrierOp_DMB -> MemBarrierOp_DMB - | ArmV8_embed_types.MemBarrierOp_ISB -> MemBarrierOp_ISB + | ArmV8_types.MemBarrierOp_DSB -> MemBarrierOp_DSB + | ArmV8_types.MemBarrierOp_DMB -> MemBarrierOp_DMB + | ArmV8_types.MemBarrierOp_ISB -> MemBarrierOp_ISB let translate_out_mBReqDomain = function - | ArmV8_embed_types.MBReqDomain_Nonshareable -> MBReqDomain_Nonshareable - | ArmV8_embed_types.MBReqDomain_InnerShareable -> MBReqDomain_InnerShareable - | ArmV8_embed_types.MBReqDomain_OuterShareable -> MBReqDomain_OuterShareable - | ArmV8_embed_types.MBReqDomain_FullSystem -> MBReqDomain_FullSystem + | ArmV8_types.MBReqDomain_Nonshareable -> MBReqDomain_Nonshareable + | ArmV8_types.MBReqDomain_InnerShareable -> MBReqDomain_InnerShareable + | ArmV8_types.MBReqDomain_OuterShareable -> MBReqDomain_OuterShareable + | ArmV8_types.MBReqDomain_FullSystem -> MBReqDomain_FullSystem let translate_out_mBReqTypes = function - | ArmV8_embed_types.MBReqTypes_Reads -> MBReqTypes_Reads - | ArmV8_embed_types.MBReqTypes_Writes -> MBReqTypes_Writes - | ArmV8_embed_types.MBReqTypes_All -> MBReqTypes_All + | ArmV8_types.MBReqTypes_Reads -> MBReqTypes_Reads + | ArmV8_types.MBReqTypes_Writes -> MBReqTypes_Writes + | ArmV8_types.MBReqTypes_All -> MBReqTypes_All let translate_out_systemHintOp = function - | ArmV8_embed_types.SystemHintOp_NOP -> SystemHintOp_NOP - | ArmV8_embed_types.SystemHintOp_YIELD -> SystemHintOp_YIELD - | ArmV8_embed_types.SystemHintOp_WFE -> SystemHintOp_WFE - | ArmV8_embed_types.SystemHintOp_WFI -> SystemHintOp_WFI - | ArmV8_embed_types.SystemHintOp_SEV -> SystemHintOp_SEV - | ArmV8_embed_types.SystemHintOp_SEVL -> SystemHintOp_SEVL + | ArmV8_types.SystemHintOp_NOP -> SystemHintOp_NOP + | ArmV8_types.SystemHintOp_YIELD -> SystemHintOp_YIELD + | ArmV8_types.SystemHintOp_WFE -> SystemHintOp_WFE + | ArmV8_types.SystemHintOp_WFI -> SystemHintOp_WFI + | ArmV8_types.SystemHintOp_SEV -> SystemHintOp_SEV + | ArmV8_types.SystemHintOp_SEVL -> SystemHintOp_SEVL let translate_out_accType = function - | ArmV8_embed_types.AccType_NORMAL -> AccType_NORMAL - | ArmV8_embed_types.AccType_VEC -> AccType_VEC - | ArmV8_embed_types.AccType_STREAM -> AccType_STREAM - | ArmV8_embed_types.AccType_VECSTREAM -> AccType_VECSTREAM - | ArmV8_embed_types.AccType_ATOMIC -> AccType_ATOMIC - | ArmV8_embed_types.AccType_ORDERED -> AccType_ORDERED - | ArmV8_embed_types.AccType_UNPRIV -> AccType_UNPRIV - | ArmV8_embed_types.AccType_IFETCH -> AccType_IFETCH - | ArmV8_embed_types.AccType_PTW -> AccType_PTW - | ArmV8_embed_types.AccType_DC -> AccType_DC - | ArmV8_embed_types.AccType_IC -> AccType_IC - | ArmV8_embed_types.AccType_AT -> AccType_AT + | ArmV8_types.AccType_NORMAL -> AccType_NORMAL + | ArmV8_types.AccType_VEC -> AccType_VEC + | ArmV8_types.AccType_STREAM -> AccType_STREAM + | ArmV8_types.AccType_VECSTREAM -> AccType_VECSTREAM + | ArmV8_types.AccType_ATOMIC -> AccType_ATOMIC + | ArmV8_types.AccType_ORDERED -> AccType_ORDERED + | ArmV8_types.AccType_UNPRIV -> AccType_UNPRIV + | ArmV8_types.AccType_IFETCH -> AccType_IFETCH + | ArmV8_types.AccType_PTW -> AccType_PTW + | ArmV8_types.AccType_DC -> AccType_DC + | ArmV8_types.AccType_IC -> AccType_IC + | ArmV8_types.AccType_AT -> AccType_AT let translate_out_memOp = function - | ArmV8_embed_types.MemOp_LOAD -> MemOp_LOAD - | ArmV8_embed_types.MemOp_STORE -> MemOp_STORE - | ArmV8_embed_types.MemOp_PREFETCH -> MemOp_PREFETCH + | ArmV8_types.MemOp_LOAD -> MemOp_LOAD + | ArmV8_types.MemOp_STORE -> MemOp_STORE + | ArmV8_types.MemOp_PREFETCH -> MemOp_PREFETCH let translate_out_moveWideOp = function - | ArmV8_embed_types.MoveWideOp_N -> MoveWideOp_N - | ArmV8_embed_types.MoveWideOp_Z -> MoveWideOp_Z - | ArmV8_embed_types.MoveWideOp_K -> MoveWideOp_K + | ArmV8_types.MoveWideOp_N -> MoveWideOp_N + | ArmV8_types.MoveWideOp_Z -> MoveWideOp_Z + | ArmV8_types.MoveWideOp_K -> MoveWideOp_K let translate_out_revOp = function - | ArmV8_embed_types.RevOp_RBIT -> RevOp_RBIT - | ArmV8_embed_types.RevOp_REV16 -> RevOp_REV16 - | ArmV8_embed_types.RevOp_REV32 -> RevOp_REV32 - | ArmV8_embed_types.RevOp_REV64 -> RevOp_REV64 + | ArmV8_types.RevOp_RBIT -> RevOp_RBIT + | ArmV8_types.RevOp_REV16 -> RevOp_REV16 + | ArmV8_types.RevOp_REV32 -> RevOp_REV32 + | ArmV8_types.RevOp_REV64 -> RevOp_REV64 let translate_out_pSTATEField = function - | ArmV8_embed_types.PSTATEField_DAIFSet -> PSTATEField_DAIFSet - | ArmV8_embed_types.PSTATEField_DAIFClr -> PSTATEField_DAIFClr - | ArmV8_embed_types.PSTATEField_SP -> PSTATEField_SP + | ArmV8_types.PSTATEField_DAIFSet -> PSTATEField_DAIFSet + | ArmV8_types.PSTATEField_DAIFClr -> PSTATEField_DAIFClr + | ArmV8_types.PSTATEField_SP -> PSTATEField_SP |