Extended inline asm: revised treatment of clobbered registers.

- Treat clobbered registers as being destroyed by EF_inline_asm builtins
  (which is the truth, semantically).
- To enable the above, represent clobbers as Coq strings rather than idents
  and move register_by_name from Machregsaux.ml to Machregs.v.
- Side benefit: more efficient implementation of Machregsaux.name_of_register.

-# Please enter the commit message for your changes. Lines starting

1 files changed, 2 insertions, 4 deletions

diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index c286e946..aa4efc53 100644
--- a/backend/Regalloc.ml
+++ b/backend/Regalloc.ml
@@ -585,13 +585,11 @@ let add_interfs_instr g instr live =
           (* like a move *)
           IRC.add_pref g arg res
       | EF_inline_asm(txt, sg, clob), _, _ ->
-          (* clobbered regs interfere with live set
-             and also with res and args for GCC compatibility *)
+          (* clobbered regs interfere with res and args for GCC compatibility *)
           List.iter (fun c ->
-            match Machregsaux.register_by_name (extern_atom c) with
+            match Machregs.register_by_name c with
             | None -> ()
             | Some mr ->
-                add_interfs_destroyed g across [mr];
                 add_interfs_list_mreg g args mr;
                 if sg.sig_res <> None then add_interfs_list_mreg g res mr)
             clob