diff options
Diffstat (limited to 'arm/ConstpropOpproof.v')
-rw-r--r-- | arm/ConstpropOpproof.v | 111 |
1 files changed, 56 insertions, 55 deletions
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index 3f98b881..25758cc8 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -88,10 +88,10 @@ Ltac InvVLMA := approximations returned by [eval_static_operation]. *) Lemma eval_static_condition_correct: - forall cond al vl b, + forall cond al vl m b, val_list_match_approx al vl -> eval_static_condition cond al = Some b -> - eval_condition cond vl = Some b. + eval_condition cond vl m = Some b. Proof. intros until b. unfold eval_static_condition. @@ -100,9 +100,9 @@ Proof. Qed. Lemma eval_static_operation_correct: - forall op sp al vl v, + forall op sp al vl m v, val_list_match_approx al vl -> - eval_operation ge sp op vl = Some v -> + eval_operation ge sp op vl m = Some v -> val_match_approx (eval_static_operation op al) v. Proof. intros until v. @@ -144,7 +144,7 @@ Proof. inv H4. destruct (Float.intoffloat f); simpl in H0; inv H0. red; auto. caseEq (eval_static_condition c vl0). - intros. generalize (eval_static_condition_correct _ _ _ _ H H1). + 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. @@ -168,6 +168,7 @@ Section STRENGTH_REDUCTION. Variable app: reg -> approx. Variable sp: val. Variable rs: regset. +Variable m: mem. Hypothesis MATCH: forall r, val_match_approx (app r) rs#r. Lemma intval_correct: @@ -183,7 +184,7 @@ Qed. Lemma cond_strength_reduction_correct: forall cond args, let (cond', args') := cond_strength_reduction app cond args in - eval_condition cond' rs##args' = eval_condition cond rs##args. + 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. @@ -191,7 +192,6 @@ Proof. caseEq (intval app r1); intros. simpl. rewrite (intval_correct _ _ H). destruct (rs#r2); auto. rewrite Int.swap_cmp. auto. - destruct c; reflexivity. caseEq (intval app r2); intros. simpl. rewrite (intval_correct _ _ H0). auto. auto. @@ -199,6 +199,7 @@ Proof. 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. @@ -217,8 +218,8 @@ Qed. Lemma make_addimm_correct: forall n r v, let (op, args) := make_addimm n r in - eval_operation ge sp Oadd (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oadd (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_addimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -230,8 +231,8 @@ 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) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oshl (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_shlimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -244,8 +245,8 @@ 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) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oshr (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_shrimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -258,8 +259,8 @@ 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) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oshru (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_shruimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -273,8 +274,8 @@ 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) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Omul (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_mulimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -282,8 +283,8 @@ Proof. 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)) - with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil)). + 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. @@ -294,8 +295,8 @@ Qed. Lemma make_andimm_correct: forall n r v, let (op, args) := make_andimm n r in - eval_operation ge sp Oand (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oand (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_andimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -308,8 +309,8 @@ Qed. Lemma make_orimm_correct: forall n r v, let (op, args) := make_orimm n r in - eval_operation ge sp Oor (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oor (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_orimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -322,8 +323,8 @@ Qed. Lemma make_xorimm_correct: forall n r v, let (op, args) := make_xorimm n r in - eval_operation ge sp Oxor (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oxor (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_xorimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -336,16 +337,16 @@ Qed. Lemma op_strength_reduction_correct: forall op args v, let (op', args') := op_strength_reduction app op args in - eval_operation ge sp op rs##args = Some v -> - eval_operation ge sp op' rs##args' = Some v. + eval_operation ge sp op rs##args m = Some v -> + eval_operation ge sp op' rs##args' m = Some v. 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)) - with (eval_operation ge sp Oadd (rs # r2 :: Vint i :: nil)). + 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. @@ -354,8 +355,8 @@ Proof. (* Oaddshift *) caseEq (intval app r2); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp (Oaddshift s) (rs # r1 :: Vint i :: nil)) - with (eval_operation ge sp Oadd (rs # r1 :: Vint (eval_shift s i) :: nil)). + 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. @@ -365,16 +366,16 @@ Proof. 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)) - with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg i) :: nil)). + 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)) - with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg (eval_shift s i)) :: nil)). + 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. @@ -386,8 +387,8 @@ Proof. (* Omul *) caseEq (intval app r1); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Omul (Vint i :: rs # r2 :: nil)) - with (eval_operation ge sp Omul (rs # r2 :: Vint i :: nil)). + 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. @@ -398,8 +399,8 @@ Proof. 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)) - with (eval_operation ge sp Oshru (rs # r1 :: Vint i0 :: nil)). + 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). @@ -412,8 +413,8 @@ Proof. (* Oand *) caseEq (intval app r1); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Oand (Vint i :: rs # r2 :: nil)) - with (eval_operation ge sp Oand (rs # r2 :: Vint i :: nil)). + 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. @@ -422,15 +423,15 @@ Proof. (* Oandshift *) caseEq (intval app r2); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp (Oandshift s) (rs # r1 :: Vint i :: nil)) - with (eval_operation ge sp Oand (rs # r1 :: Vint (eval_shift s i) :: nil)). + 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)) - with (eval_operation ge sp Oor (rs # r2 :: Vint i :: nil)). + 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. @@ -439,15 +440,15 @@ Proof. (* Oorshift *) caseEq (intval app r2); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp (Oorshift s) (rs # r1 :: Vint i :: nil)) - with (eval_operation ge sp Oor (rs # r1 :: Vint (eval_shift s i) :: nil)). + 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)) - with (eval_operation ge sp Oxor (rs # r2 :: Vint i :: nil)). + 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. @@ -456,22 +457,22 @@ Proof. (* Oxorshift *) caseEq (intval app r2); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp (Oxorshift s) (rs # r1 :: Vint i :: nil)) - with (eval_operation ge sp Oxor (rs # r1 :: Vint (eval_shift s i) :: nil)). + 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)) - with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not i) :: nil)). + 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)) - with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not (eval_shift s i)) :: nil)). + 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 *) |