From a82c9c0e4a0b8e37c9c3ea5ae99714982563606f Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 14 Jan 2012 14:23:26 +0000
Subject: Merge of the nonstrict-ops branch: - Most RTL operators now evaluate
 to Some Vundef instead of None   when undefined behavior occurs. - More
 aggressive instruction selection. - "Bertotization" of pattern-matchings now
 implemented by a proper preprocessor. - Cast optimization moved to
 cfrontend/Cminorgen; removed backend/CastOptim.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1790 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 arm/ConstpropOpproof.v | 603 ++++++++++++++++++++-----------------------------
 1 file changed, 245 insertions(+), 358 deletions(-)

(limited to 'arm/ConstpropOpproof.v')

diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index 4d430822..0e60796a 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -30,6 +30,7 @@ Require Import Constprop.
 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) 
@@ -43,7 +44,8 @@ Definition val_match_approx (a: approx) (v: val) : Prop :=
   | Unknown => True
   | I p => v = Vint p
   | F p => v = Vfloat p
-  | S symb ofs => exists b, Genv.find_symbol ge symb = Some b /\ v = Vptr b ofs
+  | G symb ofs => v = symbol_address ge symb ofs
+  | S ofs => v = Val.add sp (Vint ofs)
   | _ => False
   end.
 
@@ -62,12 +64,10 @@ Ltac SimplVMA :=
       simpl in H; (try subst v); SimplVMA
   | H: (val_match_approx (F _) ?v) |- _ =>
       simpl in H; (try subst v); SimplVMA
-  | H: (val_match_approx (S _ _) ?v) |- _ =>
-      simpl in H; 
-      (try (elim H;
-            let b := fresh "b" in let A := fresh in let B := fresh in
-            (intros b [A B]; subst v; clear H)));
-      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.
@@ -75,9 +75,9 @@ Ltac SimplVMA :=
 Ltac InvVLMA :=
   match goal with
   | H: (val_list_match_approx nil ?vl) |- _ =>
-      inversion H
+      inv H
   | H: (val_list_match_approx (?a :: ?al) ?vl) |- _ =>
-      inversion H; SimplVMA; InvVLMA
+      inv H; SimplVMA; InvVLMA
   | _ =>
       idtac
   end.
@@ -87,6 +87,12 @@ Ltac InvVLMA :=
   the given approximations, the concrete results match the
   approximations returned by [eval_static_operation]. *)
 
+Lemma eval_static_shift_correct:
+  forall s n, eval_shift s (Vint n) = Vint (eval_static_shift s n).
+Proof.
+  intros. destruct s; simpl; rewrite s_range; auto.
+Qed.
+
 Lemma eval_static_condition_correct:
   forall cond al vl m b,
   val_list_match_approx al vl ->
@@ -96,11 +102,19 @@ Proof.
   intros until b.
   unfold eval_static_condition. 
   case (eval_static_condition_match cond al); intros;
-  InvVLMA; simpl; congruence.
+  InvVLMA; simpl; try (rewrite eval_static_shift_correct); 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_operation_correct:
-  forall op sp al vl m v,
+  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.
@@ -108,53 +122,34 @@ Proof.
   intros until v.
   unfold eval_static_operation. 
   case (eval_static_operation_match op al); intros;
