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.

3 files changed, 231 insertions, 112 deletions

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: