Refactored Selection.v and Selectionproof.v into a machine-dependent part + a machine-independent part.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1125 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

2 files changed, 94 insertions, 766 deletions

diff --git a/arm/Selection.v b/arm/SelectOp.v
index 12cc1b27..8ac4ea51 100644
--- a/arm/Selection.v
+++ b/arm/SelectOp.v
@@ -10,7 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Instruction selection *)
+(** Instruction selection for operators *)
 
 (** The instruction selection pass recognizes opportunities for using
   combined arithmetic and logical operations and addressing modes
@@ -19,8 +19,22 @@
   and on the PowerPC, the expression [(x >> 6) & 0xFF] can be turned
   into a "rotate and mask" instruction.
 
-  Instruction selection proceeds by bottom-up rewriting over expressions.
-  The source language is Cminor and the target language is CminorSel. *)
+  This file defines functions for building CminorSel expressions and
+  statements, especially expressions consisting of operator
+  applications.  These functions examine their arguments to choose
+  cheaper forms of operators whenever possible.
+
+  For instance, [add e1 e2] will return a CminorSel expression semantically
+  equivalent to [Eop Oadd (e1 ::: e2 ::: Enil)], but will use a
+  [Oaddimm] operator if one of the arguments is an integer constant,
+  or suppress the addition altogether if one of the arguments is the
+  null integer.  In passing, we perform operator reassociation
+  ([(e + c1) * c2] becomes [(e * c2) + (c1 * c2)]) and a small amount
+  of constant propagation.
+
+  On top of the "smart constructor" functions defined below,
+  module [Selection] implements the actual instruction selection pass.
+*)
 
 Require Import Coqlib.
 Require Import Maps.
@@ -34,61 +48,7 @@ Require Cminor.
 Require Import Op.
 Require Import CminorSel.
 
-Infix ":::" := Econs (at level 60, right associativity) : selection_scope.
-
-Open Local Scope selection_scope.
-
-(** * Lifting of let-bound variables *)
-
-(** Some of the instruction functions generate [Elet] constructs to
-  share the evaluation of a subexpression.  Owing to the use of de
-  Bruijn indices for let-bound variables, we need to shift de Bruijn
-  indices when an expression [b] is put in a [Elet a b] context. *)
-
-Fixpoint lift_expr (p: nat) (a: expr) {struct a}: expr :=
-  match a with
-  | Evar id => Evar id
-  | Eop op bl => Eop op (lift_exprlist p bl)
-  | Eload chunk addr bl => Eload chunk addr (lift_exprlist p bl)
-  | Econdition b c d =>
-      Econdition (lift_condexpr p b) (lift_expr p c) (lift_expr p d)
-  | Elet b c => Elet (lift_expr p b) (lift_expr (S p) c)
-  | Eletvar n =>
-      if le_gt_dec p n then Eletvar (S n) else Eletvar n
-  end
-
-with lift_condexpr (p: nat) (a: condexpr) {struct a}: condexpr :=
-  match a with
-  | CEtrue => CEtrue
-  | CEfalse => CEfalse
-  | CEcond cond bl => CEcond cond (lift_exprlist p bl)
-  | CEcondition b c d =>
-      CEcondition (lift_condexpr p b) (lift_condexpr p c) (lift_condexpr p d)
-  end
-
-with lift_exprlist (p: nat) (a: exprlist) {struct a}: exprlist :=
-  match a with
-  | Enil => Enil
-  | Econs b cl => Econs (lift_expr p b) (lift_exprlist p cl)
-  end.
-
-Definition lift (a: expr): expr := lift_expr O a.
-
-(** * Smart constructors for operators *)
-
-(** This section defines functions for building CminorSel expressions
-  and statements, especially expressions consisting of operator
-  applications.  These functions examine their arguments to choose
-  cheaper forms of operators whenever possible.
-
-  For instance, [add e1 e2] will return a CminorSel expression semantically
-  equivalent to [Eop Oadd (e1 ::: e2 ::: Enil)], but will use a
-  [Oaddimm] operator if one of the arguments is an integer constant,
-  or suppress the addition altogether if one of the arguments is the
-  null integer.  In passing, we perform operator reassociation
-  ([(e + c1) * c2] becomes [(e * c2) + (c1 * c2)]) and a small amount
-  of constant propagation.
-*)
+Open Local Scope cminorsel_scope.
 
 (** ** Integer logical negation *)
 
@@ -1146,50 +1106,19 @@ Definition compu (c: comparison) (e1: expr) (e2: expr) :=
 Definition compf (c: comparison) (e1: expr) (e2: expr) :=
   Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil).
 
-(** ** Conditional expressions *)
-
-Fixpoint negate_condexpr (e: condexpr): condexpr :=
-  match e with
-  | CEtrue => CEfalse
-  | CEfalse => CEtrue
-  | CEcond c el => CEcond (negate_condition c) el
-  | CEcondition e1 e2 e3 =>
-      CEcondition e1 (negate_condexpr e2) (negate_condexpr e3)
-  end.
+(** ** Other operators, not optimized. *)
 
