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/RTL.v | |
| parent | f4b416882955d9d91bca60f3eb35b95f4124a5be (diff) | |
| download | compcert-kvx-9c7c84cc40eaacc1e2c13091165785cddecba5ad.tar.gz compcert-kvx-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/RTL.v')
| -rw-r--r-- | backend/RTL.v | 15 |
1 files changed, 13 insertions, 2 deletions
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 |