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, 12 insertions, 4 deletions

diff --git a/backend/LTL.v b/backend/LTL.v
index a44f3fa4..e1222a52 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -41,6 +41,7 @@ Inductive instruction: Type :=
   | Lstore: memory_chunk -> addressing -> list loc -> loc -> node -> instruction
   | Lcall: signature -> loc + ident -> list loc -> loc -> node -> instruction
   | Ltailcall: signature -> loc + ident -> list loc -> instruction
+  | Lbuiltin: external_function -> list loc -> loc -> node -> instruction
   | Lcond: condition -> list loc -> node -> node -> instruction
   | Ljumptable: loc -> list node -> instruction
   | Lreturn: option loc -> instruction.
@@ -61,8 +62,8 @@ Definition program := AST.program fundef unit.
 
 Definition funsig (fd: fundef) :=
   match fd with
-  | Internal f => f.(fn_sig)
-  | External ef => ef.(ef_sig)
+  | Internal f => fn_sig f
+  | External ef => ef_sig ef
   end.
 
 (** * Operational semantics *)
@@ -91,9 +92,9 @@ Definition postcall_locs (ls: locset) : locset :=
   fun (l: loc) =>
     match l with
     | R r =>
-        if In_dec Loc.eq (R r) Conventions.temporaries then
+        if In_dec Loc.eq (R r) temporaries then
           Vundef
-        else if In_dec Loc.eq (R r) Conventions.destroyed_at_call then
+        else if In_dec Loc.eq (R r) destroyed_at_call then
           Vundef
         else
           ls (R r)
@@ -196,6 +197,12 @@ Inductive step: state -> trace -> state -> Prop :=
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
       step (State s f (Vptr stk Int.zero) pc rs m)
         E0 (Callstate s f' (List.map rs args) m')
+  | exec_Lbuiltin:
+      forall s f sp pc rs m ef args res pc' t v m',
+      (fn_code f)!pc = Some(Lbuiltin ef args res pc') ->
+      external_call ef ge (map rs args) m t v m' ->
+      step (State s f sp pc rs m)
+         t (State s f sp pc' (Locmap.set res v rs) m')
   | exec_Lcond_true:
       forall s f sp pc rs m cond args ifso ifnot,
       (fn_code f)!pc = Some(Lcond cond args ifso ifnot) ->
@@ -272,6 +279,7 @@ Definition successors_instr (i: instruction) : list node :=
   | Lstore chunk addr args src s => s :: nil
   | Lcall sig ros args res s => s :: nil
   | Ltailcall sig ros args => nil
+  | Lbuiltin ef args res s => s :: nil
   | Lcond cond args ifso ifnot => ifso :: ifnot :: nil
   | Ljumptable arg tbl => tbl
   | Lreturn optarg => nil