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/SelectOpproof.v | 80 ++++++++++++++++++++++++++----------------------- 1 file changed, 42 insertions(+), 38 deletions(-) (limited to 'powerpc/SelectOpproof.v') diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 1f2c736..6d1e3c5 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -64,13 +64,13 @@ Ltac InvEval1 := Ltac InvEval2 := match goal with - | [ H: (eval_operation _ _ _ nil = Some _) |- _ ] => + | [ H: (eval_operation _ _ _ nil _ = Some _) |- _ ] => simpl in H; inv H - | [ H: (eval_operation _ _ _ (_ :: nil) = Some _) |- _ ] => + | [ H: (eval_operation _ _ _ (_ :: nil) _ = Some _) |- _ ] => simpl in H; FuncInv - | [ H: (eval_operation _ _ _ (_ :: _ :: nil) = Some _) |- _ ] => + | [ H: (eval_operation _ _ _ (_ :: _ :: nil) _ = Some _) |- _ ] => simpl in H; FuncInv - | [ H: (eval_operation _ _ _ (_ :: _ :: _ :: nil) = Some _) |- _ ] => + | [ H: (eval_operation _ _ _ (_ :: _ :: _ :: nil) _ = Some _) |- _ ] => simpl in H; FuncInv | _ => idtac @@ -167,12 +167,12 @@ Proof. eapply eval_notbool_base; eauto. inv H. eapply eval_Eop; eauto. - simpl. assert (eval_condition c vl = Some b). + simpl. assert (eval_condition c vl m = Some b). generalize H6. simpl. - case (eval_condition c vl); intros. + case (eval_condition c vl m); intros. destruct b0; inv H1; inversion H0; auto; congruence. congruence. - rewrite (Op.eval_negate_condition _ _ H). + rewrite (Op.eval_negate_condition _ _ _ H). destruct b; reflexivity. inv H. eapply eval_Econdition; eauto. @@ -542,9 +542,9 @@ Qed. Lemma eval_mod_aux: forall divop semdivop, - (forall sp x y, + (forall sp x y m, y <> Int.zero -> - eval_operation ge sp divop (Vint x :: Vint y :: nil) = + eval_operation ge sp divop (Vint x :: Vint y :: nil) m = Some (Vint (semdivop x y))) -> forall le a b x y, eval_expr ge sp e m le a (Vint x) -> @@ -715,7 +715,7 @@ Theorem eval_singleoffloat: eval_expr ge sp e m le (singleoffloat a) (Val.singleoffloat v). Proof. TrivialOp singleoffloat. Qed. -Theorem eval_comp_int: +Theorem eval_comp: forall le c a x b y, eval_expr ge sp e m le a (Vint x) -> eval_expr ge sp e m le b (Vint y) -> @@ -728,6 +728,19 @@ Proof. EvalOp. simpl. destruct (Int.cmp c x y); reflexivity. Qed. +Theorem eval_compu_int: + forall le c a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x y)). +Proof. + intros until y. + unfold compu; case (comp_match a b); intros; InvEval. + EvalOp. simpl. rewrite Int.swap_cmpu. destruct (Int.cmpu c x y); reflexivity. + EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity. + EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity. +Qed. + Remark eval_compare_null_transf: forall c x v, Cminor.eval_compare_null c x = Some v -> @@ -742,15 +755,15 @@ Proof. destruct c; try discriminate; auto. Qed. -Theorem eval_comp_ptr_int: +Theorem eval_compu_ptr_int: forall le c a x1 x2 b y v, eval_expr ge sp e m le a (Vptr x1 x2) -> eval_expr ge sp e m le b (Vint y) -> Cminor.eval_compare_null c y = Some v -> - eval_expr ge sp e m le (comp c a b) v. + eval_expr ge sp e m le (compu c a b) v. Proof. intros until v. - unfold comp; case (comp_match a b); intros; InvEval. + unfold compu; case (comp_match a b); intros; InvEval. EvalOp. simpl. apply eval_compare_null_transf; auto. EvalOp. simpl. apply eval_compare_null_transf; auto. Qed. @@ -764,58 +777,49 @@ Proof. destruct (Int.eq x Int.zero). destruct c; auto. auto. Qed. -Theorem eval_comp_int_ptr: +Theorem eval_compu_int_ptr: forall le c a x b y1 y2 v, eval_expr ge sp e m le a (Vint x) -> eval_expr ge sp e m le b (Vptr y1 y2) -> Cminor.eval_compare_null c x = Some v -> - eval_expr ge sp e m le (comp c a b) v. + eval_expr ge sp e m le (compu c a b) v. Proof. intros until v. - unfold comp; case (comp_match a b); intros; InvEval. + unfold compu; case (comp_match a b); intros; InvEval. EvalOp. simpl. apply eval_compare_null_transf. rewrite eval_compare_null_swap; auto. EvalOp. simpl. apply eval_compare_null_transf. auto. Qed. -Theorem eval_comp_ptr_ptr: +Theorem eval_compu_ptr_ptr: forall le c a x1 x2 b y1 y2, eval_expr ge sp e m le a (Vptr x1 x2) -> eval_expr ge sp e m le b (Vptr y1 y2) -> + Mem.valid_pointer m x1 (Int.unsigned x2) + && Mem.valid_pointer m y1 (Int.unsigned y2) = true -> x1 = y1 -> - eval_expr ge sp e m le (comp c a b) (Val.of_bool(Int.cmp c x2 y2)). + eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x2 y2)). Proof. intros until y2. - unfold comp; case (comp_match a b); intros; InvEval. - EvalOp. simpl. subst y1. rewrite dec_eq_true. - destruct (Int.cmp c x2 y2); reflexivity. + unfold compu; case (comp_match a b); intros; InvEval. + EvalOp. simpl. rewrite H1. subst y1. rewrite dec_eq_true. + destruct (Int.cmpu c x2 y2); reflexivity. Qed. -Theorem eval_comp_ptr_ptr_2: +Theorem eval_compu_ptr_ptr_2: forall le c a x1 x2 b y1 y2 v, eval_expr ge sp e m le a (Vptr x1 x2) -> eval_expr ge sp e m le b (Vptr y1 y2) -> + Mem.valid_pointer m x1 (Int.unsigned x2) + && Mem.valid_pointer m y1 (Int.unsigned y2) = true -> x1 <> y1 -> Cminor.eval_compare_mismatch c = Some v -> - eval_expr ge sp e m le (comp c a b) v. + eval_expr ge sp e m le (compu c a b) v. Proof. intros until y2. - unfold comp; case (comp_match a b); intros; InvEval. - EvalOp. simpl. rewrite dec_eq_false; auto. - destruct c; simpl in H2; inv H2; auto. -Qed. - -Theorem eval_compu: - forall le c a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x y)). -Proof. - intros until y. unfold compu; case (comp_match a b); intros; InvEval. - EvalOp. simpl. rewrite Int.swap_cmpu. destruct (Int.cmpu c x y); reflexivity. - EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity. - EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity. + EvalOp. simpl. rewrite H1. rewrite dec_eq_false; auto. + destruct c; simpl in H3; inv H3; auto. Qed. Theorem eval_compf: -- cgit v1.2.3