-
-Definition is_compare_neq_zero (c: condition) : bool :=
-  match c with
-  | Ccompimm Cne n => Int.eq n Int.zero
-  | Ccompuimm Cne n => Int.eq n Int.zero
-  | _ => false
-  end.
-
-Definition is_compare_eq_zero (c: condition) : bool :=
-  match c with
-  | Ccompimm Ceq n => Int.eq n Int.zero
-  | Ccompuimm Ceq n => Int.eq n Int.zero
-  | _ => false
-  end.
-
-Fixpoint condexpr_of_expr (e: expr) : condexpr :=
-  match e with
-  | Eop (Ointconst n) Enil =>
-      if Int.eq n Int.zero then CEfalse else CEtrue
-  | Eop (Ocmp c) (e1 ::: Enil) =>
-      if is_compare_neq_zero c then
-        condexpr_of_expr e1
-      else if is_compare_eq_zero c then
-        negate_condexpr (condexpr_of_expr e1)
-      else
-        CEcond c (e1 ::: Enil)
-  | Eop (Ocmp c) el =>
-      CEcond c el
-  | Econdition ce e1 e2 =>
-      CEcondition ce (condexpr_of_expr e1) (condexpr_of_expr e2)
-  | _ =>
-      CEcond (Ccompimm Cne Int.zero) (e:::Enil)
-  end.
+Definition negint (e: expr) := Eop (Orsubimm Int.zero) (e ::: Enil).
+Definition negf (e: expr) :=  Eop Onegf (e ::: Enil).
+Definition absf (e: expr) :=  Eop Oabsf (e ::: Enil).
+Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil).
+Definition intuoffloat (e: expr) := Eop Ointuoffloat (e ::: Enil).
+Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil).
+Definition floatofintu (e: expr) := Eop Ofloatofintu (e ::: Enil).
+Definition addf (e1 e2: expr) :=  Eop Oaddf (e1 ::: e2 ::: Enil).
+Definition subf (e1 e2: expr) :=  Eop Osubf (e1 ::: e2 ::: Enil).
+Definition mulf (e1 e2: expr) :=  Eop Omulf (e1 ::: e2 ::: Enil).
+Definition divf (e1 e2: expr) :=  Eop Odivf (e1 ::: e2 ::: Enil).
 
 (** ** Recognition of addressing modes for load and store operations *)
 
@@ -1264,131 +1193,3 @@ Definition addressing (chunk: memory_chunk) (e: expr) :=
       (Aindexed Int.zero, e:::Enil)
   end.
 
