diff options
| -rw-r--r-- | backend/Cminor.v | 16 | ||||
| -rw-r--r-- | backend/Op.v | 66 | ||||
| -rw-r--r-- | backend/Selectionproof.v | 47 | ||||
| -rw-r--r-- | cfrontend/Cminorgenproof.v | 55 | ||||
| -rw-r--r-- | cfrontend/Csem.v | 2 | ||||
| -rw-r--r-- | cfrontend/Cshmgenproof2.v | 8 | ||||
| -rw-r--r-- | common/Mem.v | 24 |
7 files changed, 138 insertions, 80 deletions
diff --git a/backend/Cminor.v b/backend/Cminor.v index c1e3bd1..f2eb84f 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 2094d59..b1136f9 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 07c3e7b..8b4713d 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. diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 54f5ceb..a603875 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -791,14 +791,22 @@ Proof. intros; destruct b; unfold Val.of_bool, Vtrue, Vfalse; constructor. Qed. -Remark val_inject_eval_compare_null: - forall f c i v, - eval_compare_null c i = Some v -> +Remark val_inject_eval_compare_mismatch: + forall f c v, + eval_compare_mismatch c = Some v -> val_inject f v v. Proof. - unfold eval_compare_null; intros. - destruct (Int.eq i Int.zero). + unfold eval_compare_mismatch; intros. destruct c; inv H; unfold Vfalse, Vtrue; constructor. +Qed. + +Remark val_inject_eval_compare_null: + forall f i c v, + (if Int.eq i Int.zero then eval_compare_mismatch c else None) = Some v -> + val_inject f v v. +Proof. + intros. destruct (Int.eq i Int.zero). + eapply val_inject_eval_compare_mismatch; eauto. discriminate. Qed. @@ -820,17 +828,6 @@ Ltac TrivialOp := | _ => idtac end. -Remark eval_compare_null_inv: - forall c i v, - eval_compare_null c i = Some v -> - i = Int.zero /\ (c = Ceq /\ v = Vfalse \/ c = Cne /\ v = Vtrue). -Proof. - intros until v. unfold eval_compare_null. - predSpec Int.eq Int.eq_spec i Int.zero. - case c; intro EQ; simplify_eq EQ; intro; subst v; tauto. - congruence. -Qed. - (** Correctness of [transl_constant]. *) Lemma transl_constant_correct: @@ -921,22 +918,34 @@ Proof. (* cmp ptr ptr *) caseEq (valid_pointer m b1 (Int.signed ofs1) && valid_pointer m b0 (Int.signed ofs0)); intro EQ; rewrite EQ in H4; try discriminate. - destruct (eq_block b1 b0); inv H4. - assert (b3 = b2) by congruence. subst b3. - assert (x0 = x) by congruence. subst x0. elim (andb_prop _ _ EQ); intros. - exists (Val.of_bool (Int.cmp c ofs1 ofs0)); split. exploit (Mem.valid_pointer_inject f m tm b0 ofs0); eauto. intro VP; rewrite VP; clear VP. - exploit (Mem.valid_pointer_inject f m tm b0 ofs1); eauto. + exploit (Mem.valid_pointer_inject f m tm b1 ofs1); eauto. intro VP; rewrite VP; clear VP. + destruct (eq_block b1 b0); inv H4. + (* same blocks in source *) + assert (b3 = b2) by congruence. subst b3. + assert (x0 = x) by congruence. subst x0. + exists (Val.of_bool (Int.cmp c ofs1 ofs0)); split. unfold eq_block; rewrite zeq_true; simpl. decEq. decEq. rewrite Int.translate_cmp. auto. eapply valid_pointer_inject_no_overflow; eauto. eapply valid_pointer_inject_no_overflow; eauto. - apply val_inject_val_of_bool. - (* *) + apply val_inject_val_of_bool. + (* different blocks in source *) + simpl. exists v; split; [idtac | eapply val_inject_eval_compare_mismatch; eauto]. + destruct (eq_block b2 b3); auto. + exploit different_pointers_inject; eauto. intros [A|A]. + congruence. + decEq. destruct c; simpl in H6; inv H6; unfold Int.cmp. + predSpec Int.eq Int.eq_spec (Int.add ofs1 (Int.repr x)) (Int.add ofs0 (Int.repr x0)). + congruence. auto. + predSpec Int.eq Int.eq_spec (Int.add ofs1 (Int.repr x)) (Int.add ofs0 (Int.repr x0)). + congruence. auto. + (* cmpu *) inv H0; try discriminate; inv H1; inv H; TrivialOp. + (* cmpf *) inv H0; try discriminate; inv H1; inv H; TrivialOp. Qed. diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 35d3cce..871f883 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -292,7 +292,7 @@ Function sem_cmp (c:comparison) && valid_pointer m b2 (Int.signed ofs2) then if zeq b1 b2 then Some (Val.of_bool (Int.cmp c ofs1 ofs2)) - else None + else sem_cmp_mismatch c else None | Vptr b ofs, Vint n => if Int.eq n Int.zero then sem_cmp_mismatch c else None diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v index f6bef93..2491e52 100644 --- a/cfrontend/Cshmgenproof2.v +++ b/cfrontend/Cshmgenproof2.v @@ -305,14 +305,14 @@ Proof. (* ipip ptr ptr *) inversion H10. eapply eval_Ebinop; eauto with cshm. simpl. rewrite H3. unfold eq_block. rewrite H9. auto. + inversion H10. eapply eval_Ebinop; eauto with cshm. + simpl. rewrite H3. unfold eq_block. rewrite H9. auto. (* ipip ptr int *) inversion H9. eapply eval_Ebinop; eauto with cshm. - simpl. unfold eval_compare_null. rewrite H8. - functional inversion H; subst; auto. + simpl. rewrite H8. auto. (* ipip int ptr *) inversion H9. eapply eval_Ebinop; eauto with cshm. - simpl. unfold eval_compare_null. rewrite H8. - functional inversion H; subst; auto. + simpl. rewrite H8. auto. (* ff *) inversion H8. eauto with cshm. Qed. diff --git a/common/Mem.v b/common/Mem.v index d369b80..35d93ed 100644 --- a/common/Mem.v +++ b/common/Mem.v @@ -1870,6 +1870,30 @@ Proof. eapply valid_pointer_inj; eauto. Qed. +Lemma different_pointers_inject: + forall f m m' b1 ofs1 b2 ofs2 b1' delta1 b2' delta2, + mem_inject f m m' -> + b1 <> b2 -> + valid_pointer m b1 (Int.signed ofs1) = true -> + valid_pointer m b2 (Int.signed ofs2) = true -> + f b1 = Some (b1', delta1) -> + f b2 = Some (b2', delta2) -> + b1' <> b2' \/ + Int.signed (Int.add ofs1 (Int.repr delta1)) <> + Int.signed (Int.add ofs2 (Int.repr delta2)). +Proof. + intros. + rewrite valid_pointer_valid_access in H1. + rewrite valid_pointer_valid_access in H2. + rewrite (address_inject _ _ _ _ _ _ _ _ H H1 H3). + rewrite (address_inject _ _ _ _ _ _ _ _ H H2 H4). + inv H1. simpl in H7. inv H2. simpl in H9. + exploit (mi_no_overlap _ _ _ H); eauto. + intros [A | [A | [A | [A | A]]]]. + auto. omegaContradiction. omegaContradiction. + right. omega. right. omega. +Qed. + (** Relation between injections and loads. *) Lemma load_inject: |