Extended asm: print register names according to their types

When printing an extended asm code fragment, placeholders %n
are replaced by register names.

Currently we ignore the fact that some assemblers use different
register names depending on the width of the data that resides
in the register.

For example, x86_64 uses %rax for a 64-bit quantity and %eax for
a 32-bit quantity, but CompCert always prints %rax in extended asm
statements.  This is problematic if we want to use 32-bit integer
instructions in extended asm, e.g.

             int x, y;
             asm("addl %1, %0", "=r"(x), "r"(y));
produces
             addl %rax, %rdx

which is syntactically incorrect.

Another example is ARM FP registers: D0 is a double-precision float,
but S0 is a single-precision float.

This commit partially solves this issue by taking into account the
Cminor type of the asm parameter when printing the corresponding register.
Continuing the previous example,

             int x, y;
             asm("addl %1, %0", "=r"(x), "r"(y));
now produces
             addl %eax, %edx

This is not perfect yet: we use Cminor types, because this is all we
have at hand, and not source C types, hence "char" and "short" parameters
are still printed like "int" parameters, which is not good for x86.
(I.e. we produce %eax where GCC might have produced %al or %ax.)
We'll leave this issue open.

6 files changed, 34 insertions, 19 deletions

diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 3a0814e1..03e06a65 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -113,9 +113,9 @@ struct
   let freg_single oc r = output_string oc (single_float_reg_name r)
   let freg_param_single oc r = output_string oc (single_param_reg_name r)
 
-  let preg oc = function
+  let preg_asm oc ty = function
     | IR r -> ireg oc r