-Definition load (chunk: memory_chunk) (e1: expr) :=
-  match addressing chunk e1 with
-  | (mode, args) => Eload chunk mode args
-  end.
-
-Definition store (chunk: memory_chunk) (e1 e2: expr) :=
-  match addressing chunk e1 with
-  | (mode, args) => Sstore chunk mode args e2
-  end.
-
-(** * Translation from Cminor to CminorSel *)
-
-(** Instruction selection for operator applications *)
-
-Definition sel_constant (cst: Cminor.constant) : expr :=
-  match cst with
-  | Cminor.Ointconst n => Eop (Ointconst n) Enil
-  | Cminor.Ofloatconst f => Eop (Ofloatconst f) Enil
-  | Cminor.Oaddrsymbol id ofs => Eop (Oaddrsymbol id ofs) Enil
-  | Cminor.Oaddrstack ofs => Eop (Oaddrstack ofs) Enil
-  end.
-
-Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr :=
-  match op with
-  | Cminor.Ocast8unsigned => cast8unsigned arg 
-  | Cminor.Ocast8signed => cast8signed arg 
-  | Cminor.Ocast16unsigned => cast16unsigned arg 
-  | Cminor.Ocast16signed => cast16signed arg 
-  | Cminor.Onegint => Eop (Orsubimm Int.zero) (arg ::: Enil)
-  | Cminor.Onotbool => notbool arg
-  | Cminor.Onotint => notint arg
-  | Cminor.Onegf => Eop Onegf (arg ::: Enil)
-  | Cminor.Oabsf => Eop Oabsf (arg ::: Enil)
-  | Cminor.Osingleoffloat => singleoffloat arg
-  | Cminor.Ointoffloat => Eop Ointoffloat (arg ::: Enil)
-  | Cminor.Ointuoffloat => Eop Ointuoffloat (arg ::: Enil)
-  | Cminor.Ofloatofint => Eop Ofloatofint (arg ::: Enil)
-  | Cminor.Ofloatofintu => Eop Ofloatofintu (arg ::: Enil)
-  end.
-
-Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr :=
-  match op with
-  | Cminor.Oadd => add arg1 arg2
-  | Cminor.Osub => sub arg1 arg2
-  | Cminor.Omul => mul arg1 arg2
-  | Cminor.Odiv => divs arg1 arg2
-  | Cminor.Odivu => divu arg1 arg2
-  | Cminor.Omod => mods arg1 arg2
-  | Cminor.Omodu => modu arg1 arg2
-  | Cminor.Oand => and arg1 arg2
-  | Cminor.Oor => or arg1 arg2
-  | Cminor.Oxor => xor arg1 arg2
-  | Cminor.Oshl => shl arg1 arg2
-  | Cminor.Oshr => shr arg1 arg2
-  | Cminor.Oshru => shru arg1 arg2
-  | Cminor.Oaddf => Eop Oaddf (arg1 ::: arg2 ::: Enil)
-  | Cminor.Osubf => Eop Osubf (arg1 ::: arg2 ::: Enil)
-  | Cminor.Omulf => Eop Omulf (arg1 ::: arg2 ::: Enil)
-  | Cminor.Odivf => Eop Odivf (arg1 ::: arg2 ::: Enil)
-  | Cminor.Ocmp c => comp c arg1 arg2
-  | Cminor.Ocmpu c => compu c arg1 arg2
-  | Cminor.Ocmpf c => compf c arg1 arg2
-  end.
-
-(** Conversion from Cminor expression to Cminorsel expressions *)
-
-Fixpoint sel_expr (a: Cminor.expr) : expr :=
-  match a with
-  | Cminor.Evar id => Evar id
-  | Cminor.Econst cst => sel_constant cst
-  | Cminor.Eunop op arg => sel_unop op (sel_expr arg)
-  | Cminor.Ebinop op arg1 arg2 => sel_binop op (sel_expr arg1) (sel_expr arg2)
-  | Cminor.Eload chunk addr => load chunk (sel_expr addr)
-  | Cminor.Econdition cond ifso ifnot =>
-      Econdition (condexpr_of_expr (sel_expr cond))
-                 (sel_expr ifso) (sel_expr ifnot)
-  end.
-
-Fixpoint sel_exprlist (al: list Cminor.expr) : exprlist :=
-  match al with
-  | nil => Enil
-  | a :: bl => Econs (sel_expr a) (sel_exprlist bl)
-  end.
-
-(** Conversion from Cminor statements to Cminorsel statements. *)
-
-Fixpoint sel_stmt (s: Cminor.stmt) : stmt :=
-  match s with
-  | Cminor.Sskip => Sskip
-  | Cminor.Sassign id e => Sassign id (sel_expr e)
-  | Cminor.Sstore chunk addr rhs => store chunk (sel_expr addr) (sel_expr rhs)
-  | Cminor.Scall optid sg fn args =>
-      Scall optid sg (sel_expr fn) (sel_exprlist args)
-  | Cminor.Stailcall sg fn args => 
-      Stailcall sg (sel_expr fn) (sel_exprlist args)
-  | Cminor.Sseq s1 s2 => Sseq (sel_stmt s1) (sel_stmt s2)
-  | Cminor.Sifthenelse e ifso ifnot =>
-      Sifthenelse (condexpr_of_expr (sel_expr e))
-                  (sel_stmt ifso) (sel_stmt ifnot)
-  | Cminor.Sloop body => Sloop (sel_stmt body)
-  | Cminor.Sblock body => Sblock (sel_stmt body)
-  | Cminor.Sexit n => Sexit n
-  | Cminor.Sswitch e cases dfl => Sswitch (sel_expr e) cases dfl
-  | Cminor.Sreturn None => Sreturn None
-  | Cminor.Sreturn (Some e) => Sreturn (Some (sel_expr e))
-  | Cminor.Slabel lbl body => Slabel lbl (sel_stmt body)
-  | Cminor.Sgoto lbl => Sgoto lbl
-  end.
-
-(** Conversion of functions and programs. *)
-
-Definition sel_function (f: Cminor.function) : function :=
-  mkfunction
-    f.(Cminor.fn_sig)
-    f.(Cminor.fn_params)
-    f.(Cminor.fn_vars)
-    f.(Cminor.fn_stackspace)
-    (sel_stmt f.(Cminor.fn_body)).
-
-Definition sel_fundef (f: Cminor.fundef) : fundef :=
-  transf_fundef sel_function f.
-
-Definition sel_program (p: Cminor.program) : program :=
-  transform_program sel_fundef p.
-
-(** For compatibility with PowerPC *)
-
-Parameter use_fused_mul: unit -> bool.
diff --git a/arm/Selectionproof.v b/arm/SelectOpproof.v
index cf7613b6..68b49fd8 100644
--- a/arm/Selectionproof.v
+++ b/arm/SelectOpproof.v
@@ -10,7 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Correctness of instruction selection *)
+(** Correctness of instruction selection for operators *)
 
 Require Import Coqlib.
 Require Import Maps.
@@ -25,9 +25,9 @@ Require Import Smallstep.
 Require Import Cminor.
 Require Import Op.
 Require Import CminorSel.
-Require Import Selection.
+Require Import SelectOp.
 
-Open Local Scope selection_scope.
+Open Local Scope cminorsel_scope.
 
 Section CMCONSTR.
 
@@ -36,91 +36,6 @@ Variable sp: val.
 Variable e: env.
 Variable m: mem.
 
