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/Machconcr.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/Machconcr.v')
-rw-r--r-- | backend/Machconcr.v | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/backend/Machconcr.v b/backend/Machconcr.v index 5b63fa8f..b736c8f7 100644 --- a/backend/Machconcr.v +++ b/backend/Machconcr.v @@ -23,7 +23,7 @@ Require Import Globalenvs. Require Import Smallstep. Require Import Op. Require Import Locations. -Require Conventions. +Require Import Conventions. Require Import Mach. Require Stacklayout. Require Asmgenretaddr. @@ -82,7 +82,7 @@ Inductive extcall_args: regset -> mem -> val -> list loc -> list val -> Prop := Definition extcall_arguments (rs: regset) (m: mem) (sp: val) (sg: signature) (args: list val) : Prop := - extcall_args rs m sp (Conventions.loc_arguments sg) args. + extcall_args rs m sp (loc_arguments sg) args. (** Mach execution states. *) @@ -187,6 +187,11 @@ Inductive step: state -> trace -> state -> Prop := Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' -> step (State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs m) E0 (Callstate s f' rs m') + | exec_Mbuiltin: + forall s f sp rs m ef args res b t v m', + external_call ef ge rs##args m t v m' -> + step (State s f sp (Mbuiltin ef args res :: b) rs m) + t (State s f sp b (rs#res <- v) m') | exec_Mgoto: forall s fb f sp lbl c rs m c', Genv.find_funct_ptr ge fb = Some (Internal f) -> @@ -234,8 +239,8 @@ Inductive step: state -> trace -> state -> Prop := forall s fb rs m t rs' ef args res m', Genv.find_funct_ptr ge fb = Some (External ef) -> external_call ef ge args m t res m' -> - extcall_arguments rs m (parent_sp s) ef.(ef_sig) args -> - rs' = (rs#(Conventions.loc_result ef.(ef_sig)) <- res) -> + extcall_arguments rs m (parent_sp s) (ef_sig ef) args -> + rs' = (rs#(loc_result (ef_sig ef)) <- res) -> step (Callstate s fb rs m) t (Returnstate s rs' m') | exec_return: @@ -254,7 +259,7 @@ Inductive initial_state (p: program): state -> Prop := Inductive final_state: state -> int -> Prop := | final_state_intro: forall rs m r, - rs (Conventions.loc_result (mksignature nil (Some Tint))) = Vint r -> + rs (loc_result (mksignature nil (Some Tint))) = Vint r -> final_state (Returnstate nil rs m) r. Definition exec_program (p: program) (beh: program_behavior) : Prop := |