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

48 files changed, 574 insertions, 210 deletions

diff --git a/backend/Allocation.v b/backend/Allocation.v
index b802f4ac..69fb32fa 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -101,6 +101,8 @@ Definition transfer
            (reg_sum_live ros (reg_dead res after))
       | Itailcall sig ros args =>
 	  reg_list_live args (reg_sum_live ros Regset.empty)
+      | Ibuiltin ef args res s =>
+          reg_list_live args (reg_dead res after)
       | Icond cond args ifso ifnot =>
           reg_list_live args after
       | Ijumptable arg tbl =>
@@ -167,6 +169,8 @@ Definition transf_instr
                 (assign res) s
   | Itailcall sig ros args =>
       Ltailcall sig (sum_left_map assign ros) (List.map assign args)
+  | Ibuiltin ef args res s =>
+      Lbuiltin ef (List.map assign args) (assign res) s
   | Icond cond args ifso ifnot =>
       Lcond cond (List.map assign args) ifso ifnot
   | Ijumptable arg tbl =>
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index c5d6adc3..d06c26fa 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -330,7 +330,7 @@ Lemma agree_postcall:
   forall live args ros res rs v (ls: locset),
   (forall r,
     Regset.In r live -> r <> res ->
-    ~(In (assign r) Conventions.destroyed_at_call)) ->
+    ~(In (assign r) destroyed_at_call)) ->
   (forall r,
     Regset.In r live -> r <> res -> assign r <> assign res) ->
   agree (reg_list_live args (reg_sum_live ros (reg_dead res live))) rs ls ->
@@ -676,6 +676,19 @@ Proof.
   rewrite (sig_function_translated _ _ TF). eauto.
   rewrite H1. econstructor; eauto.
 
+  (* Ibuiltin *)
+  econstructor; split.
+  eapply exec_Lbuiltin; eauto. TranslInstr.
+  replace (map ls (@map reg loc assign args)) with (rs##args).
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
+  eapply agree_eval_regs; eauto.
+  generalize (regalloc_correct_1 f env live _ _ _ _ ASG H).
+  unfold correct_alloc_instr. intro CORR.
+  MatchStates. 
+  eapply agree_assign_live; eauto.
+  eapply agree_reg_list_live; eauto.
+
   (* Icond, true *)
   assert (COND: eval_condition cond (map ls (map assign args)) = Some true).
     replace (map ls (map assign args)) with (rs##args). auto.
diff --git a/backend/Alloctyping.v b/backend/Alloctyping.v
index 260297f2..a6536831 100644
--- a/backend/Alloctyping.v
+++ b/backend/Alloctyping.v
@@ -139,6 +139,8 @@ Proof.
   split. autorewrite with allocty; auto.
   split. auto with allocty. auto.
   rewrite transf_unroll; auto.
+  (* builtin *)
+  WT.
   (* cond *)
   WT.
   (* jumptable *)
diff --git a/backend/Bounds.v b/backend/Bounds.v
index 15468c57..514895be 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -72,6 +72,7 @@ Definition instr_within_bounds (i: instruction) :=
   | Lop op args res => mreg_within_bounds res
   | Lload chunk addr args dst => mreg_within_bounds dst
   | Lcall sig ros => size_arguments sig <= bound_outgoing b
+  | Lbuiltin ef args res => mreg_within_bounds res
   | _ => True
   end.
 
@@ -103,6 +104,7 @@ Definition regs_of_instr (i: instruction) : list mreg :=
   | Lstore chunk addr args src => nil
   | Lcall sig ros => nil
   | Ltailcall sig ros => nil
+  | Lbuiltin ef args res => res :: nil
   | Llabel lbl => nil
   | Lgoto lbl => nil
   | Lcond cond args lbl => nil
diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index 84202096..1cd245ec 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -352,9 +352,7 @@ proc:
                    fn_stackspace = $8;
                    fn_body = $10 }) }
   | EXTERN STRINGLIT COLON signature 
-      { Coq_pair($2,
-        External { ef_id = $2;
-                   ef_sig = $4 }) }
+      { Coq_pair($2, External({ef_id = $2; ef_sig = $4; ef_inline = false})) }
 ;
 
 signature:
diff --git a/backend/CSE.v b/backend/CSE.v
index ff79be54..dab8fc31 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -189,7 +189,7 @@ Definition add_load (n: numbering) (rd: reg)
 
 (** [add_unknown n rd] returns a numbering where [rd] is mapped to a
    fresh value number, and no equations are added.  This is useful
-   to model instructions with unpredictable results such as [Ialloc]. *)
+   to model instructions with unpredictable results such as [Ibuiltin]. *)
 
 Definition add_unknown (n: numbering) (rd: reg) :=
   mknumbering (Psucc n.(num_next))
@@ -348,6 +348,8 @@ Definition transfer (f: function) (pc: node) (before: numbering) :=
           empty_numbering
       | Itailcall sig ros args =>
           empty_numbering
+      | Ibuiltin ef args res s =>
+          add_unknown (kill_loads before) res
       | Icond cond args ifso ifnot =>
           before
       | Ijumptable arg tbl =>
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 445c1af9..c5670e8d 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -232,7 +232,7 @@ Proof.
   apply wf_kill_loads; auto.
   apply wf_empty_numbering.
   apply wf_empty_numbering.
-(*  apply wf_add_unknown; auto. *)
+  apply wf_add_unknown. apply wf_kill_loads; auto.
 Qed.
 
 (** As a consequence, the numberings computed by the static analysis
@@ -582,21 +582,16 @@ Proof.
 Qed.
 
 Lemma kill_load_satisfiable:
-  forall n rs chunk addr v m',
-  Mem.storev chunk m addr v = Some m' ->
+  forall n rs m',
   numbering_satisfiable ge sp rs m n ->
   numbering_satisfiable ge sp rs m' (kill_loads n).
 Proof.
-  intros. inversion H0. inversion H1.
-  generalize (kill_load_eqs_incl n.(num_eqs)). intro.
+  intros. inv H. destruct H0. generalize (kill_load_eqs_incl n.(num_eqs)). intro.
   exists x. split; intros.
-  generalize (H2 _ _ (H4 _ H5)). 
-  generalize (kill_load_eqs_ops _ _ _ H5).
-  destruct rh; simpl.
-  intros. destruct addr; simpl in H; try discriminate. 
-  auto.
-  tauto.
-  apply H3. assumption.
+  generalize (H _ _ (H1 _ H2)). 
+  generalize (kill_load_eqs_ops _ _ _ H2).
+  destruct rh; simpl; tauto.
+  apply H0. auto. 
 Qed.
 
 (** Correctness of [reg_valnum]: if it returns a register [r],
@@ -902,7 +897,18 @@ Proof.
   econstructor; split.
   eapply exec_Itailcall; eauto.
   apply sig_preserved. 
-  econstructor; eauto. 
+  econstructor; eauto.
+
+  (* Ibuiltin *)
+  econstructor; split.
+  eapply exec_Ibuiltin; eauto. 
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
+  econstructor; eauto.
+  eapply analysis_correct_1; eauto. simpl; auto.
+  unfold transfer; rewrite H. 
+  apply add_unknown_satisfiable. apply wf_kill_loads. apply wf_analyze.
+  eapply kill_load_satisfiable; eauto. 
 
   (* Icond true *)
   econstructor; split.
diff --git a/backend/Cminor.v b/backend/Cminor.v
index bdfb379a..4e57d3ce 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -133,8 +133,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 (small-step) *)
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index 1e87419f..29f7178e 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -70,6 +70,7 @@ Inductive stmt : Type :=
   | Sstore : memory_chunk -> addressing -> exprlist -> expr -> stmt
   | Scall : option ident -> signature -> expr -> exprlist -> stmt
   | Stailcall: signature -> expr -> exprlist -> stmt
+  | Sbuiltin : option ident -> external_function -> exprlist -> stmt
   | Sseq: stmt -> stmt -> stmt
   | Sifthenelse: condexpr -> stmt -> stmt -> stmt
   | Sloop: stmt -> stmt
@@ -93,8 +94,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 *)
@@ -297,6 +298,12 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m)
         E0 (Callstate fd vargs (call_cont k) m')
 
+  | step_builtin: forall f optid ef al k sp e m vl t v m',
+      eval_exprlist sp e m nil al vl ->
+      external_call ef ge vl m t v m' ->
+      step (State f (Sbuiltin optid ef al) k sp e m)
+         t (State f Sskip k sp (set_optvar optid v e) m')
+
   | step_seq: forall f s1 s2 k sp e m,
       step (State f (Sseq s1 s2) k sp e m)
         E0 (State f s1 (Kseq s2 k) sp e m)
diff --git a/backend/Coloring.v b/backend/Coloring.v
index 67824ae3..28626cba 100644
--- a/backend/Coloring.v
+++ b/backend/Coloring.v
@@ -183,6 +183,8 @@ Definition add_edges_instr
       let largs := loc_arguments sig in
       add_prefs_call args largs
         (add_interf_call ros largs g)
+  | Ibuiltin ef args res s =>
+      add_interf_op res live g
   | Ireturn (Some r) =>
       add_pref_mreg r (loc_result sig) g
   | _ => g
diff --git a/backend/Coloringaux.ml b/backend/Coloringaux.ml
index d17229ea..63f21906 100644
--- a/backend/Coloringaux.ml
+++ b/backend/Coloringaux.ml
@@ -22,6 +22,7 @@ open Locations
 open RTL
 open RTLtyping
 open InterfGraph
+open Conventions1
 open Conventions
 
 (* George-Appel graph coloring *)
@@ -202,13 +203,13 @@ let rec remove_reserved = function
 
 let init_regs() =
   caller_save_registers.(0) <-
-    Array.of_list (remove_reserved Conventions.int_caller_save_regs);
+    Array.of_list (remove_reserved int_caller_save_regs);
   caller_save_registers.(1) <-
-    Array.of_list (remove_reserved Conventions.float_caller_save_regs);
+    Array.of_list (remove_reserved float_caller_save_regs);
   callee_save_registers.(0) <-
-    Array.of_list (remove_reserved Conventions.int_callee_save_regs);
+    Array.of_list (remove_reserved int_callee_save_regs);
   callee_save_registers.(1) <-
-    Array.of_list (remove_reserved Conventions.float_callee_save_regs);
+    Array.of_list (remove_reserved float_callee_save_regs);
   for i = 0 to num_register_classes - 1 do
     num_available_registers.(i) <-
       Array.length caller_save_registers.(i)
@@ -789,6 +790,7 @@ let spill_costs f =
     | Istore(chunk, addr, args, src, _) -> incr_list args; incr src
     | Icall(sg, ros, args, res, _) -> incr_ros ros; incr_list args; incr res
     | Itailcall(sg, ros, args) -> incr_ros ros; incr_list args
+    | Ibuiltin(ef, args, res, _) -> incr_list args; incr res
     | Icond(cond, args, _, _) -> incr_list args
     | Ijumptable(arg, _) -> incr arg
     | Ireturn(Some r) -> incr r
diff --git a/backend/Coloringproof.v b/backend/Coloringproof.v
index 92ac0676..5f035b40 100644
--- a/backend/Coloringproof.v
+++ b/backend/Coloringproof.v
@@ -384,6 +384,7 @@ Proof.
   apply add_interf_destroyed_incl.
   eapply graph_incl_trans; [idtac|apply add_prefs_call_incl].
   apply add_interfs_call_incl.
+  apply add_interf_op_incl.
   destruct o.
   apply add_pref_mreg_incl.
   apply graph_incl_refl.
@@ -433,6 +434,10 @@ Definition correct_interf_instr
                                  interfere_mreg rfun mr g
         | inr idfun => True
       end
+  | Ibuiltin ef args res s =>
+      forall r,
+      Regset.In r live ->
+      r <> res -> interfere r res g
   | _ =>
       True
   end.
@@ -453,7 +458,8 @@ Proof.
   split. intros. eapply interfere_mreg_incl; eauto.
   split. intros. eapply interfere_incl; eauto.
   destruct s0; auto. intros. eapply interfere_mreg_incl; eauto. 
-  destruct s0; auto. intros. eapply interfere_mreg_incl; eauto. 
+  destruct s0; auto. intros. eapply interfere_mreg_incl; eauto.
+  intros. eapply interfere_incl; eauto. 
 Qed.
 
 Lemma add_edges_instr_correct:
@@ -500,38 +506,9 @@ Proof.
   eapply interfere_mreg_incl.
   apply add_prefs_call_incl.
   apply add_interfs_call_correct. auto.
-Qed.
-
-Lemma add_edges_instrs_incl_aux:
-  forall sig live instrs g,
-  graph_incl g
-    (fold_left
-       (fun (a : graph) (p : positive * instruction) =>
-          add_edges_instr sig (snd p) live !! (fst p) a)
-       instrs g).
-Proof.
-  induction instrs; simpl; intros.
-  apply graph_incl_refl.
-  eapply graph_incl_trans; [idtac|eauto].
-  apply add_edges_instr_incl.
-Qed.
 
-Lemma add_edges_instrs_correct_aux:
-  forall sig live instrs g pc i,
-  In (pc, i) instrs ->
-  correct_interf_instr live!!pc i
-    (fold_left
-       (fun (a : graph) (p : positive * instruction) =>
-          add_edges_instr sig (snd p) live !! (fst p) a)
-       instrs g).
-Proof.
-  induction instrs; simpl; intros.
-  elim H.
-  elim H; intro.
-  subst a; simpl. eapply correct_interf_instr_incl.
-  apply add_edges_instrs_incl_aux.
-  apply add_edges_instr_correct.
-  auto.
+  (* Ibuiltin *)
+  intros. apply add_interf_op_correct; auto. 
 Qed.
 
 Lemma add_edges_instrs_correct:
@@ -539,11 +516,20 @@ Lemma add_edges_instrs_correct:
   f.(fn_code)!pc = Some i ->
   correct_interf_instr live!!pc i (add_edges_instrs f live).
 Proof.
-  intros.
-  unfold add_edges_instrs.
-  rewrite PTree.fold_spec.
-  apply add_edges_instrs_correct_aux.
-  apply PTree.elements_correct. auto.
+  intros f live.
+  set (P := fun (c: code) g =>
+         forall pc i, c!pc = Some i -> correct_interf_instr live#pc i g).
+  set (F := (fun (g : graph) (pc0 : positive) (i0 : instruction) =>
+         add_edges_instr (fn_sig f) i0 live # pc0 g)).
+  change (P f.(fn_code) (PTree.fold F f.(fn_code) empty_graph)).
+  apply PTree_Properties.fold_rec; unfold P; intros.
+  apply H0. rewrite H. auto.
+  rewrite PTree.gempty in H. congruence.
+  rewrite PTree.gsspec in H2. destruct (peq pc k). 
+  inv H2. unfold F. apply add_edges_instr_correct. 
+  apply correct_interf_instr_incl with a. 
+  unfold F; apply add_edges_instr_incl.
+  apply H1; auto.
 Qed.
 
 (** Here are the three correctness properties of the generated
@@ -783,7 +769,7 @@ Definition correct_alloc_instr
       (forall r,
         Regset.In r live!!pc ->
         r <> res ->
-        ~(In (alloc r) Conventions.destroyed_at_call))
+        ~(In (alloc r) destroyed_at_call))
    /\ (forall r,
         Regset.In r live!!pc ->
         r <> res -> alloc r <> alloc res)
@@ -796,6 +782,10 @@ Definition correct_alloc_instr
         | inl rfun => ~(In (alloc rfun) (loc_arguments sig))
         | inr idfun => True
         end)
+  | Ibuiltin ef args res s =>
+      forall r,
+      Regset.In r live!!pc ->
+      r <> res -> alloc r <> alloc res
   | _ =>
       True
   end.
@@ -877,14 +867,14 @@ Proof.
   generalize (ALL2 _ _ H2). contradiction.
   split. auto.
   destruct s0; auto. red; intros.
-  generalize (ALL3 r0). generalize (Conventions.loc_arguments_acceptable _ _ H).
+  generalize (ALL3 r0). generalize (loc_arguments_acceptable _ _ H).
   unfold loc_argument_acceptable, loc_acceptable.
   caseEq (alloc r0). intros.
   elim (ALL2 r0 m). apply C; auto. congruence. auto. 
   destruct s0; auto.
   (* Itailcall *)
   destruct s0; auto. red; intros.
-  generalize (ALL3 r). generalize (Conventions.loc_arguments_acceptable _ _ H0).
+  generalize (ALL3 r). generalize (loc_arguments_acceptable _ _ H0).
   unfold loc_argument_acceptable, loc_acceptable.
   caseEq (alloc r). intros.
   elim (ALL2 r m). apply H; auto. congruence. auto. 
diff --git a/backend/Constprop.v b/backend/Constprop.v
index e1ab2e9c..03966cdd 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -128,6 +128,8 @@ Definition transfer (f: function) (pc: node) (before: D.t) :=
           D.set dst Unknown before
       | Icall sig ros args res s =>
           D.set res Unknown before
+      | Ibuiltin ef args res s =>
+          D.set res Unknown before
       | _ =>
           before
       end
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index 16f839fc..714468aa 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -355,6 +355,17 @@ Proof.
   eapply exec_Itailcall; eauto. apply sig_function_translated; auto.
   constructor; auto. 
 
+  (* Ibuiltin *)
+  TransfInstr. intro.
+  exists (State s' (transf_function f) sp pc' (rs#res <- v) m'); split.
+  eapply exec_Ibuiltin; eauto.
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
+  econstructor; eauto. 
+  eapply analyze_correct_1; eauto. simpl; auto. 
+  unfold transfer; rewrite H. 
+  apply regs_match_approx_update; auto. simpl; auto.
+
   (* Icond, true *)
   exists (State s' (transf_function f) sp ifso rs m); split. 
   caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args);
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
diff --git a/backend/LTLin.v b/backend/LTLin.v
index 806a7aa9..ee4cb943 100644
--- a/backend/LTLin.v
+++ b/backend/LTLin.v
@@ -47,6 +47,7 @@ Inductive instruction: Type :=
   | Lstore: memory_chunk -> addressing -> list loc -> loc -> instruction
   | Lcall: signature -> loc + ident -> list loc -> loc -> instruction
   | Ltailcall: signature -> loc + ident -> list loc -> instruction
+  | Lbuiltin: external_function -> list loc -> loc -> instruction
   | Llabel: label -> instruction
   | Lgoto: label -> instruction
   | Lcond: condition -> list loc -> label -> instruction
@@ -68,8 +69,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.
 
 Definition genv := Genv.t fundef unit.
@@ -186,6 +187,11 @@ Inductive step: state -> trace -> state -> Prop :=
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
       step (State s f (Vptr stk Int.zero) (Ltailcall sig ros args :: b) rs m)
         E0 (Callstate s f' (List.map rs args) m')
+  | exec_Lbuiltin:
+      forall s f sp rs m ef args res b t v m',
+      external_call ef ge (map rs args) m t v m' ->
+      step (State s f sp (Lbuiltin ef args res :: b) rs m)
+         t (State s f sp b (Locmap.set res v rs) m')
   | exec_Llabel:
       forall s f sp lbl b rs m,
       step (State s f sp (Llabel lbl :: b) rs m)
diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v
index 69422e0c..ad3ad644 100644
--- a/backend/LTLintyping.v
+++ b/backend/LTLintyping.v
@@ -67,8 +67,15 @@ Inductive wt_instr : instruction -> Prop :=
       LTLtyping.call_loc_acceptable sig ros ->
       locs_acceptable args -> 
       sig.(sig_res) = funsig.(sig_res) ->
-      Conventions.tailcall_possible sig ->
+      tailcall_possible sig ->
       wt_instr (Ltailcall sig ros args)
+  | wt_Lbuiltin:
+      forall ef args res,
+      List.map Loc.type args = (ef_sig ef).(sig_args) ->
+      Loc.type res = proj_sig_res (ef_sig ef) ->
+      arity_ok (ef_sig ef).(sig_args) = true ->
+      locs_acceptable args -> loc_acceptable res ->
+       wt_instr (Lbuiltin ef args res)
   | wt_Llabel: forall lbl,
       wt_instr (Llabel lbl)
   | wt_Lgoto: forall lbl,
diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v
index e1e43f56..7afae2db 100644
--- a/backend/LTLtyping.v
+++ b/backend/LTLtyping.v
@@ -88,8 +88,16 @@ Inductive wt_instr : instruction -> Prop :=
       call_loc_acceptable sig ros ->
       locs_acceptable args ->
       sig.(sig_res) = funct.(fn_sig).(sig_res) ->
-      Conventions.tailcall_possible sig ->
+      tailcall_possible sig ->
       wt_instr (Ltailcall sig ros args)
+  | wt_Lbuiltin:
+      forall ef args res s,
+      List.map Loc.type args = (ef_sig ef).(sig_args) ->
+      Loc.type res = proj_sig_res (ef_sig ef) ->
+      arity_ok (ef_sig ef).(sig_args) = true ->
+      locs_acceptable args -> loc_acceptable res ->
+      valid_successor s ->
+      wt_instr (Lbuiltin ef args res s)
   | wt_Lcond:
       forall cond args s1 s2,
       List.map Loc.type args = type_of_condition cond ->
diff --git a/backend/Linear.v b/backend/Linear.v
index 71310a97..0f44206d 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -43,6 +43,7 @@ Inductive instruction: Type :=
   | Lstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction
   | Lcall: signature -> mreg + ident -> instruction
   | Ltailcall: signature -> mreg + ident -> instruction
+  | Lbuiltin: external_function -> list mreg -> mreg -> instruction
   | Llabel: label -> instruction
   | Lgoto: label -> instruction
   | Lcond: condition -> list mreg -> label -> instruction
@@ -63,8 +64,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.
 
 Definition genv := Genv.t fundef unit.
@@ -153,9 +154,9 @@ Definition return_regs (caller callee: 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
           callee (R r)
-        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
           callee (R r)
         else
           caller (R r)
@@ -275,6 +276,11 @@ Inductive step: state -> trace -> state -> Prop :=
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
       step (State s f (Vptr stk Int.zero) (Ltailcall sig ros :: b) rs m)
         E0 (Callstate s f' (return_regs (parent_locset s) rs) m')
+  | exec_Lbuiltin:
+      forall s f sp rs m ef args res b t v m',
+      external_call ef ge (reglist rs args) m t v m' ->
+      step (State s f sp (Lbuiltin ef args res :: b) rs m)
+         t (State s f sp b (Locmap.set (R res) v rs) m')
   | exec_Llabel:
       forall s f sp lbl b rs m,
       step (State s f sp (Llabel lbl :: b) rs m)
@@ -315,8 +321,8 @@ Inductive step: state -> trace -> state -> Prop :=
   | exec_function_external:
       forall s ef args res rs1 rs2 m t m',
       external_call ef ge args m t res m' ->
-      args = List.map rs1 (Conventions.loc_arguments ef.(ef_sig)) ->
-      rs2 = Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs1 ->
+      args = List.map rs1 (loc_arguments (ef_sig ef)) ->
+      rs2 = Locmap.set (R (loc_result (ef_sig ef))) res rs1 ->
       step (Callstate s (External ef) rs1 m)
          t (Returnstate s rs2 m')
   | exec_return:
@@ -337,7 +343,7 @@ Inductive initial_state (p: program): state -> Prop :=
 
 Inductive final_state: state -> int -> Prop :=
   | final_state_intro: forall rs m r,
-      rs (R (Conventions.loc_result (mksignature nil (Some Tint)))) = Vint r ->
+      rs (R (loc_result (mksignature nil (Some Tint)))) = Vint r ->
       final_state (Returnstate nil rs m) r.
 
 Definition exec_program (p: program) (beh: program_behavior) : Prop :=
diff --git a/backend/Linearize.v b/backend/Linearize.v
index 31d0318c..fd350c71 100644
--- a/backend/Linearize.v
+++ b/backend/Linearize.v
@@ -185,6 +185,8 @@ Definition linearize_instr (b: LTL.instruction) (k: code) : code :=
       Lcall sig ros args res :: add_branch s k
   | LTL.Ltailcall sig ros args =>
       Ltailcall sig ros args :: k
+  | LTL.Lbuiltin ef args res s =>
+      Lbuiltin ef args res :: add_branch s k
   | LTL.Lcond cond args s1 s2 =>
       if starts_with s1 k then
         Lcond (negate_condition cond) args s2 :: add_branch s1 k
diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
index 1f4e5fac..ce7788f4 100644
--- a/backend/Linearizeaux.ml
+++ b/backend/Linearizeaux.ml
@@ -94,6 +94,7 @@ let basic_blocks f joins =
          | Lstore (chunk, addr, args, src, s) -> next_in_block blk minpc s
          | Lcall (sig0, ros, args, res, s) -> next_in_block blk minpc s
          | Ltailcall (sig0, ros, args) -> end_block blk minpc
+         | Lbuiltin (ef, args, res, s) -> next_in_block blk minpc s
          | Lcond (cond, args, ifso, ifnot) ->
              end_block blk minpc; start_block ifso; start_block ifnot
          | Ljumptable(arg, tbl) ->
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index 5f0a2a4e..df750008 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -612,6 +612,23 @@ Proof.
   destruct (Genv.find_symbol ge i); try discriminate.  
   eapply Genv.find_funct_ptr_prop; eauto.
 
+  (* Lbuiltin *)
+  destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
+  simpl in EQ. subst c.
+  assert (REACH': (reachable f)!!pc' = true).
+  eapply reachable_successors; eauto. simpl; auto.
+  exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].
+  econstructor; split.
+  eapply plus_left'.
+  eapply exec_Lbuiltin. 
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
+  eapply add_branch_correct; eauto.
+  eapply is_tail_add_branch. eapply is_tail_cons_left. 
+  eapply is_tail_find_label. eauto.
+  traceEq.
+  econstructor; eauto.
+
   (* Lcond true *)
   destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
   simpl in EQ. subst c.
diff --git a/backend/Linearizetyping.v b/backend/Linearizetyping.v
index 716b66f1..7393535d 100644
--- a/backend/Linearizetyping.v
+++ b/backend/Linearizetyping.v
@@ -55,6 +55,7 @@ Proof.
   apply wt_add_instr. constructor; auto. apply wt_add_branch; auto.
   apply wt_add_instr. constructor; auto. apply wt_add_branch; auto.
   apply wt_add_instr. constructor; auto. auto.
+  apply wt_add_instr. constructor; auto. apply wt_add_branch; auto.
   destruct (starts_with s1 k); apply wt_add_instr.
   constructor; auto. rewrite H. destruct cond; auto. 
   apply wt_add_branch; auto.
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 028e1200..4ea2ea95 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -87,6 +87,12 @@ Inductive wt_instr : instruction -> Prop :=
       tailcall_possible sig ->
       match ros with inl r => r = IT1 | _ => True end ->
       wt_instr (Ltailcall sig ros)
+  | wt_Lbuiltin:
+      forall ef args res,
+      List.map mreg_type args = (ef_sig ef).(sig_args) ->
+      mreg_type res = proj_sig_res (ef_sig ef) ->
+      arity_ok (ef_sig ef).(sig_args) = true ->
+      wt_instr (Lbuiltin ef args res)
   | wt_Llabel:
       forall lbl,
       wt_instr (Llabel lbl)
diff --git a/backend/Locations.v b/backend/Locations.v
index 295df281..c2fda9c2 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -173,6 +173,18 @@ Module Loc.
     destruct s; destruct s0; intuition auto.
   Qed.
 
+  Lemma diff_reg_right:
+    forall l r, l <> R r -> diff (R r) l.
+  Proof.
+    intros. simpl. destruct l. congruence. auto.
+  Qed.
+
+  Lemma diff_reg_left:
+    forall l r, l <> R r -> diff l (R r).
+  Proof.
+    intros. apply diff_sym. apply diff_reg_right. auto.
+  Qed.
+
 (** [Loc.overlap l1 l2] returns [false] if [l1] and [l2] are different and
   non-overlapping, and [true] otherwise: either [l1 = l2] or they partially 
   overlap. *)
@@ -290,6 +302,14 @@ Module Loc.
     auto.
   Qed.
 
+  Lemma reg_notin:
+    forall r ll, ~(In (R r) ll) -> notin (R r) ll.
+  Proof.
+    induction ll; simpl; intros. auto. 
+    split. destruct a; auto. intuition congruence.
+    apply IHll. intuition.
+  Qed.
+
 (** [Loc.disjoint l1 l2] is true if the locations in list [l1]
   are different from all locations in list [l2]. *)
 
@@ -352,6 +372,9 @@ Module Loc.
   | norepet_cons:
       forall hd tl, notin hd tl -> norepet tl -> norepet (hd :: tl).
 
+(** [Loc.no_overlap l1 l2] holds if elements of [l1] never overlap partially
+  with elements of [l2]. *)
+
   Definition no_overlap (l1 l2 : list loc) :=
    forall r, In r l1 -> forall s, In s l2 ->  r = s \/ Loc.diff r s.
 
diff --git a/backend/Mach.v b/backend/Mach.v
index e89ff3b1..2ec312e4 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -58,6 +58,7 @@ Inductive instruction: Type :=
   | Mstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction
   | Mcall: signature -> mreg + ident -> instruction
   | Mtailcall: signature -> mreg + ident -> instruction
+  | Mbuiltin: external_function -> list mreg -> mreg -> instruction
   | Mlabel: label -> instruction
   | Mgoto: label -> instruction
   | Mcond: condition -> list mreg -> label -> instruction
@@ -80,8 +81,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.
 
 Definition genv := Genv.t fundef unit.
diff --git a/backend/Machabstr.v b/backend/Machabstr.v
index 060c6c2b..291a4682 100644
--- a/backend/Machabstr.v
+++ b/backend/Machabstr.v
@@ -24,7 +24,7 @@ Require Import Globalenvs.
 Require Import Smallstep.
 Require Import Op.
 Require Import Locations.
-Require Conventions.
+Require Import Conventions.
 Require Import Mach.
 Require Stacklayout.
 
@@ -148,7 +148,7 @@ Inductive extcall_args: regset -> frame -> list loc -> list val -> Prop :=
 
 Definition extcall_arguments
    (rs: regset) (fr: frame) (sg: signature) (args: list val) : Prop :=
-  extcall_args rs fr (Conventions.loc_arguments sg) args.
+  extcall_args rs fr (loc_arguments sg) args.
     
 End FRAME_ACCESSES.
 
@@ -267,6 +267,11 @@ Inductive step: state -> trace -> state -> Prop :=
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
       step (State s f (Vptr stk soff) (Mtailcall sig ros :: c) rs fr m)
         E0 (Callstate s f' rs m')
+  | exec_Mbuiltin:
+      forall s f sp rs fr m ef args res b t v m',
+      external_call ef ge rs##args m t v m' ->
+      step (State s f sp (Mbuiltin ef args res :: b) rs fr m)
+         t (State s f sp b (rs#res <- v) fr m')
   | exec_Mgoto:
       forall s f sp lbl c rs fr m c',
       find_label lbl f.(fn_code) = Some c' ->
@@ -304,8 +309,8 @@ Inductive step: state -> trace -> state -> Prop :=
   | exec_function_external:
       forall s ef args res rs1 rs2 m t m',
       external_call ef ge args m t res m' ->
-      extcall_arguments (parent_function s) rs1 (parent_frame s) ef.(ef_sig) args ->
-      rs2 = (rs1#(Conventions.loc_result ef.(ef_sig)) <- res) ->
+      extcall_arguments (parent_function s) rs1 (parent_frame s) (ef_sig ef) args ->
+      rs2 = (rs1#(loc_result (ef_sig ef)) <- res) ->
       step (Callstate s (External ef) rs1 m)
          t (Returnstate s rs2 m')
   | exec_return:
@@ -325,7 +330,7 @@ Inductive initial_state (p: program): state -> Prop :=
 
 Inductive final_state: state -> int -> Prop :=
   | final_state_intro: forall rs m r,
-      rs (Conventions.loc_result (mksignature nil (Some Tint))) = Vint r ->
+      rs (loc_result (mksignature nil (Some Tint))) = Vint r ->
       final_state (Returnstate nil rs m) r.
 
 Definition exec_program (p: program) (beh: program_behavior) : Prop :=
diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v
index 125cd57a..1a97dda5 100644
--- a/backend/Machabstr2concr.v
+++ b/backend/Machabstr2concr.v
@@ -28,6 +28,7 @@ Require Import Mach.
 Require Import Machtyping.
 Require Import Machabstr.
 Require Import Machconcr.
+Require Import Conventions.
 Require Import Asmgenretaddr.
 
 (** Two semantics were defined for the Mach intermediate language:
@@ -911,7 +912,7 @@ Lemma transl_extcall_arguments:
   /\ Val.lessdef_list args targs.
 Proof.
   unfold Machabstr.extcall_arguments, extcall_arguments; intros.
-  generalize (Conventions.loc_arguments sg) args H.
+  generalize (loc_arguments sg) args H.
   induction l; intros; inv H2.
   exists (@nil val); split; constructor.
   exploit IHl; eauto. intros [targs [A B]].
@@ -1023,6 +1024,16 @@ Proof.
     eapply frame_match_load_retaddr; eauto. eapply match_stacks_parent_ra_pointer; eauto.
   econstructor; eauto. eapply match_stacks_free; eauto.
 
+  (* Mbuiltin *)
+  exploit external_call_mem_extends; eauto. eapply regset_lessdef_list; eauto. 
+  intros [v' [ms' [A [B [C D]]]]].
+  econstructor; split.
+  eapply exec_Mbuiltin. eauto. 
+  econstructor; eauto with coqlib.
+  eapply match_stacks_external_call; eauto. 
+  eapply frame_match_external_call; eauto. 
+  apply regset_lessdef_set; eauto.
+
   (* Mgoto *)
   econstructor; split.
   eapply exec_Mgoto; eauto.
@@ -1104,7 +1115,7 @@ Lemma equiv_final_states:
 Proof.
   intros. inv H0. destruct H. inv H. inv STACKS.
   constructor. 
-  generalize (RLD (Conventions.loc_result (mksignature nil (Some Tint)))).
+  generalize (RLD (loc_result (mksignature nil (Some Tint)))).
   rewrite H1. intro LD. inv LD. auto. 
 Qed.
 
diff --git a/backend/Machconcr.v b/backend/Machconcr.v
index 5b63fa8f..b736c8f7 100644
--- a/backend/Machconcr.v
+++ b/backend/Machconcr.v
@@ -23,7 +23,7 @@ Require Import Globalenvs.
 Require Import Smallstep.
 Require Import Op.
 Require Import Locations.
-Require Conventions.
+Require Import Conventions.
 Require Import Mach.
 Require Stacklayout.
 Require Asmgenretaddr.
@@ -82,7 +82,7 @@ Inductive extcall_args: regset -> mem -> val -> list loc -> list val -> Prop :=
 
 Definition extcall_arguments
    (rs: regset) (m: mem) (sp: val) (sg: signature) (args: list val) : Prop :=
-  extcall_args rs m sp (Conventions.loc_arguments sg) args.
+  extcall_args rs m sp (loc_arguments sg) args.
 
 (** Mach execution states. *)
 
@@ -187,6 +187,11 @@ Inductive step: state -> trace -> state -> Prop :=
       Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' ->
       step (State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs m)
         E0 (Callstate s f' rs m')
+  | exec_Mbuiltin:
+      forall s f sp rs m ef args res b t v m',
+      external_call ef ge rs##args m t v m' ->
+      step (State s f sp (Mbuiltin ef args res :: b) rs m)
+         t (State s f sp b (rs#res <- v) m')
   | exec_Mgoto:
       forall s fb f sp lbl c rs m c',
       Genv.find_funct_ptr ge fb = Some (Internal f) ->
@@ -234,8 +239,8 @@ Inductive step: state -> trace -> state -> Prop :=
       forall s fb rs m t rs' ef args res m',
       Genv.find_funct_ptr ge fb = Some (External ef) ->
       external_call ef ge args m t res m' ->
-      extcall_arguments rs m (parent_sp s) ef.(ef_sig) args ->
-      rs' = (rs#(Conventions.loc_result ef.(ef_sig)) <- res) ->
+      extcall_arguments rs m (parent_sp s) (ef_sig ef) args ->
+      rs' = (rs#(loc_result (ef_sig ef)) <- res) ->
       step (Callstate s fb rs m)
          t (Returnstate s rs' m')
   | exec_return:
@@ -254,7 +259,7 @@ Inductive initial_state (p: program): state -> Prop :=
 
 Inductive final_state: state -> int -> Prop :=
   | final_state_intro: forall rs m r,
-      rs (Conventions.loc_result (mksignature nil (Some Tint))) = Vint r ->
+      rs (loc_result (mksignature nil (Some Tint))) = Vint r ->
       final_state (Returnstate nil rs m) r.
 
 Definition exec_program (p: program) (beh: program_behavior) : Prop :=
diff --git a/backend/Machtyping.v b/backend/Machtyping.v
index b0673ca8..7013e296 100644
--- a/backend/Machtyping.v
+++ b/backend/Machtyping.v
@@ -23,7 +23,7 @@ Require Import Events.
 Require Import Globalenvs.
 Require Import Op.
 Require Import Locations.
-Require Conventions.
+Require Import Conventions.
 Require Import Mach.
 
 (** * Typing rules *)
@@ -69,9 +69,14 @@ Inductive wt_instr : instruction -> Prop :=
       wt_instr (Mcall sig ros)
   | wt_Mtailcall:
       forall sig ros,
-      Conventions.tailcall_possible sig ->
+      tailcall_possible sig ->
       match ros with inl r => mreg_type r = Tint | inr s => True end ->
       wt_instr (Mtailcall sig ros)
+  | wt_Mbuiltin:
+     forall ef args res,
+      List.map mreg_type args = (ef_sig ef).(sig_args) ->
+      mreg_type res = proj_sig_res (ef_sig ef) ->
+      wt_instr (Mbuiltin ef args res)
   | wt_Mgoto:
       forall lbl,
       wt_instr (Mgoto lbl)
@@ -273,7 +278,7 @@ Proof.
     apply (Genv.find_funct_ptr_prop wt_fundef _ _ wt_p H).
   econstructor; eauto.
 
-(*  apply wt_setreg; auto. exact I.  *)
+  inv H0. apply wt_setreg; auto. rewrite H5. eapply external_call_well_typed; eauto.  
 
   apply is_tail_find_label with lbl; congruence.
   apply is_tail_find_label with lbl; congruence. 
@@ -286,7 +291,7 @@ Proof.
 
   econstructor; eauto. apply wt_setreg; auto.
   generalize (external_call_well_typed _ _ _ _ _ _ _ H).  
-  unfold proj_sig_res, Conventions.loc_result.
+  unfold proj_sig_res, loc_result.
   destruct (sig_res (ef_sig ef)).
   destruct t0; simpl; auto.
   simpl; auto.
diff --git a/backend/RTL.v b/backend/RTL.v
index a17c74ee..1c309a0c 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -70,6 +70,10 @@ Inductive instruction: Type :=
   | Itailcall: signature -> reg + ident -> list reg -> instruction
       (** [Itailcall sig fn args] performs a function invocation
           in tail-call position.  *)
+  | Ibuiltin: external_function -> list reg -> reg -> node -> instruction
+      (** [Ibuiltin ef args dest succ] calls the built-in function
+          identified by [ef], giving it the values of [args] as arguments.
+          It stores the return value in [dest] and branches to [succ]. *)
   | Icond: condition -> list reg -> node -> node -> instruction
       (** [Icond cond args ifso ifnot] evaluates the boolean condition
           [cond] over the values of registers [args].  If the condition
@@ -109,8 +113,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 *)
@@ -245,6 +249,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 fd rs##args m')
+  | exec_Ibuiltin:
+      forall s f sp pc rs m ef args res pc' t v m',
+      (fn_code f)!pc = Some(Ibuiltin ef args res pc') ->
+      external_call ef ge rs##args m t v m' ->
+      step (State s f sp pc rs m)
+         t (State s f sp pc' (rs#res <- v) m')
   | exec_Icond_true:
       forall s f sp pc rs m cond args ifso ifnot,
       (fn_code f)!pc = Some(Icond cond args ifso ifnot) ->
@@ -351,6 +361,7 @@ Definition successors_instr (i: instruction) : list node :=
   | Istore chunk addr args src s => s :: nil
   | Icall sig ros args res s => s :: nil
   | Itailcall sig ros args => nil
+  | Ibuiltin ef args res s => s :: nil
   | Icond cond args ifso ifnot => ifso :: ifnot :: nil
   | Ijumptable arg tbl => tbl
   | Ireturn optarg => nil
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index ff4f81c5..aec2c867 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -546,6 +546,12 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
       do n1 <- add_instr (Itailcall sig (inl _ rf) rargs);
       do n2 <- transl_exprlist map cl rargs n1;
          transl_expr map b rf n2
+  | Sbuiltin optid ef al =>
+      do rargs <- alloc_regs map al;
+      do r <- new_reg;
+      do n1 <- store_optvar map r optid nd;
+      do n2 <- add_instr (Ibuiltin ef rargs r n1);
+      transl_exprlist map al rargs n2
   | Sseq s1 s2 =>
       do ns <- transl_stmt map s2 nd nexits ngoto nret rret;
       transl_stmt map s1 ns nexits ngoto nret rret
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index a96dfbfd..a1bd6618 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -1213,6 +1213,22 @@ Proof.
   rewrite H2; eauto.
   traceEq.
   rewrite G. constructor; auto.
+
+  (* builtin *)
+  inv TS. 
+  exploit transl_exprlist_correct; eauto.
+  intros [rs' [E [F [G J]]]].
+  exploit tr_store_optvar_correct. eauto. eauto.
+  apply match_env_update_temp. eexact F. eauto. 
+  intros [rs'' [A B]].
+  econstructor; split.
+  left. eapply star_plus_trans. eexact E. eapply plus_left.
+  eapply exec_Ibuiltin. eauto. rewrite G. 
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
+  eexact A. reflexivity. traceEq. 
+  econstructor; eauto. constructor. rewrite Regmap.gss in B. auto. 
+
   (* seq *)
   inv TS. 
   econstructor; split.
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 5690bb29..0b18a99b 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -816,6 +816,12 @@ Inductive tr_stmt (c: code) (map: mapping):
      tr_exprlist c map (rf :: nil) cl n1 n2 rargs ->
      c!n2 = Some (Itailcall sig (inl _ rf) rargs) ->
      tr_stmt c map (Stailcall sig b cl) ns nd nexits ngoto nret rret
+  | tr_Sbuiltin: forall optid ef al ns nd nexits ngoto nret rret rd n1 n2 rargs,
+     tr_exprlist c map nil al ns n1 rargs ->
+     c!n1 = Some (Ibuiltin ef rargs rd n2) ->
+     tr_store_optvar c map rd optid n2 nd ->
+     ~reg_in_map map rd ->
+     tr_stmt c map (Sbuiltin optid ef al) ns nd nexits ngoto nret rret
   | tr_Sseq: forall s1 s2 ns nd nexits ngoto nret rret n,
      tr_stmt c map s2 n nd nexits ngoto nret rret ->
      tr_stmt c map s1 ns n nexits ngoto nret rret ->
@@ -1228,6 +1234,11 @@ Proof.
   eapply transl_expr_charact; eauto 3 with rtlg.
   apply tr_exprlist_incr with s4; auto.
   eapply transl_exprlist_charact; eauto 4 with rtlg.
+  (* Sbuiltin *)
+  econstructor; eauto 4 with rtlg.
+  eapply transl_exprlist_charact; eauto 3 with rtlg.
+  apply tr_store_optvar_incr with s2; auto.
+  eapply store_optvar_charact; eauto with rtlg.
   (* Sseq *)
   econstructor. 
   apply tr_stmt_incr with s0; auto. 
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 68f38c0d..533c47a9 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -25,7 +25,7 @@ Require Import Integers.
 Require Import Events.
 Require Import Smallstep.
 Require Import RTL.
-Require Conventions.
+Require Import Conventions.
 
 (** * The type system *)
 
@@ -104,8 +104,15 @@ Inductive wt_instr : instruction -> Prop :=
       match ros with inl r => env r = Tint | inr s => True end ->
       sig.(sig_res) = funct.(fn_sig).(sig_res) ->
       List.map env args = sig.(sig_args) ->
-      Conventions.tailcall_possible sig ->
+      tailcall_possible sig ->
       wt_instr (Itailcall sig ros args)
+  | wt_Ibuiltin:
+      forall ef args res s,
+      List.map env args = (ef_sig ef).(sig_args) ->
+      env res = proj_sig_res (ef_sig ef) ->
+      arity_ok (ef_sig ef).(sig_args) = true ->
+      valid_successor s ->
+      wt_instr (Ibuiltin ef args res s)
   | wt_Icond:
       forall cond args s1 s2,
       List.map env args = type_of_condition cond ->
@@ -225,7 +232,12 @@ Definition check_instr (i: instruction) : bool :=
       match ros with inl r => check_reg r Tint | inr s => true end
       && check_regs args sig.(sig_args)
       && opt_typ_eq sig.(sig_res) funct.(fn_sig).(sig_res)
-      && Conventions.tailcall_is_possible sig
+      && tailcall_is_possible sig
+  | Ibuiltin ef args res s =>
+      check_regs args (ef_sig ef).(sig_args)
+      && check_reg res (proj_sig_res (ef_sig ef))
+      && arity_ok (ef_sig ef).(sig_args)
+      && check_successor s
   | Icond cond args s1 s2 =>
       check_regs args (type_of_condition cond)
       && check_successor s1
@@ -331,7 +343,13 @@ Proof.
   destruct s0; auto. apply check_reg_correct; auto.
   eapply proj_sumbool_true; eauto.
   apply check_regs_correct; auto.
-  apply Conventions.tailcall_is_possible_correct; auto.
+  apply tailcall_is_possible_correct; auto.
+  (* builtin *)
+  constructor.
+  apply check_regs_correct; auto.
+  apply check_reg_correct; auto.
+  auto.
+  apply check_successor_correct; auto.
   (* cond *)
   constructor. apply check_regs_correct; auto.
   apply check_successor_correct; auto.
@@ -541,6 +559,10 @@ Proof.
   econstructor; eauto.
   rewrite H6; auto.
   rewrite <- H7. apply wt_regset_list. auto.
+  (* Ibuiltin *)
+  econstructor; eauto.
+  apply wt_regset_assign. auto. 
+  rewrite H6. eapply external_call_well_typed; eauto. 
   (* Icond *)
   econstructor; eauto.
   econstructor; eauto.
diff --git a/backend/RTLtypingaux.ml b/backend/RTLtypingaux.ml
index 868fb8df..657c4daa 100644
--- a/backend/RTLtypingaux.ml
+++ b/backend/RTLtypingaux.ml
@@ -86,6 +86,17 @@ let type_instr retty (Coq_pair(pc, i)) =
         raise(Type_error (Printf.sprintf "type mismatch in Itailcall(%s): %s"
                                          name msg))
       end
+  | Ibuiltin(ef, args, res, _) ->
+      begin try
+        let sg = ef_sig ef in
+        set_types args sg.sig_args;
+        set_type res (match sg.sig_res with None -> Tint | Some ty -> ty);
+        if not (Conventions.arity_ok sg.sig_args) then
+          raise(Type_error "wrong arity")
+      with Type_error msg ->
+        raise(Type_error (Printf.sprintf "type mismatch in Ibuiltin(%s): %s"
+                                         (extern_atom ef.ef_id) msg))
+      end
   | Icond(cond, args, _, _) ->
       set_types args (type_of_condition cond)
   | Ijumptable(arg, _) ->
diff --git a/backend/Reload.v b/backend/Reload.v
index 5728a628..81b61998 100644
--- a/backend/Reload.v
+++ b/backend/Reload.v
@@ -235,6 +235,11 @@ Definition transf_instr
           parallel_move args largs
             (Ltailcall sig (inr _ id) :: k)
       end
+  | LTLin.Lbuiltin ef args dst =>
+      let rargs := regs_for args in
+      let rdst := reg_for dst in
+      add_reloads args rargs
+        (Lbuiltin ef rargs rdst :: add_spill rdst dst k)
   | LTLin.Llabel lbl =>
       Llabel lbl :: k
   | LTLin.Lgoto lbl =>
diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v
index 155f7b1b..286a266d 100644
--- a/backend/Reloadproof.v
+++ b/backend/Reloadproof.v
@@ -25,6 +25,7 @@ Require Import Op.
 Require Import Locations.
 Require Import Conventions.
 Require Import Allocproof.
+Require Import RTLtyping.
 Require Import LTLin.
 Require Import LTLintyping.
 Require Import Linear.
@@ -33,33 +34,10 @@ Require Import Reload.
 
 (** * Exploitation of the typing hypothesis *)
 
-(** Reloading is applied to LTLin code that is well-typed in
-  the sense of [LTLintyping]. We exploit this hypothesis to obtain information on
-  the number of temporaries required for reloading the arguments. *)
-
-Fixpoint temporaries_ok_rec (tys: list typ) (itmps ftmps: list mreg)
-                            {struct tys} : bool :=
-  match tys with
-  | nil => true
-  | Tint :: ts =>
-      match itmps with
-      | nil => false
-      | it1 :: its => temporaries_ok_rec ts its ftmps
-      end
-  | Tfloat :: ts =>
-      match ftmps with
-      | nil => false
-      | ft1 :: fts => temporaries_ok_rec ts itmps fts
-      end
-  end.
-
-Definition temporaries_ok (tys: list typ) :=
-  temporaries_ok_rec tys int_temporaries float_temporaries.
-
-Remark temporaries_ok_rec_incr_1:
+Remark arity_ok_rec_incr_1:
   forall tys it itmps ftmps,
-  temporaries_ok_rec tys itmps ftmps = true ->
-  temporaries_ok_rec tys (it :: itmps) ftmps = true.
+  arity_ok_rec tys itmps ftmps = true ->
+  arity_ok_rec tys (it :: itmps) ftmps = true.
 Proof.
   induction tys; intros until ftmps; simpl.
   tauto.
@@ -68,10 +46,10 @@ Proof.
   destruct ftmps. congruence. auto.
 Qed.
 
-Remark temporaries_ok_rec_incr_2:
+Remark arity_ok_rec_incr_2:
   forall tys ft itmps ftmps,
-  temporaries_ok_rec tys itmps ftmps = true ->
-  temporaries_ok_rec tys itmps (ft :: ftmps) = true.
+  arity_ok_rec tys itmps ftmps = true ->
+  arity_ok_rec tys itmps (ft :: ftmps) = true.
 Proof.
   induction tys; intros until ftmps; simpl.
   tauto.
@@ -80,37 +58,37 @@ Proof.
   destruct ftmps. congruence. auto.
 Qed.
 
-Remark temporaries_ok_rec_decr:
+Remark arity_ok_rec_decr:
   forall tys ty itmps ftmps,
-  temporaries_ok_rec (ty :: tys) itmps ftmps = true ->
-  temporaries_ok_rec tys itmps ftmps = true.
+  arity_ok_rec (ty :: tys) itmps ftmps = true ->
+  arity_ok_rec tys itmps ftmps = true.
 Proof.
   intros until ftmps. simpl. destruct ty. 
-  destruct itmps. congruence. intros. apply temporaries_ok_rec_incr_1; auto.
-  destruct ftmps. congruence. intros. apply temporaries_ok_rec_incr_2; auto.
+  destruct itmps. congruence. intros. apply arity_ok_rec_incr_1; auto.
+  destruct ftmps. congruence. intros. apply arity_ok_rec_incr_2; auto.
 Qed.
 
-Lemma temporaries_ok_enough_rec:
+Lemma arity_ok_enough_rec:
   forall locs itmps ftmps,
-  temporaries_ok_rec (List.map Loc.type locs) itmps ftmps = true ->
+  arity_ok_rec (List.map Loc.type locs) itmps ftmps = true ->
   enough_temporaries_rec locs itmps ftmps = true.
 Proof.
   induction locs; intros until ftmps.
   simpl. auto.
   simpl enough_temporaries_rec. simpl map. 
-  destruct a. intros. apply IHlocs. eapply temporaries_ok_rec_decr; eauto. 
+  destruct a. intros. apply IHlocs. eapply arity_ok_rec_decr; eauto. 
   simpl. destruct (slot_type s). 
   destruct itmps; auto.
   destruct ftmps; auto.
 Qed.
 
-Lemma temporaries_ok_enough:
+Lemma arity_ok_enough:
   forall locs,
-  temporaries_ok (List.map Loc.type locs) = true ->
+  arity_ok (List.map Loc.type locs) = true ->
   enough_temporaries locs = true.
 Proof.
-  unfold temporaries_ok, enough_temporaries. intros. 
-  apply temporaries_ok_enough_rec; auto.
+  unfold arity_ok, enough_temporaries. intros. 
+  apply arity_ok_enough_rec; auto.
 Qed.
 
 Lemma enough_temporaries_op_args:
@@ -118,7 +96,7 @@ Lemma enough_temporaries_op_args:
   (List.map Loc.type args, Loc.type res) = type_of_operation op ->
   enough_temporaries args = true.
 Proof.
-  intros. apply temporaries_ok_enough.
+  intros. apply arity_ok_enough.
   replace (map Loc.type args) with (fst (type_of_operation op)).
   destruct op; try (destruct c); compute; reflexivity.
   rewrite <- H. auto.
@@ -129,7 +107,7 @@ Lemma enough_temporaries_cond:
   List.map Loc.type args = type_of_condition cond ->
   enough_temporaries args = true.
 Proof.
-  intros. apply temporaries_ok_enough. rewrite H.
+  intros. apply arity_ok_enough. rewrite H.
   destruct cond; compute; reflexivity.
 Qed.
 
@@ -138,15 +116,15 @@ Lemma enough_temporaries_addr:
   List.map Loc.type args = type_of_addressing addr ->
   enough_temporaries args = true.
 Proof.
-  intros. apply temporaries_ok_enough. rewrite H. 
+  intros. apply arity_ok_enough. rewrite H. 
   destruct addr; compute; reflexivity.
 Qed.
 
-Lemma temporaries_ok_rec_length:
+Lemma arity_ok_rec_length:
   forall tys itmps ftmps,
   (length tys <= length itmps)%nat ->
   (length tys <= length ftmps)%nat ->
-  temporaries_ok_rec tys itmps ftmps = true.
+  arity_ok_rec tys itmps ftmps = true.
 Proof.
   induction tys; intros until ftmps; simpl.
   auto.
@@ -159,8 +137,8 @@ Lemma enough_temporaries_length:
   forall args,
   (length args <= 2)%nat -> enough_temporaries args = true.
 Proof.
-  intros. apply temporaries_ok_enough. unfold temporaries_ok.
-  apply temporaries_ok_rec_length. 
+  intros. apply arity_ok_enough. unfold arity_ok.
+  apply arity_ok_rec_length. 
   rewrite list_length_map. simpl. omega.
   rewrite list_length_map. simpl. omega.
 Qed.
@@ -690,7 +668,7 @@ Proof.
   intros. unfold return_regs. 
   destruct (In_dec Loc.eq (R (loc_result sig)) temporaries). auto.
   destruct (In_dec Loc.eq (R (loc_result sig)) destroyed_at_call). auto.
-  elim n0. apply loc_result_caller_save.
+  generalize (loc_result_caller_save sig). tauto.
 Qed.
 
 (** * Preservation of labels and gotos *)
@@ -885,7 +863,7 @@ Inductive match_states: LTLin.state -> Linear.state -> Prop :=
   | match_states_call:
       forall s f args m s' ls tm
         (STACKS: match_stackframes s s' (LTLin.funsig f))
-        (AG: Val.lessdef_list args (map ls (Conventions.loc_arguments (LTLin.funsig f))))
+        (AG: Val.lessdef_list args (map ls (loc_arguments (LTLin.funsig f))))
         (PRES: forall l, ~In l temporaries -> ~In l destroyed_at_call ->
                  ls l = parent_locset s' l)
         (WT: wt_fundef f)
@@ -895,7 +873,7 @@ Inductive match_states: LTLin.state -> Linear.state -> Prop :=
   | match_states_return:
       forall s res m s' ls tm sig
         (STACKS: match_stackframes s s' sig)
-        (AG: Val.lessdef res (ls (R (Conventions.loc_result sig))))
+        (AG: Val.lessdef res (ls (R (loc_result sig))))
         (PRES: forall l, ~In l temporaries -> ~In l destroyed_at_call ->
                  ls l = parent_locset s' l)
         (MMD: Mem.extends m tm),
@@ -1216,6 +1194,29 @@ Proof.
   rewrite return_regs_arguments; auto. congruence.
   exact (return_regs_preserve (parent_locset s') ls3).
 
+  (* Lbuiltin *)
+  ExploitWT; inv WTI.
+  exploit add_reloads_correct.
+    instantiate (1 := args). apply arity_ok_enough. rewrite H3. auto.
+    apply locs_acceptable_disj_temporaries; auto.
+  intros [ls2 [A [B C]]].
+  exploit external_call_mem_extends; eauto. 
+  apply agree_locs; eauto. 
+  intros [v' [tm' [P [Q [R S]]]]].
+  exploit add_spill_correct.
+  intros [ls3 [D [E F]]].
+  left; econstructor; split.
+  eapply star_plus_trans. eauto. 
+  eapply plus_left. eapply exec_Lbuiltin. rewrite B. 
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
+  eauto. reflexivity. traceEq. 
+  econstructor; eauto with coqlib.
+  apply agree_set with ls; auto.
+  rewrite E. rewrite Locmap.gss. auto.
+  intros. rewrite F; auto. rewrite Locmap.gso. auto. 
+  apply reg_for_diff; auto.
+
   (* Llabel *)
   left; econstructor; split.
   apply plus_one. apply exec_Llabel.
@@ -1319,7 +1320,8 @@ Proof.
   econstructor; eauto.
   simpl. rewrite Locmap.gss. auto.
   intros. rewrite Locmap.gso. auto. 
-  simpl. destruct l; auto. red; intro. elim H1. subst m0. apply loc_result_caller_save.
+  simpl. destruct l; auto. red; intro. elim H1. subst m0. 
+  generalize (loc_result_caller_save (ef_sig ef)). tauto.
 
   (* return *)
   inv STACKS. 
diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v
index df0715ee..1bb462dc 100644
--- a/backend/Reloadtyping.v
+++ b/backend/Reloadtyping.v
@@ -34,7 +34,7 @@ Require Import Reloadproof.
   given sufficient typing and well-formedness hypotheses over the locations involved. *)
 
 Hint Resolve wt_Lgetstack wt_Lsetstack wt_Lopmove
-             wt_Lop wt_Lload wt_Lstore wt_Lcall wt_Ltailcall
+             wt_Lop wt_Lload wt_Lstore wt_Lcall wt_Ltailcall wt_Lbuiltin
              wt_Llabel wt_Lgoto wt_Lcond wt_Ljumptable wt_Lreturn: reloadty.
 
 Remark wt_code_cons:
@@ -292,6 +292,13 @@ Proof.
   auto 10 with reloadty.
 
   assert (map mreg_type (regs_for args) = map Loc.type args).
+    apply wt_regs_for. apply arity_ok_enough. congruence.
+  assert (mreg_type (reg_for res) = Loc.type res). eauto with reloadty.
+  auto with reloadty.
+
+
+
+  assert (map mreg_type (regs_for args) = map Loc.type args).
     eauto with reloadty.
   auto with reloadty.
 
diff --git a/backend/Selection.v b/backend/Selection.v
index e822fdf7..ebdad8a2 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -167,46 +167,73 @@ Fixpoint sel_exprlist (al: list Cminor.expr) : exprlist :=
   | a :: bl => Econs (sel_expr a) (sel_exprlist bl)
   end.
 
+(** Recognition of calls to built-in functions that should be inlined *)
+
+Definition expr_is_addrof_ident (e: Cminor.expr) : option ident :=
+  match e with
+  | Cminor.Econst (Cminor.Oaddrsymbol id ofs) =>
+      if Int.eq ofs Int.zero then Some id else None
+  | _ => None
+  end.
+
+Definition expr_is_addrof_builtin (ge: Cminor.genv) (e: Cminor.expr) : option external_function :=
+  match expr_is_addrof_ident e with
+  | None => None
+  | Some id =>
+      match Genv.find_symbol ge id with
+      | None => None
+      | Some b =>
+          match Genv.find_funct_ptr ge b with
+          | Some(External ef) => if ef.(ef_inline) then Some ef else None
+          | _ => None
+          end
+      end
+  end.
+
 (** Conversion from Cminor statements to Cminorsel statements. *)
 
-Fixpoint sel_stmt (s: Cminor.stmt) : stmt :=
+Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : stmt :=
   match s with
   | Cminor.Sskip => Sskip
   | Cminor.Sassign id e => Sassign id (sel_expr e)
   | Cminor.Sstore chunk addr rhs => store chunk (sel_expr addr) (sel_expr rhs)
   | Cminor.Scall optid sg fn args =>
-      Scall optid sg (sel_expr fn) (sel_exprlist args)
+      match expr_is_addrof_builtin ge fn with
+      | None => Scall optid sg (sel_expr fn) (sel_exprlist args)
+      | Some ef => Sbuiltin optid ef (sel_exprlist args)
+      end
   | Cminor.Stailcall sg fn args => 
       Stailcall sg (sel_expr fn) (sel_exprlist args)
-  | Cminor.Sseq s1 s2 => Sseq (sel_stmt s1) (sel_stmt s2)
+  | Cminor.Sseq s1 s2 => Sseq (sel_stmt ge s1) (sel_stmt ge s2)
   | Cminor.Sifthenelse e ifso ifnot =>
       Sifthenelse (condexpr_of_expr (sel_expr e))
-                  (sel_stmt ifso) (sel_stmt ifnot)
-  | Cminor.Sloop body => Sloop (sel_stmt body)
-  | Cminor.Sblock body => Sblock (sel_stmt body)
+                  (sel_stmt ge ifso) (sel_stmt ge ifnot)
+  | Cminor.Sloop body => Sloop (sel_stmt ge body)
+  | Cminor.Sblock body => Sblock (sel_stmt ge body)
   | Cminor.Sexit n => Sexit n
   | Cminor.Sswitch e cases dfl => Sswitch (sel_expr e) cases dfl
   | Cminor.Sreturn None => Sreturn None
   | Cminor.Sreturn (Some e) => Sreturn (Some (sel_expr e))
-  | Cminor.Slabel lbl body => Slabel lbl (sel_stmt body)
+  | Cminor.Slabel lbl body => Slabel lbl (sel_stmt ge body)
   | Cminor.Sgoto lbl => Sgoto lbl
   end.
 
 (** Conversion of functions and programs. *)
 
-Definition sel_function (f: Cminor.function) : function :=
+Definition sel_function (ge: Cminor.genv) (f: Cminor.function) : function :=
   mkfunction
     f.(Cminor.fn_sig)
     f.(Cminor.fn_params)
     f.(Cminor.fn_vars)
     f.(Cminor.fn_stackspace)
-    (sel_stmt f.(Cminor.fn_body)).
+    (sel_stmt ge f.(Cminor.fn_body)).
 
-Definition sel_fundef (f: Cminor.fundef) : fundef :=
-  transf_fundef sel_function f.
+Definition sel_fundef (ge: Cminor.genv) (f: Cminor.fundef) : fundef :=
+  transf_fundef (sel_function ge) f.
 
 Definition sel_program (p: Cminor.program) : program :=
-  transform_program sel_fundef p.
+  let ge := Genv.globalenv p in
+  transform_program (sel_fundef ge) p.
 
 
 
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index e03085a9..cb9f4fc5 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -275,6 +275,36 @@ Qed.
 
 End CMCONSTR.
 
+(** Recognition of calls to built-in functions *)
+
+Lemma expr_is_addrof_ident_correct:
+  forall e id,
+  expr_is_addrof_ident e = Some id ->
+  e = Cminor.Econst (Cminor.Oaddrsymbol id Int.zero).
+Proof.
+  intros e id. unfold expr_is_addrof_ident. 
+  destruct e; try congruence.
+  destruct c; try congruence.
+  predSpec Int.eq Int.eq_spec i0 Int.zero; congruence.
+Qed.
+
+Lemma expr_is_addrof_builtin_correct:
+  forall ge sp e m a v ef fd,
+  expr_is_addrof_builtin ge a = Some ef ->
+  Cminor.eval_expr ge sp e m a v ->
+  Genv.find_funct ge v = Some fd ->
+  fd = External ef.
+Proof.
+  intros until fd; unfold expr_is_addrof_builtin.
+  case_eq (expr_is_addrof_ident a); intros; try congruence.
+  exploit expr_is_addrof_ident_correct; eauto. intro EQ; subst a.
+  inv H1. inv H4. 
+  destruct (Genv.find_symbol ge i); try congruence.
+  inv H3. rewrite Genv.find_funct_find_funct_ptr in H2. rewrite H2 in H0. 
+  destruct fd; try congruence. 
+  destruct (ef_inline e0); congruence.
+Qed.
+
 (** * Semantic preservation for instruction selection. *)
 
 Section PRESERVATION.
@@ -297,24 +327,24 @@ Qed.
 Lemma functions_translated:
   forall (v: val) (f: Cminor.fundef),
   Genv.find_funct ge v = Some f ->
-  Genv.find_funct tge v = Some (sel_fundef f).
+  Genv.find_funct tge v = Some (sel_fundef ge f).
 Proof.  
   intros.
-  exact (Genv.find_funct_transf sel_fundef _ _ H).
+  exact (Genv.find_funct_transf (sel_fundef ge) _ _ H).
 Qed.
 
 Lemma function_ptr_translated:
   forall (b: block) (f: Cminor.fundef),
   Genv.find_funct_ptr ge b = Some f ->
-  Genv.find_funct_ptr tge b = Some (sel_fundef f).
+  Genv.find_funct_ptr tge b = Some (sel_fundef ge f).
 Proof.  
   intros. 
-  exact (Genv.find_funct_ptr_transf sel_fundef _ _ H).
+  exact (Genv.find_funct_ptr_transf (sel_fundef ge) _ _ H).
 Qed.
 
 Lemma sig_function_translated:
   forall f,
-  funsig (sel_fundef f) = Cminor.funsig f.
+  funsig (sel_fundef ge f) = Cminor.funsig f.
 Proof.
   intros. destruct f; reflexivity.
 Qed.
@@ -369,29 +399,40 @@ Hint Resolve sel_exprlist_correct: evalexpr.
 Fixpoint sel_cont (k: Cminor.cont) : CminorSel.cont :=
   match k with
   | Cminor.Kstop => Kstop
-  | Cminor.Kseq s1 k1 => Kseq (sel_stmt s1) (sel_cont k1)
+  | Cminor.Kseq s1 k1 => Kseq (sel_stmt ge s1) (sel_cont k1)
   | Cminor.Kblock k1 => Kblock (sel_cont k1)
   | Cminor.Kcall id f sp e k1 =>
-      Kcall id (sel_function f) sp e (sel_cont k1)
+      Kcall id (sel_function ge f) sp e (sel_cont k1)
   end.
 
 Inductive match_states: Cminor.state -> CminorSel.state -> Prop :=
   | match_state: forall f s k s' k' sp e m,
-      s' = sel_stmt s ->
+      s' = sel_stmt ge s ->
       k' = sel_cont k ->
       match_states
         (Cminor.State f s k sp e m)
-        (State (sel_function f) s' k' sp e m)
+        (State (sel_function ge f) s' k' sp e m)
   | match_callstate: forall f args k k' m,
       k' = sel_cont k ->
       match_states
         (Cminor.Callstate f args k m)
-        (Callstate (sel_fundef f) args k' m)
+        (Callstate (sel_fundef ge f) args k' m)
   | match_returnstate: forall v k k' m,
       k' = sel_cont k ->
       match_states
         (Cminor.Returnstate v k m)
-        (Returnstate v k' m).
+        (Returnstate v k' m)
+  | match_builtin_1: forall ef args optid f sp e k m al k',
+      k' = sel_cont k ->
+      eval_exprlist tge sp e m nil al args ->
+      match_states
+        (Cminor.Callstate (External ef) args (Cminor.Kcall optid f sp e k) m)
+        (State (sel_function ge f) (Sbuiltin optid ef al) k' sp e m)
+  | match_builtin_2: forall v optid f sp e k m k',
+      k' = sel_cont k ->
+      match_states
+        (Cminor.Returnstate v (Cminor.Kcall optid f sp e k) m)
+        (State (sel_function ge f) Sskip k' sp (set_optvar optid v e) m).
 
 Remark call_cont_commut:
   forall k, call_cont (sel_cont k) = sel_cont (Cminor.call_cont k).
@@ -401,19 +442,20 @@ Qed.
 
 Remark find_label_commut:
   forall lbl s k,
-  find_label lbl (sel_stmt s) (sel_cont k) =
-  option_map (fun sk => (sel_stmt (fst sk), sel_cont (snd sk)))
+  find_label lbl (sel_stmt ge s) (sel_cont k) =
+  option_map (fun sk => (sel_stmt ge (fst sk), sel_cont (snd sk)))
              (Cminor.find_label lbl s k).
 Proof.
   induction s; intros; simpl; auto.
   unfold store. destruct (addressing m (sel_expr e)); auto.
-  change (Kseq (sel_stmt s2) (sel_cont k))
+  destruct (expr_is_addrof_builtin ge e); auto.
+  change (Kseq (sel_stmt ge s2) (sel_cont k))
     with (sel_cont (Cminor.Kseq s2 k)).
   rewrite IHs1. rewrite IHs2. 
   destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)); auto.
   rewrite IHs1. rewrite IHs2. 
   destruct (Cminor.find_label lbl s1 k); auto.
-  change (Kseq (Sloop (sel_stmt s)) (sel_cont k))
+  change (Kseq (Sloop (sel_stmt ge s)) (sel_cont k))
     with (sel_cont (Cminor.Kseq (Cminor.Sloop s) k)).
   auto.
   change (Kblock (sel_cont k))
@@ -423,64 +465,79 @@ Proof.
   destruct (ident_eq lbl l); auto.
 Qed.
 
+Definition measure (s: Cminor.state) : nat :=
+  match s with
+  | Cminor.Callstate _ _ _ _ => 0%nat
+  | Cminor.State _ _ _ _ _ _ => 1%nat
+  | Cminor.Returnstate _ _ _ => 2%nat
+  end.
+
 Lemma sel_step_correct:
   forall S1 t S2, Cminor.step ge S1 t S2 ->
   forall T1, match_states S1 T1 ->
-  exists T2, step tge T1 t T2 /\ match_states S2 T2.
+  (exists T2, step tge T1 t T2 /\ match_states S2 T2)
+  \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 T1)%nat.
 Proof.
   induction 1; intros T1 ME; inv ME; simpl;
-  try (econstructor; split; [econstructor; eauto with evalexpr | econstructor; eauto]; fail).
+  try (left; econstructor; split; [econstructor; eauto with evalexpr | econstructor; eauto]; fail).
 
   (* skip call *)
-  econstructor; split. 
+  left; econstructor; split. 
   econstructor. destruct k; simpl in H; simpl; auto. 
   rewrite <- H0; reflexivity.
   simpl. eauto. 
   constructor; auto.
-(*
-  (* assign *)
-  exists (State (sel_function f) Sskip (sel_cont k) sp (PTree.set id v e) m); split.
-  constructor. auto with evalexpr.
-  constructor; auto.
-*)
   (* store *)
-  econstructor; split.
+  left; econstructor; split.
   eapply eval_store; eauto with evalexpr.
   constructor; auto.
   (* Scall *)
-  econstructor; split.
+  case_eq (expr_is_addrof_builtin ge a).
+  (* Scall turned into Sbuiltin *)
+  intros ef EQ. exploit expr_is_addrof_builtin_correct; eauto. intro EQ1. subst fd.
+  right; split. omega. split. auto. 
+  econstructor; eauto with evalexpr.
+  (* Scall preserved *)
+  intro EQ. left; econstructor; split.
   econstructor; eauto with evalexpr.
   apply functions_translated; eauto. 
   apply sig_function_translated.
   constructor; auto.
   (* Stailcall *)
-  econstructor; split.
+  left; econstructor; split.
   econstructor; eauto with evalexpr.
   apply functions_translated; eauto. 
   apply sig_function_translated.
   constructor; auto. apply call_cont_commut.
   (* Sifthenelse *)
-  exists (State (sel_function f) (if b then sel_stmt s1 else sel_stmt s2) (sel_cont k) sp e m); split.
+  left; exists (State (sel_function ge f) (if b then sel_stmt ge s1 else sel_stmt ge s2) (sel_cont k) sp e m); split.
   constructor. eapply eval_condition_of_expr; eauto with evalexpr.
   constructor; auto. destruct b; auto.
   (* Sreturn None *)
-  econstructor; split. 
+  left; econstructor; split. 
   econstructor. simpl; eauto. 
   constructor; auto. apply call_cont_commut.
   (* Sreturn Some *)
-  econstructor; split. 
+  left; econstructor; split. 
   econstructor. simpl. eauto with evalexpr. simpl; eauto.
   constructor; auto. apply call_cont_commut.
   (* Sgoto *)
-  econstructor; split.
+  left; econstructor; split.
   econstructor. simpl. rewrite call_cont_commut. rewrite find_label_commut.
   rewrite H. simpl. reflexivity. 
   constructor; auto.
   (* external call *)
-  econstructor; split.
+  left; econstructor; split.
   econstructor. eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
   constructor; auto.
+  (* external call turned into a Sbuiltin *)
+  left; econstructor; split.
+  econstructor. eauto. eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
+  constructor; auto.
+  (* return of an external call turned into a Sbuiltin *)
+  right; split. omega. split. auto. constructor; auto.
 Qed.
 
 Lemma sel_initial_states:
@@ -509,10 +566,10 @@ Theorem transf_program_correct:
   Cminor.exec_program prog beh -> CminorSel.exec_program tprog beh.
 Proof.
   unfold CminorSel.exec_program, Cminor.exec_program; intros.
-  eapply simulation_step_preservation; eauto.
+  eapply simulation_opt_preservation; eauto.
   eexact sel_initial_states.
   eexact sel_final_states.
-  exact sel_step_correct. 
+  eexact sel_step_correct. 
 Qed.
 
 End PRESERVATION.
diff --git a/backend/Stacking.v b/backend/Stacking.v
index 5d9cf374..f289793e 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -179,6 +179,8 @@ Definition transl_instr
   | Ltailcall sig ros =>
       restore_callee_save fe
         (Mtailcall sig ros :: k)
+  | Lbuiltin ef args dst =>
+      Mbuiltin ef args dst :: k
   | Llabel lbl =>
       Mlabel lbl :: k
   | Lgoto lbl =>
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 4406187f..68d179a6 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -650,7 +650,7 @@ Qed.
 Lemma agree_callee_save_set_result:
   forall ls1 ls2 v sg,
   agree_callee_save ls1 ls2 ->
-  agree_callee_save (Locmap.set (R (Conventions.loc_result sg)) v ls1) ls2.
+  agree_callee_save (Locmap.set (R (loc_result sg)) v ls1) ls2.
 Proof.
   intros; red; intros. rewrite H; auto. 
   symmetry; apply Locmap.gso. destruct l; simpl; auto.
@@ -1501,7 +1501,17 @@ Proof.
   econstructor; eauto. 
   intros; symmetry; eapply agree_return_regs; eauto.
   intros. inv WTI. generalize (H4 _ H0). tauto.
-  apply agree_callee_save_return_regs. 
+  apply agree_callee_save_return_regs.
+
+  (* Lbuiltin *)
+  exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b) (rs0#res <- v) fr m'); split.
+  apply plus_one. apply exec_Mbuiltin.
+  change mreg with RegEq.t.
+  rewrite (agree_eval_regs _ _ _ _ _ _ _ args AG).
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
+  econstructor; eauto with coqlib.
+  apply agree_set_reg; auto.
  
   (* Llabel *)
   econstructor; split.
diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v
index 8ba5caed..6ef86690 100644
--- a/backend/Stackingtyping.v
+++ b/backend/Stackingtyping.v
@@ -176,6 +176,9 @@ Proof.
   apply wt_restore_callee_save. apply wt_instrs_cons; auto.
   constructor; auto.
   destruct s0; auto. rewrite H5; auto.
+  (* builtin *)
+  apply wt_instrs_cons; auto.
+  constructor; auto.
   (* label *)
   apply wt_instrs_cons; auto.
   constructor.
diff --git a/backend/Tailcall.v b/backend/Tailcall.v
index 809a6a13..158002e8 100644
--- a/backend/Tailcall.v
+++ b/backend/Tailcall.v
@@ -19,7 +19,7 @@ Require Import Globalenvs.
 Require Import Registers.
 Require Import Op.
 Require Import RTL.
-Require Conventions.
+Require Import Conventions.
 
 (** An [Icall] instruction that stores its result in register [rreg]
   can be turned into a tail call if:
@@ -88,7 +88,7 @@ Definition transf_instr (f: function) (pc: node) (instr: instruction) :=
   match instr with
   | Icall sig ros args res s =>
       if is_return niter f s res
-      && Conventions.tailcall_is_possible sig
+      && tailcall_is_possible sig
       && opt_typ_eq sig.(sig_res) f.(fn_sig).(sig_res)
       then Itailcall sig ros args
       else instr
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index 2eed6e8d..11e6be20 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -24,7 +24,7 @@ Require Import Globalenvs.
 Require Import Smallstep.
 Require Import Registers.
 Require Import RTL.
-Require Conventions.
+Require Import Conventions.
 Require Import Tailcall.
 
 (** * Syntactic properties of the code transformation *)
@@ -168,7 +168,7 @@ Lemma transf_instr_charact:
   transf_instr_spec f instr (transf_instr f pc instr).
 Proof.
   intros. unfold transf_instr. destruct instr; try constructor.
-  caseEq (is_return niter f n r && Conventions.tailcall_is_possible s &&
+  caseEq (is_return niter f n r && tailcall_is_possible s &&
           opt_typ_eq (sig_res s) (sig_res (fn_sig f))); intros.
   destruct (andb_prop _ _ H0). destruct (andb_prop _ _ H1).
   eapply transf_instr_tailcall; eauto.
@@ -497,6 +497,17 @@ Proof.
   rewrite stacksize_preserved; auto.
   constructor. auto.  apply regset_get_list; auto. auto. 
 
+(* builtin *)
+  TransfInstr.
+  assert (Val.lessdef_list (rs##args) (rs'##args)). apply regset_get_list; auto. 
+  exploit external_call_mem_extends; eauto.
+  intros [v' [m'1 [A [B [C D]]]]].
+  left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' (rs'#res <- v') m'1); split.
+  eapply exec_Ibuiltin; eauto.
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
+  econstructor; eauto. apply regset_set; auto.
+
 (* cond true *)
   TransfInstr. 
   left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) ifso rs' m'); split.
diff --git a/backend/Tunneling.v b/backend/Tunneling.v
index 3ad8c4d0..6646f11f 100644
--- a/backend/Tunneling.v
+++ b/backend/Tunneling.v
@@ -104,6 +104,8 @@ Definition tunnel_instr (uf: U.t) (b: instruction) : instruction :=
       Lcall sig ros args res (U.repr uf s)
   | Ltailcall sig ros args =>
       Ltailcall sig ros args
+  | Lbuiltin ef args res s =>
+      Lbuiltin ef args res (U.repr uf s)
   | Lcond cond args s1 s2 =>
       Lcond cond args (U.repr uf s1) (U.repr uf s2)
   | Ljumptable arg tbl =>
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index 774ce853..9a14158f 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -308,6 +308,14 @@ Proof.
   rewrite sig_preserved. auto.
   apply find_function_translated; auto.
   econstructor; eauto.
+  (* Lbuiltin *)
+  generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A.
+  left; econstructor; split.
+  eapply exec_Lbuiltin; eauto. 
+  rewrite (tunnel_function_lookup _ _ _ H); simpl; auto.
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
+  econstructor; eauto.
   (* cond *)
   generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A.
   left; econstructor; split.