Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-load

19 files changed, 439 insertions, 134 deletions

diff --git a/backend/CSE.v b/backend/CSE.v
index aaaf492c..9da30f50 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -14,7 +14,7 @@
   proceeds by value numbering over extended basic blocks. *)
 
 Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
-Require Import AST Linking.
+Require Import AST Linking Builtins.
 Require Import Values Memory.
 Require Import Op Registers RTL.
 Require Import ValueDomain ValueAnalysis CSEdomain CombineOp.
@@ -444,10 +444,10 @@ Module Solver := BBlock_solver(Numbering).
   ([EF_external], [EF_runtime], [EF_malloc], [EF_free]).
 - Forget equations involving loads but keep equations over registers.
   This is appropriate for builtins that can modify memory,
-  e.g. volatile stores, or [EF_builtin]
+  e.g. volatile stores, or [EF_builtin] for unknown builtin functions.
 - Keep all equations, taking advantage of the fact that neither memory
-  nor registers are modified.  This is appropriate for annotations
-  and for volatile loads.
+  nor registers are modified.  This is appropriate for annotations,
+  volatile loads, and known builtin functions.
 *)
 
 Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numbering) :=
@@ -473,8 +473,13 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb
           match ef with
           | EF_external _ _ | EF_runtime _ _ | EF_malloc | EF_free | EF_inline_asm _ _ _ =>
               empty_numbering
-          | EF_builtin _ _ | EF_vstore _ =>
+          | EF_vstore _ =>
               set_res_unknown (kill_all_loads before) res
+          | EF_builtin name sg =>
+              match lookup_builtin_function name sg with
+              | Some bf => set_res_unknown before res
+              | None    => set_res_unknown (kill_all_loads before) res
+              end
           | EF_memcpy sz al =>
               match args with
               | dst :: src :: nil =>
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index a60c316b..03c7ecfc 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -14,7 +14,7 @@
 
 Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
 Require Import AST Linking.
-Require Import Values Memory Events Globalenvs Smallstep.
+Require Import Values Memory Builtins Events Globalenvs Smallstep.
 Require Import Op Registers RTL.
 Require Import ValueDomain ValueAOp ValueAnalysis.
 Require Import CSEdomain CombineOp CombineOpproof CSE.
@@ -1129,7 +1129,9 @@ Proof.
   { exists valu. apply set_res_unknown_holds. eapply kill_all_loads_hold; eauto. }
   destruct ef.
   + apply CASE1.
-  + apply CASE3.
+  + destruct (lookup_builtin_function name sg) as [bf|] eqn:LK.
+    ++ apply CASE2. simpl in H1; red in H1; rewrite LK in H1; inv H1. auto.
+    ++ apply CASE3.
   + apply CASE1.
   + apply CASE2; inv H1; auto.
   + apply CASE3.
diff --git a/backend/Constprop.v b/backend/Constprop.v
index b68f4cae..cf1a9171 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -15,7 +15,7 @@
   and the corresponding code rewriting. *)
 
 Require Import Coqlib Maps Integers Floats Lattice Kildall.
-Require Import AST Linking.
+Require Import AST Linking Builtins.
 Require Compopts Machregs.
 Require Import Op Registers RTL.
 Require Import Liveness ValueDomain ValueAOp ValueAnalysis.
@@ -139,6 +139,30 @@ Definition builtin_strength_reduction
   | _ => builtin_args_strength_reduction ae al (Machregs.builtin_constraints ef)
   end.
 
+(*
+Definition transf_builtin
+             (ae: AE.t) (am: amem) (rm: romem)
+             (ef: external_function)
+             (args: list (builtin_arg reg)) (res: builtin_res reg) (s: node) :=
+  let dfl := Ibuiltin ef (builtin_strength_reduction ae ef args) res s in
+  match ef, res with
+  | EF_builtin name sg, BR rd =>
+      match lookup_builtin_function name sg with
+      | Some bf => 
+          match eval_static_builtin_function ae am rm bf args with
+          | Some a =>
+              match const_for_result a with
+              | Some cop => Iop cop nil rd s
+              | None => dfl
+              end
+          | None => dfl
+          end
+      | None => dfl
+      end
+  | _, _ => dfl
+  end.
+*)
+
 Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem)
                         (pc: node) (instr: instruction) :=
   match an!!pc with
