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

4 files changed, 84 insertions, 83 deletions

diff --git a/common/AST.v b/common/AST.v
index 861795c..bca0535 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -82,6 +82,19 @@ Inductive memory_chunk : Type :=
   | Mfloat32 : memory_chunk        (**r 32-bit single-precision float *)
   | Mfloat64 : memory_chunk.       (**r 64-bit double-precision float *)
 
+(** The type (integer/pointer or float) of a chunk. *)
+
+Definition type_of_chunk (c: memory_chunk) : typ :=
+  match c with
+  | Mint8signed => Tint
+  | Mint8unsigned => Tint
+  | Mint16signed => Tint
+  | Mint16unsigned => Tint
+  | Mint32 => Tint
+  | Mfloat32 => Tfloat
+  | Mfloat64 => Tfloat
+  end.
+
 (** Initialization data for global variables. *)
 
 Inductive init_data: Type :=
@@ -390,9 +403,12 @@ Qed.
 
 Record external_function : Type := mkextfun {
   ef_id: ident;
-  ef_sig: signature
+  ef_sig: signature;
+  ef_inline: bool
 }.
 
+(** Function definitions are the union of internal and external functions. *)
+
 Inductive fundef (F: Type): Type :=
   | Internal: F -> fundef F
   | External: external_function -> fundef F.
diff --git a/common/Events.v b/common/Events.v
index 329f31c..a5c82d0 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -400,7 +400,7 @@ End EVENTVAL_INV.
 (** Each external function is of one of the following kinds: *)
 
 Inductive extfun_kind: signature -> Type :=
-  | EF_syscall (sg: signature) (name: ident): extfun_kind sg
+  | EF_syscall (name: ident) (sg: signature): extfun_kind sg
      (** A system call.  Takes integer-or-float arguments, produces a
          result that is an integer or a float, does not modify
          the memory, and produces an [Event_syscall] event in the trace. *)
@@ -985,7 +985,7 @@ This predicate is used in the semantics of all CompCert languages. *)
 
 Definition external_call (ef: external_function): extcall_sem :=
   match classify_external_function ef with
-  | EF_syscall sg name   => extcall_io_sem name sg
+  | EF_syscall name sg   => extcall_io_sem name sg
   | EF_vload chunk       => volatile_load_sem chunk
   | EF_vstore chunk      => volatile_store_sem chunk
   | EF_malloc            => extcall_malloc_sem 
@@ -994,7 +994,7 @@ Definition external_call (ef: external_function): extcall_sem :=
 
 Theorem external_call_spec:
   forall ef, 
-  extcall_properties (external_call ef) (ef.(ef_sig)).
+  extcall_properties (external_call ef) (ef_sig ef).
 Proof.
   intros. unfold external_call. destruct (classify_external_function ef). 
   apply extcall_io_ok.
diff --git a/common/Memdata.v b/common/Memdata.v
index 94a9917..20c0b10 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -103,19 +103,6 @@ Proof.
   destruct chunk1; destruct chunk2; simpl; congruence.
 Qed.
 
-(** The type (integer/pointer or float) of a chunk. *)
-
-Definition type_of_chunk (c: memory_chunk) : typ :=
-  match c with
-  | Mint8signed => Tint
-  | Mint8unsigned => Tint
-  | Mint16signed => Tint
-  | Mint16unsigned => Tint
-  | Mint32 => Tint
-  | Mfloat32 => Tfloat
-  | Mfloat64 => Tfloat
-  end.
-
 (** * Memory values *)
 
 (** A ``memory value'' is a byte-sized quantity that describes the current
diff --git a/common/Memory.v b/common/Memory.v
index 4d65c5c..1fb7816 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -80,9 +80,7 @@ Lemma mkmem_ext:
   mkmem cont1 acc1 bound1 next1 a1 b1 c1 d1 =
   mkmem cont2 acc2 bound2 next2 a2 b2 c2 d2.
 Proof.
-intros.
-subst.
-f_equal; apply proof_irr.
+  intros. subst. f_equal; apply proof_irr.
 Qed.
 
 (** * Validity of blocks and accesses *)
@@ -1699,78 +1697,78 @@ Hint Local Resolve valid_block_free_1 valid_block_free_2
 Lemma mem_access_ext:
   forall m1 m2, perm m1 = perm m2 -> mem_access m1 = mem_access m2.
 Proof.
-intros.
-apply extensionality; intro b.
-apply extensionality; intro ofs.
-case_eq (mem_access m1 b ofs); case_eq (mem_access m2 b ofs); intros; auto.
-assert (perm m1 b ofs p <-> perm m2 b ofs p) by (rewrite H; intuition).
-assert (perm m1 b ofs p0 <-> perm m2 b ofs p0) by (rewrite H; intuition).
-unfold perm, perm_order' in H2,H3.
-rewrite H0 in H2,H3; rewrite H1 in H2,H3.
-f_equal.
-assert (perm_order p p0 -> perm_order p0 p -> p0=p) by
-  (clear; intros; inv H; inv H0; auto).
-intuition.
-assert (perm m1 b ofs p <-> perm m2 b ofs p) by (rewrite H; intuition).
-unfold perm, perm_order' in H2; rewrite H0 in H2; rewrite H1 in H2.
-assert (perm_order p p) by auto with mem.
-intuition.
-assert (perm m1 b ofs p <-> perm m2 b ofs p) by (rewrite H; intuition).
-unfold perm, perm_order'  in H2; rewrite H0 in H2; rewrite H1 in H2.
-assert (perm_order p p) by auto with mem.
-intuition.
+  intros.
+  apply extensionality; intro b.
+  apply extensionality; intro ofs.
+  case_eq (mem_access m1 b ofs); case_eq (mem_access m2 b ofs); intros; auto.
+  assert (perm m1 b ofs p <-> perm m2 b ofs p) by (rewrite H; intuition).
+  assert (perm m1 b ofs p0 <-> perm m2 b ofs p0) by (rewrite H; intuition).
+  unfold perm, perm_order' in H2,H3.
+  rewrite H0 in H2,H3; rewrite H1 in H2,H3.
+  f_equal.
+  assert (perm_order p p0 -> perm_order p0 p -> p0=p) by
+    (clear; intros; inv H; inv H0; auto).
+  intuition.
+  assert (perm m1 b ofs p <-> perm m2 b ofs p) by (rewrite H; intuition).
+  unfold perm, perm_order' in H2; rewrite H0 in H2; rewrite H1 in H2.
+  assert (perm_order p p) by auto with mem.
+  intuition.
+  assert (perm m1 b ofs p <-> perm m2 b ofs p) by (rewrite H; intuition).
+  unfold perm, perm_order'  in H2; rewrite H0 in H2; rewrite H1 in H2.
+  assert (perm_order p p) by auto with mem.
+  intuition.
 Qed.
 
 Lemma mem_ext': 
   forall m1 m2, 
-       mem_access m1 = mem_access m2 ->
-       nextblock m1 = nextblock m2 ->
-       (forall b, 0 < b < nextblock m1 -> bounds m1 b = bounds m2 b) ->
-       (forall b ofs, perm_order' (mem_access m1 b ofs) Readable -> 
-                               mem_contents m1 b ofs = mem_contents m2 b ofs) ->
-       m1 = m2.
+  mem_access m1 = mem_access m2 ->
+  nextblock m1 = nextblock m2 ->
+  (forall b, 0 < b < nextblock m1 -> bounds m1 b = bounds m2 b) ->
+  (forall b ofs, perm_order' (mem_access m1 b ofs) Readable -> 
+                          mem_contents m1 b ofs = mem_contents m2 b ofs) ->
+  m1 = m2.
 Proof.
-intros.
-destruct m1; destruct m2; simpl in *.
-destruct H; subst.
-apply mkmem_ext; auto.
-apply extensionality; intro b.
-apply extensionality; intro ofs.
-destruct (perm_order'_dec (mem_access0 b ofs) Readable).
-auto.
-destruct (noread_undef0 b ofs); try contradiction.
-destruct (noread_undef1 b ofs); try contradiction.
-congruence.
-apply extensionality; intro b.
-destruct (nextblock_noaccess0 b); auto.
-destruct (nextblock_noaccess1 b); auto.
-congruence.
+  intros.
+  destruct m1; destruct m2; simpl in *.
+  destruct H; subst.
+  apply mkmem_ext; auto.
+  apply extensionality; intro b.
+  apply extensionality; intro ofs.
+  destruct (perm_order'_dec (mem_access0 b ofs) Readable).
+  auto.
+  destruct (noread_undef0 b ofs); try contradiction.
+  destruct (noread_undef1 b ofs); try contradiction.
+  congruence.
+  apply extensionality; intro b.
+  destruct (nextblock_noaccess0 b); auto.
+  destruct (nextblock_noaccess1 b); auto.
+  congruence.
 Qed.
 
 Theorem mem_ext:
-   forall m1 m2, 
-       perm m1 = perm m2 ->
-       nextblock m1 = nextblock m2 ->
-       (forall b, 0 < b < nextblock m1 -> bounds m1 b = bounds m2 b) ->
-       (forall b ofs, loadbytes m1 b ofs 1 = loadbytes m2 b ofs 1) ->
-       m1 = m2.
+  forall m1 m2, 
+  perm m1 = perm m2 ->
+  nextblock m1 = nextblock m2 ->
+  (forall b, 0 < b < nextblock m1 -> bounds m1 b = bounds m2 b) ->
+  (forall b ofs, loadbytes m1 b ofs 1 = loadbytes m2 b ofs 1) ->
+  m1 = m2.
 Proof.
-intros.
-generalize (mem_access_ext _ _ H); clear H; intro.
-apply mem_ext'; auto.
-intros.
-specialize (H2 b ofs).
-unfold loadbytes in H2; simpl in H2.
-destruct (range_perm_dec m1 b ofs (ofs+1)).
-destruct (range_perm_dec m2 b ofs (ofs+1)).
-inv H2; auto.
-contradict n.
-intros ofs' ?; assert (ofs'=ofs) by omega; subst ofs'.
-unfold perm, perm_order'.
-  rewrite <- H; destruct (mem_access m1 b ofs); try destruct p; intuition.
-contradict n.
-intros ofs' ?; assert (ofs'=ofs) by omega; subst ofs'.
-unfold perm. destruct (mem_access m1 b ofs); try destruct p; intuition.
+  intros.
+  generalize (mem_access_ext _ _ H); clear H; intro.
+  apply mem_ext'; auto.
+  intros.
+  specialize (H2 b ofs).
+  unfold loadbytes in H2; simpl in H2.
+  destruct (range_perm_dec m1 b ofs (ofs+1)).
+  destruct (range_perm_dec m2 b ofs (ofs+1)).
+  inv H2; auto.
+  contradict n.
+  intros ofs' ?; assert (ofs'=ofs) by omega; subst ofs'.
+  unfold perm, perm_order'.
+    rewrite <- H; destruct (mem_access m1 b ofs); try destruct p; intuition.
+  contradict n.
+  intros ofs' ?; assert (ofs'=ofs) by omega; subst ofs'.
+  unfold perm. destruct (mem_access m1 b ofs); try destruct p; intuition.
 Qed.
 
 (** * Generic injections *)