From a6b6bf31121d975c915c01f501618d97df7879fb Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 9 May 2015 09:00:51 +0200 Subject: 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 --- backend/Regalloc.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'backend/Regalloc.ml') 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 -- cgit