AArch64 asm clobbers: recognize more register names

Wn as alias for Xn  (integer register)
Vn Qn Sn Hn Bn as aliases for Dn  (floating-point/vector register)

Fixes: #569

Author: xavierleroy

aarch64/Machregs.v

@@ -10,7 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-From Coq Require Import String.
+From Coq Require Import String Ascii.
 Require Import Coqlib Decidableplus Maps.
 Require Import AST Op.
 
@@ -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 *)
 

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"