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 --- driver/Compiler.v | 22 +++++++++++----------- driver/Complements.v | 12 ++++++++++-- 2 files changed, 21 insertions(+), 13 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 1580fcd6..09a6c52e 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -103,7 +103,7 @@ Notation "a @@ b" := RTL, then to LTL, etc, all the way to Asm, and iterates this transformation for every function. The second translates the whole Cminor program to a RTL program, then to an LTL program, etc. - Between Cminor and Asm, we follow the first approach because it has + Between CminorSel and Asm, we follow the first approach because it has lower memory requirements. The translation from Clight to Asm follows the second approach. @@ -121,11 +121,10 @@ Definition transf_rtl_fundef (f: RTL.fundef) : res Asm.fundef := @@@ Stacking.transf_fundef @@@ Asmgen.transf_fundef. -(* Here is the translation of a Cminor function to an Asm function. *) +(* Here is the translation of a CminorSel function to an Asm function. *) -Definition transf_cminor_fundef (f: Cminor.fundef) : res Asm.fundef := +Definition transf_cminorsel_fundef (f: CminorSel.fundef) : res Asm.fundef := OK f - @@ Selection.sel_fundef @@@ RTLgen.transl_fundef @@@ transf_rtl_fundef. @@ -135,7 +134,9 @@ Definition transf_rtl_program (p: RTL.program) : res Asm.program := transform_partial_program transf_rtl_fundef p. Definition transf_cminor_program (p: Cminor.program) : res Asm.program := - transform_partial_program transf_cminor_fundef p. + OK p + @@ Selection.sel_program + @@@ transform_partial_program transf_cminorsel_fundef. Definition transf_c_program (p: Csyntax.program) : res Asm.program := match Ctyping.typecheck_program p with @@ -284,16 +285,15 @@ Theorem transf_cminor_program_correct: Cminor.exec_program p beh -> Asm.exec_program tp beh. Proof. - intros. unfold transf_cminor_program, transf_cminor_fundef in H. + intros. unfold transf_cminor_program, transf_cminorsel_fundef in H. destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p3 [X3 P3]]. clear H. destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ X3) as [p2 [X2 P2]]. clear X3. - destruct (transform_program_compose _ _ _ _ _ _ _ _ X2) as [p1 [X1 P1]]. - generalize (transform_partial_program_identity _ _ _ _ X1). clear X1. intro. subst p1. + generalize (transform_partial_program_identity _ _ _ _ X2). clear X2. intro. subst p2. apply transf_rtl_program_correct with p3; auto. - apply RTLgenproof.transf_program_correct with p2; auto. - rewrite <- P1. apply Selectionproof.transf_program_correct; auto. + apply RTLgenproof.transf_program_correct with (Selection.sel_program p); auto. + apply Selectionproof.transf_program_correct; auto. Qed. Theorem transf_c_program_correct: @@ -306,7 +306,7 @@ Proof. intros until beh; unfold transf_c_program; simpl. caseEq (Ctyping.typecheck_program p); try congruence; intro. caseEq (Cshmgen.transl_program p); simpl; try congruence; intros p1 EQ1. - caseEq (Cminorgen.transl_program p1); simpl; try congruence; intros p2 EQ2. + caseEq (Cminorgen.transl_program p1); simpl; try congruence; intros p2 EQ2. intros EQ3 NOTW SEM. eapply transf_cminor_program_correct; eauto. eapply Cminorgenproof.transl_program_correct; eauto. diff --git a/driver/Complements.v b/driver/Complements.v index 7389d291..3f32cc63 100644 --- a/driver/Complements.v +++ b/driver/Complements.v @@ -59,7 +59,14 @@ Proof. assert (i0 = i) by congruence. assert (rs'0 = rs') by congruence. assert (m'0 = m') by congruence. - subst. auto. + subst. auto. + replace i with (Pbuiltin ef args res) in H5 by congruence. simpl in H5. inv H5. + congruence. + replace i with (Pbuiltin ef args res) in H12 by congruence. simpl in H12. inv H12. + rewrite H2 in H7; inv H7. rewrite H3 in H8; inv H8. rewrite H4 in H9; inv H9. + exploit external_call_determ. eexact H5. eexact H12. auto. + intros [A [B C]]. subst. auto. + congruence. congruence. congruence. assert (ef0 = ef) by congruence. subst ef0. @@ -82,7 +89,8 @@ Lemma final_state_not_step: Proof. unfold nostep. intros. red; intros. inv H. inv H0. unfold Vzero in H1. congruence. - unfold Vzero in H1. congruence. + unfold Vzero in H1. congruence. + unfold Vzero in H1. congruence. Qed. Lemma final_state_deterministic: -- cgit