diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-06-29 08:27:14 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-06-29 08:27:14 +0000 |
commit | 9c7c84cc40eaacc1e2c13091165785cddecba5ad (patch) | |
tree | 65eafe51ad284d88fd5a949e1b2a54cd272f9f91 /backend/Selection.v | |
parent | f4b416882955d9d91bca60f3eb35b95f4124a5be (diff) | |
download | compcert-9c7c84cc40eaacc1e2c13091165785cddecba5ad.tar.gz compcert-9c7c84cc40eaacc1e2c13091165785cddecba5ad.zip |
Support for inlined built-ins.
AST: add ef_inline flag to external functions.
Selection: recognize calls to inlined built-ins and inline them as Sbuiltin.
CminorSel to Asm: added Sbuiltin/Ibuiltin instruction.
PrintAsm: adapted expansion of builtins.
C2Clight: adapted detection of builtins.
Conventions: refactored in a machine-independent part (backend/Conventions)
and a machine-dependent part (ARCH/SYS/Conventions1).
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1356 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Selection.v')
-rw-r--r-- | backend/Selection.v | 51 |
1 files changed, 39 insertions, 12 deletions
diff --git a/backend/Selection.v b/backend/Selection.v index e822fdf7..ebdad8a2 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -167,46 +167,73 @@ Fixpoint sel_exprlist (al: list Cminor.expr) : exprlist := | a :: bl => Econs (sel_expr a) (sel_exprlist bl) end. +(** Recognition of calls to built-in functions that should be inlined *) + +Definition expr_is_addrof_ident (e: Cminor.expr) : option ident := + match e with + | Cminor.Econst (Cminor.Oaddrsymbol id ofs) => + if Int.eq ofs Int.zero then Some id else None + | _ => None + end. + +Definition expr_is_addrof_builtin (ge: Cminor.genv) (e: Cminor.expr) : option external_function := + match expr_is_addrof_ident e with + | None => None + | Some id => + match Genv.find_symbol ge id with + | None => None + | Some b => + match Genv.find_funct_ptr ge b with + | Some(External ef) => if ef.(ef_inline) then Some ef else None + | _ => None + end + end + end. + (** Conversion from Cminor statements to Cminorsel statements. *) -Fixpoint sel_stmt (s: Cminor.stmt) : stmt := +Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : stmt := match s with | Cminor.Sskip => Sskip | Cminor.Sassign id e => Sassign id (sel_expr e) | Cminor.Sstore chunk addr rhs => store chunk (sel_expr addr) (sel_expr rhs) | Cminor.Scall optid sg fn args => - Scall optid sg (sel_expr fn) (sel_exprlist args) + match expr_is_addrof_builtin ge fn with + | None => Scall optid sg (sel_expr fn) (sel_exprlist args) + | Some ef => Sbuiltin optid ef (sel_exprlist args) + end | Cminor.Stailcall sg fn args => Stailcall sg (sel_expr fn) (sel_exprlist args) - | Cminor.Sseq s1 s2 => Sseq (sel_stmt s1) (sel_stmt s2) + | Cminor.Sseq s1 s2 => Sseq (sel_stmt ge s1) (sel_stmt ge s2) | Cminor.Sifthenelse e ifso ifnot => Sifthenelse (condexpr_of_expr (sel_expr e)) - (sel_stmt ifso) (sel_stmt ifnot) - | Cminor.Sloop body => Sloop (sel_stmt body) - | Cminor.Sblock body => Sblock (sel_stmt body) + (sel_stmt ge ifso) (sel_stmt ge ifnot) + | Cminor.Sloop body => Sloop (sel_stmt ge body) + | Cminor.Sblock body => Sblock (sel_stmt ge body) | Cminor.Sexit n => Sexit n | Cminor.Sswitch e cases dfl => Sswitch (sel_expr e) cases dfl | Cminor.Sreturn None => Sreturn None | Cminor.Sreturn (Some e) => Sreturn (Some (sel_expr e)) - | Cminor.Slabel lbl body => Slabel lbl (sel_stmt body) + | Cminor.Slabel lbl body => Slabel lbl (sel_stmt ge body) | Cminor.Sgoto lbl => Sgoto lbl end. (** Conversion of functions and programs. *) -Definition sel_function (f: Cminor.function) : function := +Definition sel_function (ge: Cminor.genv) (f: Cminor.function) : function := mkfunction f.(Cminor.fn_sig) f.(Cminor.fn_params) f.(Cminor.fn_vars) f.(Cminor.fn_stackspace) - (sel_stmt f.(Cminor.fn_body)). + (sel_stmt ge f.(Cminor.fn_body)). -Definition sel_fundef (f: Cminor.fundef) : fundef := - transf_fundef sel_function f. +Definition sel_fundef (ge: Cminor.genv) (f: Cminor.fundef) : fundef := + transf_fundef (sel_function ge) f. Definition sel_program (p: Cminor.program) : program := - transform_program sel_fundef p. + let ge := Genv.globalenv p in + transform_program (sel_fundef ge) p. |