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/Linear.v | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) (limited to 'backend/Linear.v') diff --git a/backend/Linear.v b/backend/Linear.v index 71310a97..0f44206d 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -43,6 +43,7 @@ Inductive instruction: Type := | Lstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction | Lcall: signature -> mreg + ident -> instruction | Ltailcall: signature -> mreg + ident -> instruction + | Lbuiltin: external_function -> list mreg -> mreg -> instruction | Llabel: label -> instruction | Lgoto: label -> instruction | Lcond: condition -> list mreg -> label -> instruction @@ -63,8 +64,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. Definition genv := Genv.t fundef unit. @@ -153,9 +154,9 @@ Definition return_regs (caller callee: locset) : locset := fun (l: loc) => match l with | R r => - if In_dec Loc.eq (R r) Conventions.temporaries then + if In_dec Loc.eq (R r) temporaries then callee (R r) - else if In_dec Loc.eq (R r) Conventions.destroyed_at_call then + else if In_dec Loc.eq (R r) destroyed_at_call then callee (R r) else caller (R r) @@ -275,6 +276,11 @@ Inductive step: state -> trace -> state -> Prop := Mem.free m stk 0 f.(fn_stacksize) = Some m' -> step (State s f (Vptr stk Int.zero) (Ltailcall sig ros :: b) rs m) E0 (Callstate s f' (return_regs (parent_locset s) rs) m') + | exec_Lbuiltin: + forall s f sp rs m ef args res b t v m', + external_call ef ge (reglist rs args) m t v m' -> + step (State s f sp (Lbuiltin ef args res :: b) rs m) + t (State s f sp b (Locmap.set (R res) v rs) m') | exec_Llabel: forall s f sp lbl b rs m, step (State s f sp (Llabel lbl :: b) rs m) @@ -315,8 +321,8 @@ Inductive step: state -> trace -> state -> Prop := | exec_function_external: forall s ef args res rs1 rs2 m t m', external_call ef ge args m t res m' -> - args = List.map rs1 (Conventions.loc_arguments ef.(ef_sig)) -> - rs2 = Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs1 -> + args = List.map rs1 (loc_arguments (ef_sig ef)) -> + rs2 = Locmap.set (R (loc_result (ef_sig ef))) res rs1 -> step (Callstate s (External ef) rs1 m) t (Returnstate s rs2 m') | exec_return: @@ -337,7 +343,7 @@ Inductive initial_state (p: program): state -> Prop := Inductive final_state: state -> int -> Prop := | final_state_intro: forall rs m r, - rs (R (Conventions.loc_result (mksignature nil (Some Tint)))) = Vint r -> + rs (R (loc_result (mksignature nil (Some Tint)))) = Vint r -> final_state (Returnstate nil rs m) r. Definition exec_program (p: program) (beh: program_behavior) : Prop := -- cgit