diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-05-30 14:28:57 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-05-30 14:28:57 +0000 |
commit | 72c5d592af9c9c0b417becc6abe5c2364d81639a (patch) | |
tree | 96b5b896605b31ab6ddab385b33fda87a8a40d8a /backend | |
parent | f4b41226d60ca57c5981b0a46e0a495152b5301f (diff) | |
download | compcert-72c5d592af9c9c0b417becc6abe5c2364d81639a.tar.gz compcert-72c5d592af9c9c0b417becc6abe5c2364d81639a.zip |
Revu les comparaisons de pointeurs: == et <> sont definis entre 2 pointeurs vers des blocs differents!
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@649 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Cminor.v | 16 | ||||
-rw-r--r-- | backend/Op.v | 66 | ||||
-rw-r--r-- | backend/Selectionproof.v | 47 |
3 files changed, 77 insertions, 52 deletions
diff --git a/backend/Cminor.v b/backend/Cminor.v index c1e3bd18..f2eb84fd 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -246,10 +246,8 @@ Definition eval_unop (op: unary_operation) (arg: val) : option val := | _, _ => None end. -Definition eval_compare_null (c: comparison) (n: int) : option val := - if Int.eq n Int.zero - then match c with Ceq => Some Vfalse | Cne => Some Vtrue | _ => None end - else None. +Definition eval_compare_mismatch (c: comparison) : option val := + match c with Ceq => Some Vfalse | Cne => Some Vtrue | _ => None end. Definition eval_binop (op: binary_operation) (arg1 arg2: val) (m: mem): option val := @@ -288,11 +286,15 @@ Definition eval_binop | Ocmp c, Vptr b1 n1, Vptr b2 n2 => if valid_pointer m b1 (Int.signed n1) && valid_pointer m b2 (Int.signed n2) then - if eq_block b1 b2 then Some(Val.of_bool(Int.cmp c n1 n2)) else None + if eq_block b1 b2 + then Some(Val.of_bool(Int.cmp c n1 n2)) + else eval_compare_mismatch c else None - | Ocmp c, Vptr b1 n1, Vint n2 => eval_compare_null c n2 - | Ocmp c, Vint n1, Vptr b2 n2 => eval_compare_null c n1 + | Ocmp c, Vptr b1 n1, Vint n2 => + if Int.eq n2 Int.zero then eval_compare_mismatch c else None + | Ocmp c, Vint n1, Vptr b2 n2 => + if Int.eq n1 Int.zero then eval_compare_mismatch c else None | Ocmpu c, Vint n1, Vint n2 => Some (Val.of_bool(Int.cmpu c n1 n2)) | Ocmpf c, Vfloat f1, Vfloat f2 => diff --git a/backend/Op.v b/backend/Op.v index 2094d597..b1136f97 100644 --- a/backend/Op.v +++ b/backend/Op.v @@ -117,10 +117,8 @@ Inductive addressing: Set := operations such as division by zero. [eval_condition] returns a boolean, [eval_operation] and [eval_addressing] return a value. *) -Definition eval_compare_null (c: comparison) (n: int) : option bool := - if Int.eq n Int.zero - then match c with Ceq => Some false | Cne => Some true | _ => None end - else None. +Definition eval_compare_mismatch (c: comparison) : option bool := + match c with Ceq => Some false | Cne => Some true | _ => None end. Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool := @@ -130,18 +128,20 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): | Ccomp c, Vptr b1 n1 :: Vptr b2 n2 :: nil => if valid_pointer m b1 (Int.signed n1) && valid_pointer m b2 (Int.signed n2) then - if eq_block b1 b2 then Some (Int.cmp c n1 n2) else None + if eq_block b1 b2 + then Some (Int.cmp c n1 n2) + else eval_compare_mismatch c else None | Ccomp c, Vptr b1 n1 :: Vint n2 :: nil => - eval_compare_null c n2 + if Int.eq n2 Int.zero then eval_compare_mismatch c else None | Ccomp c, Vint n1 :: Vptr b2 n2 :: nil => - eval_compare_null c n1 + if Int.eq n1 Int.zero then eval_compare_mismatch c else None | Ccompu c, Vint n1 :: Vint n2 :: nil => Some (Int.cmpu c n1 n2) | Ccompimm c n, Vint n1 :: nil => Some (Int.cmp c n1 n) | Ccompimm c n, Vptr b1 n1 :: nil => - eval_compare_null c n + if Int.eq n Int.zero then eval_compare_mismatch c else None | Ccompuimm c n, Vint n1 :: nil => Some (Int.cmpu c n1 n) | Ccompf c, Vfloat f1 :: Vfloat f2 :: nil => @@ -294,15 +294,13 @@ Ltac FuncInv := idtac end. -Remark eval_negate_compare_null: - forall c n b, - eval_compare_null c n = Some b -> - eval_compare_null (negate_comparison c) n = Some (negb b). +Remark eval_negate_compare_mismatch: + forall c b, + eval_compare_mismatch c = Some b -> + eval_compare_mismatch (negate_comparison c) = Some (negb b). Proof. - intros until b. unfold eval_compare_null. - case (Int.eq n Int.zero). - destruct c; intro EQ; simplify_eq EQ; intros; subst b; reflexivity. - intro; discriminate. + intros until b. unfold eval_compare_mismatch. + destruct c; intro EQ; inv EQ; auto. Qed. Lemma eval_negate_condition: @@ -313,15 +311,16 @@ Proof. intros. destruct cond; simpl in H; FuncInv; try subst b; simpl. rewrite Int.negate_cmp. auto. - apply eval_negate_compare_null; auto. - apply eval_negate_compare_null; auto. + destruct (Int.eq i Int.zero). apply eval_negate_compare_mismatch; auto. discriminate. + destruct (Int.eq i0 Int.zero). apply eval_negate_compare_mismatch; auto. discriminate. destruct (valid_pointer m b0 (Int.signed i) && valid_pointer m b1 (Int.signed i0)). destruct (eq_block b0 b1). rewrite Int.negate_cmp. congruence. - discriminate. discriminate. + apply eval_negate_compare_mismatch; auto. + discriminate. rewrite Int.negate_cmpu. auto. rewrite Int.negate_cmp. auto. - apply eval_negate_compare_null; auto. + destruct (Int.eq i Int.zero). apply eval_negate_compare_mismatch; auto. discriminate. rewrite Int.negate_cmpu. auto. auto. rewrite negb_elim. auto. @@ -688,14 +687,21 @@ Definition eval_addressing_total | _, _ => Vundef end. +Lemma eval_compare_mismatch_weaken: + forall c b, + eval_compare_mismatch c = Some b -> + Val.cmp_mismatch c = Val.of_bool b. +Proof. + unfold eval_compare_mismatch. intros. destruct c; inv H; auto. +Qed. + Lemma eval_compare_null_weaken: - forall c i b, - eval_compare_null c i = Some b -> - (if Int.eq i Int.zero then Val.cmp_mismatch c else Vundef) = Val.of_bool b. + forall n c b, + (if Int.eq n Int.zero then eval_compare_mismatch c else None) = Some b -> + (if Int.eq n Int.zero then Val.cmp_mismatch c else Vundef) = Val.of_bool b. Proof. - unfold eval_compare_null. intros. - destruct (Int.eq i Int.zero); try discriminate. - destruct c; try discriminate; inversion H; reflexivity. + intros. destruct (Int.eq n Int.zero). apply eval_compare_mismatch_weaken. auto. + discriminate. Qed. Lemma eval_condition_weaken: @@ -709,7 +715,9 @@ Proof. try (apply eval_compare_null_weaken; auto). destruct (valid_pointer m b0 (Int.signed i) && valid_pointer m b1 (Int.signed i0)). - unfold eq_block in H. destruct (zeq b0 b1); congruence. + unfold eq_block in H. destruct (zeq b0 b1). + congruence. + apply eval_compare_mismatch_weaken; auto. discriminate. symmetry. apply Val.notbool_negb_1. symmetry. apply Val.notbool_negb_1. @@ -814,10 +822,8 @@ Proof. generalize H0. caseEq (valid_pointer m1 b0 (Int.signed i)); intro; simpl; try congruence. caseEq (valid_pointer m1 b1 (Int.signed i0)); intro; simpl; try congruence. - destruct (eq_block b0 b1); try congruence. - intro. inv H2. rewrite (Mem.valid_pointer_lessdef _ _ _ _ MEM H1). - rewrite (Mem.valid_pointer_lessdef _ _ _ _ MEM H). + rewrite (Mem.valid_pointer_lessdef _ _ _ _ MEM H). simpl. auto. Qed. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 07c3e7b9..8b4713db 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -808,16 +808,16 @@ 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 -> + (if Int.eq y Int.zero then Cminor.eval_compare_mismatch c else None) = 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. + EvalOp. simpl. destruct (Int.eq y Int.zero); try discriminate. + unfold Cminor.eval_compare_mismatch in H1. unfold eval_compare_mismatch. 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. + EvalOp. simpl. destruct (Int.eq y Int.zero); try discriminate. + unfold Cminor.eval_compare_mismatch in H1. unfold eval_compare_mismatch. destruct c; try discriminate; auto. Qed. @@ -825,17 +825,17 @@ 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 -> + (if Int.eq x Int.zero then Cminor.eval_compare_mismatch c else None) = 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. + EvalOp. simpl. destruct (Int.eq x Int.zero); try discriminate. + unfold Cminor.eval_compare_mismatch in H1. unfold eval_compare_mismatch. + destruct c; try discriminate; auto. + EvalOp. simpl. destruct (Int.eq x Int.zero); try discriminate. + unfold Cminor.eval_compare_mismatch in H1. unfold eval_compare_mismatch. + destruct c; try discriminate; auto. Qed. Theorem eval_comp_ptr_ptr: @@ -849,11 +849,26 @@ Theorem eval_comp_ptr_ptr: Proof. intros until y2. unfold comp; case (comp_match a b); intros; InvEval. - EvalOp. simpl. rewrite H1. simpl. - subst y1. rewrite dec_eq_true. + EvalOp. simpl. rewrite H1. subst y1. rewrite dec_eq_true. destruct (Int.cmp c x2 y2); reflexivity. Qed. +Theorem eval_comp_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) -> + valid_pointer m x1 (Int.signed x2) && + valid_pointer m y1 (Int.signed y2) = true -> + x1 <> y1 -> + Cminor.eval_compare_mismatch c = Some v -> + eval_expr ge sp e m le (comp c a b) v. +Proof. + intros until y2. + unfold comp; case (comp_match a b); intros; InvEval. + EvalOp. simpl. rewrite H1. rewrite dec_eq_false; auto. + destruct c; simpl in H3; inv H3; auto. +Qed. + Theorem eval_compu: forall le c a x b y, eval_expr ge sp e m le a (Vint x) -> @@ -1133,7 +1148,9 @@ Proof. 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_comp_ptr_ptr; eauto. + eapply eval_comp_ptr_ptr_2; eauto. + discriminate. eapply eval_compu; eauto. eapply eval_compf; eauto. Qed. |