From 9c7c84cc40eaacc1e2c13091165785cddecba5ad Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 29 Jun 2010 08:27:14 +0000 Subject: 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 --- backend/RTL.v | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) (limited to 'backend/RTL.v') diff --git a/backend/RTL.v b/backend/RTL.v index a17c74ee..1c309a0c 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -70,6 +70,10 @@ Inductive instruction: Type := | Itailcall: signature -> reg + ident -> list reg -> instruction (** [Itailcall sig fn args] performs a function invocation in tail-call position. *) + | Ibuiltin: external_function -> list reg -> reg -> node -> instruction + (** [Ibuiltin ef args dest succ] calls the built-in function + identified by [ef], giving it the values of [args] as arguments. + It stores the return value in [dest] and branches to [succ]. *) | Icond: condition -> list reg -> node -> node -> instruction (** [Icond cond args ifso ifnot] evaluates the boolean condition [cond] over the values of registers [args]. If the condition @@ -109,8 +113,8 @@ Definition program := AST.program fundef unit. Definition funsig (fd: fundef) := match fd with - | Internal f => f.(fn_sig) - | External ef => ef.(ef_sig) + | Internal f => fn_sig f + | External ef => ef_sig ef end. (** * Operational semantics *) @@ -245,6 +249,12 @@ Inductive step: state -> trace -> state -> Prop := Mem.free m stk 0 f.(fn_stacksize) = Some m' -> step (State s f (Vptr stk Int.zero) pc rs m) E0 (Callstate s fd rs##args m') + | exec_Ibuiltin: + forall s f sp pc rs m ef args res pc' t v m', + (fn_code f)!pc = Some(Ibuiltin ef args res pc') -> + external_call ef ge rs##args m t v m' -> + step (State s f sp pc rs m) + t (State s f sp pc' (rs#res <- v) m') | exec_Icond_true: forall s f sp pc rs m cond args ifso ifnot, (fn_code f)!pc = Some(Icond cond args ifso ifnot) -> @@ -351,6 +361,7 @@ Definition successors_instr (i: instruction) : list node := | Istore chunk addr args src s => s :: nil | Icall sig ros args res s => s :: nil | Itailcall sig ros args => nil + | Ibuiltin ef args res s => s :: nil | Icond cond args ifso ifnot => ifso :: ifnot :: nil | Ijumptable arg tbl => tbl | Ireturn optarg => nil -- cgit