@@ -176,7 +200,23 @@ Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem)
       | Itailcall sig ros args =>
           Itailcall sig (transf_ros ae ros) args
       | Ibuiltin ef args res s =>
-          Ibuiltin ef (builtin_strength_reduction ae ef args) res s
+          let dfl := Ibuiltin ef (builtin_strength_reduction ae ef args) res s in
+          match ef, res with
+          | EF_builtin name sg, BR rd =>
+              match lookup_builtin_function name sg with
+              | Some bf => 
+                  match eval_static_builtin_function ae am rm bf args with
+                  | Some a =>
+                      match const_for_result a with
+                      | Some cop => Iop cop nil rd s
+                      | None => dfl
+                      end
+                 | None => dfl
+                 end
+             | None => dfl
+             end
+          | _, _ => dfl
+          end
       | Icond cond args s1 s2 =>
           let aargs := aregs ae args in
           match resolve_branch (eval_static_condition cond aargs) with
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index e28519ca..a5d08a0f 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -14,7 +14,7 @@
 
 Require Import Coqlib Maps Integers Floats Lattice Kildall.
 Require Import AST Linking.
-Require Import Values Events Memory Globalenvs Smallstep.
+Require Import Values Builtins Events Memory Globalenvs Smallstep.
 Require Compopts Machregs.
 Require Import Op Registers RTL.
 Require Import Liveness ValueDomain ValueAOp ValueAnalysis.
@@ -474,19 +474,41 @@ Proof.
 - (* Ibuiltin *)
   rename pc'0 into pc. TransfInstr; intros.
 Opaque builtin_strength_reduction.
