From abe2bb5c40260a31ce5ee27b841bcbd647ff8b88 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 9 Apr 2011 16:59:13 +0000 Subject: Merge of branch "unsigned-offsets": - In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int. (Fixes issue with wrong comparison of pointers across 0x8000_0000) - Revised Stacking pass to not use negative SP offsets. - Add pointer validity checks to Cminor ... Mach to support the use of memory injections in Stacking. - Cleaned up Stacklayout modules. - IA32: improved code generation for Mgetparam. - ARM: improved code generation for op-immediate instructions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1632 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/ConstpropOpproof.v | 83 +++++++++++++++++++++++----------------------- 1 file changed, 42 insertions(+), 41 deletions(-) (limited to 'powerpc/ConstpropOpproof.v') diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index ac15c0d3..bf065b78 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/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. @@ -150,7 +150,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. @@ -174,6 +174,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: @@ -189,20 +190,20 @@ 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. 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. 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. @@ -212,8 +213,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. @@ -225,8 +226,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. @@ -239,8 +240,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. @@ -251,8 +252,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. @@ -265,8 +266,8 @@ Qed. Lemma make_mulimm_correct: forall n r v, let (op, args) := make_mulimm n 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. @@ -274,8 +275,8 @@ Proof. generalize (Int.eq_spec n Int.one); case (Int.eq n Int.one); intros. subst n. simpl in H1. simpl. FuncInv. rewrite Int.mul_one in H0. 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 _ _ H1). change (Z_of_nat Int.wordsize) with 32. intro. rewrite H2. @@ -286,8 +287,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. @@ -300,8 +301,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. @@ -314,8 +315,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. @@ -326,16 +327,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. @@ -346,16 +347,16 @@ Proof. rewrite (intval_correct _ _ H) in H0. assumption. 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. (* 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. simpl. destruct rs#r2; auto. rewrite Int.mul_commut; auto. caseEq (intval app r2); intros. @@ -375,8 +376,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). @@ -389,8 +390,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. @@ -399,8 +400,8 @@ Proof. (* 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. @@ -409,8 +410,8 @@ Proof. (* 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. -- cgit