-    | FR r -> freg oc r
+    | FR r -> if ty = Tsingle then freg_single oc r else freg oc r
     | _    -> assert false
 
   (* In Thumb2 mode, some arithmetic instructions have shorter encodings
@@ -480,7 +480,7 @@ struct
             (P.to_int kind) (extern_atom txt) args
         | EF_inline_asm(txt, sg, clob) ->
           fprintf oc "%s begin inline assembly\n\t" comment;
-          print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res;
+          print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res;
           fprintf oc "%s end inline assembly\n" comment
         | _ ->
           assert false
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 7e075f04..8652b2c5 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -245,14 +245,15 @@ let print_debug_info comment print_line preg_string sp_name oc kind txt args =
 
 (** Inline assembly *)
 
-let print_asm_argument print_preg oc modifier = function
-  | BA r -> print_preg oc r
+let print_asm_argument print_preg oc modifier typ = function 
+  | BA r -> print_preg oc typ r
   | BA_splitlong(BA hi, BA lo) ->
       begin match modifier with
-      | "R" -> print_preg oc hi
-      | "Q" -> print_preg oc lo
-      |  _  -> fprintf oc "%a:%a" print_preg hi print_preg lo
-                  (* Probably not what was intended *)
+      | "R" -> print_preg oc Tint hi
+      | "Q" -> print_preg oc Tint lo
+      |  _  -> print_preg oc Tint hi; fprintf oc ":"; print_preg oc Tint lo
+               (* This case (printing a split long in full) should never
+                  happen because of the checks done in ExtendedAsm.ml *)
       end
   | _ -> failwith "bad asm argument"
 
@@ -265,8 +266,10 @@ let re_asm_param_1 = Str.regexp "%%\\|%[QR]?[0-9]+"
 let re_asm_param_2 = Str.regexp "%\\([QR]?\\)\\([0-9]+\\)"
 
 let print_inline_asm print_preg oc txt sg args res =
-  let operands =
-    if sg.sig_res = None then args else builtin_arg_of_res res :: args in
+  let (operands, ty_operands) =
+    match sg.sig_res with
+    | None -> (args, sg.sig_args)
+    | Some tres -> (builtin_arg_of_res res :: args, tres :: sg.sig_args) in
   let print_fragment = function
   | Str.Text s ->
       output_string oc s
@@ -277,7 +280,9 @@ let print_inline_asm print_preg oc txt sg args res =
       let modifier = Str.matched_group 1 s
       and number = int_of_string (Str.matched_group 2 s) in
       try
-        print_asm_argument print_preg oc modifier (List.nth operands number)
+        print_asm_argument print_preg oc modifier
+                           (List.nth ty_operands number)
+                           (List.nth operands number)
       with Failure _ ->
         fprintf oc "<bad parameter %s>" s in
   List.iter print_fragment (Str.full_split re_asm_param_1 txt);
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index a1338561..0f608d25 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -340,7 +340,7 @@ module Target (System : SYSTEM):TARGET =
     let ireg_or_zero oc r =
       if r = GPR0 then output_string oc "0" else ireg oc r
 
-    let preg oc = function
+    let preg_asm oc ty = function
       | IR r -> ireg oc r
       | FR r -> freg oc r
       | _    -> assert false
@@ -863,7 +863,7 @@ module Target (System : SYSTEM):TARGET =
                                (P.to_int kind) (extern_atom txt) args
           | EF_inline_asm(txt, sg, clob) ->
               fprintf oc "%s begin inline assembly\n\t" comment;
-              print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res;
+              print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res;
               fprintf oc "%s end inline assembly\n" comment
           | _ ->
               assert false
diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml
index 92df7a76..64bcea4c 100644
--- a/riscV/TargetPrinter.ml
+++ b/riscV/TargetPrinter.ml
@@ -93,7 +93,7 @@ module Target : TARGET =
       | X0 -> output_string oc "x0"
       | X r -> ireg oc r
 
-    let preg oc = function
+    let preg_asm oc ty = function
       | IR r -> ireg oc r
       | FR r -> freg oc r
       | _    -> assert false
@@ -582,7 +582,7 @@ module Target : TARGET =
                                (P.to_int kind) (extern_atom txt) args
           | EF_inline_asm(txt, sg, clob) ->
               fprintf oc "%s begin inline assembly\n\t" comment;
-              print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res;
+              print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res;
               fprintf oc "%s end inline assembly\n" comment
           | _ ->
               assert false
diff --git a/test/regression/extasm.c b/test/regression/extasm.c
index babc57f1..83a07a05 100644
--- a/test/regression/extasm.c
+++ b/test/regression/extasm.c
@@ -33,6 +33,7 @@ int main()
   void * y;
   long long z;
   double f;
+  float sf;
   char c[16];
 
   /* No inputs, no outputs */
@@ -72,6 +73,15 @@ int main()
 #ifdef FAILURES
   asm("FAIL4 a:%[a]" : "=r"(x) : [z]"i"(0));
 #endif
+  /* One argument of each type */
+  asm("TEST15 int32 %0" : : "r" (x));
+#ifdef SIXTYFOUR
+  asm("TEST15 int64 %0" : : "r" (z));
+#else
+  asm("TEST15 int64 %Q0 / %R0" : : "r" (z));
+#endif
+  asm("TEST15 float64 %0" : : "r" (f));
+  asm("TEST15 float32 %0" : : "r" (sf));
   /* Various failures */
 #ifdef FAILURES
   asm("FAIL5 out:%0,%1" : "=r"(x), "=r"(y));
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
index 3025d2e7..cd54e08b 100644
--- a/x86/TargetPrinter.ml
+++ b/x86/TargetPrinter.ml
@@ -62,8 +62,8 @@ let ireg64 oc r = output_string oc (int64_reg_name r)
 let ireg = if Archi.ptr64 then ireg64 else ireg32
 let freg oc r = output_string oc (float_reg_name r)
 
-let preg oc = function
-  | IR r -> ireg oc r
+let preg_asm oc ty = function
+  | IR r -> if ty = Tlong then ireg64 oc r else ireg32 oc r
   | FR r -> freg oc r
   | _    -> assert false
 
@@ -826,7 +826,7 @@ module Target(System: SYSTEM):TARGET =
                                (P.to_int kind) (extern_atom txt) args
           | EF_inline_asm(txt, sg, clob) ->
               fprintf oc "%s begin inline assembly\n\t" comment;
-              print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res;
+              print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res;
               fprintf oc "%s end inline assembly\n" comment
           | _ ->
               assert false