-  InvVLMA; simpl in *; FuncInv; try congruence.
-
-  destruct (Genv.find_symbol ge s). exists b. intuition congruence.
-  congruence.
-
-  rewrite <- H3. replace v0 with (Vint n1). reflexivity. congruence.
-  rewrite <- H3. replace v0 with (Vint n1). reflexivity. congruence.
-  rewrite <- H3. replace v0 with (Vint n1). reflexivity. congruence.
-  rewrite <- H3. replace v0 with (Vint n1). reflexivity. congruence.
-
-  exists b. split. auto. congruence. 
-  exists b. split. auto. congruence.
-  exists b. split. auto. congruence.
-  exists b. split. auto. congruence.
-  exists b. split. auto. congruence.
-
-  replace n2 with i0. destruct (Int.eq i0 Int.zero). 
-  discriminate. injection H0; intro; subst v. simpl. congruence. congruence.
-
-  replace n2 with i0. destruct (Int.eq i0 Int.zero). 
-  discriminate. injection H0; intro; subst v. simpl. congruence. congruence.
-
-  replace n2 with i0. destruct (Int.ltu i0 Int.iwordsize).
-  injection H0; intro; subst v. simpl. congruence. discriminate. congruence. 
-
-  replace n2 with i0. destruct (Int.ltu i0 Int.iwordsize).
-  injection H0; intro; subst v. simpl. congruence. discriminate. congruence. 
-
-  replace n2 with i0. destruct (Int.ltu i0 Int.iwordsize).
-  injection H0; intro; subst v. simpl. congruence. discriminate. congruence. 
-
-  rewrite <- H3. replace v0 with (Vfloat n1). reflexivity. congruence.
-
-  inv H4. destruct (Float.intoffloat f); simpl in H0; inv H0. red; auto.
-
-  inv H4. destruct (Float.intuoffloat f); simpl in H0; inv H0. red; auto.
-
-  caseEq (eval_static_condition c vl0).
-  intros. generalize (eval_static_condition_correct _ _ _ m _ H H1).
-  intro. rewrite H2 in H0. 
-  destruct b; injection H0; intro; subst v; simpl; auto.
-  intros; simpl; auto.
-
-  replace n1 with i. destruct (Int.ltu n (Int.repr 31)).
-  injection H0; intro; subst v. simpl. auto. congruence. congruence.
-
-  auto.
+  InvVLMA; simpl in *; FuncInv; try (subst v); try (rewrite eval_static_shift_correct); auto.
+
+  rewrite shift_symbol_address; auto. 
+  rewrite shift_symbol_address; auto.
+  rewrite Val.add_assoc; auto.
+  rewrite Val.add_assoc; auto.
+  fold (Val.add (Vint n1) (symbol_address ge s2 n2)).
+  rewrite Int.add_commut. rewrite Val.add_commut. rewrite shift_symbol_address; auto.
+  fold (Val.add (Vint n1) (Val.add sp (Vint n2))). 
+  rewrite Val.add_permut. auto.
+  rewrite shift_symbol_address. auto.
+  rewrite Val.add_assoc. auto.
+  rewrite Int.sub_add_opp. rewrite shift_symbol_address. rewrite Val.sub_add_opp. auto.
+  rewrite Val.sub_add_opp. rewrite Val.add_assoc. rewrite Int.sub_add_opp. auto.
+  rewrite Int.sub_add_opp. rewrite shift_symbol_address. rewrite Val.sub_add_opp. auto.
+  destruct (Int.eq n2 Int.zero); 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 n2 Int.iwordsize); simpl; auto.
+  destruct (Int.ltu n2 Int.iwordsize); simpl; auto.
+  unfold eval_static_intoffloat. destruct (Float.intoffloat n1); simpl in H0; inv H0; simpl; auto.
+  unfold eval_static_intuoffloat. destruct (Float.intuoffloat n1); simpl in H0; inv H0; simpl; auto.
+
+  unfold eval_static_condition_val, Val.of_optbool.
+  destruct (eval_static_condition c vl0) as []_eqn.
+  rewrite (eval_static_condition_correct _ _ _ m _ H Heqo).
+  destruct b; simpl; auto. 
+  simpl; auto.
 Qed.
 
 (** * Correctness of strength reduction *)
@@ -167,367 +162,259 @@ Qed.
 
 Section STRENGTH_REDUCTION.
 
-Variable app: reg -> approx.
-Variable sp: val.
+Variable app: D.t.
 Variable rs: regset.
 Variable m: mem.
-Hypothesis MATCH: forall r, val_match_approx (app r) rs#r.
+Hypothesis MATCH: forall r, val_match_approx (approx_reg app r) rs#r.
 
