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/Machabstr2concr.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/Machabstr2concr.v')
-rw-r--r-- | backend/Machabstr2concr.v | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v index 125cd57a..1a97dda5 100644 --- a/backend/Machabstr2concr.v +++ b/backend/Machabstr2concr.v @@ -28,6 +28,7 @@ Require Import Mach. Require Import Machtyping. Require Import Machabstr. Require Import Machconcr. +Require Import Conventions. Require Import Asmgenretaddr. (** Two semantics were defined for the Mach intermediate language: @@ -911,7 +912,7 @@ Lemma transl_extcall_arguments: /\ Val.lessdef_list args targs. Proof. unfold Machabstr.extcall_arguments, extcall_arguments; intros. - generalize (Conventions.loc_arguments sg) args H. + generalize (loc_arguments sg) args H. induction l; intros; inv H2. exists (@nil val); split; constructor. exploit IHl; eauto. intros [targs [A B]]. @@ -1023,6 +1024,16 @@ Proof. eapply frame_match_load_retaddr; eauto. eapply match_stacks_parent_ra_pointer; eauto. econstructor; eauto. eapply match_stacks_free; eauto. + (* Mbuiltin *) + exploit external_call_mem_extends; eauto. eapply regset_lessdef_list; eauto. + intros [v' [ms' [A [B [C D]]]]]. + econstructor; split. + eapply exec_Mbuiltin. eauto. + econstructor; eauto with coqlib. + eapply match_stacks_external_call; eauto. + eapply frame_match_external_call; eauto. + apply regset_lessdef_set; eauto. + (* Mgoto *) econstructor; split. eapply exec_Mgoto; eauto. @@ -1104,7 +1115,7 @@ Lemma equiv_final_states: Proof. intros. inv H0. destruct H. inv H. inv STACKS. constructor. - generalize (RLD (Conventions.loc_result (mksignature nil (Some Tint)))). + generalize (RLD (loc_result (mksignature nil (Some Tint)))). rewrite H1. intro LD. inv LD. auto. Qed. |