Merge of branch value-analysis.

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

1 files changed, 263 insertions, 254 deletions

diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v
index a4cb402..d9e6068 100644
--- a/ia32/ConstpropOpproof.v
+++ b/ia32/ConstpropOpproof.v
@@ -10,7 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Correctness proof for constant propagation (processor-dependent part). *)
+(** Correctness proof for operator strength reduction. *)
 
 Require Import Coqlib.
 Require Import Integers.
@@ -22,157 +22,8 @@ Require Import Events.
 Require Import Op.
 Require Import Registers.
 Require Import RTL.
+Require Import ValueDomain.
 Require Import ConstpropOp.
-Require Import Constprop.
-
-(** * Correctness of the static analysis *)
-
-Section ANALYSIS.
-
-Variable ge: genv.
-Variable sp: val.
-
-(** We first show that the dataflow analysis is correct with respect
-  to the dynamic semantics: the approximations (sets of values) 
-  of a register at a program point predicted by the static analysis
-  are a superset of the values actually encountered during concrete
-  executions.  We formalize this correspondence between run-time values and
-  compile-time approximations by the following predicate. *)
-
-Definition val_match_approx (a: approx) (v: val) : Prop :=
-  match a with
-  | Unknown => True
-  | I p => v = Vint p
-  | F p => v = Vfloat p
-  | L p => v = Vlong p
-  | G symb ofs => v = symbol_address ge symb ofs
-  | S ofs => v = Val.add sp (Vint ofs)
-  | Novalue => False
-  end.
-
-Inductive val_list_match_approx: list approx -> list val -> Prop :=
-  | vlma_nil:
-      val_list_match_approx nil nil
-  | vlma_cons:
-      forall a al v vl,
-      val_match_approx a v ->
-      val_list_match_approx al vl ->
-      val_list_match_approx (a :: al) (v :: vl).
-
-Ltac SimplVMA :=
-  match goal with
-  | H: (val_match_approx (I _) ?v) |- _ =>
-      simpl in H; (try subst v); SimplVMA
-  | H: (val_match_approx (F _) ?v) |- _ =>
-      simpl in H; (try subst v); SimplVMA
-  | H: (val_match_approx (L _) ?v) |- _ =>
-      simpl in H; (try subst v); SimplVMA
-  | H: (val_match_approx (G _ _) ?v) |- _ =>
-      simpl in H; (try subst v); SimplVMA
-  | H: (val_match_approx (S _) ?v) |- _ =>
-      simpl in H; (try subst v); SimplVMA
-  | _ =>
-      idtac
-  end.
-
-Ltac InvVLMA :=
-  match goal with
-  | H: (val_list_match_approx nil ?vl) |- _ =>
-      inv H
-  | H: (val_list_match_approx (?a :: ?al) ?vl) |- _ =>
-      inv H; SimplVMA; InvVLMA
-  | _ =>
-      idtac
-  end.
-
-(** We then show that [eval_static_operation] is a correct abstract
-  interpretations of [eval_operation]: if the concrete arguments match
-  the given approximations, the concrete results match the
-  approximations returned by [eval_static_operation]. *)
-
-Lemma eval_static_condition_correct:
-  forall cond al vl m b,
-  val_list_match_approx al vl ->
-  eval_static_condition cond al = Some b ->
-  eval_condition cond vl m = Some b.
-Proof.
-  intros until b.
-  unfold eval_static_condition. 
-  case (eval_static_condition_match cond al); intros;
-  InvVLMA; simpl; congruence.
-Qed.
-
-Remark shift_symbol_address:
-  forall symb ofs n,
-  symbol_address ge symb (Int.add ofs n) = Val.add (symbol_address ge symb ofs) (Vint n).
-Proof.
-  unfold symbol_address; intros. destruct (Genv.find_symbol ge symb); auto. 
-Qed.
-
-Lemma eval_static_addressing_correct:
-  forall addr al vl v,
-  val_list_match_approx al vl ->
-  eval_addressing ge sp addr vl = Some v ->
-  val_match_approx (eval_static_addressing addr al) v.
-Proof.
-  intros until v. unfold eval_static_addressing.
-  case (eval_static_addressing_match addr al); intros;
-  InvVLMA; simpl in *; FuncInv; try subst v; auto.
-  rewrite shift_symbol_address; auto.
-  rewrite Val.add_assoc. auto.
-  repeat rewrite shift_symbol_address. auto.
-  fold (Val.add (Vint n1) (symbol_address ge id ofs)).
-  repeat rewrite shift_symbol_address. repeat rewrite Val.add_assoc. rewrite Val.add_permut. auto.
-  repeat rewrite Val.add_assoc. decEq; simpl. rewrite Int.add_assoc. auto.
-  fold (Val.add (Vint n1) (Val.add sp (Vint ofs))).
-  rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_assoc. 
-  simpl. rewrite Int.add_assoc; auto.
-  rewrite shift_symbol_address. auto.
-  rewrite Val.add_assoc. auto. 
-  rewrite shift_symbol_address. auto.
-  rewrite shift_symbol_address. rewrite Int.mul_commut; auto. 
-Qed.
-
-Lemma eval_static_operation_correct:
-  forall op al vl m v,
-  val_list_match_approx al vl ->
-  eval_operation ge sp op vl m = Some v ->
-  val_match_approx (eval_static_operation op al) v.
-Proof.
-  intros until v.
-  unfold eval_static_operation. 
-  case (eval_static_operation_match op al); intros;
-  InvVLMA; simpl in *; FuncInv; try subst v; auto.
-  destruct (propagate_float_constants tt); simpl; auto.
-  rewrite Int.sub_add_opp. rewrite shift_symbol_address. rewrite Val.sub_add_opp. auto.
-  destruct (Int.eq n2 Int.zero). inv H0. 
-    destruct (Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone); inv H0; simpl; auto.
-  destruct (Int.eq n2 Int.zero); inv H0; simpl; auto.
-  destruct (Int.eq n2 Int.zero). inv H0. 
-    destruct (Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone); inv H0; simpl; auto.
-  destruct (Int.eq n2 Int.zero); inv H0; simpl; auto.
-  destruct (Int.ltu n2 Int.iwordsize); simpl; auto.
-  destruct (Int.ltu n Int.iwordsize); simpl; auto.
-  destruct (Int.ltu n2 Int.iwordsize); simpl; auto.
-  destruct (Int.ltu n Int.iwordsize); simpl; auto.
-  destruct (Int.ltu n (Int.repr 31)); inv H0. simpl; auto.
-  destruct (Int.ltu n2 Int.iwordsize); simpl; auto.
-  destruct (Int.ltu n Int.iwordsize); simpl; auto.
-  destruct (Int.ltu n Int.iwordsize); simpl; auto.
-  destruct (Int.ltu n Int.iwordsize);
-  destruct (Int.ltu (Int.sub Int.iwordsize n) Int.iwordsize); simpl; auto.
-  eapply eval_static_addressing_correct; eauto.
-  unfold eval_static_intoffloat.
-  destruct (Float.intoffloat n1) eqn:?; simpl in H0; inv H0.
-  simpl; auto.
-  destruct (propagate_float_constants tt); simpl; auto.
-  unfold eval_static_condition_val. destruct (eval_static_condition c vl0) as [b|] eqn:?.
-  rewrite (eval_static_condition_correct _ _ _ m _ H Heqo). 
-  destruct b; simpl; auto.
-  simpl; auto.
-Qed.
-
-(** * Correctness of strength reduction *)
 
 (** We now show that strength reduction over operators and addressing
   modes preserve semantics: the strength-reduced operations and
@@ -182,130 +33,197 @@ Qed.
 
 Section STRENGTH_REDUCTION.
 
-Variable app: D.t.
-Variable rs: regset.
+Variable bc: block_classification.
+Variable ge: genv.
+Hypothesis GENV: genv_match bc ge.
+Variable sp: block.
+Hypothesis STACK: bc sp = BCstack.
+Variable ae: AE.t.
+Variable e: regset.
 Variable m: mem.
-Hypothesis MATCH: forall r, val_match_approx (approx_reg app r) rs#r.
+Hypothesis MATCH: ematch bc e ae.
+
+Lemma match_G:
+  forall r id ofs,
+  AE.get r ae = Ptr(Gl id ofs) -> Val.lessdef e#r (symbol_address ge id ofs).
+Proof.
+  intros. apply vmatch_ptr_gl with bc; auto. rewrite <- H. apply MATCH. 
+Qed.
+
+Lemma match_S:
+  forall r ofs,
+  AE.get r ae = Ptr(Stk ofs) -> Val.lessdef e#r (Vptr sp ofs).
+Proof.
+  intros. apply vmatch_ptr_stk with bc; auto. rewrite <- H. apply MATCH.
+Qed.
 
 Ltac InvApproxRegs :=
   match goal with
   | [ H: _ :: _ = _ :: _ |- _ ] => 
         injection H; clear H; intros; InvApproxRegs
-  | [ H: ?v = approx_reg app ?r |- _ ] => 
+  | [ H: ?v = AE.get ?r ae |- _ ] => 
         generalize (MATCH r); rewrite <- H; clear H; intro; InvApproxRegs
   | _ => idtac
   end.
 
+Ltac SimplVM :=
+  match goal with
+  | [ H: vmatch _ ?v (I ?n) |- _ ] =>
+      let E := fresh in
+      assert (E: v = Vint n) by (inversion H; auto);
+      rewrite E in *; clear H; SimplVM
+  | [ H: vmatch _ ?v (F ?n) |- _ ] =>
+      let E := fresh in
+      assert (E: v = Vfloat n) by (inversion H; auto);
+      rewrite E in *; clear H; SimplVM
+  | [ H: vmatch _ ?v (Ptr(Gl ?id ?ofs)) |- _ ] =>
+      let E := fresh in
+      assert (E: Val.lessdef v (Op.symbol_address ge id ofs)) by (eapply vmatch_ptr_gl; eauto); 
+      clear H; SimplVM
+  | [ H: vmatch _ ?v (Ptr(Stk ?ofs)) |- _ ] =>
+      let E := fresh in
+      assert (E: Val.lessdef v (Vptr sp ofs)) by (eapply vmatch_ptr_stk; eauto); 
+      clear H; SimplVM
+  | _ => idtac
+  end.
+
 Lemma cond_strength_reduction_correct:
   forall cond args vl,
-  vl = approx_regs app args ->
+  vl = map (fun r => AE.get r ae) args ->
   let (cond', args') := cond_strength_reduction cond args vl in
-  eval_condition cond' rs##args' m = eval_condition cond rs##args m.
+  eval_condition cond' e##args' m = eval_condition cond e##args m.
 Proof.
   intros until vl. unfold cond_strength_reduction.
-  case (cond_strength_reduction_match cond args vl); simpl; intros; InvApproxRegs; SimplVMA.
-  rewrite H0. apply Val.swap_cmp_bool. 
-  rewrite H. auto.
-  rewrite H0. apply Val.swap_cmpu_bool.
-  rewrite H. auto.
-  auto.
+  case (cond_strength_reduction_match cond args vl); simpl; intros; InvApproxRegs; SimplVM.
+- apply Val.swap_cmp_bool.
+- auto.
+- apply Val.swap_cmpu_bool.
+- auto.
+- auto.
+Qed.
+
+Remark shift_symbol_address:
+  forall symb ofs n,
+  Op.symbol_address ge symb (Int.add ofs n) = Val.add (Op.symbol_address ge symb ofs) (Vint n).
+Proof.
+  unfold Op.symbol_address; intros. destruct (Genv.find_symbol ge symb); auto. 
 Qed.
 
 Lemma addr_strength_reduction_correct:
-  forall addr args vl,
-  vl = approx_regs app args ->
+  forall addr args vl res,
+  vl = map (fun r => AE.get r ae) args ->
+  eval_addressing ge (Vptr sp Int.zero) addr e##args = Some res ->
   let (addr', args') := addr_strength_reduction addr args vl in
-  eval_addressing ge sp addr' rs##args' = eval_addressing ge sp addr rs##args.
+  exists res', eval_addressing ge (Vptr sp Int.zero) addr' e##args' = Some res' /\ Val.lessdef res res'.
 Proof.
-  intros until vl. unfold addr_strength_reduction.
-  destruct (addr_strength_reduction_match addr args vl); simpl; intros; InvApproxRegs; SimplVMA.
-  rewrite shift_symbol_address; congruence.
-  rewrite H. rewrite Val.add_assoc; auto.
-  rewrite H; rewrite H0. repeat rewrite shift_symbol_address. auto.
-  rewrite H; rewrite H0. rewrite Int.add_assoc. rewrite Int.add_permut. repeat rewrite shift_symbol_address.
-  rewrite Val.add_assoc. rewrite Val.add_permut. auto.
-  rewrite H; rewrite H0. repeat rewrite Val.add_assoc. rewrite Int.add_assoc. auto.
-  rewrite H; rewrite H0. repeat rewrite Val.add_assoc. rewrite Val.add_permut. 
-  rewrite Int.add_assoc. auto.
-  rewrite H0. rewrite shift_symbol_address. repeat rewrite Val.add_assoc. 
-  decEq; decEq. apply Val.add_commut.
-  rewrite H. rewrite shift_symbol_address. repeat rewrite Val.add_assoc.
-  rewrite (Val.add_permut (rs#r1)). decEq; decEq. apply Val.add_commut.
-  rewrite H0. rewrite Val.add_assoc. rewrite Val.add_permut. auto.
-  rewrite H. rewrite Val.add_assoc. auto.
-  rewrite H; rewrite H0. rewrite Int.add_assoc. repeat rewrite shift_symbol_address. auto.
-  rewrite H0. rewrite shift_symbol_address. rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut.
-  rewrite H. auto.
-  rewrite H. rewrite shift_symbol_address. auto.
-  rewrite H. rewrite shift_symbol_address. rewrite Int.mul_commut; auto.
-  auto.
+  intros until res. unfold addr_strength_reduction.
+  destruct (addr_strength_reduction_match addr args vl); simpl;
+  intros VL EA; InvApproxRegs; SimplVM; try (inv EA).
+- rewrite shift_symbol_address. econstructor; split. eauto. apply Val.add_lessdef; auto.
+- econstructor; split; eauto. rewrite Int.add_zero_l.
+  change (Vptr sp (Int.add n ofs)) with (Val.add (Vptr sp n) (Vint ofs)). apply Val.add_lessdef; auto.
+- econstructor; split; eauto. rewrite Int.add_assoc. rewrite shift_symbol_address. 
+  rewrite Val.add_assoc. apply Val.add_lessdef; auto.
+- econstructor; split; eauto.
+  fold (Val.add (Vint n1) e#r2). rewrite (Val.add_commut (Vint n1)).
+  rewrite shift_symbol_address. apply Val.add_lessdef; auto.
+  rewrite Int.add_commut. rewrite shift_symbol_address. apply Val.add_lessdef; auto. 
+- econstructor; split; eauto. rewrite Int.add_zero_l. rewrite Int.add_assoc. 
+  change (Vptr sp (Int.add n1 (Int.add n2 ofs)))
+    with (Val.add (Vptr sp n1) (Vint (Int.add n2 ofs))).
+  rewrite Val.add_assoc. apply Val.add_lessdef; auto. 
+- econstructor; split; eauto. rewrite Int.add_zero_l. 
+  fold (Val.add (Vint n1) e#r2). rewrite (Int.add_commut n1). 
+  change (Vptr sp (Int.add (Int.add n2 n1) ofs))
+    with (Val.add (Val.add (Vint n1) (Vptr sp n2)) (Vint ofs)).
+  apply Val.add_lessdef; auto. apply Val.add_lessdef; auto. 
+- econstructor; split; eauto. rewrite shift_symbol_address. 
+  rewrite ! Val.add_assoc. apply Val.add_lessdef; auto. 
+  rewrite Val.add_commut. apply Val.add_lessdef; auto. 
+- econstructor; split; eauto. rewrite shift_symbol_address.
+  rewrite (Val.add_commut e#r1). rewrite ! Val.add_assoc.
+  apply Val.add_lessdef; auto. rewrite Val.add_commut. apply Val.add_lessdef; auto.
+- fold (Val.add (Vint n1) e#r2). econstructor; split; eauto. 
+  rewrite (Val.add_commut (Vint n1)). rewrite Val.add_assoc. 
+  apply Val.add_lessdef; eauto. 
+- econstructor; split; eauto.  rewrite ! Val.add_assoc.
+  apply Val.add_lessdef; eauto. 
+- econstructor; split; eauto. rewrite Int.add_assoc. 
+  rewrite shift_symbol_address. apply Val.add_lessdef; auto. 
+- econstructor; split; eauto. 
+  rewrite shift_symbol_address. rewrite ! Val.add_assoc. apply Val.add_lessdef; auto.
+  rewrite Val.add_commut; auto.
+- econstructor; split; eauto.
+- econstructor; split; eauto. rewrite shift_symbol_address. auto.
+- econstructor; split; eauto. rewrite shift_symbol_address. rewrite Int.mul_commut; auto.
+- econstructor; eauto.
 Qed.
 
 Lemma make_addimm_correct:
   forall n r,
   let (op, args) := make_addimm n r in
-  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.add rs#r (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.add e#r (Vint n)) v.
 Proof.
   intros. unfold make_addimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. 
-  subst. exists (rs#r); split; auto. destruct (rs#r); simpl; auto; rewrite Int.add_zero; auto.
-  exists (Val.add rs#r (Vint n)); auto.
+  subst. exists (e#r); split; auto. destruct (e#r); simpl; auto; rewrite Int.add_zero; auto.
+  exists (Val.add e#r (Vint n)); auto.
 Qed.
   
 Lemma make_shlimm_correct:
   forall n r1,
   let (op, args) := make_shlimm n r1 in
-  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.shl rs#r1 (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.shl e#r1 (Vint n)) v.
 Proof.
   intros; unfold make_shlimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
-  exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.shl_zero. auto.
+  exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shl_zero. auto.
   econstructor; split. simpl. eauto. auto.
 Qed.
 
 Lemma make_shrimm_correct:
   forall n r1,
   let (op, args) := make_shrimm n r1 in
-  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.shr rs#r1 (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.shr e#r1 (Vint n)) v.
 Proof.
   intros; unfold make_shrimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
-  exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.shr_zero. auto.
+  exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shr_zero. auto.
   econstructor; split; eauto. simpl. auto.
 Qed.
 
 Lemma make_shruimm_correct:
   forall n r1,
   let (op, args) := make_shruimm n r1 in
-  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.shru rs#r1 (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.shru e#r1 (Vint n)) v.
 Proof.
   intros; unfold make_shruimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
-  exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.shru_zero. auto.
+  exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shru_zero. auto.
   econstructor; split; eauto. simpl. congruence.
 Qed.
 
 Lemma make_mulimm_correct:
   forall n r1,
   let (op, args) := make_mulimm n r1 in
-  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.mul rs#r1 (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.mul e#r1 (Vint n)) v.
 Proof.
   intros; unfold make_mulimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
-  exists (Vint Int.zero); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.mul_zero; auto.
+  exists (Vint Int.zero); split; auto. destruct (e#r1); simpl; auto. rewrite Int.mul_zero; auto.
   predSpec Int.eq Int.eq_spec n Int.one; intros. subst.
-  exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.mul_one; auto.
+  exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.mul_one; auto.
   destruct (Int.is_power2 n) eqn:?; intros.
-  rewrite (Val.mul_pow2 rs#r1 _ _ Heqo). apply make_shlimm_correct; auto. 
+  rewrite (Val.mul_pow2 e#r1 _ _ Heqo). apply make_shlimm_correct; auto. 
   econstructor; split; eauto. auto. 
 Qed.
 
 Lemma make_divimm_correct:
   forall n r1 r2 v,
-  Val.divs rs#r1 rs#r2 = Some v ->
-  rs#r2 = Vint n ->
+  Val.divs e#r1 e#r2 = Some v ->
+  e#r2 = Vint n ->
   let (op, args) := make_divimm n r1 r2 in
-  exists w, eval_operation ge sp op rs##args m = Some w /\ Val.lessdef v w.
+  exists w, eval_operation ge (Vptr sp Int.zero) op e##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_divimm.
   destruct (Int.is_power2 n) eqn:?.
@@ -317,14 +235,14 @@ Qed.
 
 Lemma make_divuimm_correct:
   forall n r1 r2 v,
-  Val.divu rs#r1 rs#r2 = Some v ->
-  rs#r2 = Vint n ->
+  Val.divu e#r1 e#r2 = Some v ->
+  e#r2 = Vint n ->
   let (op, args) := make_divuimm n r1 r2 in
-  exists w, eval_operation ge sp op rs##args m = Some w /\ Val.lessdef v w.
+  exists w, eval_operation ge (Vptr sp Int.zero) op e##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_divuimm.
   destruct (Int.is_power2 n) eqn:?.
-  replace v with (Val.shru rs#r1 (Vint i)). 
+  replace v with (Val.shru e#r1 (Vint i)). 
   eapply make_shruimm_correct; eauto.
   eapply Val.divu_pow2; eauto. congruence.
   exists v; auto.
@@ -332,10 +250,10 @@ Qed.
 
 Lemma make_moduimm_correct:
   forall n r1 r2 v,
-  Val.modu rs#r1 rs#r2 = Some v ->
-  rs#r2 = Vint n ->
+  Val.modu e#r1 e#r2 = Some v ->
+  e#r2 = Vint n ->
   let (op, args) := make_moduimm n r1 r2 in
-  exists w, eval_operation ge sp op rs##args m = Some w /\ Val.lessdef v w.
+  exists w, eval_operation ge (Vptr sp Int.zero) op e##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_moduimm.
   destruct (Int.is_power2 n) eqn:?.
@@ -344,125 +262,216 @@ Proof.
 Qed.
 
 Lemma make_andimm_correct:
-  forall n r,
-  let (op, args) := make_andimm n r in
-  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.and rs#r (Vint n)) v.
+  forall n r x,
+  vmatch bc e#r x ->
+  let (op, args) := make_andimm n r x in
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.and e#r (Vint n)) v.
 Proof.
   intros; unfold make_andimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
-  subst n. exists (Vint Int.zero); split; auto. destruct (rs#r); simpl; auto. rewrite Int.and_zero; auto.
+  subst n. exists (Vint Int.zero); split; auto. destruct (e#r); simpl; auto. rewrite Int.and_zero; auto.
   predSpec Int.eq Int.eq_spec n Int.mone; intros.
-  subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.and_mone; auto.
+  subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int.and_mone; auto.
+  destruct (match x with Uns k => Int.eq (Int.zero_ext k (Int.not n)) Int.zero
+                       | _ => false end) eqn:UNS.
+  destruct x; try congruence. 
+  exists (e#r); split; auto.
+  inv H; auto. simpl. replace (Int.and i n) with i; auto.
+  generalize (Int.eq_spec (Int.zero_ext n0 (Int.not n)) Int.zero); rewrite UNS; intro EQ.
+  Int.bit_solve. destruct (zlt i0 n0).
+  replace (Int.testbit n i0) with (negb (Int.testbit Int.zero i0)).
+  rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto. 
+  rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto. 
+  rewrite Int.bits_not by auto. apply negb_involutive. 
+  rewrite H5 by auto. auto. 
   econstructor; split; eauto. auto. 
 Qed.
 
 Lemma make_orimm_correct:
   forall n r,
   let (op, args) := make_orimm n r in
-  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.or rs#r (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.or e#r (Vint n)) v.
 Proof.
   intros; unfold make_orimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
-  subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.or_zero; auto.
+  subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int.or_zero; auto.
   predSpec Int.eq Int.eq_spec n Int.mone; intros.
-  subst n. exists (Vint Int.mone); split; auto. destruct (rs#r); simpl; auto. rewrite Int.or_mone; auto.
+  subst n. exists (Vint Int.mone); split; auto. destruct (e#r); simpl; auto. rewrite Int.or_mone; auto.
   econstructor; split; eauto. auto. 
 Qed.
 
 Lemma make_xorimm_correct:
   forall n r,
   let (op, args) := make_xorimm n r in
-  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.xor rs#r (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.xor e#r (Vint n)) v.
 Proof.
   intros; unfold make_xorimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
-  subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.xor_zero; auto.
+  subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int.xor_zero; auto.
   econstructor; split; eauto. auto. 
 Qed.
 
 Lemma make_mulfimm_correct:
   forall n r1 r2,
-  rs#r2 = Vfloat n ->
+  e#r2 = Vfloat n ->
   let (op, args) := make_mulfimm n r1 r1 r2 in
-  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v.
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.mulf e#r1 e#r2) v.
 Proof.
   intros; unfold make_mulfimm. 
   destruct (Float.eq_dec n (Float.floatofint (Int.repr 2))); intros. 
   simpl. econstructor; split. eauto. rewrite H; subst n.
-  destruct (rs#r1); simpl; auto. rewrite Float.mul2_add; auto. 
+  destruct (e#r1); simpl; auto. rewrite Float.mul2_add; auto. 
   simpl. econstructor; split; eauto. 
 Qed.
 
 Lemma make_mulfimm_correct_2:
   forall n r1 r2,
-  rs#r1 = Vfloat n ->
+  e#r1 = Vfloat n ->
   let (op, args) := make_mulfimm n r2 r1 r2 in
-  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v.
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.mulf e#r1 e#r2) v.
 Proof.
   intros; unfold make_mulfimm. 
   destruct (Float.eq_dec n (Float.floatofint (Int.repr 2))); intros. 
   simpl. econstructor; split. eauto. rewrite H; subst n.
-  destruct (rs#r2); simpl; auto. rewrite Float.mul2_add; auto. 
+  destruct (e#r2); simpl; auto. rewrite Float.mul2_add; auto. 
   rewrite Float.mul_commut; auto. 
   simpl. econstructor; split; eauto. 
 Qed.
 
+Lemma make_cast8signed_correct:
+  forall r x,
+  vmatch bc e#r x ->
+  let (op, args) := make_cast8signed r x in
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.sign_ext 8 e#r) v.
+Proof.
+  intros; unfold make_cast8signed. destruct (vincl x (Sgn 8)) eqn:INCL. 
+  exists e#r; split; auto. 
+  assert (V: vmatch bc e#r (Sgn 8)).
+  { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
+  inv V; simpl; auto. rewrite is_sgn_sign_ext in H3 by auto. rewrite H3; auto.
+  econstructor; split; simpl; eauto.
+Qed.
+
+Lemma make_cast8unsigned_correct:
+  forall r x,
+  vmatch bc e#r x ->
+  let (op, args) := make_cast8unsigned r x in
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.zero_ext 8 e#r) v.
+Proof.
+  intros; unfold make_cast8unsigned. destruct (vincl x (Uns 8)) eqn:INCL. 
+  exists e#r; split; auto. 
+  assert (V: vmatch bc e#r (Uns 8)).
+  { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
+  inv V; simpl; auto. rewrite is_uns_zero_ext in H3 by auto. rewrite H3; auto.
+  econstructor; split; simpl; eauto.
+Qed.
+
+Lemma make_cast16signed_correct:
+  forall r x,
+  vmatch bc e#r x ->
+  let (op, args) := make_cast16signed r x in
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.sign_ext 16 e#r) v.
+Proof.
+  intros; unfold make_cast16signed. destruct (vincl x (Sgn 16)) eqn:INCL. 
+  exists e#r; split; auto. 
+  assert (V: vmatch bc e#r (Sgn 16)).
+  { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
+  inv V; simpl; auto. rewrite is_sgn_sign_ext in H3 by auto. rewrite H3; auto.
+  econstructor; split; simpl; eauto.
+Qed.
+
+Lemma make_cast16unsigned_correct:
+  forall r x,
+  vmatch bc e#r x ->
+  let (op, args) := make_cast16unsigned r x in
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.zero_ext 16 e#r) v.
+Proof.
+  intros; unfold make_cast16unsigned. destruct (vincl x (Uns 16)) eqn:INCL. 
+  exists e#r; split; auto. 
+  assert (V: vmatch bc e#r (Uns 16)).
+  { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
+  inv V; simpl; auto. rewrite is_uns_zero_ext in H3 by auto. rewrite H3; auto.
+  econstructor; split; simpl; eauto.
+Qed.
+
+Lemma make_singleoffloat_correct:
+  forall r x,
+  vmatch bc e#r x ->
+  let (op, args) := make_singleoffloat r x in
+  exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.singleoffloat e#r) v.
+Proof.
+  intros; unfold make_singleoffloat.
+  destruct (vincl x Fsingle && generate_float_constants tt) eqn:INCL. 
+  InvBooleans. exists e#r; split; auto. 
+  assert (V: vmatch bc e#r Fsingle).
+  { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
+  inv V; simpl; auto. rewrite Float.singleoffloat_of_single by auto. auto.
+  econstructor; split; simpl; eauto.
+Qed.
+
 Lemma op_strength_reduction_correct:
   forall op args vl v,
-  vl = approx_regs app args ->
-  eval_operation ge sp op rs##args m = Some v ->
+  vl = map (fun r => AE.get r ae) args ->
+  eval_operation ge (Vptr sp Int.zero) op e##args m = Some v ->
   let (op', args') := op_strength_reduction op args vl in
-  exists w, eval_operation ge sp op' rs##args' m = Some w /\ Val.lessdef v w.
+  exists w, eval_operation ge (Vptr sp Int.zero) op' e##args' m = Some w /\ Val.lessdef v w.
 Proof.
   intros until v; unfold op_strength_reduction;
   case (op_strength_reduction_match op args vl); simpl; intros.
+(* cast8signed *)
+  InvApproxRegs; SimplVM; inv H0. apply make_cast8signed_correct; auto.
+(* cast8unsigned *)
+  InvApproxRegs; SimplVM; inv H0. apply make_cast8unsigned_correct; auto.
+(* cast16signed *)
+  InvApproxRegs; SimplVM; inv H0. apply make_cast16signed_correct; auto.
+(* cast16unsigned *)
+  InvApproxRegs; SimplVM; inv H0. apply make_cast16unsigned_correct; auto.
 (* sub *)
-  InvApproxRegs. SimplVMA. inv H0; rewrite H. rewrite Val.sub_add_opp. apply make_addimm_correct; auto. 
+  InvApproxRegs; SimplVM; inv H0. rewrite Val.sub_add_opp. apply make_addimm_correct; auto. 
 (* mul *)
-  InvApproxRegs. SimplVMA. inv H0; rewrite H1. rewrite Val.mul_commut. apply make_mulimm_correct; auto.
-  InvApproxRegs. SimplVMA. inv H0; rewrite H. apply make_mulimm_correct; auto.
+  rewrite Val.mul_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_mulimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. apply make_mulimm_correct; auto.
 (* divs *) 
-  assert (rs#r2 = Vint n2). clear H0. InvApproxRegs; SimplVMA; auto.
+  assert (e#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto.
   apply make_divimm_correct; auto.
 (* divu *) 
-  assert (rs#r2 = Vint n2). clear H0. InvApproxRegs; SimplVMA; auto.
+  assert (e#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto.
   apply make_divuimm_correct; auto.
 (* modu *) 
-  assert (rs#r2 = Vint n2). clear H0. InvApproxRegs; SimplVMA; auto.
+  assert (e#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto.
   apply make_moduimm_correct; auto.
 (* and *)
-  InvApproxRegs. SimplVMA. inv H0; rewrite H1. rewrite Val.and_commut. apply make_andimm_correct; auto.
-  InvApproxRegs. SimplVMA. inv H0; rewrite H. apply make_andimm_correct; auto.
+  rewrite Val.and_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_andimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. apply make_andimm_correct; auto.
+  inv H; inv H0. apply make_andimm_correct; auto.
 (* or *)
-  InvApproxRegs. SimplVMA. inv H0; rewrite H1. rewrite Val.or_commut. apply make_orimm_correct; auto.
-  InvApproxRegs. SimplVMA. inv H0; rewrite H. apply make_orimm_correct; auto.
+  rewrite Val.or_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_orimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. apply make_orimm_correct; auto.
 (* xor *)
-  InvApproxRegs. SimplVMA. inv H0; rewrite H1. rewrite Val.xor_commut. apply make_xorimm_correct; auto.
-  InvApproxRegs. SimplVMA. inv H0; rewrite H. apply make_xorimm_correct; auto.
+  rewrite Val.xor_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_xorimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. apply make_xorimm_correct; auto.
 (* shl *)
-  InvApproxRegs. SimplVMA. inv H0; rewrite H. apply make_shlimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. apply make_shlimm_correct; auto.
 (* shr *)
-  InvApproxRegs. SimplVMA. inv H0; rewrite H. apply make_shrimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. apply make_shrimm_correct; auto.
 (* shru *)
-  InvApproxRegs. SimplVMA. inv H0; rewrite H. apply make_shruimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. apply make_shruimm_correct; auto.
 (* lea *)
-  generalize (addr_strength_reduction_correct addr args0 vl0 H). 
+  exploit addr_strength_reduction_correct; eauto. 
   destruct (addr_strength_reduction addr args0 vl0) as [addr' args'].
-  intro EQ. exists v; split; auto. simpl. congruence.
+  auto.
+(* singleoffloat *)
+  InvApproxRegs; SimplVM; inv H0. apply make_singleoffloat_correct; auto.
 (* cond *)
   generalize (cond_strength_reduction_correct c args0 vl0 H). 
   destruct (cond_strength_reduction c args0 vl0) as [c' args']; intros.
   rewrite <- H1 in H0; auto. econstructor; split; eauto.
 (* mulf *)
-  inv H0. assert (rs#r2 = Vfloat n2). InvApproxRegs; SimplVMA; auto.
-  apply make_mulfimm_correct; auto.
-  inv H0. assert (rs#r1 = Vfloat n1). InvApproxRegs; SimplVMA; auto.
-  apply make_mulfimm_correct_2; auto.
+  InvApproxRegs; SimplVM; inv H0. rewrite <- H2. apply make_mulfimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. fold (Val.mulf (Vfloat n1) e#r2).
+  rewrite <- H2. apply make_mulfimm_correct_2; auto.
 (* default *)
   exists v; auto.
 Qed.
 
 End STRENGTH_REDUCTION.
-
-End ANALYSIS.
-