From 845148dea58bbdd041c399a8c9196d9e67bec629 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 27 Mar 2008 14:40:45 +0000 Subject: Meilleure selection pour if ((a && b) != 0), etc git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@581 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Selection.v | 93 +++++++++++++++++++-- backend/Selectionproof.v | 211 ++++++++++++++++++++++++++++++++++++++++++----- 2 files changed, 277 insertions(+), 27 deletions(-) (limited to 'backend') diff --git a/backend/Selection.v b/backend/Selection.v index 8a69adec..23d8d22f 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -902,16 +902,95 @@ Definition singleoffloat (e: expr) := | singleoffloat_default e1 => Eop Osingleoffloat (e1 ::: Enil) end. +(** ** Comparisons *) + +Inductive comp_cases: forall (e1: expr) (e2: expr), Set := + | comp_case1: + forall n1 t2, + comp_cases (Eop (Ointconst n1) Enil) (t2) + | comp_case2: + forall t1 n2, + comp_cases (t1) (Eop (Ointconst n2) Enil) + | comp_default: + forall (e1: expr) (e2: expr), + comp_cases e1 e2. + +Definition comp_match (e1: expr) (e2: expr) := + match e1 as z1, e2 as z2 return comp_cases z1 z2 with + | Eop (Ointconst n1) Enil, t2 => + comp_case1 n1 t2 + | t1, Eop (Ointconst n2) Enil => + comp_case2 t1 n2 + | e1, e2 => + comp_default e1 e2 + end. + +Definition comp (c: comparison) (e1: expr) (e2: expr) := + match comp_match e1 e2 with + | comp_case1 n1 t2 => + Eop (Ocmp (Ccompimm (swap_comparison c) n1)) (t2 ::: Enil) + | comp_case2 t1 n2 => + Eop (Ocmp (Ccompimm c n2)) (t1 ::: Enil) + | comp_default e1 e2 => + Eop (Ocmp (Ccomp c)) (e1 ::: e2 ::: Enil) + end. + +Definition compu (c: comparison) (e1: expr) (e2: expr) := + match comp_match e1 e2 with + | comp_case1 n1 t2 => + Eop (Ocmp (Ccompuimm (swap_comparison c) n1)) (t2 ::: Enil) + | comp_case2 t1 n2 => + Eop (Ocmp (Ccompuimm c n2)) (t1 ::: Enil) + | comp_default e1 e2 => + Eop (Ocmp (Ccompu c)) (e1 ::: e2 ::: Enil) + end. + +Definition compf (c: comparison) (e1: expr) (e2: expr) := + Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil). + (** ** Conditional expressions *) +Fixpoint negate_condexpr (e: condexpr): condexpr := + match e with + | CEtrue => CEfalse + | CEfalse => CEtrue + | CEcond c el => CEcond (negate_condition c) el + | CEcondition e1 e2 e3 => + CEcondition e1 (negate_condexpr e2) (negate_condexpr e3) + end. + + +Definition is_compare_neq_zero (c: condition) : bool := + match c with + | Ccompimm Cne n => Int.eq n Int.zero + | Ccompuimm Cne n => Int.eq n Int.zero + | _ => false + end. + +Definition is_compare_eq_zero (c: condition) : bool := + match c with + | Ccompimm Ceq n => Int.eq n Int.zero + | Ccompuimm Ceq n => Int.eq n Int.zero + | _ => false + end. + Fixpoint condexpr_of_expr (e: expr) : condexpr := match e with | Eop (Ointconst n) Enil => if Int.eq n Int.zero then CEfalse else CEtrue - | Eop (Ocmp c) el => CEcond c el - | Econdition e1 e2 e3 => - CEcondition e1 (condexpr_of_expr e2) (condexpr_of_expr e3) - | e => CEcond (Ccompimm Cne Int.zero) (e:::Enil) + | Eop (Ocmp c) (e1 ::: Enil) => + if is_compare_neq_zero c then + condexpr_of_expr e1 + else if is_compare_eq_zero c then + negate_condexpr (condexpr_of_expr e1) + else + CEcond c (e1 ::: Enil) + | Eop (Ocmp c) el => + CEcond c el + | Econdition ce e1 e2 => + CEcondition ce (condexpr_of_expr e1) (condexpr_of_expr e2) + | _ => + CEcond (Ccompimm Cne Int.zero) (e:::Enil) end. (** ** Recognition of addressing modes for load and store operations *) @@ -1039,9 +1118,9 @@ Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr := | Cminor.Osubf => subf arg1 arg2 | Cminor.Omulf => Eop Omulf (arg1 ::: arg2 ::: Enil) | Cminor.Odivf => Eop Odivf (arg1 ::: arg2 ::: Enil) - | Cminor.Ocmp c => Eop (Ocmp (Ccomp c)) (arg1 ::: arg2 ::: Enil) - | Cminor.Ocmpu c => Eop (Ocmp (Ccompu c)) (arg1 ::: arg2 ::: Enil) - | Cminor.Ocmpf c => Eop (Ocmp (Ccompf c)) (arg1 ::: arg2 ::: Enil) + | Cminor.Ocmp c => comp c arg1 arg2 + | Cminor.Ocmpu c => compu c arg1 arg2 + | Cminor.Ocmpf c => compf c arg1 arg2 end. (** Conversion from Cminor expression to Cminorsel expressions *) diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index e28bfaf3..4674e1d9 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -791,6 +791,131 @@ Proof. EvalOp. Qed. +Theorem eval_comp_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 (comp c a b) (Val.of_bool(Int.cmp c x y)). +Proof. + intros until y. + unfold comp; case (comp_match a b); intros; InvEval. + EvalOp. simpl. rewrite Int.swap_cmp. destruct (Int.cmp c x y); reflexivity. + EvalOp. simpl. destruct (Int.cmp c x y); reflexivity. + EvalOp. simpl. destruct (Int.cmp c x y); reflexivity. +Qed. + +Theorem eval_comp_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. +Proof. + intros until v. + unfold comp; case (comp_match a b); intros; InvEval. + EvalOp. simpl. unfold Cminor.eval_compare_null in H1. unfold eval_compare_null. + destruct (Int.eq y Int.zero); try discriminate. + destruct c; try discriminate; auto. + EvalOp. simpl. unfold Cminor.eval_compare_null in H1. unfold eval_compare_null. + destruct (Int.eq y Int.zero); try discriminate. + destruct c; try discriminate; auto. +Qed. + +Theorem eval_comp_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. +Proof. + intros until v. + unfold comp; case (comp_match a b); intros; InvEval. + EvalOp. simpl. unfold Cminor.eval_compare_null in H1. unfold eval_compare_null. + destruct (Int.eq x Int.zero); try discriminate. + destruct c; simpl; try discriminate; auto. + EvalOp. simpl. unfold Cminor.eval_compare_null in H1. unfold eval_compare_null. + destruct (Int.eq x Int.zero); try discriminate. + destruct c; simpl; try discriminate; auto. +Qed. + +Theorem eval_comp_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) -> + valid_pointer m x1 (Int.signed x2) && + valid_pointer m y1 (Int.signed y2) = true -> + x1 = y1 -> + eval_expr ge sp e m le (comp c a b) (Val.of_bool(Int.cmp c x2 y2)). +Proof. + intros until y2. + unfold comp; case (comp_match a b); intros; InvEval. + EvalOp. simpl. rewrite H1. simpl. + subst y1. rewrite dec_eq_true. + destruct (Int.cmp c x2 y2); reflexivity. +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. +Qed. + +Theorem eval_compf: + forall le c a x b y, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le b (Vfloat y) -> + eval_expr ge sp e m le (compf c a b) (Val.of_bool(Float.cmp c x y)). +Proof. + intros. unfold compf. EvalOp. simpl. + destruct (Float.cmp c x y); reflexivity. +Qed. + +Lemma negate_condexpr_correct: + forall le a b, + eval_condexpr ge sp e m le a b -> + eval_condexpr ge sp e m le (negate_condexpr a) (negb b). +Proof. + induction 1; simpl. + constructor. + constructor. + econstructor. eauto. apply eval_negate_condition. auto. + econstructor. eauto. destruct vb1; auto. +Qed. + +Scheme expr_ind2 := Induction for expr Sort Prop + with exprlist_ind2 := Induction for exprlist Sort Prop. + +Fixpoint forall_exprlist (P: expr -> Prop) (el: exprlist) {struct el}: Prop := + match el with + | Enil => True + | Econs e el' => P e /\ forall_exprlist P el' + end. + +Lemma expr_induction_principle: + forall (P: expr -> Prop), + (forall i : ident, P (Evar i)) -> + (forall (o : operation) (e : exprlist), + forall_exprlist P e -> P (Eop o e)) -> + (forall (m : memory_chunk) (a : Op.addressing) (e : exprlist), + forall_exprlist P e -> P (Eload m a e)) -> + (forall (c : condexpr) (e : expr), + P e -> forall e0 : expr, P e0 -> P (Econdition c e e0)) -> + (forall e : expr, P e -> forall e0 : expr, P e0 -> P (Elet e e0)) -> + (forall n : nat, P (Eletvar n)) -> + forall e : expr, P e. +Proof. + intros. apply expr_ind2 with (P := P) (P0 := forall_exprlist P); auto. + simpl. auto. + intros. simpl. auto. +Qed. + Lemma eval_base_condition_of_expr: forall le a v b, eval_expr ge sp e m le a v -> @@ -804,28 +929,79 @@ Proof. inversion H0; simpl. rewrite Int.eq_false; auto. auto. auto. Qed. +Lemma is_compare_neq_zero_correct: + forall c v b, + is_compare_neq_zero c = true -> + eval_condition c (v :: nil) m = Some b -> + Val.bool_of_val v b. +Proof. + intros. + destruct c; simpl in H; try discriminate; + destruct c; simpl in H; try discriminate; + generalize (Int.eq_spec i Int.zero); rewrite H; intro; subst i. + + simpl in H0. destruct v; inv H0. + generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intros; simpl. + subst i; constructor. constructor; auto. constructor. + + simpl in H0. destruct v; inv H0. + generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intros; simpl. + subst i; constructor. constructor; auto. +Qed. + +Lemma is_compare_eq_zero_correct: + forall c v b, + is_compare_eq_zero c = true -> + eval_condition c (v :: nil) m = Some b -> + Val.bool_of_val v (negb b). +Proof. + intros. apply is_compare_neq_zero_correct with (negate_condition c). + destruct c; simpl in H; simpl; try discriminate; + destruct c; simpl; try discriminate; auto. + apply eval_negate_condition; auto. +Qed. + Lemma eval_condition_of_expr: forall a le v b, eval_expr ge sp e m le a v -> Val.bool_of_val v b -> eval_condexpr ge sp e m le (condexpr_of_expr a) b. Proof. - induction a; simpl; intros; + intro a0; pattern a0. + apply expr_induction_principle; simpl; intros; try (eapply eval_base_condition_of_expr; eauto; fail). destruct o; try (eapply eval_base_condition_of_expr; eauto; fail). destruct e0. InvEval. - inversion H0. + inversion H1. rewrite Int.eq_false; auto. constructor. subst i; rewrite Int.eq_true. constructor. eapply eval_base_condition_of_expr; eauto. - inv H. eapply eval_CEcond; eauto. simpl in H6. - destruct (eval_condition c vl m); try discriminate. - destruct b0; inv H6; inversion H0; congruence. + inv H0. simpl in H7. + assert (eval_condition c vl m = Some b). + destruct (eval_condition c vl m); try discriminate. + destruct b0; inv H7; inversion H1; congruence. + assert (eval_condexpr ge sp e m le (CEcond c e0) b). + eapply eval_CEcond; eauto. + destruct e0; auto. destruct e1; auto. + simpl in H. destruct H. + inv H5. inv H11. + + case_eq (is_compare_neq_zero c); intros. + eapply H; eauto. + apply is_compare_neq_zero_correct with c; auto. + + case_eq (is_compare_eq_zero c); intros. + replace b with (negb (negb b)). apply negate_condexpr_correct. + eapply H; eauto. + apply is_compare_eq_zero_correct with c; auto. + apply negb_involutive. - inv H. destruct v1; eauto with evalexpr. + auto. + + inv H1. destruct v1; eauto with evalexpr. Qed. Lemma eval_addressing: @@ -950,20 +1126,15 @@ Proof. apply eval_subf; auto. EvalOp. EvalOp. - EvalOp. simpl. destruct (Int.cmp c i i0); auto. - EvalOp. simpl. generalize H1; unfold eval_compare_null, Cminor.eval_compare_null. - destruct (Int.eq i Int.zero). destruct c; intro EQ; inv EQ; auto. - auto. - EvalOp. simpl. generalize H1; unfold eval_compare_null, Cminor.eval_compare_null. - destruct (Int.eq i0 Int.zero). destruct c; intro EQ; inv EQ; auto. - auto. - EvalOp. simpl. - destruct (valid_pointer m b (Int.signed i) && valid_pointer m b0 (Int.signed i0)). - destruct (eq_block b b0); inv H1. - destruct (Int.cmp c i i0); auto. - auto. - EvalOp. simpl. destruct (Int.cmpu c i i0); auto. - EvalOp. simpl. destruct (Float.cmp c f f0); auto. + apply eval_comp_int; auto. + eapply eval_comp_int_ptr; eauto. + eapply eval_comp_ptr_int; eauto. + generalize H1; clear H1. + case_eq (valid_pointer m b (Int.signed i) && valid_pointer m b0 (Int.signed i0)); intros. + destruct (eq_block b b0); inv H2. + eapply eval_comp_ptr_ptr; eauto. discriminate. + eapply eval_compu; eauto. + eapply eval_compf; eauto. Qed. End CMCONSTR. -- cgit