From 1b5db339bb05f773a6a132be4c0b8cea54d50461 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 17 Apr 2015 16:30:43 +0200 Subject: Experiment: support a subset of GCC's extended asm statements. --- backend/CMparser.mly | 2 +- backend/CSE.v | 2 +- backend/PrintAnnot.ml | 24 +++++++++++++++++++++++- 3 files changed, 25 insertions(+), 3 deletions(-) (limited to 'backend') diff --git a/backend/CMparser.mly b/backend/CMparser.mly index 69b70e72..bcfa4548 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -60,7 +60,7 @@ let mkef sg toks = if sg.sig_args = [] then raise Parsing.Parse_error; EF_annot_val(intern_string txt, List.hd sg.sig_args) | [EFT_tok "inline_asm"; EFT_string txt] -> - EF_inline_asm(intern_string txt) + EF_inline_asm(intern_string txt, sg) | _ -> raise Parsing.Parse_error diff --git a/backend/CSE.v b/backend/CSE.v index 2c0c5f33..9f295402 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -476,7 +476,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb empty_numbering | Ibuiltin ef args res s => match ef with - | EF_external _ _ | EF_malloc | EF_free | EF_inline_asm _ => + | EF_external _ _ | EF_malloc | EF_free | EF_inline_asm _ _ => empty_numbering | EF_builtin _ _ | EF_vstore _ | EF_vstore_global _ _ _ => set_unknown (kill_all_loads before) res diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml index 995f22dd..88f5d8d6 100644 --- a/backend/PrintAnnot.ml +++ b/backend/PrintAnnot.ml @@ -148,7 +148,29 @@ let print_annot_val print_preg oc txt args = print_annot_text print_preg "" oc txt (List.map (fun r -> AA_base r) args) -(* Print CompCert version and command-line as asm comment *) +(** Inline assembly *) + +let re_asm_param = Str.regexp "%%\\|%[0-9]+" + +let print_inline_asm print_preg oc txt sg args res = + let operands = + if sg.sig_res = None then args else res @ args in + let print_fragment = function + | Str.Text s -> + output_string oc s + | Str.Delim "%%" -> + output_char oc '%' + | Str.Delim s -> + let n = int_of_string (String.sub s 1 (String.length s - 1)) in + try + print_preg oc (List.nth operands n) + with Failure _ -> + fprintf oc "" s in + List.iter print_fragment (Str.full_split re_asm_param txt); + fprintf oc "\n" + + +(** Print CompCert version and command-line as asm comment *) let print_version_and_options oc comment = fprintf oc "%s File generated by CompCert %s\n" comment Configuration.version; -- cgit From 426881cde464691b61c5c49cf5038d21aace75fe Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 21 Apr 2015 10:21:06 +0200 Subject: Support for GCC-style extended asm, continued: - support "r", "m" and "i" constraints - support "%Q" and "%R" modifiers for register pairs - support register clobbers - split off analysis and transformation of asm statements in cparser/ExtendedAsm.ml --- backend/CSE.v | 2 +- backend/Regalloc.ml | 18 +++++++++++++++++- 2 files changed, 18 insertions(+), 2 deletions(-) (limited to 'backend') diff --git a/backend/CSE.v b/backend/CSE.v index 9f295402..e9006d4f 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -476,7 +476,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb empty_numbering | Ibuiltin ef args res s => match ef with - | EF_external _ _ | EF_malloc | EF_free | EF_inline_asm _ _ => + | EF_external _ _ | EF_malloc | EF_free | EF_inline_asm _ _ _ => empty_numbering | EF_builtin _ _ | EF_vstore _ | EF_vstore_global _ _ _ => set_unknown (kill_all_loads before) res diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index 3a7f5d99..c286e946 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -510,6 +510,9 @@ let add_interfs_live g live v = let add_interfs_list g v vl = List.iter (IRC.add_interf g v) vl +let add_interfs_list_mreg g vl mr = + List.iter (fun v -> IRC.add_interf g v (L (R mr))) vl + let rec add_interfs_pairwise g = function | [] -> () | v1 :: vl -> add_interfs_list g v1 vl; add_interfs_pairwise g vl @@ -578,7 +581,20 @@ let add_interfs_instr g instr live = add_interfs_pairwise g res; add_interfs_destroyed g across (destroyed_by_builtin ef); begin match ef, args, res with - | EF_annot_val _, [arg], [res] -> IRC.add_pref g arg res (* like a move *) + | EF_annot_val _, [arg], [res] -> + (* 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 *) + List.iter (fun c -> + match Machregsaux.register_by_name (extern_atom 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 | _ -> () end | Xannot(ef, args) -> -- cgit From 832685e5dc7c17c434146d353b60c2158e3edd11 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 21 Apr 2015 11:36:56 +0200 Subject: Cleanups and updates for extended asm. --- backend/CMparser.mly | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backend') diff --git a/backend/CMparser.mly b/backend/CMparser.mly index bcfa4548..f62e05d4 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -60,7 +60,7 @@ let mkef sg toks = if sg.sig_args = [] then raise Parsing.Parse_error; EF_annot_val(intern_string txt, List.hd sg.sig_args) | [EFT_tok "inline_asm"; EFT_string txt] -> - EF_inline_asm(intern_string txt, sg) + EF_inline_asm(intern_string txt, sg, []) | _ -> raise Parsing.Parse_error -- cgit