aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backend/Selectionproof.v2
-rw-r--r--backend/ValueDomain.v6
-rw-r--r--cfrontend/Cop.v3
-rw-r--r--cfrontend/Cshmgenproof.v1
-rw-r--r--cfrontend/Ctyping.v1
-rw-r--r--cfrontend/SimplLocalsproof.v3
-rw-r--r--common/Values.v50
-rw-r--r--ia32/Asmgenproof1.v6
-rw-r--r--ia32/Op.v3
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.
diff --git a/ia32/Op.v b/ia32/Op.v
index 846d094f..ecc67c46 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -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 *)
generated by cgit (git 2.34.1) at 2024-06-02 14:29:16 +0000