-(** * Lifting of let-bound variables *)
-
-Inductive insert_lenv: letenv -> nat -> val -> letenv -> Prop :=
-  | insert_lenv_0:
-      forall le v,
-      insert_lenv le O v (v :: le)
-  | insert_lenv_S:
-      forall le p w le' v,
-      insert_lenv le p w le' ->
-      insert_lenv (v :: le) (S p) w (v :: le').
-
-Lemma insert_lenv_lookup1:
-  forall le p w le',
-  insert_lenv le p w le' ->
-  forall n v,
-  nth_error le n = Some v -> (p > n)%nat ->
-  nth_error le' n = Some v.
-Proof.
-  induction 1; intros.
-  omegaContradiction.
-  destruct n; simpl; simpl in H0. auto. 
-  apply IHinsert_lenv. auto. omega.
-Qed.
-
-Lemma insert_lenv_lookup2:
-  forall le p w le',
-  insert_lenv le p w le' ->
-  forall n v,
-  nth_error le n = Some v -> (p <= n)%nat ->
-  nth_error le' (S n) = Some v.
-Proof.
-  induction 1; intros.
-  simpl. assumption.
-  simpl. destruct n. omegaContradiction. 
-  apply IHinsert_lenv. exact H0. omega.
-Qed.
-
-Hint Resolve eval_Evar eval_Eop eval_Eload eval_Econdition
-             eval_Elet eval_Eletvar 
-             eval_CEtrue eval_CEfalse eval_CEcond
-             eval_CEcondition eval_Enil eval_Econs: evalexpr.
-
-Lemma eval_lift_expr:
-  forall w le a v,
-  eval_expr ge sp e m le a v ->
-  forall p le', insert_lenv le p w le' ->
-  eval_expr ge sp e m le' (lift_expr p a) v.
-Proof.
-  intro w.
-  apply (eval_expr_ind3 ge sp e m
-    (fun le a v =>
-      forall p le', insert_lenv le p w le' ->
-      eval_expr ge sp e m le' (lift_expr p a) v)
-    (fun le a v =>
-      forall p le', insert_lenv le p w le' ->
-      eval_condexpr ge sp e m le' (lift_condexpr p a) v)
-    (fun le al vl =>
-      forall p le', insert_lenv le p w le' ->
-      eval_exprlist ge sp e m le' (lift_exprlist p al) vl));
-  simpl; intros; eauto with evalexpr.
-
-  destruct v1; eapply eval_Econdition;
-  eauto with evalexpr; simpl; eauto with evalexpr.
-
-  eapply eval_Elet. eauto. apply H2. apply insert_lenv_S; auto.
-
-  case (le_gt_dec p n); intro. 
-  apply eval_Eletvar. eapply insert_lenv_lookup2; eauto.
-  apply eval_Eletvar. eapply insert_lenv_lookup1; eauto.
-
-  destruct vb1; eapply eval_CEcondition;
-  eauto with evalexpr; simpl; eauto with evalexpr.
-Qed.
-
-Lemma eval_lift:
-  forall le a v w,
-  eval_expr ge sp e m le a v ->
-  eval_expr ge sp e m (w::le) (lift a) v.
-Proof.
-  intros. unfold lift. eapply eval_lift_expr.
-  eexact H. apply insert_lenv_0. 
-Qed.
-
-Hint Resolve eval_lift: evalexpr.
-
 (** * Useful lemmas and tactics *)
 
 (** The following are trivial lemmas and custom tactics that help
@@ -961,132 +876,75 @@ Proof.
   destruct (Float.cmp c x y); reflexivity.
 Qed.
 
-Lemma negate_condexpr_correct:
-  forall le a b,
-  eval_condexpr ge sp e m le a b ->
-  eval_condexpr ge sp e m le (negate_condexpr a) (negb b).
-Proof.
-  induction 1; simpl.
-  constructor.
-  constructor.
-  econstructor. eauto. apply eval_negate_condition. auto.
-  econstructor. eauto. destruct vb1; auto.
-Qed. 
+Theorem eval_negint:
+  forall le a x,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le (negint a) (Vint (Int.neg x)).
+Proof. intros; unfold negint; EvalOp. Qed.
 
-Scheme expr_ind2 := Induction for expr Sort Prop
-  with exprlist_ind2 := Induction for exprlist Sort Prop.
+Theorem eval_negf:
+  forall le a x,
+  eval_expr ge sp e m le a (Vfloat x) ->
+  eval_expr ge sp e m le (negf a) (Vfloat (Float.neg x)).
+Proof. intros; unfold negf; EvalOp. Qed.
 
-Fixpoint forall_exprlist (P: expr -> Prop) (el: exprlist) {struct el}: Prop :=
-  match el with
-  | Enil => True
-  | Econs e el' => P e /\ forall_exprlist P el'
-  end.
+Theorem eval_absf:
+  forall le a x,
+  eval_expr ge sp e m le a (Vfloat x) ->
+  eval_expr ge sp e m le (absf a) (Vfloat (Float.abs x)).
+Proof. intros; unfold absf; EvalOp. Qed.
 
-Lemma expr_induction_principle:
-  forall (P: expr -> Prop),
-  (forall i : ident, P (Evar i)) ->
-  (forall (o : operation) (e : exprlist),
-     forall_exprlist P e -> P (Eop o e)) ->
-  (forall (m : memory_chunk) (a : Op.addressing) (e : exprlist),
-     forall_exprlist P e -> P (Eload m a e)) ->
-  (forall (c : condexpr) (e : expr),
-     P e -> forall e0 : expr, P e0 -> P (Econdition c e e0)) ->
-  (forall e : expr, P e -> forall e0 : expr, P e0 -> P (Elet e e0)) ->
-  (forall n : nat, P (Eletvar n)) ->
-  forall e : expr, P e.
-Proof.
-  intros. apply expr_ind2 with (P := P) (P0 := forall_exprlist P); auto.
-  simpl. auto.
-  intros. simpl. auto.
-Qed.
+Theorem eval_intoffloat:
+  forall le a x,
+  eval_expr ge sp e m le a (Vfloat x) ->
+  eval_expr ge sp e m le (intoffloat a) (Vint (Float.intoffloat x)).
+Proof. intros; unfold intoffloat; EvalOp. Qed.
 
-Lemma eval_base_condition_of_expr:
-  forall le a v b,
-  eval_expr ge sp e m le a v ->
-  Val.bool_of_val v b ->
-  eval_condexpr ge sp e m le 
-                (CEcond (Ccompimm Cne Int.zero) (a ::: Enil))
-                b.
-Proof.
-  intros. 
-  eapply eval_CEcond. eauto with evalexpr. 
-  inversion H0; simpl. rewrite Int.eq_false; auto. auto. auto.
-Qed.
+Theorem eval_intuoffloat:
+  forall le a x,
+  eval_expr ge sp e m le a (Vfloat x) ->
+  eval_expr ge sp e m le (intuoffloat a) (Vint (Float.intuoffloat x)).
+Proof. intros; unfold intuoffloat; EvalOp. Qed.
 
-Lemma is_compare_neq_zero_correct:
-  forall c v b,
-  is_compare_neq_zero c = true ->
-  eval_condition c (v :: nil) = Some b ->
-  Val.bool_of_val v b.
-Proof.
-  intros.
-  destruct c; simpl in H; try discriminate;
-  destruct c; simpl in H; try discriminate;
-  generalize (Int.eq_spec i Int.zero); rewrite H; intro; subst i.
-
-  simpl in H0. destruct v; inv H0. 
-  generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intros; simpl.
-  subst i; constructor. constructor; auto. constructor.
-
-  simpl in H0. destruct v; inv H0. 
-  generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intros; simpl.
-  subst i; constructor. constructor; auto.
-Qed.
+Theorem eval_floatofint:
+  forall le a x,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le (floatofint a) (Vfloat (Float.floatofint x)).
+Proof. intros; unfold floatofint; EvalOp. Qed.
 
-Lemma is_compare_eq_zero_correct:
-  forall c v b,
-  is_compare_eq_zero c = true ->
-  eval_condition c (v :: nil) = Some b ->
-  Val.bool_of_val v (negb b).
-Proof.
-  intros. apply is_compare_neq_zero_correct with (negate_condition c).
-  destruct c; simpl in H; simpl; try discriminate;
-  destruct c; simpl; try discriminate; auto.
-  apply eval_negate_condition; auto.
-Qed.
+Theorem eval_floatofintu:
+  forall le a x,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le (floatofintu a) (Vfloat (Float.floatofintu x)).
+Proof. intros; unfold floatofintu; EvalOp. Qed.
 
-Lemma eval_condition_of_expr:
-  forall a le v b,
-  eval_expr ge sp e m le a v ->
-  Val.bool_of_val v b ->
-  eval_condexpr ge sp e m le (condexpr_of_expr a) b.
-Proof.
-  intro a0; pattern a0.
-  apply expr_induction_principle; simpl; intros;
-    try (eapply eval_base_condition_of_expr; eauto; fail).
-  
-  destruct o; try (eapply eval_base_condition_of_expr; eauto; fail).
+Theorem eval_addf:
+  forall le a x b y,
+  eval_expr ge sp e m le a (Vfloat x) ->
+  eval_expr ge sp e m le b (Vfloat y) ->
+  eval_expr ge sp e m le (addf a b) (Vfloat (Float.add x y)).
+Proof. intros; unfold addf; EvalOp. Qed.
 
-  destruct e0. InvEval. 
-  inversion H1. 
-  rewrite Int.eq_false; auto. constructor.
-  subst i; rewrite Int.eq_true. constructor.
-  eapply eval_base_condition_of_expr; eauto.
-
-  inv H0. simpl in H7.
-  assert (eval_condition c vl = Some b).
-    destruct (eval_condition c vl); try discriminate.
-    destruct b0; inv H7; inversion H1; congruence.
-  assert (eval_condexpr ge sp e m le (CEcond c e0) b).
-    eapply eval_CEcond; eauto.
-  destruct e0; auto. destruct e1; auto.
-  simpl in H. destruct H.
-  inv H5. inv H11.
-
-  case_eq (is_compare_neq_zero c); intros.
-  eapply H; eauto.
-  apply is_compare_neq_zero_correct with c; auto.
-
-  case_eq (is_compare_eq_zero c); intros.
-  replace b with (negb (negb b)). apply negate_condexpr_correct.
-  eapply H; eauto.
-  apply is_compare_eq_zero_correct with c; auto.
-  apply negb_involutive.
-
-  auto.
-
-  inv H1. destruct v1; eauto with evalexpr.
-Qed.
+Theorem eval_subf:
+  forall le a x b y,
+  eval_expr ge sp e m le a (Vfloat x) ->
+  eval_expr ge sp e m le b (Vfloat y) ->
+  eval_expr ge sp e m le (subf a b) (Vfloat (Float.sub x y)).
+Proof. intros; unfold subf; EvalOp. Qed.
+
+Theorem eval_mulf:
+  forall le a x b y,
+  eval_expr ge sp e m le a (Vfloat x) ->
+  eval_expr ge sp e m le b (Vfloat y) ->
+  eval_expr ge sp e m le (mulf a b) (Vfloat (Float.mul x y)).
+Proof. intros; unfold mulf; EvalOp. Qed.
+
+Theorem eval_divf:
+  forall le a x b y,
+  eval_expr ge sp e m le a (Vfloat x) ->
+  eval_expr ge sp e m le b (Vfloat y) ->
+  eval_expr ge sp e m le (divf a b) (Vfloat (Float.div x y)).
+Proof. intros; unfold divf; EvalOp. Qed.
 
 Lemma eval_addressing:
   forall le chunk a v b ofs,
@@ -1125,335 +983,4 @@ Proof.
     subst v. simpl. rewrite Int.add_zero. auto.
 Qed.
 
-Lemma eval_load:
-  forall le a v chunk v',
-  eval_expr ge sp e m le a v ->
-  Mem.loadv chunk m v = Some v' ->
-  eval_expr ge sp e m le (load chunk a) v'.
-Proof.
-  intros. generalize H0; destruct v; simpl; intro; try discriminate.
-  unfold load. 
-  generalize (eval_addressing _ chunk _ _ _ _ H (refl_equal _)).
-  destruct (addressing chunk a). intros [vl [EV EQ]]. 
-  eapply eval_Eload; eauto. 
-Qed.
-
-Lemma eval_store:
-  forall chunk a1 a2 v1 v2 f k m',
-  eval_expr ge sp e m nil a1 v1 ->
-  eval_expr ge sp e m nil a2 v2 ->
-  Mem.storev chunk m v1 v2 = Some m' ->
-  step ge (State f (store chunk a1 a2) k sp e m)
-       E0 (State f Sskip k sp e m').
-Proof.
-  intros. generalize H1; destruct v1; simpl; intro; try discriminate.
-  unfold store.
-  generalize (eval_addressing _ chunk _ _ _ _ H (refl_equal _)).
-  destruct (addressing chunk a1). intros [vl [EV EQ]]. 
-  eapply step_store; eauto. 
-Qed.
-
-(** * Correctness of instruction selection for operators *)
-
-(** We now prove a semantic preservation result for the [sel_unop]
-  and [sel_binop] selection functions.  The proof exploits
-  the results of the previous section. *)
-
-Lemma eval_sel_unop:
-  forall le op a1 v1 v,
-  eval_expr ge sp e m le a1 v1 ->
-  eval_unop op v1 = Some v ->
-  eval_expr ge sp e m le (sel_unop op a1) v.
-Proof.
-  destruct op; simpl; intros; FuncInv; try subst v.
-  apply eval_cast8unsigned; auto.
-  apply eval_cast8signed; auto.
-  apply eval_cast16unsigned; auto.
-  apply eval_cast16signed; auto.
-  EvalOp. 
-  generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intro.
-  change true with (negb false). eapply eval_notbool; eauto. subst i; constructor.
-  change false with (negb true). eapply eval_notbool; eauto. constructor; auto.
-  change Vfalse with (Val.of_bool (negb true)).
-  eapply eval_notbool; eauto. constructor.
-  apply eval_notint; auto.
-  EvalOp.
-  EvalOp.
-  apply eval_singleoffloat; auto.
-  EvalOp.
-  EvalOp.
-  EvalOp.
-  EvalOp.
-Qed.
-
-Lemma eval_sel_binop:
-  forall le op a1 a2 v1 v2 v,
-  eval_expr ge sp e m le a1 v1 ->
-  eval_expr ge sp e m le a2 v2 ->
-  eval_binop op v1 v2 = Some v ->
-  eval_expr ge sp e m le (sel_binop op a1 a2) v.
-Proof.
-  destruct op; simpl; intros; FuncInv; try subst v.
-  apply eval_add; auto.
-  apply eval_add_ptr_2; auto.
-  apply eval_add_ptr; auto.
-  apply eval_sub; auto.
-  apply eval_sub_ptr_int; auto.
-  destruct (eq_block b b0); inv H1. 
-  eapply eval_sub_ptr_ptr; eauto.
-  apply eval_mul; eauto.
-  generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1.
-  apply eval_divs; eauto.
-  generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1.
-  apply eval_divu; eauto.
-  generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1.
-  apply eval_mods; eauto.
-  generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1.
-  apply eval_modu; eauto.
-  apply eval_and; auto.
-  apply eval_or; auto.
-  apply eval_xor; auto.
-  caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1.
-  apply eval_shl; auto.
-  caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1.
-  apply eval_shr; auto.
-  caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1.
-  apply eval_shru; auto.
-  EvalOp.
-  EvalOp.
-  EvalOp.
-  EvalOp.
-  apply eval_comp_int; auto.
-  eapply eval_comp_int_ptr; eauto.
-  eapply eval_comp_ptr_int; eauto.
-  destruct (eq_block b b0); inv H1.
-  eapply eval_comp_ptr_ptr; eauto.
-  eapply eval_comp_ptr_ptr_2; eauto.
-  eapply eval_compu; eauto.
-  eapply eval_compf; eauto.
-Qed.
-
 End CMCONSTR.
-
-(** * Semantic preservation for instruction selection. *)
-
-Section PRESERVATION.
-
-Variable prog: Cminor.program.
-Let tprog := sel_program prog.
-Let ge := Genv.globalenv prog.
-Let tge := Genv.globalenv tprog.
-
-(** Relationship between the global environments for the original
-  CminorSel program and the generated RTL program. *)
-
-Lemma symbols_preserved:
-  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof.
-  intros; unfold ge, tge, tprog, sel_program. 
-  apply Genv.find_symbol_transf.
-Qed.
-
-Lemma functions_translated:
-  forall (v: val) (f: Cminor.fundef),
-  Genv.find_funct ge v = Some f ->
-  Genv.find_funct tge v = Some (sel_fundef f).
-Proof.  
-  intros.
-  exact (Genv.find_funct_transf sel_fundef H).
-Qed.
-
-Lemma function_ptr_translated:
-  forall (b: block) (f: Cminor.fundef),
-  Genv.find_funct_ptr ge b = Some f ->
-  Genv.find_funct_ptr tge b = Some (sel_fundef f).
-Proof.  
-  intros. 
-  exact (Genv.find_funct_ptr_transf sel_fundef H).
-Qed.
-
-Lemma sig_function_translated:
-  forall f,
-  funsig (sel_fundef f) = Cminor.funsig f.
-Proof.
-  intros. destruct f; reflexivity.
-Qed.
-
-(** Semantic preservation for expressions. *)
-
-Lemma sel_expr_correct:
-  forall sp e m a v,
-  Cminor.eval_expr ge sp e m a v ->
-  forall le,
-  eval_expr tge sp e m le (sel_expr a) v.
-Proof.
-  induction 1; intros; simpl.
-  (* Evar *)
-  constructor; auto.
-  (* Econst *)
-  destruct cst; simpl; simpl in H; (econstructor; [constructor|simpl;auto]).
-  rewrite symbols_preserved. auto.
-  (* Eunop *)
-  eapply eval_sel_unop; eauto.
-  (* Ebinop *)
-  eapply eval_sel_binop; eauto.
-  (* Eload *)
-  eapply eval_load; eauto.
-  (* Econdition *)
-  econstructor; eauto. eapply eval_condition_of_expr; eauto. 
-  destruct b1; auto.
-Qed.
-
-Hint Resolve sel_expr_correct: evalexpr.
-
-Lemma sel_exprlist_correct:
-  forall sp e m a v,
-  Cminor.eval_exprlist ge sp e m a v ->
-  forall le,
-  eval_exprlist tge sp e m le (sel_exprlist a) v.
-Proof.
-  induction 1; intros; simpl; constructor; auto with evalexpr.
-Qed.
-
-Hint Resolve sel_exprlist_correct: evalexpr.
-
-(** Semantic preservation for terminating function calls and statements. *)
-
-Fixpoint sel_cont (k: Cminor.cont) : CminorSel.cont :=
-  match k with
-  | Cminor.Kstop => Kstop
-  | Cminor.Kseq s1 k1 => Kseq (sel_stmt s1) (sel_cont k1)
-  | Cminor.Kblock k1 => Kblock (sel_cont k1)
-  | Cminor.Kcall id f sp e k1 =>
-      Kcall id (sel_function f) sp e (sel_cont k1)
-  end.
-
-Inductive match_states: Cminor.state -> CminorSel.state -> Prop :=
-  | match_state: forall f s k s' k' sp e m,
-      s' = sel_stmt s ->
-      k' = sel_cont k ->
-      match_states
-        (Cminor.State f s k sp e m)
-        (State (sel_function f) s' k' sp e m)
-  | match_callstate: forall f args k k' m,
-      k' = sel_cont k ->
-      match_states
-        (Cminor.Callstate f args k m)
-        (Callstate (sel_fundef f) args k' m)
-  | match_returnstate: forall v k k' m,
-      k' = sel_cont k ->
-      match_states
-        (Cminor.Returnstate v k m)
-        (Returnstate v k' m).
-
-Remark call_cont_commut:
-  forall k, call_cont (sel_cont k) = sel_cont (Cminor.call_cont k).
-Proof.
-  induction k; simpl; auto.
-Qed.
-
-Remark find_label_commut:
-  forall lbl s k,
-  find_label lbl (sel_stmt s) (sel_cont k) =
-  option_map (fun sk => (sel_stmt (fst sk), sel_cont (snd sk)))
-             (Cminor.find_label lbl s k).
-Proof.
-  induction s; intros; simpl; auto.
-  unfold store. destruct (addressing m (sel_expr e)); auto.
-  change (Kseq (sel_stmt s2) (sel_cont k))
-    with (sel_cont (Cminor.Kseq s2 k)).
-  rewrite IHs1. rewrite IHs2. 
-  destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)); auto.
-  rewrite IHs1. rewrite IHs2. 
-  destruct (Cminor.find_label lbl s1 k); auto.
-  change (Kseq (Sloop (sel_stmt s)) (sel_cont k))
-    with (sel_cont (Cminor.Kseq (Cminor.Sloop s) k)).
-  auto.
-  change (Kblock (sel_cont k))
-    with (sel_cont (Cminor.Kblock k)).
-  auto.
-  destruct o; auto.
-  destruct (ident_eq lbl l); auto.
-Qed.
-
-Lemma sel_step_correct:
-  forall S1 t S2, Cminor.step ge S1 t S2 ->
-  forall T1, match_states S1 T1 ->
-  exists T2, step tge T1 t T2 /\ match_states S2 T2.
-Proof.
-  induction 1; intros T1 ME; inv ME; simpl;
-  try (econstructor; split; [econstructor; eauto with evalexpr | econstructor; eauto]; fail).
-
-  (* skip call *)
-  econstructor; split. 
-  econstructor. destruct k; simpl in H; simpl; auto. 
-  rewrite <- H0; reflexivity.
-  constructor; auto.
-  (* store *)
-  econstructor; split.
-  eapply eval_store; eauto with evalexpr.
-  constructor; auto.
-  (* Scall *)
-  econstructor; split.
-  econstructor; eauto with evalexpr.
-  apply functions_translated; eauto. 
-  apply sig_function_translated.
-  constructor; auto.
-  (* Stailcall *)
-  econstructor; split.
-  econstructor; eauto with evalexpr.
-  apply functions_translated; eauto. 
-  apply sig_function_translated.
-  constructor; auto. apply call_cont_commut.
-  (* Sifthenelse *)
-  exists (State (sel_function f) (if b then sel_stmt s1 else sel_stmt s2) (sel_cont k) sp e m); split.
-  constructor. eapply eval_condition_of_expr; eauto with evalexpr.
-  constructor; auto. destruct b; auto.
-  (* Sreturn None *)
-  econstructor; split. 
-  econstructor. 
-  constructor; auto. apply call_cont_commut.
-  (* Sreturn Some *)
-  econstructor; split. 
-  econstructor. simpl. eauto with evalexpr. 
-  constructor; auto. apply call_cont_commut.
-  (* Sgoto *)
-  econstructor; split.
-  econstructor. simpl. rewrite call_cont_commut. rewrite find_label_commut.
-  rewrite H. simpl. reflexivity. 
-  constructor; auto.
-Qed.
-
-Lemma sel_initial_states:
-  forall S, Cminor.initial_state prog S ->
-  exists R, initial_state tprog R /\ match_states S R.
-Proof.
-  induction 1.
-  econstructor; split.
-  econstructor.
-  simpl. fold tge. rewrite symbols_preserved. eexact H.
-  apply function_ptr_translated. eauto. 
-  rewrite <- H1. apply sig_function_translated; auto.
-  unfold tprog, sel_program. rewrite Genv.init_mem_transf.
-  constructor; auto.
-Qed.
-
-Lemma sel_final_states:
-  forall S R r,
-  match_states S R -> Cminor.final_state S r -> final_state R r.
-Proof.
-  intros. inv H0. inv H. simpl. constructor.
-Qed.
-
-Theorem transf_program_correct:
-  forall (beh: program_behavior), not_wrong beh ->
-  Cminor.exec_program prog beh -> CminorSel.exec_program tprog beh.
-Proof.
-  unfold CminorSel.exec_program, Cminor.exec_program; intros.
-  eapply simulation_step_preservation; eauto.
-  eexact sel_initial_states.
-  eexact sel_final_states.
-  exact sel_step_correct. 
-Qed.
-
-End PRESERVATION.