diff options
| -rw-r--r-- | backend/Selectionproof.v | 22 | ||||
| -rw-r--r-- | cfrontend/Cshmgenproof.v | 6 | ||||
| -rw-r--r-- | common/Values.v | 129 | ||||
| -rw-r--r-- | ia32/SelectOpproof.v | 10 | ||||
| -rw-r--r-- | powerpc/SelectOpproof.v | 10 |
5 files changed, 74 insertions, 103 deletions
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 0aa2b6b..79c039f 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -103,16 +103,10 @@ 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. + generalize (Int.eq_spec i Int.zero); rewrite H; intros; subst. - 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. - - 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. constructor. + simpl in H0. destruct v; inv H0. constructor. constructor. Qed. Lemma is_compare_eq_zero_correct: @@ -139,17 +133,13 @@ Proof. destruct o; try (eapply eval_condition_of_expr_base; eauto; fail). - destruct e0. inv H0. inv H5. simpl in H7. inv H7. - inversion H1. - rewrite Int.eq_false; auto. constructor. - subst i; rewrite Int.eq_true. constructor. + destruct e0. inv H0. inv H5. simpl in H7. inv H7. inv H1. + destruct (Int.eq i Int.zero); constructor. eapply eval_condition_of_expr_base; eauto. inv H0. simpl in H7. assert (eval_condition c vl m = Some b). - destruct (eval_condition c vl m). - destruct b0; inv H7; inversion H1; congruence. - inv H7. inv H1. + inv H7. eapply Val.bool_of_val_of_optbool; eauto. assert (eval_condexpr ge sp e m le (CEcond c e0) b). eapply eval_CEcond; eauto. destruct e0; auto. destruct e1; auto. diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 47bc1c6..6a02e1d 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -443,9 +443,7 @@ Lemma make_boolean_correct: /\ Val.bool_of_val vb b. Proof. assert (VBI: forall n, Val.bool_of_val (Vint n) (negb (Int.eq n Int.zero))). - intros. predSpec Int.eq Int.eq_spec n Int.zero; simpl. - subst. constructor. - constructor. auto. + constructor. intros. functional inversion H0; subst; simpl. exists (Vint n); split; auto. exists (Vint n); split; auto. @@ -458,7 +456,7 @@ Proof. rewrite <- Float.cmp_ne_eq. exists (Val.of_bool (Float.cmp Cne f Float.zero)); split. econstructor; eauto with cshm. - destruct (Float.cmp Cne f Float.zero); simpl; constructor. apply Int.one_not_zero. + destruct (Float.cmp Cne f Float.zero); simpl; constructor. Qed. Lemma make_neg_correct: diff --git a/common/Values.v b/common/Values.v index bcb7c4f..9f73e33 100644 --- a/common/Values.v +++ b/common/Values.v @@ -74,27 +74,14 @@ Fixpoint has_type_list (vl: list val) (tl: list typ) {struct vl} : Prop := The integer 0 (also used to represent the null pointer) is [False]. [Vundef] and floats are neither true nor false. *) -Definition is_true (v: val) : Prop := - match v with - | Vint n => n <> Int.zero - | Vptr b ofs => True - | _ => False - end. - -Definition is_false (v: val) : Prop := - match v with - | Vint n => n = Int.zero - | _ => False - end. - Inductive bool_of_val: val -> bool -> Prop := - | bool_of_val_int_true: - forall n, n <> Int.zero -> bool_of_val (Vint n) true - | bool_of_val_int_false: - bool_of_val (Vint Int.zero) false + | bool_of_val_int: + forall n, bool_of_val (Vint n) (negb (Int.eq n Int.zero)) | bool_of_val_ptr: forall b ofs, bool_of_val (Vptr b ofs) true. +(** Arithmetic operations *) + Definition neg (v: val) : val := match v with | Vint n => Vint (Int.neg n) @@ -357,6 +344,8 @@ Definition divf (v1 v2: val): val := | _, _ => Vundef end. +(** Comparisons *) + Section COMPARISONS. Variable valid_ptr: block -> Z -> bool. @@ -449,60 +438,18 @@ Proof. change 65535 with (two_p 16 - 1). apply Int.zero_ext_and. vm_compute; auto. Qed. -Theorem istrue_not_isfalse: - forall v, is_false v -> is_true (notbool v). -Proof. - destruct v; simpl; try contradiction. - intros. subst i. simpl. discriminate. -Qed. - -Theorem isfalse_not_istrue: - forall v, is_true v -> is_false (notbool v). -Proof. - destruct v; simpl; try contradiction. - intros. generalize (Int.eq_spec i Int.zero). - case (Int.eq i Int.zero); intro. - contradiction. simpl. auto. - auto. -Qed. - -Theorem bool_of_true_val: - forall v, is_true v -> bool_of_val v true. -Proof. - intro. destruct v; simpl; intros; try contradiction. - constructor; auto. constructor. -Qed. - -Theorem bool_of_true_val2: - forall v, bool_of_val v true -> is_true v. -Proof. - intros. inversion H; simpl; auto. -Qed. - -Theorem bool_of_true_val_inv: - forall v b, is_true v -> bool_of_val v b -> b = true. -Proof. - intros. inversion H0; subst v b; simpl in H; auto. -Qed. - -Theorem bool_of_false_val: - forall v, is_false v -> bool_of_val v false. -Proof. - intro. destruct v; simpl; intros; try contradiction. - subst i; constructor. -Qed. - -Theorem bool_of_false_val2: - forall v, bool_of_val v false -> is_false v. +Theorem bool_of_val_of_bool: + forall b1 b2, bool_of_val (of_bool b1) b2 -> b1 = b2. Proof. - intros. inversion H; simpl; auto. + intros. destruct b1; simpl in H; inv H; auto. Qed. -Theorem bool_of_false_val_inv: - forall v b, is_false v -> bool_of_val v b -> b = false. +Theorem bool_of_val_of_optbool: + forall ob b, bool_of_val (of_optbool ob) b -> ob = Some b. Proof. - intros. inversion H0; subst v b; simpl in H. - congruence. auto. contradiction. + intros. destruct ob; simpl in H. + destruct b0; simpl in H; inv H; auto. + inv H. Qed. Theorem notbool_negb_1: @@ -932,6 +879,54 @@ Proof. destruct (Float.cmp Cgt f f0); destruct (Float.cmp Ceq f f0); auto. Qed. +Theorem cmp_ne_0_optbool: + forall ob, cmp Cne (of_optbool ob) (Vint Int.zero) = of_optbool ob. +Proof. + intros. destruct ob; simpl; auto. destruct b; auto. +Qed. + +Theorem cmp_eq_1_optbool: + forall ob, cmp Ceq (of_optbool ob) (Vint Int.one) = of_optbool ob. +Proof. + intros. destruct ob; simpl; auto. destruct b; auto. +Qed. + +Theorem cmp_eq_0_optbool: + forall ob, cmp Ceq (of_optbool ob) (Vint Int.zero) = of_optbool (option_map negb ob). +Proof. + intros. destruct ob; simpl; auto. destruct b; auto. +Qed. + +Theorem cmp_ne_1_optbool: + forall ob, cmp Cne (of_optbool ob) (Vint Int.one) = of_optbool (option_map negb ob). +Proof. + intros. destruct ob; simpl; auto. destruct b; auto. +Qed. + +Theorem cmpu_ne_0_optbool: + forall valid_ptr ob, cmpu valid_ptr Cne (of_optbool ob) (Vint Int.zero) = of_optbool ob. +Proof. + intros. destruct ob; simpl; auto. destruct b; auto. +Qed. + +Theorem cmpu_eq_1_optbool: + forall valid_ptr ob, cmpu valid_ptr Ceq (of_optbool ob) (Vint Int.one) = of_optbool ob. +Proof. + intros. destruct ob; simpl; auto. destruct b; auto. +Qed. + +Theorem cmpu_eq_0_optbool: + forall valid_ptr ob, cmpu valid_ptr Ceq (of_optbool ob) (Vint Int.zero) = of_optbool (option_map negb ob). +Proof. + intros. destruct ob; simpl; auto. destruct b; auto. +Qed. + +Theorem cmpu_ne_1_optbool: + forall valid_ptr ob, cmpu valid_ptr Cne (of_optbool ob) (Vint Int.one) = of_optbool (option_map negb ob). +Proof. + intros. destruct ob; simpl; auto. destruct b; auto. +Qed. + Lemma zero_ext_and: forall n v, 0 < n < Z_of_nat Int.wordsize -> diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v index f30bb88..27d8574 100644 --- a/ia32/SelectOpproof.v +++ b/ia32/SelectOpproof.v @@ -770,15 +770,9 @@ Theorem eval_cond_of_expr: Proof. intros until v. unfold cond_of_expr; case (cond_of_expr_match a); intros; InvEval. subst v. exists (v1 :: nil); split; auto with evalexpr. - simpl. destruct b. - generalize (Val.bool_of_true_val2 _ H0); clear H0; intro ISTRUE. - destruct v1; simpl in ISTRUE; try contradiction. - rewrite Int.eq_false; auto. - generalize (Val.bool_of_false_val2 _ H0); clear H0; intro ISFALSE. - destruct v1; simpl in ISFALSE; try contradiction. - rewrite ISFALSE. rewrite Int.eq_true; auto. + simpl. destruct v1; unfold Val.and in H0; inv H0; auto. exists (v :: nil); split; auto with evalexpr. - simpl. inversion H0; simpl. rewrite Int.eq_false; auto. auto. auto. + simpl. inv H0; auto. Qed. End CMCONSTR. diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 7d3ae83..f34dc8f 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -826,15 +826,9 @@ Theorem eval_cond_of_expr: Proof. intros until v. unfold cond_of_expr; case (cond_of_expr_match a); intros; InvEval. subst v. exists (v1 :: nil); split; auto with evalexpr. - simpl. destruct b. - generalize (Val.bool_of_true_val2 _ H0); clear H0; intro ISTRUE. - destruct v1; simpl in ISTRUE; try contradiction. - rewrite Int.eq_false; auto. - generalize (Val.bool_of_false_val2 _ H0); clear H0; intro ISFALSE. - destruct v1; simpl in ISFALSE; try contradiction. - rewrite ISFALSE. rewrite Int.eq_true; auto. + simpl. destruct v1; unfold Val.and in H0; inv H0; auto. exists (v :: nil); split; auto with evalexpr. - simpl. inversion H0; simpl. rewrite Int.eq_false; auto. auto. auto. + simpl. inv H0; auto. Qed. End CMCONSTR. |