-  exploit builtin_strength_reduction_correct; eauto. intros (vargs' & P & Q).
-  exploit (@eval_builtin_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)).
+  set (dfl := Ibuiltin ef (builtin_strength_reduction ae ef args) res pc') in *.
+  set (rm := romem_for cu) in *.
+  assert (DFL: (fn_code (transf_function rm f))!pc = Some dfl ->
+          exists (n2 : nat) (s2' : state),
+            step tge
+             (State s' (transf_function rm f) (Vptr sp0 Ptrofs.zero) pc rs' m'0) t s2' /\
+            match_states n2
+             (State s f (Vptr sp0 Ptrofs.zero) pc' (regmap_setres res vres rs) m') s2').
+  {
+    exploit builtin_strength_reduction_correct; eauto. intros (vargs' & P & Q).
+    exploit (@eval_builtin_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)).
     apply REGS. eauto. eexact P.
-  intros (vargs'' & U & V).
-  exploit external_call_mem_extends; eauto.
-  intros [v' [m2' [A [B [C D]]]]].
+    intros (vargs'' & U & V).
+    exploit external_call_mem_extends; eauto.
+    intros (v' & m2' & A & B & C & D).
+    econstructor; econstructor; split.
+    eapply exec_Ibuiltin; eauto.
+    eapply eval_builtin_args_preserved. eexact symbols_preserved. eauto.
+    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+    eapply match_states_succ; eauto.
+    apply set_res_lessdef; auto.
+  }
+  destruct ef; auto.
+  destruct res; auto.
+  destruct (lookup_builtin_function name sg) as [bf|] eqn:LK; auto.
+  destruct (eval_static_builtin_function ae am rm bf args) as [a|] eqn:ES; auto.
+  destruct (const_for_result a) as [cop|] eqn:CR; auto.
+  clear DFL. simpl in H1; red in H1; rewrite LK in H1; inv H1.
+  exploit const_for_result_correct; eauto. 
+  eapply eval_static_builtin_function_sound; eauto.
+  intros (v' & A & B).
   left; econstructor; econstructor; split.
-  eapply exec_Ibuiltin; eauto.
-  eapply eval_builtin_args_preserved. eexact symbols_preserved. eauto.
-  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+  eapply exec_Iop; eauto.
   eapply match_states_succ; eauto.
-  apply set_res_lessdef; auto.
-
+  apply set_reg_lessdef; auto.
 - (* Icond, preserved *)
   rename pc'0 into pc. TransfInstr.
   set (ac := eval_static_condition cond (aregs ae args)).
diff --git a/backend/Conventions.v b/backend/Conventions.v
index 989bfa05..6025c6b4 100644
--- a/backend/Conventions.v
+++ b/backend/Conventions.v
@@ -128,8 +128,6 @@ Definition callee_save_loc (l: loc) :=
   | S sl ofs ty => sl <> Outgoing
   end.
 
-Hint Unfold callee_save_loc.
-
 Definition agree_callee_save (ls1 ls2: Locmap.t) : Prop :=
   forall l, callee_save_loc l -> ls1 l = ls2 l.
 
diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
index 46d5c3f1..902724e0 100644
--- a/backend/Linearizeaux.ml
+++ b/backend/Linearizeaux.ml
@@ -106,7 +106,7 @@ let flatten_blocks blks =
   let cmp_minpc (mpc1, _) (mpc2, _) =
     if mpc1 = mpc2 then 0 else if mpc1 > mpc2 then -1 else 1
   in
-    List.flatten (List.map Pervasives.snd (List.sort cmp_minpc blks))
+    List.flatten (List.map snd (List.sort cmp_minpc blks))
 
 (* Build the enumeration *)
 
diff --git a/backend/OpHelpersproof.v b/backend/OpHelpersproof.v
index 63040c5f..08da8a36 100644
--- a/backend/OpHelpersproof.v
+++ b/backend/OpHelpersproof.v
@@ -75,4 +75,4 @@ Definition helper_functions_declared {F V: Type} (p: AST.program (AST.fundef F)
   /\ helper_declared p i32_umod "__compcert_i32_umod" sig_ii_i
   /\ helper_declared p f32_div  "__compcert_f32_div"  sig_ss_s
   /\ helper_declared p f64_div  "__compcert_f64_div"  sig_ff_f
-.
+.
\ No newline at end of file
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index dd428808..155f5e55 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -13,7 +13,6 @@
 
 open AST
 open Camlcoq
-open DwarfPrinter
 open PrintAsmaux
 open Printf
 open Sections
@@ -177,7 +176,7 @@ module Printer(Target:TARGET) =
         let address = Target.address
       end
 
-    module DebugPrinter = DwarfPrinter (DwarfTarget)
+    module DebugPrinter = DwarfPrinter.DwarfPrinter (DwarfTarget)
   end
 
 let print_program oc p =
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 7e075f04..8652b2c5 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -245,14 +245,15 @@ let print_debug_info comment print_line preg_string sp_name oc kind txt args =
 
 (** Inline assembly *)
 
-let print_asm_argument print_preg oc modifier = function
-  | BA r -> print_preg oc r
+let print_asm_argument print_preg oc modifier typ = function 
+  | BA r -> print_preg oc typ r
   | BA_splitlong(BA hi, BA lo) ->
       begin match modifier with
-      | "R" -> print_preg oc hi
-      | "Q" -> print_preg oc lo
-      |  _  -> fprintf oc "%a:%a" print_preg hi print_preg lo
-                  (* Probably not what was intended *)
+      | "R" -> print_preg oc Tint hi
+      | "Q" -> print_preg oc Tint lo
+      |  _  -> print_preg oc Tint hi; fprintf oc ":"; print_preg oc Tint lo
+               (* This case (printing a split long in full) should never
+                  happen because of the checks done in ExtendedAsm.ml *)
       end
   | _ -> failwith "bad asm argument"
 
@@ -265,8 +266,10 @@ let re_asm_param_1 = Str.regexp "%%\\|%[QR]?[0-9]+"
 let re_asm_param_2 = Str.regexp "%\\([QR]?\\)\\([0-9]+\\)"
 
 let print_inline_asm print_preg oc txt sg args res =
-  let operands =
-    if sg.sig_res = None then args else builtin_arg_of_res res :: args in
+  let (operands, ty_operands) =
+    match sg.sig_res with
+    | None -> (args, sg.sig_args)
+    | Some tres -> (builtin_arg_of_res res :: args, tres :: sg.sig_args) in
   let print_fragment = function
   | Str.Text s ->
       output_string oc s
@@ -277,7 +280,9 @@ let print_inline_asm print_preg oc txt sg args res =
       let modifier = Str.matched_group 1 s
       and number = int_of_string (Str.matched_group 2 s) in
       try
-        print_asm_argument print_preg oc modifier (List.nth operands number)
+        print_asm_argument print_preg oc modifier
+                           (List.nth ty_operands number)
+                           (List.nth operands number)
       with Failure _ ->
         fprintf oc "<bad parameter %s>" s in
   List.iter print_fragment (Str.full_split re_asm_param_1 txt);
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index f68c1267..8c255a65 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -16,7 +16,7 @@
 (** Pretty-printer for Cminor *)
 
 open Format
-open Camlcoq
+open !Camlcoq
 open Integers
 open AST
 open PrintAST
diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml
index d0557073..1c449e74 100644
--- a/backend/PrintLTL.ml
+++ b/backend/PrintLTL.ml
@@ -112,7 +112,7 @@ let print_function pp id f =
   fprintf pp "%s() {\n" (extern_atom id);
   let instrs =
     List.sort
-      (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1)
+      (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
       (List.rev_map
         (fun (pc, i) -> (P.to_int pc, i))
         (PTree.elements f.fn_code)) in
diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml
index ba336b0a..841540b6 100644
--- a/backend/PrintRTL.ml
+++ b/backend/PrintRTL.ml
@@ -93,7 +93,7 @@ let print_function pp id f =
   fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params;
   let instrs =
     List.sort
-      (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1)
+      (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
       (List.rev_map
         (fun (pc, i) -> (P.to_int pc, i))
         (PTree.elements f.fn_code)) in
diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml
index cc1f7d49..6432682a 100644
--- a/backend/PrintXTL.ml
+++ b/backend/PrintXTL.ml
@@ -138,7 +138,7 @@ let print_function pp ?alloc ?live f =
   fprintf pp "f() {\n";
   let instrs =
     List.sort
-      (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1)
+      (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
       (List.map
         (fun (pc, i) -> (P.to_int pc, i))
         (PTree.elements f.fn_code)) in
diff --git a/backend/Selection.v b/backend/Selection.v
index 2d407094..4ab3331e 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 OpHelpers 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,16 +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)))
-      (* sel_builtin_default optid ef args *)
-         (* THIS IS WHERE TO ACTIVATE OUR OWN BUILTINS
-            change sel_builtin_default to sel_builtin *)
+      | 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/Selectionaux.ml b/backend/Selectionaux.ml
index 4e366564..574c31f0 100644
--- a/backend/Selectionaux.ml
+++ b/backend/Selectionaux.ml
@@ -80,10 +80,10 @@ let fast_cmove ty =
   | a, m -> failwith (Printf.sprintf "fast_cmove: unknown arch %s %s" a m)
 
 (* The if-conversion heuristic depend on the
-   -fif-conversion and -ffavor-branchless flags.
+   -fif-conversion and -Obranchless flags.
 
 With [-fno-if-conversion] or [-0O], if-conversion is turned off entirely.
-With [-ffavor-branchless], if-conversion is performed whenever semantically
+With [-Obranchless], if-conversion is performed whenever semantically
 correct, regardless of how much it could cost.
 Otherwise (and by default), optimization is performed when it seems beneficial.
 
@@ -96,22 +96,17 @@ If-conversion seems beneficial if:
 Intuition: on a modern processor, the "then" and the "else" branches
 can generally be computed in parallel, there is enough ILP for that.
 So, the bad case is if the most taken branch is much cheaper than the
-<<<<<<< HEAD
-other branch.  Since our cost estimates are very imprecise, the
-bound on the total cost acts as a safety guard, 
-=======
 other branch.  Another bad case is if both branches are big: since the
 code for one branch precedes entirely the code for the other branch,
 if the first branch contains a lot of instructions,
 dynamic reordering of instructions will not look ahead far enough
 to execute instructions from the other branch in parallel with
 instructions from the first branch.
->>>>>>> ddb2c968e6c57d2117434f169471d87f643d831a
 *)
 
 let if_conversion_heuristic cond ifso ifnot ty =
   if not !Clflags.option_fifconversion then false else
-  if !Clflags.option_ffavor_branchless then true else
+  if !Clflags.option_Obranchless then true else
   if not (fast_cmove ty) then false else
   let c1 = cost_expr ifso and c2 = cost_expr ifnot in
   c1 + c2 <= 24 && abs (c1 - c2) <= 8
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 40db5d4b..8a827af2 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 OpHelpers OpHelpersproof.
 Require Import SelectOp SelectDiv SplitLong SelectLong Selection.
@@ -217,19 +218,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:
@@ -354,6 +352,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 *)
@@ -794,6 +838,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:
@@ -983,19 +1072,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)
@@ -1003,11 +1091,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',
@@ -1079,6 +1167,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' ->
@@ -1094,8 +1190,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] | ];
@@ -1189,9 +1288,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.
@@ -1208,12 +1305,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.
@@ -1304,11 +1397,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.
@@ -1316,7 +1406,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 6718ba5b..c8e3b94c 100644
--- a/backend/SplitLongproof.v
+++ b/backend/SplitLongproof.v
@@ -15,13 +15,16 @@
 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 OpHelpers OpHelpersproof.
+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.
 
+(** * Properties of the helper functions *)
+
 (** * Correctness of the instruction selection functions for 64-bit operators *)
 
 Section CMCONSTR.
@@ -38,56 +41,64 @@ Ltac UseHelper := decompose [Logic.and] arith_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 :=
@@ -336,9 +347,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.
@@ -360,7 +372,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:
@@ -370,7 +382,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:
@@ -379,8 +391,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:
@@ -389,8 +402,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:
@@ -427,8 +441,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:
@@ -437,8 +452,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.
@@ -565,7 +581,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.
@@ -576,7 +594,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:
@@ -610,7 +628,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.
@@ -621,7 +641,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:
@@ -659,7 +679,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.
@@ -670,7 +692,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.
@@ -680,7 +702,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.
@@ -703,7 +725,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.
@@ -734,7 +756,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.
@@ -782,14 +804,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:
@@ -831,7 +853,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:
@@ -842,7 +864,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:
@@ -853,7 +875,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:
@@ -864,7 +886,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/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 605d7e90..5072448a 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -13,7 +13,7 @@
 Require Import FunInd.
 Require Import Coqlib Maps Integers Floats Lattice Kildall.
 Require Import Compopts AST Linking.
-Require Import Values Memory Globalenvs Events.
+Require Import Values Memory Globalenvs Builtins Events.
 Require Import Registers Op RTL.
 Require Import ValueDomain ValueAOp Liveness.
 
@@ -78,6 +78,15 @@ Definition transfer_builtin_default
   let (av, am') := analyze_call am (map (abuiltin_arg ae am rm) args) in
   VA.State (set_builtin_res res av ae) am'.
 
+Definition eval_static_builtin_function
+              (ae: aenv) (am: amem) (rm: romem)
+              (bf: builtin_function) (args: list (builtin_arg reg)) :=
+  match builtin_function_sem bf
+                 (map val_of_aval (map (abuiltin_arg ae am rm) args)) with
+  | Some v => aval_of_val v
+  | None => None
+  end.
+
 Definition transfer_builtin
               (ae: aenv) (am: amem) (rm: romem) (ef: external_function)
               (args: list (builtin_arg reg)) (res: builtin_res reg) :=
@@ -105,6 +114,15 @@ Definition transfer_builtin
   | EF_annot_val _ _ _, v :: nil =>
       let av := abuiltin_arg ae am rm v in
       VA.State (set_builtin_res res av ae) am
+  | EF_builtin name sg, _ =>
+      match lookup_builtin_function name sg with
+      | Some bf => 
+          match eval_static_builtin_function ae am rm bf args with
+          | Some av => VA.State (set_builtin_res res av ae) am
+          | None => transfer_builtin_default ae am rm args res
+          end
+      | None => transfer_builtin_default ae am rm args res
+      end
   | _, _ =>
       transfer_builtin_default ae am rm args res
   end.
@@ -372,6 +390,31 @@ Proof.
   intros. destruct res; simpl; auto. apply ematch_update; auto.
 Qed.
 
+Lemma eval_static_builtin_function_sound:
+  forall bc ge rs sp m ae rm am (bf: builtin_function) al vl v va,
+  ematch bc rs ae ->
+  romatch bc m rm ->
+  mmatch bc m am ->
+  genv_match bc ge ->
+  bc sp = BCstack ->
+  eval_builtin_args ge (fun r => rs#r) (Vptr sp Ptrofs.zero) m al vl ->
+  eval_static_builtin_function ae am rm bf al = Some va ->
+  builtin_function_sem bf vl = Some v ->
+  vmatch bc v va.
+Proof.
+  unfold eval_static_builtin_function; intros.
+  exploit abuiltin_args_sound; eauto. 
+  set (vla := map (abuiltin_arg ae am rm) al) in *. intros VMA.
+  destruct (builtin_function_sem bf (map val_of_aval vla)) as [v0|] eqn:A; try discriminate.
+  assert (LD: Val.lessdef v0 v).
+  { apply val_inject_lessdef.
+    exploit (bs_inject _ (builtin_function_sem bf)). 
+    apply val_inject_list_lessdef. eapply list_val_of_aval_sound; eauto.
+    rewrite A, H6; simpl. auto.
+  }
+  inv LD. apply aval_of_val_sound; auto. discriminate.
+Qed.
+
 (** ** Constructing block classifications *)
 
 Definition bc_nostack (bc: block_classification) : Prop :=
@@ -1343,6 +1386,13 @@ Proof.
   }
   unfold transfer_builtin in TR.
   destruct ef; auto.
++ (* builtin function *)
+  destruct (lookup_builtin_function name sg) as [bf|] eqn:LK; auto.
+  destruct (eval_static_builtin_function ae am rm bf args) as [av|] eqn:ES; auto.
+  simpl in H1. red in H1. rewrite LK in H1. inv H1.
+  eapply sound_succ_state; eauto. simpl; auto.
+  apply set_builtin_res_sound; auto.
+  eapply eval_static_builtin_function_sound; eauto.
 + (* volatile load *)
   inv H0; auto. inv H3; auto. inv H1.
   exploit abuiltin_arg_sound; eauto. intros VM1.
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index f6afa836..fd3bd5ae 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -13,7 +13,7 @@
 Require Import FunInd.
 Require Import Zwf Coqlib Maps Zbits Integers Floats Lattice.
 Require Import Compopts AST.
-Require Import Values Memory Globalenvs Events.
+Require Import Values Memory Globalenvs Builtins Events.
 Require Import Registers RTL.
 
 (** The abstract domains for value analysis *)
@@ -3038,7 +3038,47 @@ Proof with (auto using provenance_monotone with va).
 - destruct (zlt n 16)...
 Qed.
 
-(** Abstracting memory blocks *)
+(** Analysis of known builtin functions.  All we have is a dynamic semantics
+  as a function [list val -> option val], but we can still perform 
+  some constant propagation. *)
+
+Definition val_of_aval (a: aval) : val :=
+  match a with
+  | I n => Vint n
+  | L n => Vlong n
+  | F f => Vfloat f
+  | FS f => Vsingle f
+  | _ => Vundef
+  end.
+
+Definition aval_of_val (v: val) : option aval :=
+  match v with
+  | Vint n => Some (I n)
+  | Vlong n => Some (L n)
+  | Vfloat f => Some (F f)
+  | Vsingle f => Some (FS f)
+  | _ => None
+  end.
+
+Lemma val_of_aval_sound:
+  forall v a, vmatch v a -> Val.lessdef (val_of_aval a) v.
+Proof.
+  destruct 1; simpl; auto.
+Qed.
+
+Corollary list_val_of_aval_sound:
+  forall vl al, list_forall2 vmatch vl al -> Val.lessdef_list (map val_of_aval al) vl.
+Proof.
+  induction 1; simpl; constructor; auto using val_of_aval_sound.
+Qed.
+
+Lemma aval_of_val_sound:
+  forall v a, aval_of_val v = Some a -> vmatch v a. 
+Proof.
+  intros v a E; destruct v; simpl in E; inv E; constructor.
+Qed.
+
+(** * Abstracting memory blocks *)
 
 Inductive acontent : Type :=
  | ACval (chunk: memory_chunk) (av: aval).