summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--backend/Cminor.v16
-rw-r--r--backend/Op.v66
-rw-r--r--backend/Selectionproof.v47
-rw-r--r--cfrontend/Cminorgenproof.v55
-rw-r--r--cfrontend/Csem.v2
-rw-r--r--cfrontend/Cshmgenproof2.v8
-rw-r--r--common/Mem.v24
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: