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

1 files changed, 17 insertions, 1 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.