-Lemma intval_correct:
-  forall r n,
-  intval app r = Some n -> rs#r = Vint n.
-Proof.
-  intros until n.
-  unfold intval. caseEq (app r); intros; try discriminate.
-  generalize (MATCH r). unfold val_match_approx. rewrite H.
-  congruence. 
-Qed.
+Ltac InvApproxRegs :=
+  match goal with
+  | [ H: _ :: _ = _ :: _ |- _ ] => 
+        injection H; clear H; intros; InvApproxRegs
+  | [ H: ?v = approx_reg app ?r |- _ ] => 
+        generalize (MATCH r); rewrite <- H; clear H; intro; InvApproxRegs
+  | _ => idtac
+  end.
 
 Lemma cond_strength_reduction_correct:
-  forall cond args,
-  let (cond', args') := cond_strength_reduction app cond args in
+  forall cond args vl,
+  vl = approx_regs app args ->
+  let (cond', args') := cond_strength_reduction cond args vl in
   eval_condition cond' rs##args' m = eval_condition cond rs##args m.
 Proof.
-  intros. unfold cond_strength_reduction.
-  case (cond_strength_reduction_match cond args); intros.
-
-  caseEq (intval app r1); intros.
-  simpl. rewrite (intval_correct _ _ H). 
-  destruct (rs#r2); auto. rewrite Int.swap_cmp. auto.
-  caseEq (intval app r2); intros.
-  simpl. rewrite (intval_correct _ _ H0). auto.
-  auto.
-
-  caseEq (intval app r1); intros.
-  simpl. rewrite (intval_correct _ _ H). 
-  destruct (rs#r2); auto. rewrite Int.swap_cmpu. auto.
-  destruct c; reflexivity.
-  caseEq (intval app r2); intros.
-  simpl. rewrite (intval_correct _ _ H0). auto.
-  auto.
-
-  caseEq (intval app r2); intros.
-  simpl. rewrite (intval_correct _ _ H). auto.
-  auto.
-
-  caseEq (intval app r2); intros.
-  simpl. rewrite (intval_correct _ _ H). auto.
-  auto.
-
+  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.
+  rewrite H. rewrite eval_static_shift_correct. auto.
+  rewrite H. rewrite eval_static_shift_correct. auto.
   auto.
 Qed.
 
 Lemma make_addimm_correct:
-  forall n r v,
+  forall n r,
   let (op, args) := make_addimm n r in
-  eval_operation ge sp Oadd (rs#r :: Vint n :: nil) m = Some v ->
-  eval_operation ge sp op rs##args m = Some v.
+  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.add rs#r (Vint n)) v.
 Proof.
-  intros; unfold make_addimm.
-  generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
-  subst n. simpl in *. FuncInv. rewrite Int.add_zero in H. congruence.
-  rewrite Int.add_zero in H. congruence.
-  exact H0.
+  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.
 Qed.
-  
+
 Lemma make_shlimm_correct:
-  forall n r v,
-  let (op, args) := make_shlimm n r in
-  eval_operation ge sp Oshl (rs#r :: Vint n :: nil) m = Some v ->
-  eval_operation ge sp op rs##args m = Some v.
+  forall n r1 r2,
+  rs#r2 = Vint n ->
+  let (op, args) := make_shlimm n r1 r2 in
+  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.shl rs#r1 (Vint n)) v.
 Proof.
+  Opaque mk_shift_amount.
   intros; unfold make_shlimm.
-  generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
-  subst n. simpl in *. FuncInv. rewrite Int.shl_zero in H. congruence.
-  unfold is_shift_amount. destruct (is_shift_amount_aux n); intros.
-  simpl in *. FuncInv. rewrite e in H0. auto.
-  simpl in *. FuncInv. rewrite e in H0. discriminate.
+  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.
+  destruct (Int.ltu n Int.iwordsize) as []_eqn; intros.
+  econstructor; split. simpl; eauto.  rewrite mk_shift_amount_eq; auto. 
+  econstructor; split; eauto. simpl. congruence.
 Qed.
 
 Lemma make_shrimm_correct:
-  forall n r v,
-  let (op, args) := make_shrimm n r in
-  eval_operation ge sp Oshr (rs#r :: Vint n :: nil) m = Some v ->
-  eval_operation ge sp op rs##args m = Some v.
+  forall n r1 r2,
+  rs#r2 = Vint n ->
+  let (op, args) := make_shrimm n r1 r2 in
+  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.shr rs#r1 (Vint n)) v.
 Proof.
   intros; unfold make_shrimm.
-  generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
-  subst n. simpl in *. FuncInv. rewrite Int.shr_zero in H. congruence.
-  unfold is_shift_amount. destruct (is_shift_amount_aux n); intros.
-  simpl in *. FuncInv. rewrite e in H0. auto.
-  simpl in *. FuncInv. rewrite e in H0. discriminate.
+  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.
+  destruct (Int.ltu n Int.iwordsize) as []_eqn; intros.
+  econstructor; split. simpl; eauto.  rewrite mk_shift_amount_eq; auto. 
+  econstructor; split; eauto. simpl. congruence.
 Qed.
 
 Lemma make_shruimm_correct:
-  forall n r v,
-  let (op, args) := make_shruimm n r in
-  eval_operation ge sp Oshru (rs#r :: Vint n :: nil) m = Some v ->
-  eval_operation ge sp op rs##args m = Some v.
+  forall n r1 r2,
+  rs#r2 = Vint n ->
+  let (op, args) := make_shruimm n r1 r2 in
+  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.shru rs#r1 (Vint n)) v.
 Proof.
   intros; unfold make_shruimm.
-  generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
-  subst n. simpl in *. FuncInv. rewrite Int.shru_zero in H. congruence.
-  unfold is_shift_amount. destruct (is_shift_amount_aux n); intros.
-  simpl in *. FuncInv. rewrite e in H0. auto.
-  simpl in *. FuncInv. rewrite e in H0. discriminate.
+  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.
+  destruct (Int.ltu n Int.iwordsize) as []_eqn; intros.
+  econstructor; split. simpl; eauto.  rewrite mk_shift_amount_eq; auto. 
+  econstructor; split; eauto. simpl. congruence.
 Qed.
 
 Lemma make_mulimm_correct:
-  forall n r r' v,
-  rs#r' = Vint n ->
-  let (op, args) := make_mulimm n r r' in
-  eval_operation ge sp Omul (rs#r :: Vint n :: nil) m = Some v ->
-  eval_operation ge sp op rs##args m = Some v.
+  forall n r1 r2,
+  rs#r2 = Vint n ->
+  let (op, args) := make_mulimm n r1 r2 in
+  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.mul rs#r1 (Vint n)) v.
 Proof.
   intros; unfold make_mulimm.
-  generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
-  subst n. simpl in H1. FuncInv. rewrite Int.mul_zero in H0. simpl. congruence.
-  generalize (Int.eq_spec n Int.one); case (Int.eq n Int.one); intros.
-  subst n. simpl in H2. simpl. FuncInv. rewrite Int.mul_one in H1. congruence.
-  caseEq (Int.is_power2 n); intros.
-  replace (eval_operation ge sp Omul (rs # r :: Vint n :: nil) m)
-     with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil) m).
-  apply make_shlimm_correct. 
-  simpl. generalize (Int.is_power2_range _ _ H2). 
-  change (Z_of_nat Int.wordsize) with 32. intro. rewrite H3.
-  destruct rs#r; auto. rewrite (Int.mul_pow2 i0 _ _ H2). auto.
-  simpl List.map. rewrite H. auto.
+  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.
+  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.
+  destruct (Int.is_power2 n) as []_eqn; intros.
+  exploit Int.is_power2_range; eauto. intros R.
+  econstructor; split. simpl; eauto. rewrite mk_shift_amount_eq; auto.  
+  rewrite (Val.mul_pow2 rs#r1 _ _ Heqo). auto.
+  econstructor; split; eauto. simpl. congruence.
+Qed.
+
+Lemma make_divimm_correct:
+  forall n r1 r2 v,
+  Val.divs rs#r1 rs#r2 = Some v ->
+  rs#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.
+Proof.
+  intros; unfold make_divimm.
+  destruct (Int.is_power2 n) as []_eqn.
+  destruct (Int.ltu i (Int.repr 31)) as []_eqn.
+  exists v; split; auto. simpl. eapply Val.divs_pow2; eauto. congruence. 
+  exists v; auto.
+  exists v; auto.
+Qed.
+
+Lemma make_divuimm_correct:
+  forall n r1 r2 v,
+  Val.divu rs#r1 rs#r2 = Some v ->
+  rs#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.
+Proof.
+  intros; unfold make_divuimm.
+  destruct (Int.is_power2 n) as []_eqn.
+  replace v with (Val.shru rs#r1 (Vint i)). 
+  econstructor; split. simpl. rewrite mk_shift_amount_eq. eauto. 
+  eapply Int.is_power2_range; eauto. auto.
+  eapply Val.divu_pow2; eauto. congruence.
+  exists v; auto.
 Qed.
 
 Lemma make_andimm_correct:
-  forall n r v,
+  forall n r,
   let (op, args) := make_andimm n r in
-  eval_operation ge sp Oand (rs#r :: Vint n :: nil) m = Some v ->
-  eval_operation ge sp op rs##args m = Some v.
+  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.and rs#r (Vint n)) v.
 Proof.
   intros; unfold make_andimm.
-  generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
-  subst n. simpl in *. FuncInv. rewrite Int.and_zero in H. congruence.
-  generalize (Int.eq_spec n Int.mone); case (Int.eq n Int.mone); intros.
-  subst n. simpl in *. FuncInv. rewrite Int.and_mone in H0. congruence.
-  exact H1.
+  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.
+  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.
+  econstructor; split; eauto. auto. 
 Qed.
 
 Lemma make_orimm_correct:
-  forall n r v,
+  forall n r,
   let (op, args) := make_orimm n r in
-  eval_operation ge sp Oor (rs#r :: Vint n :: nil) m = Some v ->
-  eval_operation ge sp op rs##args m = Some v.
+  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.or rs#r (Vint n)) v.
 Proof.
   intros; unfold make_orimm.
-  generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
-  subst n. simpl in *. FuncInv. rewrite Int.or_zero in H. congruence.
-  generalize (Int.eq_spec n Int.mone); case (Int.eq n Int.mone); intros.
-  subst n. simpl in *. FuncInv. rewrite Int.or_mone in H0. congruence.
-  exact H1.
+  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.
+  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.
+  econstructor; split; eauto. auto. 
 Qed.
 
 Lemma make_xorimm_correct:
-  forall n r v,
+  forall n r,
   let (op, args) := make_xorimm n r in
-  eval_operation ge sp Oxor (rs#r :: Vint n :: nil) m = Some v ->
-  eval_operation ge sp op rs##args m = Some v.
+  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.xor rs#r (Vint n)) v.
 Proof.
   intros; unfold make_xorimm.
-  generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
-  subst n. simpl in *. FuncInv. rewrite Int.xor_zero in H. congruence.
-  generalize (Int.eq_spec n Int.mone); case (Int.eq n Int.mone); intros.
-  subst n. simpl in *. FuncInv. decEq. auto.
-  exact H1.
+  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.
+  predSpec Int.eq Int.eq_spec n Int.mone; intros.
+  subst n. exists (Val.notint (rs#r)); split. auto.
+  destruct (rs#r); simpl; auto. 
+  econstructor; split; eauto. auto. 
 Qed.
 
 Lemma op_strength_reduction_correct:
-  forall op args v,
-  let (op', args') := op_strength_reduction app op args in
+  forall op args vl v,
+  vl = approx_regs app args ->
   eval_operation ge sp op rs##args m = Some v ->
-  eval_operation ge sp op' rs##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.
 Proof.
-  intros; unfold op_strength_reduction;
-  case (op_strength_reduction_match op args); intros; simpl List.map.
-  (* Oadd *)
-  caseEq (intval app r1); intros.
-  rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp Oadd (Vint i :: rs # r2 :: nil) m)
-     with (eval_operation ge sp Oadd (rs # r2 :: Vint i :: nil) m).
-  apply make_addimm_correct. 
-  simpl. destruct rs#r2; auto. rewrite Int.add_commut; auto.
-  caseEq (intval app r2); intros.
-  rewrite (intval_correct _ _ H0). apply make_addimm_correct.
-  assumption.
-  (* Oaddshift *)
-  caseEq (intval app r2); intros.
-  rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp (Oaddshift s) (rs # r1 :: Vint i :: nil) m)
-     with (eval_operation ge sp Oadd (rs # r1 :: Vint (eval_shift s i) :: nil) m).
-  apply make_addimm_correct. 
-  simpl. destruct rs#r1; auto.
-  assumption.
-  (* Osub *)
-  caseEq (intval app r1); intros.
-  rewrite (intval_correct _ _ H) in H0.
-  simpl in *. destruct rs#r2; auto. 
-  caseEq (intval app r2); intros.
-  rewrite (intval_correct _ _ H0).
-  replace (eval_operation ge sp Osub (rs # r1 :: Vint i :: nil) m)
-     with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg i) :: nil) m).
-  apply make_addimm_correct.
-  simpl. destruct rs#r1; auto; rewrite Int.sub_add_opp; auto.
-  assumption.
-  (* Osubshift *)
-  caseEq (intval app r2); intros.
-  rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp (Osubshift s) (rs # r1 :: Vint i :: nil) m)
-     with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg (eval_shift s i)) :: nil) m).
-  apply make_addimm_correct. 
-  simpl. destruct rs#r1; auto; rewrite Int.sub_add_opp; auto.
-  assumption.
-  (* Orsubshift *)
-  caseEq (intval app r2). intros n H.
-  rewrite (intval_correct _ _ H).
-  simpl. destruct rs#r1; auto. 
-  auto.
-  (* Omul *)
-  caseEq (intval app r1); intros.
-  rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp Omul (Vint i :: rs # r2 :: nil) m)
-     with (eval_operation ge sp Omul (rs # r2 :: Vint i :: nil) m).
-  apply make_mulimm_correct. apply intval_correct; auto. 
-  simpl. destruct rs#r2; auto. rewrite Int.mul_commut; auto.
-  caseEq (intval app r2); intros.
-  rewrite (intval_correct _ _ H0). apply make_mulimm_correct.
-  apply intval_correct; auto.
-  assumption.
-  (* Odivu *)
-  caseEq (intval app r2); intros.
-  caseEq (Int.is_power2 i); intros.
-  rewrite (intval_correct _ _ H).
-  replace (eval_operation ge sp Odivu (rs # r1 :: Vint i :: nil) m)
-     with (eval_operation ge sp Oshru (rs # r1 :: Vint i0 :: nil) m).
-  apply make_shruimm_correct. 
-  simpl. destruct rs#r1; auto. 
-  change 32 with (Z_of_nat Int.wordsize). 
-  rewrite (Int.is_power2_range _ _ H0). 
-  generalize (Int.eq_spec i Int.zero); case (Int.eq i Int.zero); intros.
-  subst i. discriminate. 
-  rewrite (Int.divu_pow2 i1 _ _ H0). auto.
-  assumption.
-  assumption.
-  (* Oand *)
-  caseEq (intval app r1); intros.
-  rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp Oand (Vint i :: rs # r2 :: nil) m)
-     with (eval_operation ge sp Oand (rs # r2 :: Vint i :: nil) m).
-  apply make_andimm_correct. 
-  simpl. destruct rs#r2; auto. rewrite Int.and_commut; auto.
-  caseEq (intval app r2); intros.
-  rewrite (intval_correct _ _ H0). apply make_andimm_correct.
-  assumption.
-  (* Oandshift *)
-  caseEq (intval app r2); intros.
-  rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp (Oandshift s) (rs # r1 :: Vint i :: nil) m)
-     with (eval_operation ge sp Oand (rs # r1 :: Vint (eval_shift s i) :: nil) m).
-  apply make_andimm_correct. reflexivity.
-  assumption.
-  (* Oor *)
-  caseEq (intval app r1); intros.
-  rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp Oor (Vint i :: rs # r2 :: nil) m)
-     with (eval_operation ge sp Oor (rs # r2 :: Vint i :: nil) m).
-  apply make_orimm_correct. 
-  simpl. destruct rs#r2; auto. rewrite Int.or_commut; auto.
-  caseEq (intval app r2); intros.
-  rewrite (intval_correct _ _ H0). apply make_orimm_correct.
-  assumption.
-  (* Oorshift *)
-  caseEq (intval app r2); intros.
-  rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp (Oorshift s) (rs # r1 :: Vint i :: nil) m)
-     with (eval_operation ge sp Oor (rs # r1 :: Vint (eval_shift s i) :: nil) m).
-  apply make_orimm_correct. reflexivity.
-  assumption.
-  (* Oxor *)
-  caseEq (intval app r1); intros.
-  rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp Oxor (Vint i :: rs # r2 :: nil) m)
-     with (eval_operation ge sp Oxor (rs # r2 :: Vint i :: nil) m).
-  apply make_xorimm_correct. 
-  simpl. destruct rs#r2; auto. rewrite Int.xor_commut; auto.
-  caseEq (intval app r2); intros.
-  rewrite (intval_correct _ _ H0). apply make_xorimm_correct.
-  assumption.
-  (* Oxorshift *)
-  caseEq (intval app r2); intros.
-  rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp (Oxorshift s) (rs # r1 :: Vint i :: nil) m)
-     with (eval_operation ge sp Oxor (rs # r1 :: Vint (eval_shift s i) :: nil) m).
-  apply make_xorimm_correct. reflexivity.
-  assumption.
-  (* Obic *)
-  caseEq (intval app r2); intros.
-  rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp Obic (rs # r1 :: Vint i :: nil) m)
-     with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not i) :: nil) m).
-  apply make_andimm_correct. reflexivity.
-  assumption.
-  (* Obicshift *)
-  caseEq (intval app r2); intros.
-  rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp (Obicshift s) (rs # r1 :: Vint i :: nil) m)
-     with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not (eval_shift s i)) :: nil) m).
-  apply make_andimm_correct. reflexivity.
-  assumption.
-  (* Oshl *)
-  caseEq (intval app r2); intros.
-  caseEq (Int.ltu i Int.iwordsize); intros.
-  rewrite (intval_correct _ _ H). apply make_shlimm_correct.
-  assumption.
-  assumption.
-  (* Oshr *)
-  caseEq (intval app r2); intros.
-  caseEq (Int.ltu i Int.iwordsize); intros.
-  rewrite (intval_correct _ _ H). apply make_shrimm_correct.
-  assumption.
-  assumption.
-  (* Oshru *)
-  caseEq (intval app r2); intros.
-  caseEq (Int.ltu i Int.iwordsize); intros.
-  rewrite (intval_correct _ _ H). apply make_shruimm_correct.
-  assumption.
-  assumption.
-  (* Ocmp *)
-  generalize (cond_strength_reduction_correct c rl).
-  destruct (cond_strength_reduction app c rl).
-  simpl. intro. rewrite H. auto.
-  (* default *)
-  assumption.
+  intros until v; unfold op_strength_reduction;
+  case (op_strength_reduction_match op args vl); simpl; intros.
+(* add *)
+  InvApproxRegs. SimplVMA. inv H0. rewrite H1. rewrite Val.add_commut. apply make_addimm_correct.
+  InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_addimm_correct.
+(* addshift *)
+  InvApproxRegs. SimplVMA. inv H0. rewrite H. rewrite eval_static_shift_correct. apply make_addimm_correct.
+(* sub *)
+  InvApproxRegs; SimplVMA. inv H0. rewrite H1. econstructor; split; eauto. 
+  InvApproxRegs; SimplVMA. inv H0. rewrite H. rewrite Val.sub_add_opp. apply make_addimm_correct.
+(* subshift *)
+  InvApproxRegs; SimplVMA. inv H0. rewrite H. rewrite eval_static_shift_correct. rewrite Val.sub_add_opp. apply make_addimm_correct.
+(* rsubshift *)
+  InvApproxRegs; SimplVMA. inv H0. rewrite H. rewrite eval_static_shift_correct. econstructor; split; eauto.
+(* 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.
+(* divs *)
+  assert (rs#r2 = Vint n2). clear H0. InvApproxRegs; SimplVMA; auto.
+  apply make_divimm_correct; auto.
+(* divu *)
+  assert (rs#r2 = Vint n2). clear H0. InvApproxRegs; SimplVMA; auto.
+  apply make_divuimm_correct; auto.
+(* and *)
+  InvApproxRegs. SimplVMA. inv H0. rewrite H1. rewrite Val.and_commut. apply make_andimm_correct.
+  InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_andimm_correct.
+(* andshift *)
+  InvApproxRegs. SimplVMA. inv H0. rewrite H. rewrite eval_static_shift_correct. apply make_andimm_correct.
+(* or *)
+  InvApproxRegs. SimplVMA. inv H0. rewrite H1. rewrite Val.or_commut. apply make_orimm_correct.
+  InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_orimm_correct.
+(* orshift *)
+  InvApproxRegs. SimplVMA. inv H0. rewrite H. rewrite eval_static_shift_correct. apply make_orimm_correct.
+(* xor *)
+  InvApproxRegs. SimplVMA. inv H0. rewrite H1. rewrite Val.xor_commut. apply make_xorimm_correct.
+  InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_xorimm_correct.
+(* xorshift *)
+  InvApproxRegs. SimplVMA. inv H0. rewrite H. rewrite eval_static_shift_correct. apply make_xorimm_correct.
+(* bic *)
+  InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_andimm_correct.
+(* bicshift *)
+  InvApproxRegs. SimplVMA. inv H0. rewrite H. rewrite eval_static_shift_correct. apply make_andimm_correct.
+(* shl *)
+  InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_shlimm_correct; auto.
+(* shr *)
+  InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_shrimm_correct; auto.
+(* shru *)
+  InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_shruimm_correct; auto.
+(* cmp *)
+  generalize (cond_strength_reduction_correct c args0 vl0). 
+  destruct (cond_strength_reduction c args0 vl0) as [c' args']; intros.
+  rewrite <- H1 in H0; auto. econstructor; split; eauto.
+(* default *)
+  exists v; auto.
 Qed.
  
 Lemma addr_strength_reduction_correct:
-  forall addr args,
-  let (addr', args') := addr_strength_reduction app addr args in
+  forall addr args vl,
+  vl = approx_regs app args ->
+  let (addr', args') := addr_strength_reduction addr args vl in
   eval_addressing ge sp addr' rs##args' = eval_addressing ge sp addr rs##args.
 Proof.
-  intros. 
-
-  unfold addr_strength_reduction;
-  case (addr_strength_reduction_match addr args); intros.
-
-  (* Aindexed2 *)
-  caseEq (intval app r1); intros.
-  simpl; rewrite (intval_correct _ _ H).
-  destruct rs#r2; auto. rewrite Int.add_commut; auto.
-  caseEq (intval app r2); intros.
-  simpl; rewrite (intval_correct _ _ H0). auto.
+  intros until vl. unfold addr_strength_reduction.
+  destruct (addr_strength_reduction_match addr args vl); simpl; intros; InvApproxRegs; SimplVMA.
+  rewrite H; rewrite H0. rewrite Val.add_assoc; auto.
+  rewrite H; rewrite H0. rewrite Val.add_permut; auto. 
+  rewrite H0. rewrite Val.add_commut. auto.
+  rewrite H. auto.
+  rewrite H; rewrite H0. rewrite Val.add_assoc. rewrite eval_static_shift_correct. auto.
+  rewrite H. rewrite eval_static_shift_correct. auto.
+  rewrite H. rewrite Val.add_assoc. auto.
   auto.
-
-  (* Aindexed2shift *)
-  caseEq (intval app r2); intros.
-  simpl; rewrite (intval_correct _ _ H). auto.
-  auto.
-
-  (* default *)
-  reflexivity.
 Qed.
 
 End STRENGTH_REDUCTION.
-- 
cgit