diff options
-rw-r--r-- | backend/Selectionproof.v | 2 | ||||
-rw-r--r-- | backend/ValueDomain.v | 6 | ||||
-rw-r--r-- | cfrontend/Cop.v | 3 | ||||
-rw-r--r-- | cfrontend/Cshmgenproof.v | 1 | ||||
-rw-r--r-- | cfrontend/Ctyping.v | 1 | ||||
-rw-r--r-- | cfrontend/SimplLocalsproof.v | 3 | ||||
-rw-r--r-- | common/Values.v | 50 | ||||
-rw-r--r-- | ia32/Asmgenproof1.v | 6 | ||||
-rw-r--r-- | ia32/Op.v | 3 |
9 files changed, 44 insertions, 31 deletions
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index bb9bd592..20b6cf93 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -135,7 +135,7 @@ Proof. inv H. econstructor; eauto. (* default *) econstructor. constructor. eauto. constructor. - simpl. inv H0. auto. auto. + simpl. inv H0. auto. Qed. Lemma eval_load: diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 92004a2f..ff3ccfa1 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -2121,12 +2121,14 @@ Proof. assert (IP: forall i b ofs, cmatch (Val.cmpu_bool valid c (Vint i) (Vptr b ofs)) (cmp_different_blocks c)). { - intros. simpl. destruct (Int.eq i Int.zero). apply cmp_different_blocks_sound. apply cmp_different_blocks_none. + intros. simpl. destruct (Int.eq i Int.zero && (valid b (Int.unsigned ofs) || valid b (Int.unsigned ofs - 1))). + apply cmp_different_blocks_sound. apply cmp_different_blocks_none. } assert (PI: forall i b ofs, cmatch (Val.cmpu_bool valid c (Vptr b ofs) (Vint i)) (cmp_different_blocks c)). { - intros. simpl. destruct (Int.eq i Int.zero). apply cmp_different_blocks_sound. apply cmp_different_blocks_none. + intros. simpl. destruct (Int.eq i Int.zero && (valid b (Int.unsigned ofs) || valid b (Int.unsigned ofs - 1))). + apply cmp_different_blocks_sound. apply cmp_different_blocks_none. } unfold cmpu_bool; inversion H; subst; inversion H0; subst; auto using cmatch_top, cmp_different_blocks_none, pcmp_none, diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index 4e572277..b6b75abe 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -273,7 +273,6 @@ Definition sem_cast (v: val) (t1 t2: type) : option val := | cast_case_p2bool => match v with | Vint i => Some (Vint (cast_int_int IBool Signed i)) - | Vptr _ _ => Some (Vint Int.one) | _ => None end | cast_case_l2l => @@ -391,7 +390,6 @@ Definition bool_val (v: val) (t: type) : option bool := | bool_case_p => match v with | Vint n => Some (negb (Int.eq n Int.zero)) - | Vptr b ofs => Some true | _ => None end | bool_case_l => @@ -426,7 +424,6 @@ Definition sem_notbool (v: val) (ty: type) : option val := | bool_case_p => match v with | Vint n => Some (Val.of_bool (Int.eq n Int.zero)) - | Vptr _ _ => Some Vfalse | _ => None end | bool_case_l => diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 7f61c657..847e4856 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -333,7 +333,6 @@ Proof. econstructor; split. econstructor; eauto with cshm. simpl. eauto. unfold Val.cmpu, Val.cmpu_bool. simpl. destruct (Int.eq i Int.zero); simpl; constructor. - exists Vtrue; split. econstructor; eauto with cshm. constructor. (* long *) econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmpl. simpl. eauto. destruct (Int64.eq i Int64.zero); simpl; constructor. diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 43d34007..bdeeff2a 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -1390,7 +1390,6 @@ Proof. destruct (Float.cmp Ceq f Float.zero); constructor; auto with ty. destruct (Float32.cmp Ceq f Float32.zero); constructor; auto with ty. destruct (Int.eq i Int.zero); constructor; auto with ty. - constructor; auto with ty. destruct (Int64.eq i Int64.zero); constructor; auto with ty. - (* notint *) unfold sem_notint in SEM; DestructCases; auto with ty. diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 5cf59d94..3364ec6a 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -267,11 +267,8 @@ Proof. constructor. simpl. destruct (Float32.cmp Ceq f Float32.zero); auto. constructor. simpl. destruct (Float.cmp Ceq f Float.zero); auto. constructor. simpl. destruct (Int.eq i Int.zero); auto. - constructor; auto. constructor. simpl. destruct (Int.eq i Int.zero); auto. - constructor; auto. constructor. simpl. destruct (Int.eq i Int.zero); auto. - constructor; auto. (* long *) destruct ty; try (destruct f); try discriminate. destruct v; inv H. constructor. diff --git a/common/Values.v b/common/Values.v index a12fb636..e7dce7e9 100644 --- a/common/Values.v +++ b/common/Values.v @@ -111,15 +111,13 @@ Proof. simpl in *. InvBooleans. destruct H0. split; auto. eapply has_subtype; eauto. Qed. -(** Truth values. Pointers and non-zero integers are treated as [True]. +(** Truth values. Non-zero integers are treated as [True]. The integer 0 (also used to represent the null pointer) is [False]. - [Vundef] and floats are neither true nor false. *) + Other values are neither true nor false. *) Inductive bool_of_val: val -> bool -> Prop := | 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. + forall n, bool_of_val (Vint n) (negb (Int.eq n Int.zero)). (** Arithmetic operations *) @@ -695,7 +693,9 @@ Definition cmpu_bool (c: comparison) (v1 v2: val): option bool := | Vint n1, Vint n2 => Some (Int.cmpu c n1 n2) | Vint n1, Vptr b2 ofs2 => - if Int.eq n1 Int.zero then cmp_different_blocks c else None + if Int.eq n1 Int.zero && weak_valid_ptr b2 (Int.unsigned ofs2) + then cmp_different_blocks c + else None | Vptr b1 ofs1, Vptr b2 ofs2 => if eq_block b1 b2 then if weak_valid_ptr b1 (Int.unsigned ofs1) @@ -708,7 +708,9 @@ Definition cmpu_bool (c: comparison) (v1 v2: val): option bool := then cmp_different_blocks c else None | Vptr b1 ofs1, Vint n2 => - if Int.eq n2 Int.zero then cmp_different_blocks c else None + if Int.eq n2 Int.zero && weak_valid_ptr b1 (Int.unsigned ofs1) + then cmp_different_blocks c + else None | _, _ => None end. @@ -1175,8 +1177,8 @@ Proof. destruct c; auto. destruct x; destruct y; simpl; auto. rewrite Int.negate_cmpu. auto. - destruct (Int.eq i Int.zero); auto. - destruct (Int.eq i0 Int.zero); auto. + destruct (Int.eq i Int.zero && (valid_ptr b (Int.unsigned i0) || valid_ptr b (Int.unsigned i0 - 1))); auto. + destruct (Int.eq i0 Int.zero && (valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1))); auto. destruct (eq_block b b0). destruct ((valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1)) && (valid_ptr b0 (Int.unsigned i0) || valid_ptr b0 (Int.unsigned i0 - 1))). @@ -1222,8 +1224,8 @@ Proof. destruct c; auto. destruct x; destruct y; simpl; auto. rewrite Int.swap_cmpu. auto. - case (Int.eq i Int.zero); auto. - case (Int.eq i0 Int.zero); auto. + destruct (Int.eq i Int.zero && (valid_ptr b (Int.unsigned i0) || valid_ptr b (Int.unsigned i0 - 1))); auto. + destruct (Int.eq i0 Int.zero && (valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1))); auto. destruct (eq_block b b0); subst. rewrite dec_eq_true. destruct (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1)); @@ -1423,19 +1425,23 @@ Lemma cmpu_bool_lessdef: cmpu_bool valid_ptr' c v1' v2' = Some b. Proof. intros. + assert (A: forall b ofs, valid_ptr b ofs || valid_ptr b (ofs - 1) = true -> + valid_ptr' b ofs || valid_ptr' b (ofs - 1) = true). + { intros until ofs. rewrite ! orb_true_iff. intuition. } destruct v1; simpl in H2; try discriminate; destruct v2; simpl in H2; try discriminate; inv H0; inv H1; simpl; auto. + destruct (Int.eq i Int.zero && (valid_ptr b0 (Int.unsigned i0) || valid_ptr b0 (Int.unsigned i0 - 1))) eqn:E; try discriminate. + InvBooleans. rewrite H0, A by auto. auto. + destruct (Int.eq i0 Int.zero && (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1))) eqn:E; try discriminate. + InvBooleans. rewrite H0, A by auto. auto. destruct (eq_block b0 b1). - assert (forall b ofs, valid_ptr b ofs || valid_ptr b (ofs - 1) = true -> - valid_ptr' b ofs || valid_ptr' b (ofs - 1) = true). - intros until ofs. rewrite ! orb_true_iff. intuition. destruct (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1)) eqn:?; try discriminate. destruct (valid_ptr b1 (Int.unsigned i0) || valid_ptr b1 (Int.unsigned i0 - 1)) eqn:?; try discriminate. - erewrite !H0 by eauto. auto. + erewrite ! A by eauto. auto. destruct (valid_ptr b0 (Int.unsigned i)) eqn:?; try discriminate. destruct (valid_ptr b1 (Int.unsigned i0)) eqn:?; try discriminate. - erewrite !H by eauto. auto. + erewrite ! H by eauto. auto. Qed. Lemma of_optbool_lessdef: @@ -1599,7 +1605,17 @@ Lemma val_cmpu_bool_inject: Proof. Local Opaque Int.add. intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto. - fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1. +- fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1. + fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))). + destruct (Int.eq i Int.zero); auto. + destruct (weak_valid_ptr1 b1 (Int.unsigned ofs1)) eqn:E; try discriminate. + erewrite weak_valid_ptr_inj by eauto. auto. +- fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1. + fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))). + destruct (Int.eq i Int.zero); auto. + destruct (weak_valid_ptr1 b1 (Int.unsigned ofs1)) eqn:E; try discriminate. + erewrite weak_valid_ptr_inj by eauto. auto. +- fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1. fold (weak_valid_ptr1 b0 (Int.unsigned ofs0)) in H1. fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))). fold (weak_valid_ptr2 b3 (Int.unsigned (Int.add ofs0 (Int.repr delta0)))). diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 7d71d1a2..0ca343fb 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -462,12 +462,14 @@ Proof. rewrite (int_ltu_not i i0). destruct (Int.ltu i i0); destruct (Int.eq i i0); reflexivity. destruct (Int.ltu i i0); reflexivity. (* int ptr *) - destruct (Int.eq i Int.zero) eqn:?; try discriminate. + destruct (Int.eq i Int.zero && + (Mem.valid_pointer m b0 (Int.unsigned i0) || Mem.valid_pointer m b0 (Int.unsigned i0 - 1))) eqn:?; try discriminate. destruct c; simpl in *; inv H1. rewrite Heqb1; reflexivity. rewrite Heqb1; reflexivity. (* ptr int *) - destruct (Int.eq i0 Int.zero) eqn:?; try discriminate. + destruct (Int.eq i0 Int.zero && + (Mem.valid_pointer m b0 (Int.unsigned i) || Mem.valid_pointer m b0 (Int.unsigned i - 1))) eqn:?; try discriminate. destruct c; simpl in *; inv H1. rewrite Heqb1; reflexivity. rewrite Heqb1; reflexivity. @@ -647,6 +647,7 @@ Definition is_trivial_op (op: operation) : bool := Definition op_depends_on_memory (op: operation) : bool := match op with | Ocmp (Ccompu _) => true + | Ocmp (Ccompuimm _ _) => true | _ => false end. @@ -656,7 +657,7 @@ Lemma op_depends_on_memory_correct: eval_operation ge sp op args m1 = eval_operation ge sp op args m2. Proof. intros until m2. destruct op; simpl; try congruence. - destruct c; simpl; try congruence. reflexivity. + destruct c; simpl; auto; congruence. Qed. (** Global variables mentioned in an operation or addressing mode *) |