Give formal semantics to some built-in functions and run-time functions

This commit adds mechanisms to
- recognize certain built-in and run-time functions by name and signature;
- associate semantics to these functions, as a partial function from
  list of values to values;
- interpret external calls to these functions according to this semantics
  (pure function from values to values, memory unchanged, no observable
  events in the trace);
- external calls to unknown built-in and run-time functions remain
  interpreted as generating observable events and possibly changing
  memory, like before.

The description of the built-ins is split into a target-independent
part (in common/Builtins0.v) and a target-specific part (in
$ARCH/Builtins1.v).

Instruction selection uses the new mechanism in order to
- recognize some built-in functions and turn them into operations
  of the target processor.  Currently, this is done for
  __builtin_sel and __builtin_fabs; more to come.
- remove the axioms about int64 helper functions from the standard
  library.  More precisely, the behavior of these functions is
  still axiomatized, but now it is specified using the more general
  machinery introduced in this commit, rather than ad-hoc axioms
  in backend/SplitLongproof.

The only built-ins currently described are __builtin_fsqrt (for all platforms)
and __builtin_fmin / __builtin_fmax (for x86).  More built-ins will be
added later.

20 files changed, 1154 insertions, 187 deletions

diff --git a/Makefile b/Makefile
index 1e578006..ae19225a 100644
--- a/Makefile
+++ b/Makefile
@@ -63,7 +63,7 @@ VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \
 COMMON=Errors.v AST.v Linking.v \
   Events.v Globalenvs.v Memdata.v Memtype.v Memory.v \
   Values.v Smallstep.v Behaviors.v Switch.v Determinism.v Unityping.v \
-  Separation.v
+  Separation.v Builtins0.v Builtins1.v Builtins.v
 
 # Back-end modules (in backend/, $(ARCH)/)
 
diff --git a/arm/Builtins1.v b/arm/Builtins1.v
new file mode 100644
index 00000000..f6e643d2
--- /dev/null
+++ b/arm/Builtins1.v
@@ -0,0 +1,33 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, Collège de France and Inria Paris            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Platform-specific built-in functions *)
+
+Require Import String Coqlib.
+Require Import AST Integers Floats Values.
+Require Import Builtins0.
+
+Inductive platform_builtin : Type := .
+
+Local Open Scope string_scope.
+
+Definition platform_builtin_table : list (string * platform_builtin) :=
+  nil.
+
+Definition platform_builtin_sig (b: platform_builtin) : signature :=
+  match b with end.
+
+Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) :=
+  match b with end.
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index d04832d6..1220abc4 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -38,11 +38,8 @@
 
 Require Import Coqlib.
 Require Import Compopts.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Op.
-Require Import CminorSel.
+Require Import AST Integers Floats Builtins.
+Require Import Op CminorSel.
 
 Local Open Scope cminorsel_scope.
 
@@ -518,3 +515,8 @@ Nondetfunction builtin_arg (e: expr) :=
   | Eop (Oaddimm n) (e1:::Enil) => BA_addptr (BA e1) (BA_int n)
   | _ => BA e
   end.
+
+(** Platform-specific known builtins *)
+
+Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
+  None.
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index 8b546971..5d54d94f 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -13,16 +13,9 @@
 (** Correctness of instruction selection for operators *)
 
 Require Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Cminor.
-Require Import Op.
-Require Import CminorSel.
+Require Import AST Integers Floats.
+Require Import Values Memory Builtins Globalenvs.
+Require Import Cminor Op CminorSel.
 Require Import SelectOp.
 
 Local Open Scope cminorsel_scope.
@@ -909,4 +902,16 @@ Proof.
 - constructor; auto.
 Qed.
 
+(** Platform-specific known builtins *)
+
+Theorem eval_platform_builtin:
+  forall bf al a vl v le,
+  platform_builtin bf al = Some a ->
+  eval_exprlist ge sp e m le al vl ->
+  platform_builtin_sem bf vl = Some v ->
+  exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'.
+Proof.
+  intros. discriminate.
+Qed.
+
 End CMCONSTR.
diff --git a/backend/Selection.v b/backend/Selection.v
index 4154659c..c9771d99 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -24,7 +24,7 @@
 
 Require String.
 Require Import Coqlib Maps.
-Require Import AST Errors Integers Globalenvs Switch.
+Require Import AST Errors Integers Globalenvs Builtins Switch.
 Require Cminor.
 Require Import Op CminorSel Cminortyping.
 Require Import SelectOp SplitLong SelectLong SelectDiv.
@@ -162,6 +162,13 @@ Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr :=
   | Cminor.Ocmplu c => cmplu c arg1 arg2
   end.
 
+Definition sel_select (ty: typ) (cnd ifso ifnot: expr) : expr :=
+   let (cond, args) := condition_of_expr cnd in
+   match SelectOp.select ty cond args ifso ifnot with
+   | Some a => a
+   | None => Econdition (condexpr_of_expr cnd) ifso ifnot
+   end.
+
 (** Conversion from Cminor expression to Cminorsel expressions *)
 
 Fixpoint sel_expr (a: Cminor.expr) : expr :=
@@ -231,6 +238,43 @@ Definition sel_builtin_res (optid: option ident) : builtin_res ident :=
   | Some id => BR id
   end.
 
+(** Known builtin functions *)
+
+Function sel_known_builtin (bf: builtin_function) (args: exprlist) :=
+  match bf, args with
+  | BI_platform b, _ =>
+      SelectOp.platform_builtin b args
+  | BI_standard (BI_select ty), a1 ::: a2 ::: a3 ::: Enil =>
+      Some (sel_select ty a1 a2 a3)
+  | BI_standard BI_fabs, a1 ::: Enil =>
+      Some (SelectOp.absf a1)
+  | _, _ =>
+      None
+  end.
+
+(** Builtin functions in general *)
+
+Definition sel_builtin_default (optid: option ident) (ef: external_function)
+                               (args: list Cminor.expr) :=
+  Sbuiltin (sel_builtin_res optid) ef
+           (sel_builtin_args args (Machregs.builtin_constraints ef)).
+
+Definition sel_builtin (optid: option ident) (ef: external_function)
+                               (args: list Cminor.expr) :=
+  match optid, ef with
+  | Some id, EF_builtin name sg =>
+      match lookup_builtin_function name sg with
+      | Some bf =>
+          match sel_known_builtin bf (sel_exprlist args) with
+          | Some a => Sassign id a
+          | None => sel_builtin_default optid ef args
+          end
+      | None => sel_builtin_default optid ef args
+      end
+  | _, _ =>
+      sel_builtin_default optid ef args
+  end.
+
 (** Conversion of Cminor [switch] statements to decision trees. *)
 
 Parameter compile_switch: Z -> nat -> table -> comptree.
@@ -342,13 +386,10 @@ Fixpoint sel_stmt (ki: known_idents) (env: typenv) (s: Cminor.stmt) : res stmt :
       OK (match classify_call fn with
       | Call_default => Scall optid sg (inl _ (sel_expr fn)) (sel_exprlist args)
       | Call_imm id  => Scall optid sg (inr _ id) (sel_exprlist args)
-      | Call_builtin ef => Sbuiltin (sel_builtin_res optid) ef
-                                    (sel_builtin_args args
-                                       (Machregs.builtin_constraints ef))
+      | Call_builtin ef => sel_builtin optid ef args
       end)
   | Cminor.Sbuiltin optid ef args =>
