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

2 files changed, 21 insertions, 13 deletions

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: