diff --git a/aarch64/Machregs.v b/aarch64/Machregs.v index 3687a744a..d5ef86137 100644 --- a/aarch64/Machregs.v +++ b/aarch64/Machregs.v @@ -119,13 +119,68 @@ Definition register_names := :: ("D28", F28) :: ("D29", F29) :: ("D30", F30) :: ("D31", F31) :: nil. +Definition register_aliases := + ("W0", R0) :: ("W1", R1) :: ("W2", R2) :: ("W3", R3) + :: ("W4", R4) :: ("W5", R5) :: ("W6", R6) :: ("W7", R7) + :: ("W8", R8) :: ("W9", R9) :: ("W10", R10) :: ("W11", R11) + :: ("W12", R12) :: ("W13", R13) :: ("W14", R14) :: ("W15", R15) + :: ("W17", R17) :: ("W19", R19) + :: ("W20", R20) :: ("W21", R21) :: ("W22", R22) :: ("W23", R23) + :: ("W24", R24) :: ("W25", R25) :: ("W26", R26) :: ("W27", R27) + :: ("W28", R28) :: ("W29", R29) + :: ("V0", F0) :: ("V1", F1) :: ("V2", F2) :: ("V3", F3) + :: ("V4", F4) :: ("V5", F5) :: ("V6", F6) :: ("V7", F7) + :: ("V8", F8) :: ("V9", F9) :: ("V10", F10) :: ("V11", F11) + :: ("V12", F12) :: ("V13", F13) :: ("V14", F14) :: ("V15", F15) + :: ("V16", F16) :: ("V17", F17) :: ("V18", F18) :: ("V19", F19) + :: ("V20", F20) :: ("V21", F21) :: ("V22", F22) :: ("V23", F23) + :: ("V24", F24) :: ("V25", F25) :: ("V26", F26) :: ("V27", F27) + :: ("V28", F28) :: ("V29", F29) :: ("V30", F30) :: ("V31", F31) + :: ("Q0", F0) :: ("Q1", F1) :: ("Q2", F2) :: ("Q3", F3) + :: ("Q4", F4) :: ("Q5", F5) :: ("Q6", F6) :: ("Q7", F7) + :: ("Q8", F8) :: ("Q9", F9) :: ("Q10", F10) :: ("Q11", F11) + :: ("Q12", F12) :: ("Q13", F13) :: ("Q14", F14) :: ("Q15", F15) + :: ("Q16", F16) :: ("Q17", F17) :: ("Q18", F18) :: ("Q19", F19) + :: ("Q20", F20) :: ("Q21", F21) :: ("Q22", F22) :: ("Q23", F23) + :: ("Q24", F24) :: ("Q25", F25) :: ("Q26", F26) :: ("Q27", F27) + :: ("Q28", F28) :: ("Q29", F29) :: ("Q30", F30) :: ("Q31", F31) + :: ("S0", F0) :: ("S1", F1) :: ("S2", F2) :: ("S3", F3) + :: ("S4", F4) :: ("S5", F5) :: ("S6", F6) :: ("S7", F7) + :: ("S8", F8) :: ("S9", F9) :: ("S10", F10) :: ("S11", F11) + :: ("S12", F12) :: ("S13", F13) :: ("S14", F14) :: ("S15", F15) + :: ("S16", F16) :: ("S17", F17) :: ("S18", F18) :: ("S19", F19) + :: ("S20", F20) :: ("S21", F21) :: ("S22", F22) :: ("S23", F23) + :: ("S24", F24) :: ("S25", F25) :: ("S26", F26) :: ("S27", F27) + :: ("S28", F28) :: ("S29", F29) :: ("S30", F30) :: ("S31", F31) + :: ("H0", F0) :: ("H1", F1) :: ("H2", F2) :: ("H3", F3) + :: ("H4", F4) :: ("H5", F5) :: ("H6", F6) :: ("H7", F7) + :: ("H8", F8) :: ("H9", F9) :: ("H10", F10) :: ("H11", F11) + :: ("H12", F12) :: ("H13", F13) :: ("H14", F14) :: ("H15", F15) + :: ("H16", F16) :: ("H17", F17) :: ("H18", F18) :: ("H19", F19) + :: ("H20", F20) :: ("H21", F21) :: ("H22", F22) :: ("H23", F23) + :: ("H24", F24) :: ("H25", F25) :: ("H26", F26) :: ("H27", F27) + :: ("H28", F28) :: ("H29", F29) :: ("H30", F30) :: ("H31", F31) + :: ("B0", F0) :: ("B1", F1) :: ("B2", F2) :: ("B3", F3) + :: ("B4", F4) :: ("B5", F5) :: ("B6", F6) :: ("B7", F7) + :: ("B8", F8) :: ("B9", F9) :: ("B10", F10) :: ("B11", F11) + :: ("B12", F12) :: ("B13", F13) :: ("B14", F14) :: ("B15", F15) + :: ("B16", F16) :: ("B17", F17) :: ("B18", F18) :: ("B19", F19) + :: ("B20", F20) :: ("B21", F21) :: ("B22", F22) :: ("B23", F23) + :: ("B24", F24) :: ("B25", F25) :: ("B26", F26) :: ("B27", F27) + :: ("B28", F28) :: ("B29", F29) :: ("B30", F30) :: ("B31", F31) + :: nil. + Definition register_by_name (s: string) : option mreg := let fix assoc (l: list (string * mreg)) : option mreg := match l with | nil => None | (s1, r1) :: l' => if string_dec s s1 then Some r1 else assoc l' end - in assoc register_names. + in + match assoc register_names with + | Some res => Some res + | None => assoc register_aliases + end. (** ** Destroyed registers, preferred registers *) diff --git a/aarch64/Machregsaux.ml b/aarch64/Machregsaux.ml index 5f3c1a8d0..3d5017d59 100644 --- a/aarch64/Machregsaux.ml +++ b/aarch64/Machregsaux.ml @@ -13,4 +13,5 @@ (** Auxiliary functions on machine registers *) let is_scratch_register s = - s = "X16" || s = "x16" || s = "X30" || s = "x30" + s = "X16" || s = "x16" || s = "W16" || s = "w16" || + s = "X30" || s = "x30" || s = "W30" || s = "w30"