-      OK (Sbuiltin (sel_builtin_res optid) ef
-                   (sel_builtin_args args (Machregs.builtin_constraints ef)))
+      OK (sel_builtin optid ef args)
   | Cminor.Stailcall sg fn args =>
       OK (match classify_call fn with
       | Call_imm id  => Stailcall sg (inr _ id) (sel_exprlist args)
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 50875086..ee3ed358 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -14,7 +14,8 @@
 
 Require Import FunInd.
 Require Import Coqlib Maps.
-Require Import AST Linking Errors Integers Values Memory Events Globalenvs Smallstep.
+Require Import AST Linking Errors Integers.
+Require Import Values Memory Builtins Events Globalenvs Smallstep.
 Require Import Switch Cminor Op CminorSel Cminortyping.
 Require Import SelectOp SelectDiv SplitLong SelectLong Selection.
 Require Import SelectOpproof SelectDivproof SplitLongproof SelectLongproof.
@@ -216,19 +217,16 @@ Lemma eval_condition_of_expr:
   forall a le v b,
   eval_expr tge sp e m le a v ->
   Val.bool_of_val v b ->
-  let (cond, al) := condition_of_expr a in
   exists vl,
-     eval_exprlist tge sp e m le al vl
-  /\ eval_condition cond vl m = Some b.
+     eval_exprlist tge sp e m le (snd (condition_of_expr a)) vl
+  /\ eval_condition (fst (condition_of_expr a)) vl m = Some b.
 Proof.
-  intros until a. functional induction (condition_of_expr a); intros.
-(* compare *)
-  inv H. simpl in H6. inv H6. apply Val.bool_of_val_of_optbool in H0.
-  exists vl; auto.
-(* default *)
-  exists (v :: nil); split.
-  econstructor. auto. constructor.
-  simpl. inv H0. auto.
+  intros a; functional induction (condition_of_expr a); intros; simpl.
+- inv H. exists vl; split; auto.
+  simpl in H6. inv H6. apply Val.bool_of_val_of_optbool in H0. auto.
+- exists (v :: nil); split.
+  constructor; auto; constructor.
+  inv H0; simpl; auto.
 Qed.
 
 Lemma eval_load:
@@ -353,6 +351,52 @@ Proof.
   exists v; split; auto. eapply eval_cmplu; eauto.
 Qed.
 
+Lemma eval_sel_select:
+  forall le a1 a2 a3 v1 v2 v3 b ty,
+  eval_expr tge sp e m le a1 v1 ->
+  eval_expr tge sp e m le a2 v2 ->
+  eval_expr tge sp e m le a3 v3 ->
+  Val.bool_of_val v1 b ->
+  exists v, eval_expr tge sp e m le (sel_select ty a1 a2 a3) v
+        /\  Val.lessdef (Val.select (Some b) v2 v3 ty) v.
+Proof.
+  unfold sel_select; intros.
+  specialize (eval_condition_of_expr _ _ _ _ H H2). 
+  destruct (condition_of_expr a1) as [cond args]; simpl fst; simpl snd. intros (vl & A & B).
+  destruct (select ty cond args a2 a3) as [a|] eqn:SEL.
+- eapply eval_select; eauto. 
+- exists (if b then v2 else v3); split.
+  econstructor; eauto. eapply eval_condexpr_of_expr; eauto. destruct b; auto.
+  apply Val.lessdef_normalize.
+Qed.
+
+(** Known built-in functions *)
+
+Lemma eval_sel_known_builtin:
+  forall bf args a vl v le,
+  sel_known_builtin bf args = Some a ->
+  eval_exprlist tge sp e m le args vl ->
+  builtin_function_sem bf vl = Some v ->
+  exists v', eval_expr tge sp e m le a v' /\ Val.lessdef v v'.
+Proof.
+  intros until le; intros SEL ARGS SEM.
+  destruct bf as [bf|bf]; simpl in SEL.
+- destruct bf; try discriminate.
++ (* select *)
+  inv ARGS; try discriminate. inv H0; try discriminate. inv H2; try discriminate. inv H3; try discriminate.
+  inv SEL.
+  simpl in SEM. destruct v1; inv SEM.
+  replace (Val.normalize (if Int.eq i Int.zero then v2 else v0) t)
+     with (Val.select (Some (negb (Int.eq i Int.zero))) v0 v2 t)
+       by (destruct (Int.eq i Int.zero); reflexivity).
+  eapply eval_sel_select; eauto. constructor.
++ (* fabs *)
+  inv ARGS; try discriminate. inv H0; try discriminate.
+  inv SEL.  
+  simpl in SEM; inv SEM. apply eval_absf; auto.
+- eapply eval_platform_builtin; eauto.
+Qed.
+
 End CMCONSTR.
 
 (** Recognition of calls to built-in functions *)
@@ -793,6 +837,51 @@ Proof.
   intros. destruct oid; simpl; auto. apply set_var_lessdef; auto.
 Qed.
 
+Lemma sel_builtin_default_correct:
+  forall optid ef al sp e1 m1 vl t v m2 e1' m1' f k,
+  Cminor.eval_exprlist ge sp e1 m1 al vl ->
+  external_call ef ge vl m1 t v m2 ->
+  env_lessdef e1 e1' -> Mem.extends m1 m1' ->
+  exists e2' m2',
+     step tge (State f (sel_builtin_default optid ef al) k sp e1' m1')
+            t (State f Sskip k sp e2' m2')
+  /\ env_lessdef (set_optvar optid v e1) e2'
+  /\ Mem.extends m2 m2'.
+Proof.
+  intros. unfold sel_builtin_default.
+  exploit sel_builtin_args_correct; eauto. intros (vl' & A & B).
+  exploit external_call_mem_extends; eauto. intros (v' & m2' & D & E & F & _).
+  econstructor; exists m2'; split.
+  econstructor. eexact A. eapply external_call_symbols_preserved. eexact senv_preserved. eexact D.
+  split; auto. apply sel_builtin_res_correct; auto.
+Qed. 
+
+Lemma sel_builtin_correct:
+  forall optid ef al sp e1 m1 vl t v m2 e1' m1' f k,
+  Cminor.eval_exprlist ge sp e1 m1 al vl ->
+  external_call ef ge vl m1 t v m2 ->
+  env_lessdef e1 e1' -> Mem.extends m1 m1' ->
+  exists e2' m2',
+     step tge (State f (sel_builtin optid ef al) k sp e1' m1')
+            t (State f Sskip k sp e2' m2')
+  /\ env_lessdef (set_optvar optid v e1) e2'
+  /\ Mem.extends m2 m2'.
+Proof.
+  intros. 
+  exploit sel_exprlist_correct; eauto. intros (vl' & A & B).
+  exploit external_call_mem_extends; eauto. intros (v' & m2' & D & E & F & _).
+  unfold sel_builtin.
+  destruct optid as [id|]; eauto using sel_builtin_default_correct.
+  destruct ef; eauto using sel_builtin_default_correct.
+  destruct (lookup_builtin_function name sg) as [bf|] eqn:LKUP; eauto using sel_builtin_default_correct.
+  destruct (sel_known_builtin bf (sel_exprlist al)) as [a|] eqn:SKB; eauto using sel_builtin_default_correct.
+  simpl in D. red in D. rewrite LKUP in D. inv D.
+  exploit eval_sel_known_builtin; eauto. intros (v'' & U & V).
+  econstructor; exists m2'; split.
+  econstructor. eexact U.
+  split; auto. apply set_var_lessdef; auto. apply Val.lessdef_trans with v'; auto.
+Qed.
+
 (** If-conversion *)
 
 Lemma classify_stmt_sound_1:
@@ -982,19 +1071,18 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop :=
       match_states
         (Cminor.Returnstate v k m)
         (Returnstate v' k' m')
-  | match_builtin_1: forall cunit hf ef args args' optid f sp e k m al f' e' k' m' env
+  | match_builtin_1: forall cunit hf ef args optid f sp e k m al f' e' k' m' env
         (LINK: linkorder cunit prog)
         (HF: helper_functions_declared cunit hf)
         (TF: sel_function (prog_defmap cunit) hf f = OK f')
         (TYF: type_function f = OK env)
         (MC: match_cont cunit hf (known_id f) env k k')
-        (LDA: Val.lessdef_list args args')
+        (EA: Cminor.eval_exprlist ge sp e m al args)
         (LDE: env_lessdef e e')
-        (ME: Mem.extends m m')
-        (EA: list_forall2 (CminorSel.eval_builtin_arg tge sp e' m') al args'),
+        (ME: Mem.extends m m'),
       match_states
         (Cminor.Callstate (External ef) args (Cminor.Kcall optid f sp e k) m)
-        (State f' (Sbuiltin (sel_builtin_res optid) ef al) k' sp e' m')
+        (State f' (sel_builtin optid ef al) k' sp e' m')
   | match_builtin_2: forall cunit hf v v' optid f sp e k m f' e' m' k' env
         (LINK: linkorder cunit prog)
         (HF: helper_functions_declared cunit hf)
@@ -1002,11 +1090,11 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop :=
         (TYF: type_function f = OK env)
         (MC: match_cont cunit hf (known_id f) env k k')
         (LDV: Val.lessdef v v')
-        (LDE: env_lessdef e e')
+        (LDE: env_lessdef (set_optvar optid v e) e')
         (ME: Mem.extends m m'),
       match_states
         (Cminor.Returnstate v (Cminor.Kcall optid f sp e k) m)
-        (State f' Sskip k' sp (set_builtin_res (sel_builtin_res optid) v' e') m').
+        (State f' Sskip k' sp e' m').
 
 Remark call_cont_commut:
   forall cunit hf ki env k k',
@@ -1078,6 +1166,14 @@ Proof.
   destruct (ident_eq id id0). conclude. discriminate.
 Qed.
 
+Remark sel_builtin_nolabel:
+  forall (hf: helper_functions) optid ef args, nolabel' (sel_builtin optid ef args).
+Proof.
+  unfold sel_builtin; intros; red; intros.
+  destruct optid; auto. destruct ef; auto. destruct lookup_builtin_function; auto.
+  destruct sel_known_builtin; auto. 
+Qed. 
+
 Remark find_label_commut:
   forall cunit hf ki env lbl s k s' k',
   match_cont cunit hf ki env k k' ->
@@ -1093,8 +1189,11 @@ Proof.
   unfold store. destruct (addressing m (sel_expr e)); simpl; auto.
 (* call *)
   destruct (classify_call (prog_defmap cunit) e); simpl; auto.
+  rewrite sel_builtin_nolabel; auto.
 (* tailcall *)
   destruct (classify_call (prog_defmap cunit) e); simpl; auto.
+(* builtin *)
+  rewrite sel_builtin_nolabel; auto.
 (* seq *)
   exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. eauto.
   destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)) as [[sx kx] | ];
@@ -1188,9 +1287,7 @@ Proof.
   eapply match_cont_call with (cunit := cunit) (hf := hf); eauto.
 + (* turned into Sbuiltin *)
   intros EQ. subst fd.
-  exploit sel_builtin_args_correct; eauto. intros [vargs' [C D]].
-  right; left; split. simpl. omega. split. auto.
-  econstructor; eauto.
+  right; left; split. simpl; omega. split; auto. econstructor; eauto.
 - (* Stailcall *)
   exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]].
   erewrite <- stackspace_function_translated in P by eauto.
@@ -1207,12 +1304,8 @@ Proof.
   eapply match_callstate with (cunit := cunit'); eauto.
   eapply call_cont_commut; eauto.
 - (* Sbuiltin *)
-  exploit sel_builtin_args_correct; eauto. intros [vargs' [P Q]].
-  exploit external_call_mem_extends; eauto.
-  intros [vres' [m2 [A [B [C D]]]]].
-  left; econstructor; split.
-  econstructor. eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
-  econstructor; eauto. apply sel_builtin_res_correct; auto.
+  exploit sel_builtin_correct; eauto. intros (e2' & m2' & P & Q & R).
+  left; econstructor; split. eexact P. econstructor; eauto.
 - (* Seq *)
   left; econstructor; split.
   constructor.
@@ -1303,11 +1396,8 @@ Proof.
   econstructor. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   econstructor; eauto.
 - (* external call turned into a Sbuiltin *)
-  exploit external_call_mem_extends; eauto.
-  intros [vres' [m2 [A [B [C D]]]]].
-  left; econstructor; split.
-  econstructor. eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
-  econstructor; eauto.
+  exploit sel_builtin_correct; eauto. intros (e2' & m2' & P & Q & R).
+  left; econstructor; split. eexact P. econstructor; eauto.
 - (* return *)
   inv MC.
   left; econstructor; split.
@@ -1315,7 +1405,6 @@ Proof.
   econstructor; eauto. destruct optid; simpl; auto. apply set_var_lessdef; auto.
 - (* return of an external call turned into a Sbuiltin *)
   right; left; split. simpl; omega. split. auto. econstructor; eauto.
-  apply sel_builtin_res_correct; auto.
 Qed.
 
 Lemma sel_initial_states:
diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v
index f1e8b590..18c1f18d 100644
--- a/backend/SplitLongproof.v
+++ b/backend/SplitLongproof.v
@@ -15,42 +15,13 @@
 Require Import String.
 Require Import Coqlib Maps.
 Require Import AST Errors Integers Floats.
-Require Import Values Memory Globalenvs Events Cminor Op CminorSel.
+Require Import Values Memory Globalenvs Builtins Events Cminor Op CminorSel.
 Require Import SelectOp SelectOpproof SplitLong.
 
 Local Open Scope cminorsel_scope.
 Local Open Scope string_scope.
 
-(** * Axiomatization of the helper functions *)
-
-Definition external_implements (name: string) (sg: signature) (vargs: list val) (vres: val) : Prop :=
-  forall F V (ge: Genv.t F V) m,
-  external_call (EF_runtime name sg) ge vargs m E0 vres m.
-
-Definition builtin_implements (name: string) (sg: signature) (vargs: list val) (vres: val) : Prop :=
-  forall F V (ge: Genv.t F V) m,
-  external_call (EF_builtin name sg) ge vargs m E0 vres m.
-
-Axiom i64_helpers_correct :
-    (forall x z, Val.longoffloat x = Some z -> external_implements "__compcert_i64_dtos" sig_f_l (x::nil) z)
- /\ (forall x z, Val.longuoffloat x = Some z -> external_implements "__compcert_i64_dtou" sig_f_l (x::nil) z)
- /\ (forall x z, Val.floatoflong x = Some z -> external_implements "__compcert_i64_stod" sig_l_f (x::nil) z)
- /\ (forall x z, Val.floatoflongu x = Some z -> external_implements "__compcert_i64_utod" sig_l_f (x::nil) z)
- /\ (forall x z, Val.singleoflong x = Some z -> external_implements "__compcert_i64_stof" sig_l_s (x::nil) z)
- /\ (forall x z, Val.singleoflongu x = Some z -> external_implements "__compcert_i64_utof" sig_l_s (x::nil) z)
- /\ (forall x, builtin_implements "__builtin_negl" sig_l_l (x::nil) (Val.negl x))
- /\ (forall x y, builtin_implements "__builtin_addl" sig_ll_l (x::y::nil) (Val.addl x y))
- /\ (forall x y, builtin_implements "__builtin_subl" sig_ll_l (x::y::nil) (Val.subl x y))
- /\ (forall x y, builtin_implements "__builtin_mull" sig_ii_l (x::y::nil) (Val.mull' x y))
- /\ (forall x y z, Val.divls x y = Some z -> external_implements "__compcert_i64_sdiv" sig_ll_l (x::y::nil) z)
- /\ (forall x y z, Val.divlu x y = Some z -> external_implements "__compcert_i64_udiv" sig_ll_l (x::y::nil) z)
- /\ (forall x y z, Val.modls x y = Some z -> external_implements "__compcert_i64_smod" sig_ll_l (x::y::nil) z)
- /\ (forall x y z, Val.modlu x y = Some z -> external_implements "__compcert_i64_umod" sig_ll_l (x::y::nil) z)
- /\ (forall x y, external_implements "__compcert_i64_shl" sig_li_l (x::y::nil) (Val.shll x y))
- /\ (forall x y, external_implements "__compcert_i64_shr" sig_li_l (x::y::nil) (Val.shrlu x y))
- /\ (forall x y, external_implements "__compcert_i64_sar" sig_li_l (x::y::nil) (Val.shrl x y))
- /\ (forall x y, external_implements "__compcert_i64_umulh" sig_ll_l (x::y::nil) (Val.mullhu x y))
- /\ (forall x y, external_implements "__compcert_i64_smulh" sig_ll_l (x::y::nil) (Val.mullhs x y)).
+(** * Properties of the helper functions *)
 
 Definition helper_declared {F V: Type} (p: AST.program (AST.fundef F) V) (id: ident) (name: string) (sg: signature) : Prop :=
   (prog_defmap p)!id = Some (Gfun (External (EF_runtime name sg))).
@@ -84,60 +55,67 @@ Variable sp: val.
 Variable e: env.
 Variable m: mem.
 
-Ltac UseHelper := decompose [Logic.and] i64_helpers_correct; eauto.
 Ltac DeclHelper := red in HELPERS; decompose [Logic.and] HELPERS; eauto.
 
 Lemma eval_helper:
-  forall le id name sg args vargs vres,
+  forall bf le id name sg args vargs vres,
   eval_exprlist ge sp e m le args vargs ->
   helper_declared prog id name sg  ->
-  external_implements name sg vargs vres ->
+  lookup_builtin_function name sg = Some bf ->
+  builtin_function_sem bf vargs = Some vres ->
   eval_expr ge sp e m le (Eexternal id sg args) vres.
 Proof.
   intros.
   red in H0. apply Genv.find_def_symbol in H0. destruct H0 as (b & P & Q).
   rewrite <- Genv.find_funct_ptr_iff in Q.
-  econstructor; eauto.
+  econstructor; eauto. 
+  simpl. red. rewrite H1. constructor; auto.
 Qed.
 
 Corollary eval_helper_1:
-  forall le id name sg arg1 varg1 vres,
+  forall bf le id name sg arg1 varg1 vres,
   eval_expr ge sp e m le arg1 varg1 ->
   helper_declared prog id name sg  ->
-  external_implements name sg (varg1::nil) vres ->
+  lookup_builtin_function name sg = Some bf ->
+  builtin_function_sem bf (varg1 :: nil) = Some vres ->
   eval_expr ge sp e m le (Eexternal id sg (arg1 ::: Enil)) vres.
 Proof.
   intros. eapply eval_helper; eauto. constructor; auto. constructor.
 Qed.
 
 Corollary eval_helper_2:
-  forall le id name sg arg1 arg2 varg1 varg2 vres,
+  forall bf le id name sg arg1 arg2 varg1 varg2 vres,
   eval_expr ge sp e m le arg1 varg1 ->
   eval_expr ge sp e m le arg2 varg2 ->
   helper_declared prog id name sg  ->
-  external_implements name sg (varg1::varg2::nil) vres ->
+  lookup_builtin_function name sg = Some bf ->
+  builtin_function_sem bf (varg1 :: varg2 :: nil) = Some vres ->
   eval_expr ge sp e m le (Eexternal id sg (arg1 ::: arg2 ::: Enil)) vres.
 Proof.
   intros. eapply eval_helper; eauto. constructor; auto. constructor; auto. constructor.
 Qed.
 
 Remark eval_builtin_1:
-  forall le id sg arg1 varg1 vres,
+  forall bf le id sg arg1 varg1 vres,
   eval_expr ge sp e m le arg1 varg1 ->
-  builtin_implements id sg (varg1::nil) vres ->
+  lookup_builtin_function id sg = Some bf ->
+  builtin_function_sem bf (varg1 :: nil) = Some vres ->
   eval_expr ge sp e m le (Ebuiltin (EF_builtin id sg) (arg1 ::: Enil)) vres.
 Proof.
-  intros. econstructor. econstructor. eauto. constructor. apply H0.
+  intros. econstructor. econstructor. eauto. constructor.
+  simpl. red. rewrite H0. constructor. auto.
 Qed.
 
 Remark eval_builtin_2:
-  forall le id sg arg1 arg2 varg1 varg2 vres,
+  forall bf le id sg arg1 arg2 varg1 varg2 vres,
   eval_expr ge sp e m le arg1 varg1 ->
   eval_expr ge sp e m le arg2 varg2 ->
-  builtin_implements id sg (varg1::varg2::nil) vres ->
+  lookup_builtin_function id sg = Some bf ->
+  builtin_function_sem bf (varg1 :: varg2 :: nil) = Some vres ->
   eval_expr ge sp e m le (Ebuiltin (EF_builtin id sg) (arg1 ::: arg2 ::: Enil)) vres.
 Proof.
-  intros. econstructor. constructor; eauto. constructor; eauto. constructor. apply H1.
+  intros. econstructor. constructor; eauto. constructor; eauto. constructor.
+  simpl. red. rewrite H1. constructor. auto.
 Qed.
 
 Definition unary_constructor_sound (cstr: expr -> expr) (sem: val -> val) : Prop :=
@@ -386,9 +364,10 @@ Qed.
 Theorem eval_negl: unary_constructor_sound negl Val.negl.
 Proof.
   unfold negl; red; intros. destruct (is_longconst a) eqn:E.
-  econstructor; split. apply eval_longconst.
+- econstructor; split. apply eval_longconst.
   exploit is_longconst_sound; eauto. intros EQ; subst x. simpl. auto.
-  econstructor; split. eapply eval_builtin_1; eauto. UseHelper. auto.
+- exists (Val.negl x); split; auto.
+  eapply (eval_builtin_1 (BI_standard BI_negl)); eauto.
 Qed.
 
 Theorem eval_notl: unary_constructor_sound notl Val.notl.
@@ -410,7 +389,7 @@ Theorem eval_longoffloat:
   exists v, eval_expr ge sp e m le (longoffloat a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold longoffloat. econstructor; split.
-  eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto.
+  eapply (eval_helper_1 (BI_standard BI_i64_dtos)); eauto. DeclHelper. auto. auto.
 Qed.
 
 Theorem eval_longuoffloat:
@@ -420,7 +399,7 @@ Theorem eval_longuoffloat:
   exists v, eval_expr ge sp e m le (longuoffloat a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold longuoffloat. econstructor; split.
-  eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto.
+  eapply (eval_helper_1 (BI_standard BI_i64_dtou)); eauto. DeclHelper. auto. auto.
 Qed.
 
 Theorem eval_floatoflong:
@@ -429,8 +408,9 @@ Theorem eval_floatoflong:
   Val.floatoflong x = Some y ->
   exists v, eval_expr ge sp e m le (floatoflong a) v /\ Val.lessdef y v.
 Proof.
-  intros; unfold floatoflong. econstructor; split.
-  eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto.
+  intros; unfold floatoflong. exists y; split; auto.
+  eapply (eval_helper_1 (BI_standard BI_i64_stod)); eauto. DeclHelper. auto.
+  simpl. destruct x; simpl in H0; inv H0; auto.
 Qed.
 
 Theorem eval_floatoflongu:
@@ -439,8 +419,9 @@ Theorem eval_floatoflongu:
   Val.floatoflongu x = Some y ->
   exists v, eval_expr ge sp e m le (floatoflongu a) v /\ Val.lessdef y v.
 Proof.
-  intros; unfold floatoflongu. econstructor; split.
-  eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto.
+  intros; unfold floatoflongu. exists y; split; auto.
+  eapply (eval_helper_1 (BI_standard BI_i64_utod)); eauto. DeclHelper. auto.
+  simpl. destruct x; simpl in H0; inv H0; auto.
 Qed.
 
 Theorem eval_longofsingle:
@@ -477,8 +458,9 @@ Theorem eval_singleoflong:
   Val.singleoflong x = Some y ->
   exists v, eval_expr ge sp e m le (singleoflong a) v /\ Val.lessdef y v.
 Proof.
-  intros; unfold singleoflong. econstructor; split.
-  eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto.
+  intros; unfold singleoflong. exists y; split; auto.
+  eapply (eval_helper_1 (BI_standard BI_i64_stof)); eauto. DeclHelper. auto.
+  simpl. destruct x; simpl in H0; inv H0; auto.
 Qed.
 
 Theorem eval_singleoflongu:
@@ -487,8 +469,9 @@ Theorem eval_singleoflongu:
   Val.singleoflongu x = Some y ->
   exists v, eval_expr ge sp e m le (singleoflongu a) v /\ Val.lessdef y v.
 Proof.
-  intros; unfold singleoflongu. econstructor; split.
-  eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto.
+  intros; unfold singleoflongu. exists y; split; auto.
+  eapply (eval_helper_1 (BI_standard BI_i64_utof)); eauto. DeclHelper. auto.
+  simpl. destruct x; simpl in H0; inv H0; auto.
 Qed.
 
 Theorem eval_andl: binary_constructor_sound andl Val.andl.
@@ -615,7 +598,9 @@ Proof.
     simpl. erewrite <- Int64.decompose_shl_2. instantiate (1 := Int64.hiword i).
     rewrite Int64.ofwords_recompose. auto. auto.
   + (* n >= 64 *)
-    econstructor; split. eapply eval_helper_2; eauto. EvalOp. DeclHelper. UseHelper. auto.
+    econstructor; split.
+    eapply eval_helper_2; eauto. EvalOp. DeclHelper. reflexivity. reflexivity.
+    auto.
 Qed.
 
 Theorem eval_shll: binary_constructor_sound shll Val.shll.
@@ -626,7 +611,7 @@ Proof.
   exploit is_intconst_sound; eauto. intros EQ; subst y; clear H0.
   eapply eval_shllimm; eauto.
 - (* General case *)
-  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
+  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. reflexivity. reflexivity. auto.
 Qed.
 
 Lemma eval_shrluimm:
@@ -660,7 +645,9 @@ Proof.
     simpl. erewrite <- Int64.decompose_shru_2. instantiate (1 := Int64.loword i).
     rewrite Int64.ofwords_recompose. auto. auto.
   + (* n >= 64 *)
-    econstructor; split. eapply eval_helper_2; eauto. EvalOp. DeclHelper. UseHelper. auto.
+    econstructor; split.
+    eapply eval_helper_2; eauto. EvalOp. DeclHelper. reflexivity. reflexivity.
+    auto.
 Qed.
 
 Theorem eval_shrlu: binary_constructor_sound shrlu Val.shrlu.
@@ -671,7 +658,7 @@ Proof.
   exploit is_intconst_sound; eauto. intros EQ; subst y; clear H0.
   eapply eval_shrluimm; eauto.
 - (* General case *)
-  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
+  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. reflexivity. reflexivity. auto.
 Qed.
 
 Lemma eval_shrlimm:
@@ -709,7 +696,9 @@ Proof.
     erewrite <- Int64.decompose_shr_2. instantiate (1 := Int64.loword i).
     rewrite Int64.ofwords_recompose. auto. auto.
   + (* n >= 64 *)
-    econstructor; split. eapply eval_helper_2; eauto. EvalOp. DeclHelper. UseHelper. auto.
+    econstructor; split.
+    eapply eval_helper_2; eauto. EvalOp. DeclHelper. reflexivity. reflexivity.
+    auto.
 Qed.
 
 Theorem eval_shrl: binary_constructor_sound shrl Val.shrl.
@@ -720,7 +709,7 @@ Proof.
   exploit is_intconst_sound; eauto. intros EQ; subst y; clear H0.
   eapply eval_shrlimm; eauto.
 - (* General case *)
-  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
+  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. reflexivity. reflexivity. auto.
 Qed.
 
 Theorem eval_addl: Archi.ptr64 = false -> binary_constructor_sound addl Val.addl.
@@ -730,7 +719,7 @@ Proof.
   assert (DEFAULT:
     exists v, eval_expr ge sp e m le default v /\ Val.lessdef (Val.addl x y) v).
   {
-    econstructor; split. eapply eval_builtin_2; eauto. UseHelper. auto.
+    econstructor; split. eapply eval_builtin_2; eauto. reflexivity. reflexivity. auto.
   }
   destruct (is_longconst a) as [p|] eqn:LC1;
   destruct (is_longconst b) as [q|] eqn:LC2.
@@ -753,7 +742,7 @@ Proof.
   assert (DEFAULT:
     exists v, eval_expr ge sp e m le default v /\ Val.lessdef (Val.subl x y) v).
   {
-    econstructor; split. eapply eval_builtin_2; eauto. UseHelper. auto.
+    econstructor; split. eapply eval_builtin_2; eauto. reflexivity. reflexivity. auto.
   }
   destruct (is_longconst a) as [p|] eqn:LC1;
   destruct (is_longconst b) as [q|] eqn:LC2.
@@ -784,7 +773,7 @@ Proof.
   exploit eval_add. eexact E2. eexact E3. intros [v5 [E5 L5]].
   exploit eval_add. eexact E5. eexact E4. intros [v6 [E6 L6]].
   exists (Val.longofwords v6 (Val.loword p)); split.
-  EvalOp. eapply eval_builtin_2; eauto. UseHelper.
+  EvalOp. eapply eval_builtin_2; eauto. reflexivity. reflexivity. 
   intros. unfold le1, p in *; subst; simpl in *.
   inv L3. inv L4. inv L5. simpl in L6. inv L6.
   simpl. f_equal. symmetry. apply Int64.decompose_mul.
@@ -832,14 +821,14 @@ Theorem eval_mullhu:
   forall n, unary_constructor_sound (fun a => mullhu a n) (fun v => Val.mullhu v (Vlong n)).
 Proof.
   unfold mullhu; intros; red; intros. econstructor; split; eauto.
-  eapply eval_helper_2; eauto. apply eval_longconst. DeclHelper; eauto. UseHelper.
+  eapply eval_helper_2; eauto. apply eval_longconst. DeclHelper. reflexivity. reflexivity.
 Qed.
 
 Theorem eval_mullhs:
   forall n, unary_constructor_sound (fun a => mullhs a n) (fun v => Val.mullhs v (Vlong n)).
 Proof.
   unfold mullhs; intros; red; intros. econstructor; split; eauto.
-  eapply eval_helper_2; eauto. apply eval_longconst. DeclHelper; eauto. UseHelper.
+  eapply eval_helper_2; eauto. apply eval_longconst. DeclHelper. reflexivity. reflexivity.
 Qed.
 
 Theorem eval_shrxlimm:
@@ -881,7 +870,7 @@ Theorem eval_divlu_base:
   exists v, eval_expr ge sp e m le (divlu_base a b) v /\ Val.lessdef z v.
 Proof.
   intros; unfold divlu_base.
-  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
+  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. reflexivity. eassumption. auto.
 Qed.
 
 Theorem eval_modlu_base:
@@ -892,7 +881,7 @@ Theorem eval_modlu_base:
   exists v, eval_expr ge sp e m le (modlu_base a b) v /\ Val.lessdef z v.
 Proof.
   intros; unfold modlu_base.
-  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
+  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. reflexivity. eassumption. auto.
 Qed.
 
 Theorem eval_divls_base:
@@ -903,7 +892,7 @@ Theorem eval_divls_base:
   exists v, eval_expr ge sp e m le (divls_base a b) v /\ Val.lessdef z v.
 Proof.
   intros; unfold divls_base.
-  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
+  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. reflexivity. eassumption. auto.
 Qed.
 
 Theorem eval_modls_base:
@@ -914,7 +903,7 @@ Theorem eval_modls_base:
   exists v, eval_expr ge sp e m le (modls_base a b) v /\ Val.lessdef z v.
 Proof.
   intros; unfold modls_base.
-  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
+  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. reflexivity. eassumption. auto.
 Qed.
 
 Remark decompose_cmpl_eq_zero:
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 7f5fe355..e6bf2129 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -16,7 +16,7 @@ Require Import FunInd.
 Require Import Axioms Classical.
 Require Import String Coqlib Decidableplus.
 Require Import Errors Maps Integers Floats.
-Require Import AST Values Memory Events Globalenvs Determinism.
+Require Import AST Values Memory Events Globalenvs Builtins Determinism.
 Require Import Ctypes Cop Csyntax Csem.
 Require Cstrategy.
 
@@ -501,12 +501,19 @@ Definition do_ef_debug (kind: positive) (text: ident) (targs: list typ)
        (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
   Some(w, E0, Vundef, m).
 
+Definition do_builtin_or_external (name: string) (sg: signature)
+       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
+  match lookup_builtin_function name sg with
+  | Some bf => match builtin_function_sem bf vargs with Some v => Some(w, E0, v, m) | None => None end
+  | None    => do_external_function name sg ge w vargs m
+  end.
+
 Definition do_external (ef: external_function):
        world -> list val -> mem -> option (world * trace * val * mem) :=
   match ef with
   | EF_external name sg => do_external_function name sg ge
-  | EF_builtin name sg => do_external_function name sg ge
-  | EF_runtime name sg => do_external_function name sg ge
+  | EF_builtin name sg => do_builtin_or_external name sg
+  | EF_runtime name sg => do_builtin_or_external name sg
   | EF_vload chunk => do_ef_volatile_load chunk
   | EF_vstore chunk => do_ef_volatile_store chunk
   | EF_malloc => do_ef_malloc
@@ -523,17 +530,26 @@ Lemma do_ef_external_sound:
   do_external ef w vargs m = Some(w', t, vres, m') ->
   external_call ef ge vargs m t vres m' /\ possible_trace w t w'.
 Proof with try congruence.
+  intros until m'.
   assert (SIZE: forall v sz, do_alloc_size v = Some sz -> v = Vptrofs sz).
   { intros until sz; unfold Vptrofs; destruct v; simpl; destruct Archi.ptr64 eqn:SF; 
     intros EQ; inv EQ; f_equal; symmetry; eauto with ptrofs. }
-  intros until m'.
+  assert (BF_EX: forall name sg,
+    do_builtin_or_external name sg w vargs m = Some (w', t, vres, m') ->
+    builtin_or_external_sem name sg ge vargs m t vres m' /\ possible_trace w t w').
+  { unfold do_builtin_or_external, builtin_or_external_sem; intros. 
+    destruct (lookup_builtin_function name sg ) as [bf|].
+  - destruct (builtin_function_sem bf vargs) as [vres1|] eqn:BF; inv H.
+    split. constructor; auto. constructor.
+  - eapply do_external_function_sound; eauto.
+  }
   destruct ef; simpl.
 (* EF_external *)
   eapply do_external_function_sound; eauto.
 (* EF_builtin *)
-  eapply do_external_function_sound; eauto.
+  eapply BF_EX; eauto.
 (* EF_runtime *)
-  eapply do_external_function_sound; eauto.
+  eapply BF_EX; eauto.
 (* EF_vload *)
   unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs...
   mydestr. destruct p as [[w'' t''] v]; mydestr.
@@ -575,17 +591,26 @@ Lemma do_ef_external_complete:
   external_call ef ge vargs m t vres m' -> possible_trace w t w' ->
   do_external ef w vargs m = Some(w', t, vres, m').
 Proof.
+  intros.
   assert (SIZE: forall n, do_alloc_size (Vptrofs n) = Some n).
   { unfold Vptrofs, do_alloc_size; intros; destruct Archi.ptr64 eqn:SF. 
     rewrite Ptrofs.of_int64_to_int64; auto.
     rewrite Ptrofs.of_int_to_int; auto. }
-  intros. destruct ef; simpl in *.
+  assert (BF_EX: forall name sg,
+    builtin_or_external_sem name sg ge vargs m t vres m' ->
+    do_builtin_or_external name sg w vargs m = Some (w', t, vres, m')).
+  { unfold do_builtin_or_external, builtin_or_external_sem; intros.
+    destruct (lookup_builtin_function name sg) as [bf|].
+  - inv H1. inv H0. rewrite H2. auto.
+  - eapply do_external_function_complete; eauto.
+  }
+  destruct ef; simpl in *.
 (* EF_external *)
   eapply do_external_function_complete; eauto.
 (* EF_builtin *)
-  eapply do_external_function_complete; eauto.
+  eapply BF_EX; eauto.
 (* EF_runtime *)
-  eapply do_external_function_complete; eauto.
+  eapply BF_EX; eauto.
 (* EF_vload *)
   inv H; unfold do_ef_volatile_load.
   exploit do_volatile_load_complete; eauto. intros EQ; rewrite EQ; auto.
diff --git a/common/Builtins.v b/common/Builtins.v
new file mode 100644
index 00000000..c9097e86
--- /dev/null
+++ b/common/Builtins.v
@@ -0,0 +1,58 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, Collège de France and Inria Paris            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Known built-in functions *)
+
+Require Import String Coqlib.
+Require Import AST Integers Floats Values.
+Require Export Builtins0 Builtins1.
+
+Inductive builtin_function : Type :=
+  | BI_standard (b: standard_builtin)
+  | BI_platform (b: platform_builtin).
+
+Definition builtin_function_sig (b: builtin_function) : signature :=
+  match b with
+  | BI_standard b => standard_builtin_sig b
+  | BI_platform b => platform_builtin_sig b
+  end.
+
+Definition builtin_function_sem (b: builtin_function) : builtin_sem (proj_sig_res (builtin_function_sig b)) :=
+  match b with
+  | BI_standard b => standard_builtin_sem b
+  | BI_platform b => platform_builtin_sem b
+  end.
+
+Definition lookup_builtin_function (name: string) (sg: signature) : option builtin_function :=
+  match lookup_builtin standard_builtin_sig name sg standard_builtin_table with
+  | Some b => Some (BI_standard b)
+  | None => 
+  match lookup_builtin platform_builtin_sig name sg platform_builtin_table with
+  | Some b => Some (BI_platform b)
+  | None => None
+  end end.
+
+Lemma lookup_builtin_function_sig:
+  forall name sg b, lookup_builtin_function name sg = Some b -> builtin_function_sig b = sg.
+Proof.
+  unfold lookup_builtin_function; intros.
+  destruct (lookup_builtin standard_builtin_sig name sg standard_builtin_table) as [bs|] eqn:E.
+  inv H. simpl. eapply lookup_builtin_sig; eauto.
+  destruct (lookup_builtin platform_builtin_sig name sg platform_builtin_table) as [bp|] eqn:E'.
+  inv H. simpl. eapply lookup_builtin_sig; eauto.
+  discriminate.
+Qed.
+
+
diff --git a/common/Builtins0.v b/common/Builtins0.v
new file mode 100644
index 00000000..c6a299d9
--- /dev/null
+++ b/common/Builtins0.v
@@ -0,0 +1,509 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, Collège de France and Inria Paris            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Associating semantics to built-in functions *)
+
+Require Import String Coqlib.
+Require Import AST Integers Floats Values.
+
+(** This module provides definitions and mechanisms to associate semantics
+  with names of built-in functions.
+
+  This module is independent of the target architecture.  Each target
+  provides a [Builtins1] module that lists the built-ins semantics
+  appropriate for the target.
+*)
+
+Definition val_opt_has_type (ov: option val) (t: typ) : Prop :=
+  match ov with Some v => Val.has_type v t | None => True end.
+
+Definition val_opt_inject (j: meminj) (ov ov': option val) : Prop :=
+  match ov, ov' with
+  | None, _ => True
+  | Some v, Some v' => Val.inject j v v'
+  | _, None => False
+  end.
+
+(** The semantics of a built-in function is a partial function
+  from list of values to values.  
+  It must agree with the return type stated in the signature,
+  and be compatible with value injections.
+*)
+
+Record builtin_sem (tret: typ) : Type := mkbuiltin {
+  bs_sem :> list val -> option val;
+  bs_well_typed: forall vl, 
+    val_opt_has_type (bs_sem vl) tret;
+  bs_inject: forall j vl vl',
+    Val.inject_list j vl vl' -> val_opt_inject j (bs_sem vl) (bs_sem vl')
+}.
+
+(** Builtin functions can be created from functions over values, such as those
+  from the [Values.Val] module.  Proofs of well-typedness and compatibility with
+  injections must be provided. The constructor functions have names
+- [mkbuiltin_vNt] for a [t]otal function of [N] arguments that are [v]alues, or
+- [mkbuiltin_vNp] for a [p]artial function of [N] arguments that are [v]alues.
+*)
+
+Local Unset Program Cases.
+
+Program Definition mkbuiltin_v1t 
+     (tret: typ) (f: val -> val)
+     (WT: forall v1, Val.has_type (f v1) tret)
+     (INJ: forall j v1 v1', Val.inject j v1 v1' -> Val.inject j (f v1) (f v1')) :=
+  mkbuiltin tret (fun vl => match vl with v1 :: nil => Some (f v1) | _ => None end) _ _.
+Next Obligation.
+  red; destruct vl; auto. destruct vl; auto.
+Qed.
+Next Obligation.
+  red; inv H; auto. inv H1; auto. 
+Qed.
+
+Program Definition mkbuiltin_v2t 
+     (tret: typ) (f: val -> val -> val)
+     (WT: forall v1 v2, Val.has_type (f v1 v2) tret)
+     (INJ: forall j v1 v1' v2 v2',
+           Val.inject j v1 v1' -> Val.inject j v2 v2' ->
+           Val.inject j (f v1 v2) (f v1' v2')) :=
+  mkbuiltin tret (fun vl => match vl with v1 :: v2 :: nil => Some (f v1 v2) | _ => None end) _ _.
+Next Obligation.
+  red; destruct vl; auto. destruct vl; auto. destruct vl; auto.
+Qed.
+Next Obligation.
+  red; inv H; auto. inv H1; auto. inv H2; auto.
+Qed.
+
+Program Definition mkbuiltin_v3t 
+     (tret: typ) (f: val -> val -> val -> val)
+     (WT: forall v1 v2 v3, Val.has_type (f v1 v2 v3) tret)
+     (INJ: forall j v1 v1' v2 v2' v3 v3',
+           Val.inject j v1 v1' -> Val.inject j v2 v2' -> Val.inject j v3 v3' ->
+           Val.inject j (f v1 v2 v3) (f v1' v2' v3')) :=
+  mkbuiltin tret (fun vl => match vl with v1 :: v2 :: v3 :: nil => Some (f v1 v2 v3) | _ => None end) _ _.
+Next Obligation.
+  red; destruct vl; auto. destruct vl; auto. destruct vl; auto. destruct vl; auto.
+Qed.
+Next Obligation.
+  red; inv H; auto. inv H1; auto. inv H2; auto. inv H3; auto.
+Qed.
+
+Program Definition mkbuiltin_v1p
+     (tret: typ) (f: val -> option val)
+     (WT: forall v1, val_opt_has_type (f v1) tret)
+     (INJ: forall j v1 v1',
+        Val.inject j v1 v1' -> val_opt_inject j (f v1) (f v1')) :=
+  mkbuiltin tret (fun vl => match vl with v1 :: nil => f v1 | _ => None end) _ _.
+Next Obligation.
+  red; destruct vl; auto. destruct vl; auto. apply WT.
+Qed.
+Next Obligation.
+  red; inv H; auto. inv H1; auto. apply INJ; auto. 
+Qed.
+
+Program Definition mkbuiltin_v2p
+     (tret: typ) (f: val -> val -> option val)
+     (WT: forall v1 v2, val_opt_has_type (f v1 v2) tret)
+     (INJ: forall j v1 v1' v2 v2',
+        Val.inject j v1 v1' -> Val.inject j v2 v2' ->
+        val_opt_inject j (f v1 v2) (f v1' v2')) :=
+  mkbuiltin tret (fun vl => match vl with v1 :: v2 :: nil => f v1 v2 | _ => None end)  _ _.
+Next Obligation.
+  red; destruct vl; auto. destruct vl; auto. destruct vl; auto. apply WT.
+Qed.
+Next Obligation.
+  red; inv H; auto. inv H1; auto. inv H2; auto. apply INJ; auto. 
+Qed.
+
+(** For numerical functions, involving only integers and floating-point numbers
+  but no pointer values, we can automate the proofs of well-typedness and
+  of compatibility with injections. *)
+
+(** First we define a mapping from syntactic Cminor types ([Tint], [Tfloat], etc) to semantic Coq types. *)
+
+Definition valty (t: typ) : Type :=
+  match t with
+  | Tint => int
+  | Tlong => int64
+  | Tfloat => float
+  | Tsingle => float32
+  | Tany32 | Tany64 => Empty_set (**r no clear semantic meaning *)
+  end.
+
+(** We can inject and project between the numerical type [valty t] and the type [val]. *)
+
+Definition inj_num (t: typ) : valty t -> val :=
+  match t with
+  | Tint => Vint
+  | Tlong => Vlong
+  | Tfloat => Vfloat
+  | Tsingle => Vsingle
+  | Tany32 | Tany64 => fun _ => Vundef
+  end.
+
+Definition proj_num {A: Type} (t: typ) (k0: A) (v: val): (valty t -> A) -> A :=
+  match t with
+  | Tint => fun k1 => match v with Vint n => k1 n | _ => k0 end
+  | Tlong => fun k1 => match v with Vlong n => k1 n | _ => k0 end
+  | Tfloat => fun k1 => match v with Vfloat n => k1 n | _ => k0 end
+  | Tsingle => fun k1 => match v with Vsingle n => k1 n | _ => k0 end
+  | Tany32 | Tany64 => fun k1 => k0
+  end.
+
+Lemma inj_num_wt: forall t x, Val.has_type (inj_num t x) t.
+Proof.
+  destruct t; intros; exact I.
+Qed.
+
+Lemma inj_num_inject: forall j t x, Val.inject j (inj_num t x) (inj_num t x).
+Proof.
+  destruct t; intros; constructor.
+Qed.
+
+Lemma inj_num_opt_wt: forall t x, val_opt_has_type (option_map (inj_num t) x) t.
+Proof.
+  intros. destruct x; simpl. apply inj_num_wt. auto. 
+Qed.
+
+Lemma inj_num_opt_inject: forall j t x,
+  val_opt_inject j (option_map (inj_num t) x) (option_map (inj_num t) x).
+Proof.
+  destruct x; simpl. apply inj_num_inject. auto.
+Qed.
+
+Lemma proj_num_wt:
+  forall tres t k1 v,
+  (forall x, Val.has_type (k1 x) tres) ->
+  Val.has_type (proj_num t Vundef v k1) tres.
+Proof.
+  intros. destruct t; simpl; destruct v; auto; exact I.
+Qed.
+
+Lemma proj_num_inject:
+  forall j t k1 v k1' v',
+  (forall x, Val.inject j (k1 x) (k1' x)) ->
+  Val.inject j v v' -> 
+  Val.inject j (proj_num t Vundef v k1) (proj_num t Vundef v' k1').
+Proof.
+  intros. destruct t; simpl; inv H0; auto.
+Qed.
+
+Lemma proj_num_opt_wt:
+  forall tres t k0 k1 v,
+  k0 = None \/ k0 = Some Vundef ->
+  (forall x, val_opt_has_type (k1 x) tres) ->
+  val_opt_has_type (proj_num t k0 v k1) tres.
+Proof.
+  intros.
+  assert (val_opt_has_type k0 tres). { destruct H; subst k0; exact I. }
+  destruct t; simpl; destruct v; auto.
+Qed.
+
+Lemma proj_num_opt_inject:
+  forall j k0 t k1 v k1' v',
+  (forall ov, val_opt_inject j k0 ov) ->
+  (forall x, val_opt_inject j (k1 x) (k1' x)) ->
+  Val.inject j v v' -> 
+  val_opt_inject j (proj_num t k0 v k1) (proj_num t k0 v' k1').
+Proof.
+  intros. destruct t; simpl; inv H1; auto.
+Qed.
+
+(** Wrapping numerical functions as built-ins.  The constructor functions
+  have names
+- [mkbuiltin_nNt] for a [t]otal function of [N] numbers, or
+- [mkbuiltin_vNp] for a [p]artial function of [N] numbers.
+ *)
+
+Program Definition mkbuiltin_n1t 
+    (targ1: typ) (tres: typ)
+    (f: valty targ1 -> valty tres) :=
+  mkbuiltin_v1t tres
+    (fun v1 => proj_num targ1 Vundef v1 (fun x => inj_num tres (f x)))
+    _ _.
+Next Obligation.
+  auto using proj_num_wt, inj_num_wt.
+Qed.
+Next Obligation.
+  auto using proj_num_inject, inj_num_inject.
+Qed.
+
+Program Definition mkbuiltin_n2t 
+    (targ1 targ2: typ) (tres: typ)
+    (f: valty targ1 -> valty targ2 -> valty tres) :=
+  mkbuiltin_v2t tres
+    (fun v1 v2 =>
+       proj_num targ1 Vundef v1 (fun x1 =>
+       proj_num targ2 Vundef v2 (fun x2 => inj_num tres (f x1 x2))))
+    _ _.
+Next Obligation.
+  auto using proj_num_wt, inj_num_wt.
+Qed.
+Next Obligation.
+  auto using proj_num_inject, inj_num_inject.
+Qed.
+
+Program Definition mkbuiltin_n3t 
+    (targ1 targ2 targ3: typ) (tres: typ)
+    (f: valty targ1 -> valty targ2 -> valty targ3 -> valty tres) :=
+  mkbuiltin_v3t tres
+    (fun v1 v2 v3 =>
+       proj_num targ1 Vundef v1 (fun x1 =>
+       proj_num targ2 Vundef v2 (fun x2 =>
+       proj_num targ3 Vundef v3 (fun x3 => inj_num tres (f x1 x2 x3)))))
+    _ _.
+Next Obligation.
+  auto using proj_num_wt, inj_num_wt.
+Qed.
+Next Obligation.
+  auto using proj_num_inject, inj_num_inject.
+Qed.
+
+Program Definition mkbuiltin_n1p
+    (targ1: typ) (tres: typ)
+    (f: valty targ1 -> option (valty tres)) :=
+  mkbuiltin_v1p tres
+    (fun v1 => proj_num targ1 None v1 (fun x => option_map (inj_num tres) (f x)))
+    _ _.
+Next Obligation.
+  auto using proj_num_opt_wt, inj_num_opt_wt.
+Qed.
+Next Obligation.
+  apply proj_num_opt_inject; auto. intros; red; auto. intros; apply inj_num_opt_inject.
+Qed.
+
+Program Definition mkbuiltin_n2p
+    (targ1 targ2: typ) (tres: typ)
+    (f: valty targ1 -> valty targ2 -> option (valty tres)) :=
+  mkbuiltin_v2p tres
+    (fun v1 v2 =>
+      proj_num targ1 None v1 (fun x1 =>
+      proj_num targ2 None v2 (fun x2 => option_map (inj_num tres) (f x1 x2))))
+    _ _.
+Next Obligation.
+  auto using proj_num_opt_wt, inj_num_opt_wt.
+Qed.
+Next Obligation.
+  apply proj_num_opt_inject; auto. intros; red; auto. intros.
+  apply proj_num_opt_inject; auto. intros; red; auto. intros.
+  apply inj_num_opt_inject.
+Qed.
+
+(** Looking up builtins by name and signature *)
+
+Section LOOKUP.
+
+Context {A: Type} (sig_of: A -> signature).
+
+Fixpoint lookup_builtin (name: string) (sg: signature) (l: list (string * A)) : option A :=
+  match l with
+  | nil => None
+  | (n, b) :: l =>
+      if string_dec name n && signature_eq sg (sig_of b)
+      then Some b
+      else lookup_builtin name sg l
+  end.
+
+Lemma lookup_builtin_sig: forall name sg b l,
+  lookup_builtin name sg l = Some b -> sig_of b = sg.
+Proof.
+  induction l as [ | [n b'] l ]; simpl; intros.
+- discriminate.
+- destruct (string_dec name n && signature_eq sg (sig_of b')) eqn:E.
++ InvBooleans. congruence.
++ auto.
+Qed.
+
+End LOOKUP.
+
+(** The standard, platform-independent built-ins *)
+
+Inductive standard_builtin : Type :=
+  | BI_select (t: typ)
+  | BI_fabs
+  | BI_fsqrt
+  | BI_negl
+  | BI_addl
+  | BI_subl
+  | BI_mull
+  | BI_i64_umulh
+  | BI_i64_smulh
+  | BI_i64_sdiv
+  | BI_i64_udiv
+  | BI_i64_smod
+  | BI_i64_umod
+  | BI_i64_shl
+  | BI_i64_shr
+  | BI_i64_sar
+  | BI_i64_dtos
+  | BI_i64_dtou
+  | BI_i64_stod
+  | BI_i64_utod
+  | BI_i64_stof
+  | BI_i64_utof.
+
+Local Open Scope string_scope.
+
+Definition standard_builtin_table : list (string * standard_builtin) :=
+    ("__builtin_sel", BI_select Tint)
+ :: ("__builtin_sel", BI_select Tlong)
+ :: ("__builtin_sel", BI_select Tfloat)
+ :: ("__builtin_sel", BI_select Tsingle)
+ :: ("__builtin_fabs", BI_fabs)
+ :: ("__builtin_fsqrt", BI_fsqrt)
+ :: ("__builtin_negl", BI_negl)
+ :: ("__builtin_addl", BI_addl)
+ :: ("__builtin_subl", BI_subl)
+ :: ("__builtin_mull", BI_mull)
+ :: ("__compcert_i64_umulh", BI_i64_umulh)
+ :: ("__compcert_i64_smulh", BI_i64_smulh)
+ :: ("__compcert_i64_sdiv", BI_i64_sdiv)
+ :: ("__compcert_i64_udiv", BI_i64_udiv)
+ :: ("__compcert_i64_smod", BI_i64_smod)
+ :: ("__compcert_i64_umod", BI_i64_umod)
+ :: ("__compcert_i64_shl", BI_i64_shl)
+ :: ("__compcert_i64_shr", BI_i64_shr)
+ :: ("__compcert_i64_sar", BI_i64_sar)
+ :: ("__compcert_i64_dtos", BI_i64_dtos)
+ :: ("__compcert_i64_dtou", BI_i64_dtou)
+ :: ("__compcert_i64_stod", BI_i64_stod)
+ :: ("__compcert_i64_utod", BI_i64_utod)
+ :: ("__compcert_i64_stof", BI_i64_stof)
+ :: ("__compcert_i64_utof", BI_i64_utof)
+ :: nil.
+
+Definition standard_builtin_sig (b: standard_builtin) : signature :=
+  match b with
+  | BI_select t =>
+      mksignature (Tint :: t :: t :: nil) (Some t) cc_default
+  | BI_fabs | BI_fsqrt =>
+      mksignature (Tfloat :: nil) (Some Tfloat) cc_default
+  | BI_negl =>
+      mksignature (Tlong :: nil) (Some Tlong) cc_default
+  | BI_addl | BI_subl | BI_i64_umulh| BI_i64_smulh 
+  | BI_i64_sdiv | BI_i64_udiv | BI_i64_smod | BI_i64_umod =>
+      mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default
+  | BI_mull =>
+      mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default
+  | BI_i64_shl  | BI_i64_shr | BI_i64_sar =>
+      mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default
+  | BI_i64_dtos | BI_i64_dtou =>
+      mksignature (Tfloat :: nil) (Some Tlong) cc_default
+  | BI_i64_stod | BI_i64_utod =>
+      mksignature (Tlong :: nil) (Some Tfloat) cc_default
+  | BI_i64_stof | BI_i64_utof =>
+      mksignature (Tlong :: nil) (Some Tsingle) cc_default
+  end.
+
+Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (proj_sig_res (standard_builtin_sig b)) :=
+  match b with
+  | BI_select t =>
+      mkbuiltin t 
+       (fun vargs => match vargs with
+          | Vint n :: v1 :: v2 :: nil => Some (Val.normalize (if Int.eq n Int.zero then v2 else v1) t)
+          | _ => None
+        end) _ _
+  | BI_fabs => mkbuiltin_n1t Tfloat Tfloat Float.abs
+  | BI_fsqrt => mkbuiltin_n1t Tfloat Tfloat Float.sqrt
+  | BI_negl => mkbuiltin_n1t Tlong Tlong Int64.neg
+  | BI_addl => mkbuiltin_v2t Tlong Val.addl _ _ 
+  | BI_subl => mkbuiltin_v2t Tlong Val.subl _ _
+  | BI_mull => mkbuiltin_v2t Tlong Val.mull' _ _
+  | BI_i64_umulh => mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhu
+  | BI_i64_smulh => mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhs
+  | BI_i64_sdiv => mkbuiltin_v2p Tlong Val.divls _ _
+  | BI_i64_udiv => mkbuiltin_v2p Tlong Val.divlu _ _
+  | BI_i64_smod => mkbuiltin_v2p Tlong Val.modls _ _
+  | BI_i64_umod => mkbuiltin_v2p Tlong Val.modlu _ _
+  | BI_i64_shl => mkbuiltin_v2t Tlong Val.shll _ _
+  | BI_i64_shr => mkbuiltin_v2t Tlong Val.shrlu _ _
+  | BI_i64_sar => mkbuiltin_v2t Tlong Val.shrl _ _
+  | BI_i64_dtos => mkbuiltin_n1p Tfloat Tlong Float.to_long
+  | BI_i64_dtou => mkbuiltin_n1p Tfloat Tlong Float.to_longu
+  | BI_i64_stod => mkbuiltin_n1t Tlong Tfloat Float.of_long
+  | BI_i64_utod => mkbuiltin_n1t Tlong Tfloat Float.of_longu
+  | BI_i64_stof => mkbuiltin_n1t Tlong Tsingle Float32.of_long
+  | BI_i64_utof => mkbuiltin_n1t Tlong Tsingle Float32.of_longu
+  end.
+Next Obligation. 
+  red. destruct vl; auto. destruct v; auto. 
+  destruct vl; auto. destruct vl; auto. destruct vl; auto.
+  apply Val.normalize_type.
+Qed.
+Next Obligation.
+  red. inv H; auto. inv H0; auto. inv H1; auto. inv H0; auto. inv H2; auto.
+  apply Val.normalize_inject. destruct (Int.eq i Int.zero); auto.
+Qed.
+Next Obligation.
+  unfold Val.addl, Val.has_type; destruct v1; auto; destruct v2; auto; destruct Archi.ptr64; auto.
+Qed.
+Next Obligation.
+  apply Val.addl_inject; auto.
+Qed.   
+Next Obligation.
+  unfold Val.subl, Val.has_type, negb; destruct v1; auto; destruct v2; auto;
+  destruct Archi.ptr64; auto; destruct (eq_block b0 b1); auto.
+Qed.
+Next Obligation.
+  apply Val.subl_inject; auto.
+Qed.
+Next Obligation.
+  unfold Val.mull', Val.has_type; destruct v1; simpl; auto; destruct v2; auto.
+Qed.
+Next Obligation.
+  inv H; simpl; auto. inv H0; auto.
+Qed.
+Next Obligation.
+  red. destruct v1; simpl; auto. destruct v2; auto. destruct orb; exact I.
+Qed.
+Next Obligation.
+  red. inv H; simpl; auto. inv H0; auto. destruct orb; auto.
+Qed.
+Next Obligation.
+  red. destruct v1; simpl; auto. destruct v2; auto. destruct Int64.eq; exact I.
+Qed.
+Next Obligation.
+  red. inv H; simpl; auto. inv H0; auto. destruct Int64.eq; auto.
+Qed.
+Next Obligation.
+  red. destruct v1; simpl; auto. destruct v2; auto. destruct orb; exact I.
+Qed.
+Next Obligation.
+  red. inv H; simpl; auto. inv H0; auto. destruct orb; auto.
+Qed.
+Next Obligation.
+  red. destruct v1; simpl; auto. destruct v2; auto. destruct Int64.eq; exact I.
+Qed.
+Next Obligation.
+  red. inv H; simpl; auto. inv H0; auto. destruct Int64.eq; auto.
+Qed.
+Next Obligation.
+  red. destruct v1; simpl; auto. destruct v2; auto. destruct Int.ltu; auto.
+Qed.
+Next Obligation.
+  inv H; simpl; auto. inv H0; auto. destruct Int.ltu; auto.
+Qed.
+Next Obligation.
+  red. destruct v1; simpl; auto. destruct v2; auto. destruct Int.ltu; auto.
+Qed.
+Next Obligation.
+  inv H; simpl; auto. inv H0; auto. destruct Int.ltu; auto.
+Qed.
+Next Obligation.
+  red. destruct v1; simpl; auto. destruct v2; auto. destruct Int.ltu; auto.
+Qed.
+Next Obligation.
+  inv H; simpl; auto. inv H0; auto. destruct Int.ltu; auto.
+Qed.
+
diff --git a/common/Events.v b/common/Events.v
index 26dd505f..3fb84f49 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -24,6 +24,7 @@ Require Import Floats.
 Require Import Values.
 Require Import Memory.
 Require Import Globalenvs.
+Require Import Builtins.
 
 (** * Events and traces *)
 
@@ -1377,12 +1378,67 @@ Proof.
   split. constructor. auto.
 Qed.
 
+(** ** Semantics of known built-in functions. *)
+
+(** Some built-in functions and runtime support functions have known semantics
+  as defined in the [Builtin] modules.
+  These built-in functions have no observable effects and do not access memory. *)
+
+Inductive known_builtin_sem (bf: builtin_function) (ge: Senv.t):
+              list val -> mem -> trace -> val -> mem -> Prop :=
+  | known_builtin_sem_intro: forall vargs vres m,
+      builtin_function_sem bf vargs = Some vres ->
+      known_builtin_sem bf ge vargs m E0 vres m.
+
+Lemma known_builtin_ok: forall bf,
+  extcall_properties (known_builtin_sem bf) (builtin_function_sig bf).
+Proof.
+  intros. set (bsem := builtin_function_sem bf). constructor; intros.
+(* well typed *)
+- inv H.
+  specialize (bs_well_typed  _ bsem vargs). unfold val_opt_has_type, bsem; rewrite H0.
+  auto.
+(* symbols *)
+- inv H0. econstructor; eauto.
+(* valid blocks *)
+- inv H; auto.
+(* perms *)
+- inv H; auto.
+(* readonly *)
+- inv H. apply Mem.unchanged_on_refl.
+(* mem extends *)
+- inv H. fold bsem in H2. apply val_inject_list_lessdef in H1.
+  specialize (bs_inject _ bsem _ _ _ H1).
+  unfold val_opt_inject; rewrite H2; intros.
+  destruct (bsem vargs') as [vres'|] eqn:?; try contradiction.
+  exists vres', m1'; intuition auto using Mem.extends_refl, Mem.unchanged_on_refl.
+  constructor; auto.
+  apply val_inject_lessdef; auto.
+(* mem injects *)
+- inv H0. fold bsem in H3.
+  specialize (bs_inject _ bsem _ _ _ H2).
+  unfold val_opt_inject; rewrite H3; intros.
+  destruct (bsem vargs') as [vres'|] eqn:?; try contradiction.
+  exists f, vres', m1'; intuition auto using Mem.extends_refl, Mem.unchanged_on_refl.
+  constructor; auto.
+  red; intros; congruence.
+(* trace length *)
+- inv H; simpl; omega.
+(* receptive *)
+- inv H; inv H0. exists vres1, m1; constructor; auto. 
+(* determ *)
+- inv H; inv H0.
+  split. constructor. intuition congruence. 
+Qed.
+
 (** ** Semantics of external functions. *)
 
-(** For functions defined outside the program ([EF_external],
-  [EF_builtin] and [EF_runtime]), we do not define their
-  semantics, but only assume that it satisfies
-  [extcall_properties]. *)
+(** For functions defined outside the program ([EF_external]),
+  we do not define their semantics, but only assume that it satisfies
+  [extcall_properties].
+  We do the same for built-in functions and runtime support functions that
+  are not described in [Builtins].
+*)
 
 Parameter external_functions_sem: String.string -> signature -> extcall_sem.
 
@@ -1398,6 +1454,22 @@ Axiom inline_assembly_properties:
 
 (** ** Combined semantics of external calls *)
 
+Definition builtin_or_external_sem name sg :=
+  match lookup_builtin_function name sg with
+  | Some bf => known_builtin_sem bf
+  | None => external_functions_sem name sg
+  end.
+
+Lemma builtin_or_external_sem_ok: forall name sg,
+  extcall_properties (builtin_or_external_sem name sg) sg.
+Proof.
+  unfold builtin_or_external_sem; intros. 
+  destruct (lookup_builtin_function name sg) as [bf|] eqn:L.
+- exploit lookup_builtin_function_sig; eauto. intros EQ; subst sg.
+  apply known_builtin_ok.
+- apply external_functions_properties.
+Qed.
+
 (** Combining the semantics given above for the various kinds of external calls,
   we define the predicate [external_call] that relates:
 - the external function being invoked
@@ -1412,8 +1484,8 @@ This predicate is used in the semantics of all CompCert languages. *)
 Definition external_call (ef: external_function): extcall_sem :=
   match ef with
   | EF_external name sg  => external_functions_sem name sg
-  | EF_builtin name sg   => external_functions_sem name sg
-  | EF_runtime name sg   => external_functions_sem name sg
+  | EF_builtin name sg   => builtin_or_external_sem name sg
+  | EF_runtime name sg   => builtin_or_external_sem name sg
   | EF_vload chunk       => volatile_load_sem chunk
   | EF_vstore chunk      => volatile_store_sem chunk
   | EF_malloc            => extcall_malloc_sem
@@ -1431,8 +1503,8 @@ Theorem external_call_spec:
 Proof.
   intros. unfold external_call, ef_sig; destruct ef.
   apply external_functions_properties.
-  apply external_functions_properties.
-  apply external_functions_properties.
+  apply builtin_or_external_sem_ok.
+  apply builtin_or_external_sem_ok.
   apply volatile_load_ok.
   apply volatile_store_ok.
   apply extcall_malloc_ok.
diff --git a/powerpc/Builtins1.v b/powerpc/Builtins1.v
new file mode 100644
index 00000000..f6e643d2
--- /dev/null
+++ b/powerpc/Builtins1.v
@@ -0,0 +1,33 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, Collège de France and Inria Paris            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Platform-specific built-in functions *)
+
+Require Import String Coqlib.
+Require Import AST Integers Floats Values.
+Require Import Builtins0.
+
+Inductive platform_builtin : Type := .
+
+Local Open Scope string_scope.
+
+Definition platform_builtin_table : list (string * platform_builtin) :=
+  nil.
+
+Definition platform_builtin_sig (b: platform_builtin) : signature :=
+  match b with end.
+
+Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) :=
+  match b with end.
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index 24aeb531..ba6612e8 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -38,11 +38,8 @@
 
 Require Import Coqlib.
 Require Import Compopts.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Op.
-Require Import CminorSel.
+Require Import AST Integers Floats Builtins.
+Require Import Op CminorSel.
 Require Archi.
 
 Local Open Scope cminorsel_scope.
@@ -566,3 +563,8 @@ Nondetfunction builtin_arg (e: expr) :=
   | Eop Oadd (e1:::e2:::Enil) => BA_addptr (BA e1) (BA e2)
   | _ => BA e
   end.
+
+(** Platform-specific known builtins *)
+
+Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
+  None.
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 5d7cd52b..1f23f4bd 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -13,17 +13,10 @@
 (** Correctness of instruction selection for operators *)
 
 Require Import Coqlib.
-Require Import Maps.
+Require Import AST Integers Floats.
+Require Import Values Memory Builtins Globalenvs.
+Require Import Cminor Op CminorSel.
 Require Import Compopts.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Cminor.
-Require Import Op.
-Require Import CminorSel.
 Require Import SelectOp.
 
 Local Open Scope cminorsel_scope.
@@ -1065,4 +1058,16 @@ Proof.
 - constructor; auto.
 Qed.
 
+(** Platform-specific known builtins *)
+
+Theorem eval_platform_builtin:
+  forall bf al a vl v le,
+  platform_builtin bf al = Some a ->
+  eval_exprlist ge sp e m le al vl ->
+  platform_builtin_sem bf vl = Some v ->
+  exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'.
+Proof.
+  intros. discriminate.
+Qed.
+
 End CMCONSTR.
diff --git a/riscV/Builtins1.v b/riscV/Builtins1.v
new file mode 100644
index 00000000..f6e643d2
--- /dev/null
+++ b/riscV/Builtins1.v
@@ -0,0 +1,33 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, Collège de France and Inria Paris            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Platform-specific built-in functions *)
+
+Require Import String Coqlib.
+Require Import AST Integers Floats Values.
+Require Import Builtins0.
+
+Inductive platform_builtin : Type := .
+
+Local Open Scope string_scope.
+
+Definition platform_builtin_table : list (string * platform_builtin) :=
+  nil.
+
+Definition platform_builtin_sig (b: platform_builtin) : signature :=
+  match b with end.
+
+Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) :=
+  match b with end.
diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp
index 760f06af..99806006 100644
--- a/riscV/SelectOp.vp
+++ b/riscV/SelectOp.vp
@@ -44,11 +44,8 @@
 Require Archi.
 Require Import Coqlib.
 Require Import Compopts.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Op.
-Require Import CminorSel.
+Require Import AST Integers Floats Builtins.
+Require Import Op CminorSel.
 
 Local Open Scope cminorsel_scope.
 
@@ -454,3 +451,8 @@ Nondetfunction builtin_arg (e: expr) :=
       if Archi.ptr64 then BA_addptr (BA e1) (BA_long n) else BA e
   | _ => BA e
   end.
+
+(** Platform-specific known builtins *)
+
+Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
+  None.
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index d0e6979c..18bc5dfe 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -17,18 +17,10 @@
 
 (** Correctness of instruction selection for operators *)
 
-Require Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import Zbits.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Cminor.
-Require Import Op.
-Require Import CminorSel.
+Require Import Coqlib Zbits.
+Require Import AST Integers Floats.
+Require Import Values Memory Builtins Globalenvs.
+Require Import Cminor Op CminorSel.
 Require Import SelectOp.
 
 Local Open Scope cminorsel_scope.
@@ -937,4 +929,16 @@ Proof.
 - constructor; auto.
 Qed.
 
+(** Platform-specific known builtins *)
+
+Theorem eval_platform_builtin:
+  forall bf al a vl v le,
+  platform_builtin bf al = Some a ->
+  eval_exprlist ge sp e m le al vl ->
+  platform_builtin_sem bf vl = Some v ->
+  exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'.
+Proof.
+  intros. discriminate.
+Qed.
+
 End CMCONSTR.
diff --git a/x86/Builtins1.v b/x86/Builtins1.v
new file mode 100644
index 00000000..6103cc4c
--- /dev/null
+++ b/x86/Builtins1.v
@@ -0,0 +1,54 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, Collège de France and Inria Paris            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Platform-specific built-in functions *)
+
+Require Import String Coqlib.
+Require Import AST Integers Floats Values.
+Require Import Builtins0.
+
+Inductive platform_builtin : Type :=
+  | BI_fmin
+  | BI_fmax.
+
+Local Open Scope string_scope.
+
+Definition platform_builtin_table : list (string * platform_builtin) :=
+     ("__builtin_fmin", BI_fmin)
+  :: ("__builtin_fmax", BI_fmax)
+  :: nil.
+
+Definition platform_builtin_sig (b: platform_builtin) : signature :=
+  match b with
+  | BI_fmin | BI_fmax =>
+      mksignature (Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default
+  end.
+
+Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) :=
+  match b with
+  | BI_fmin =>
+      mkbuiltin_n2t Tfloat Tfloat Tfloat
+        (fun f1 f2 => match Float.compare f1 f2 with
+                      | Some Eq | Some Lt => f1
+                      | Some Gt | None => f2
+                      end)
+  | BI_fmax =>
+      mkbuiltin_n2t Tfloat Tfloat Tfloat
+        (fun f1 f2 => match Float.compare f1 f2 with
+                      | Some Eq | Some Gt => f1
+                      | Some Lt | None => f2
+                      end)
+  end.
+
diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp
index cf0f37ec..378590ce 100644
--- a/x86/SelectOp.vp
+++ b/x86/SelectOp.vp
@@ -38,7 +38,7 @@
 
 Require Import Coqlib.
 Require Import Compopts.
-Require Import AST Integers Floats.
+Require Import AST Integers Floats Builtins.
 Require Import Op CminorSel.
 
 Local Open Scope cminorsel_scope.
@@ -568,3 +568,8 @@ Nondetfunction builtin_arg (e: expr) :=
   | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs
   | _ => BA e
   end.
+
+(** Platform-specific known builtins *)
+
+Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
+  None.
diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v
index b412ccf7..821a54e8 100644
--- a/x86/SelectOpproof.v
+++ b/x86/SelectOpproof.v
@@ -13,15 +13,9 @@
 (** Correctness of instruction selection for operators *)
 
 Require Import Coqlib.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Cminor.
-Require Import Op.
-Require Import CminorSel.
+Require Import AST Integers Floats.
+Require Import Values Memory Builtins Globalenvs.
+Require Import Cminor Op CminorSel.
 Require Import SelectOp.
 
 Local Open Scope cminorsel_scope.
@@ -1010,4 +1004,16 @@ Proof.
 - constructor; auto.
 Qed.
 
+(** Platform-specific known builtins *)
+
+Theorem eval_platform_builtin:
+  forall bf al a vl v le,
+  platform_builtin bf al = Some a ->
+  eval_exprlist ge sp e m le al vl ->
+  platform_builtin_sem bf vl = Some v ->
+  exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'.
+Proof.
+  intros. discriminate.
+Qed.
+
 End CMCONSTR.