summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Changelog4
-rw-r--r--arm/Asmgen.v8
-rw-r--r--arm/Asmgenproof.v4
-rw-r--r--arm/Asmgenproof1.v16
-rw-r--r--arm/Op.v123
-rw-r--r--backend/Inlining.v2
-rw-r--r--backend/Inliningproof.v10
-rw-r--r--backend/Inliningspec.v4
-rw-r--r--backend/Reloadtyping.v5
-rw-r--r--cfrontend/Cminorgenproof.v41
-rw-r--r--cfrontend/Cop.v29
-rw-r--r--cfrontend/Cshmgenproof.v3
-rw-r--r--cfrontend/Initializersproof.v15
-rw-r--r--cfrontend/SimplLocalsproof.v45
-rw-r--r--common/Events.v6
-rw-r--r--common/Memory.v173
-rw-r--r--common/Memtype.v53
-rw-r--r--common/Values.v167
-rw-r--r--ia32/Asmgenproof1.v9
-rw-r--r--ia32/Op.v88
-rw-r--r--powerpc/Op.v84
21 files changed, 565 insertions, 324 deletions
diff --git a/Changelog b/Changelog
index 81429ef..243cdff 100644
--- a/Changelog
+++ b/Changelog
@@ -7,7 +7,9 @@ Development version
reductions to be incorrectly merged.
- Better error and warning messages for declarations of variables
of size >= 2^32 bits.
-
+- Comparisons involving pointers "one past" the end of a block are
+ now defined. (They used to be undefined behavior.)
+ (Contributed by Robbert Krebbers).
Release 1.12.1, 2013-01-29
==========================
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index b78dfb6..05e7010 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -57,9 +57,9 @@ Definition is_immed_mem_float (x: int) : bool :=
Fixpoint decompose_int_rec (N: nat) (n p: int) : list int :=
match N with
| Datatypes.O =>
- if Int.eq_dec n Int.zero then nil else n :: nil
+ if Int.eq n Int.zero then nil else n :: nil
| Datatypes.S M =>
- if Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero then
+ if Int.eq (Int.and n (Int.shl (Int.repr 3) p)) Int.zero then
decompose_int_rec M n (Int.add p (Int.repr 2))
else
let m := Int.shl (Int.repr 255) p in
@@ -86,14 +86,14 @@ Definition iterate_op (op1 op2: shift_op -> instruction) (l: list int) (k: code)
Definition loadimm (r: ireg) (n: int) (k: code) :=
let d1 := decompose_int n in
let d2 := decompose_int (Int.not n) in
- if le_dec (List.length d1) (List.length d2)
+ if NPeano.leb (List.length d1) (List.length d2)
then iterate_op (Pmov r) (Porr r r) d1 k
else iterate_op (Pmvn r) (Pbic r r) d2 k.
Definition addimm (r1 r2: ireg) (n: int) (k: code) :=
let d1 := decompose_int n in
let d2 := decompose_int (Int.neg n) in
- if le_dec (List.length d1) (List.length d2)
+ if NPeano.leb (List.length d1) (List.length d2)
then iterate_op (Padd r1 r2) (Padd r1 r1) d1 k
else iterate_op (Psub r1 r2) (Psub r1 r1) d2 k.
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index b0598e9..365917c 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -348,7 +348,7 @@ Remark loadimm_label:
forall r n k, find_label lbl (loadimm r n k) = find_label lbl k.
Proof.
intros. unfold loadimm.
- destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.not n))));
+ destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.not n))));
auto with labels.
Qed.
Hint Rewrite loadimm_label: labels.
@@ -357,7 +357,7 @@ Remark addimm_label:
forall r1 r2 n k, find_label lbl (addimm r1 r2 n k) = find_label lbl k.
Proof.
intros; unfold addimm.
- destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.neg n))));
+ destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.neg n))));
auto with labels.
Qed.
Hint Rewrite addimm_label: labels.
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index 19edcd9..658fc98 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -480,10 +480,10 @@ Lemma decompose_int_rec_or:
forall N n p x, List.fold_left Int.or (decompose_int_rec N n p) x = Int.or x n.
Proof.
induction N; intros; simpl.
- destruct (Int.eq_dec n Int.zero); simpl.
+ predSpec Int.eq Int.eq_spec n Int.zero; simpl.
subst n. rewrite Int.or_zero. auto.
auto.
- destruct (Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero).
+ predSpec Int.eq Int.eq_spec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero.
auto.
simpl. rewrite IHN. rewrite Int.or_assoc. decEq. rewrite <- Int.and_or_distrib.
rewrite Int.or_not_self. apply Int.and_mone.
@@ -493,10 +493,10 @@ Lemma decompose_int_rec_xor:
forall N n p x, List.fold_left Int.xor (decompose_int_rec N n p) x = Int.xor x n.
Proof.
induction N; intros; simpl.
- destruct (Int.eq_dec n Int.zero); simpl.
+ predSpec Int.eq Int.eq_spec n Int.zero; simpl.
subst n. rewrite Int.xor_zero. auto.
auto.
- destruct (Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero).
+ predSpec Int.eq Int.eq_spec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero.
auto.
simpl. rewrite IHN. rewrite Int.xor_assoc. decEq. rewrite <- Int.and_xor_distrib.
rewrite Int.xor_not_self. apply Int.and_mone.
@@ -506,10 +506,10 @@ Lemma decompose_int_rec_add:
forall N n p x, List.fold_left Int.add (decompose_int_rec N n p) x = Int.add x n.
Proof.
induction N; intros; simpl.
- destruct (Int.eq_dec n Int.zero); simpl.
+ predSpec Int.eq Int.eq_spec n Int.zero; simpl.
subst n. rewrite Int.add_zero. auto.
auto.
- destruct (Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero).
+ predSpec Int.eq Int.eq_spec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero.
auto.
simpl. rewrite IHN. rewrite Int.add_assoc. decEq. rewrite Int.add_and.
rewrite Int.or_not_self. apply Int.and_mone. apply Int.and_not_self.
@@ -647,7 +647,7 @@ Lemma loadimm_correct:
/\ forall r': preg, r' <> r -> r' <> PC -> rs'#r' = rs#r'.
Proof.
intros. unfold loadimm.
- destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.not n)))).
+ destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.not n)))).
(* mov - orr* *)
replace (Vint n) with (List.fold_left (fun v i => Val.or v (Vint i)) (decompose_int n) Vzero).
apply iterate_op_correct.
@@ -672,7 +672,7 @@ Lemma addimm_correct:
/\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
Proof.
intros. unfold addimm.
- destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.neg n)))).
+ destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.neg n)))).
(* add - add* *)
replace (Val.add (rs r2) (Vint n))
with (List.fold_left (fun v i => Val.add v (Vint i)) (decompose_int n) (rs r2)).
diff --git a/arm/Op.v b/arm/Op.v
index f26bccc..291d64f 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -697,10 +697,16 @@ Hypothesis valid_pointer_inj:
Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
-Hypothesis valid_pointer_no_overflow:
+Hypothesis weak_valid_pointer_inj:
forall b1 ofs b2 delta,
f b1 = Some(b2, delta) ->
- Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+ Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+ Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+
+Hypothesis weak_valid_pointer_no_overflow:
+ forall b1 ofs b2 delta,
+ f b1 = Some(b2, delta) ->
+ Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
Hypothesis valid_different_pointers_inj:
@@ -728,25 +734,6 @@ Ltac InvInject :=
| _ => idtac
end.
-Remark val_add_inj:
- forall v1 v1' v2 v2',
- val_inject f v1 v1' -> val_inject f v2 v2' -> val_inject f (Val.add v1 v2) (Val.add v1' v2').
-Proof.
- intros. inv H; inv H0; simpl; econstructor; eauto.
- repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
- repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-Qed.
-
-Remark val_sub_inj:
- forall v1 v1' v2 v2',
- val_inject f v1 v1' -> val_inject f v2 v2' -> val_inject f (Val.sub v1 v2) (Val.sub v1' v2').
-Proof.
- intros. inv H; inv H0; simpl; auto.
- econstructor; eauto. rewrite Int.sub_add_l. auto.
- destruct (zeq b1 b0); auto. subst. rewrite H1 in H. inv H. rewrite zeq_true.
- rewrite Int.sub_shifted. auto.
-Qed.
-
Remark eval_shift_inj:
forall s v v', val_inject f v v' -> val_inject f (eval_shift s v) (eval_shift s v').
Proof.
@@ -759,45 +746,13 @@ Lemma eval_condition_inj:
eval_condition cond vl1 m1 = Some b ->
eval_condition cond vl2 m2 = Some b.
Proof.
-Opaque Int.add.
- assert (CMP:
- forall c v1 v2 v1' v2' b,
- val_inject f v1 v1' ->
- val_inject f v2 v2' ->
- Val.cmp_bool c v1 v2 = Some b ->
- Val.cmp_bool c v1' v2' = Some b).
- intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto.
-
- assert (CMPU:
- forall c v1 v2 v1' v2' b,
- val_inject f v1 v1' ->
- val_inject f v2 v2' ->
- Val.cmpu_bool (Mem.valid_pointer m1) c v1 v2 = Some b ->
- Val.cmpu_bool (Mem.valid_pointer m2) c v1' v2' = Some b).
- intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto.
- destruct (Mem.valid_pointer m1 b1 (Int.unsigned ofs1)) eqn:?; try discriminate.
- destruct (Mem.valid_pointer m1 b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
- rewrite (valid_pointer_inj _ H2 Heqb4).
- rewrite (valid_pointer_inj _ H Heqb0). simpl.
- destruct (zeq b1 b0); simpl in H1.
- inv H1. rewrite H in H2; inv H2. rewrite zeq_true.
- decEq. apply Int.translate_cmpu.
- eapply valid_pointer_no_overflow; eauto.
- eapply valid_pointer_no_overflow; eauto.
- exploit valid_different_pointers_inj; eauto. intros P.
- destruct (zeq b2 b3); auto.
- destruct P. congruence.
- destruct c; simpl in H1; inv H1.
- simpl; decEq. rewrite Int.eq_false; auto. congruence.
- simpl; decEq. rewrite Int.eq_false; auto. congruence.
-
intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl.
- eapply CMP; eauto.
- eapply CMPU; eauto.
- eapply CMP. eauto. eapply eval_shift_inj. eauto. auto.
- eapply CMPU. eauto. eapply eval_shift_inj. eauto. auto.
- eapply CMP; try eassumption; eauto.
- eapply CMPU; try eassumption; eauto.
+ eauto 4 using val_cmp_bool_inject.
+ eauto 4 using val_cmpu_bool_inject, Mem.valid_pointer_implies.
+ eauto using val_cmp_bool_inject, eval_shift_inj.
+ eauto 4 using val_cmpu_bool_inject, Mem.valid_pointer_implies, eval_shift_inj.
+ eauto 4 using val_cmp_bool_inject.
+ eauto 4 using val_cmpu_bool_inject, Mem.valid_pointer_implies.
inv H3; inv H2; simpl in H0; inv H0; auto.
inv H3; inv H2; simpl in H0; inv H0; auto.
inv H3; simpl in H0; inv H0; auto.
@@ -819,15 +774,15 @@ Lemma eval_operation_inj:
exists v2, eval_operation genv sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2.
Proof.
intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
- apply val_add_inj; auto.
- apply val_add_inj; auto.
- apply val_add_inj; auto. apply eval_shift_inj; auto.
- apply val_add_inj; auto.
+ apply Values.val_add_inject; auto.
+ apply Values.val_add_inject; auto.
+ apply Values.val_add_inject; auto. apply eval_shift_inj; auto.
+ apply Values.val_add_inject; auto.
- apply val_sub_inj; auto.
- apply val_sub_inj; auto. apply eval_shift_inj; auto.
- apply val_sub_inj; auto. apply eval_shift_inj; auto.
- apply (@val_sub_inj (Vint i) (Vint i) v v'); auto.
+ apply Values.val_sub_inject; auto.
+ apply Values.val_sub_inject; auto. apply eval_shift_inj; auto.
+ apply Values.val_sub_inject; auto. apply eval_shift_inj; auto.
+ apply (@Values.val_sub_inject f (Vint i) (Vint i) v v'); auto.
inv H4; inv H2; simpl; auto.
inv H4; inv H3; simpl in H1; inv H1. simpl.
@@ -888,10 +843,10 @@ Proof.
val_inject f (symbol_address genv id ofs) (symbol_address genv id ofs)).
exact symbol_address_inj.
intros. destruct addr; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
- apply val_add_inj; auto.
- apply val_add_inj; auto.
- apply val_add_inj; auto. apply eval_shift_inj; auto.
- apply val_add_inj; auto.
+ apply Values.val_add_inject; auto.
+ apply Values.val_add_inject; auto.
+ apply Values.val_add_inject; auto. apply eval_shift_inj; auto.
+ apply Values.val_add_inject; auto.
Qed.
End EVAL_COMPAT.
@@ -913,10 +868,20 @@ Proof.
intros. inv H0. rewrite Int.add_zero. eapply Mem.valid_pointer_extends; eauto.
Qed.
-Remark valid_pointer_no_overflow_extends:
+Remark weak_valid_pointer_extends:
+ forall m1 m2, Mem.extends m1 m2 ->
+ forall b1 ofs b2 delta,
+ Some(b1, 0) = Some(b2, delta) ->
+ Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+ Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+Proof.
+ intros. inv H0. rewrite Int.add_zero. eapply Mem.weak_valid_pointer_extends; eauto.
+Qed.
+
+Remark weak_valid_pointer_no_overflow_extends:
forall m1 b1 ofs b2 delta,
Some(b1, 0) = Some(b2, delta) ->
- Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+ Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
Proof.
intros. inv H. rewrite Zplus_0_r. apply Int.unsigned_range_2.
@@ -944,7 +909,8 @@ Lemma eval_condition_lessdef:
Proof.
intros. eapply eval_condition_inj with (f := fun b => Some(b, 0)) (m1 := m1).
apply valid_pointer_extends; auto.
- apply valid_pointer_no_overflow_extends; auto.
+ apply weak_valid_pointer_extends; auto.
+ apply weak_valid_pointer_no_overflow_extends.
apply valid_different_pointers_extends; auto.
rewrite <- val_list_inject_lessdef. eauto. auto.
Qed.
@@ -963,7 +929,8 @@ Proof.
eapply eval_operation_inj with (m1 := m1) (sp1 := sp).
intros. rewrite <- val_inject_lessdef; auto.
apply valid_pointer_extends; auto.
- apply valid_pointer_no_overflow_extends; auto.
+ apply weak_valid_pointer_extends; auto.
+ apply weak_valid_pointer_no_overflow_extends.
apply valid_different_pointers_extends; auto.
rewrite <- val_inject_lessdef; auto.
eauto. auto.
@@ -1019,7 +986,8 @@ Lemma eval_condition_inject:
Proof.
intros. eapply eval_condition_inj with (f := f) (m1 := m1); eauto.
intros; eapply Mem.valid_pointer_inject_val; eauto.
- intros; eapply Mem.valid_pointer_inject_no_overflow; eauto.
+ intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
+ intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
intros; eapply Mem.different_pointers_inject; eauto.
Qed.
@@ -1051,7 +1019,8 @@ Proof.
eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto.
exact symbol_address_inject.
intros; eapply Mem.valid_pointer_inject_val; eauto.
- intros; eapply Mem.valid_pointer_inject_no_overflow; eauto.
+ intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
+ intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
intros; eapply Mem.different_pointers_inject; eauto.
Qed.
diff --git a/backend/Inlining.v b/backend/Inlining.v
index 5075fd6..a9b1e7e 100644
--- a/backend/Inlining.v
+++ b/backend/Inlining.v
@@ -454,7 +454,7 @@ Local Open Scope string_scope.
Definition transf_function (fenv: funenv) (f: function) : Errors.res function :=
let '(R ctx s _) := expand_function fenv f initstate in
- if zle s.(st_stksize) Int.max_unsigned then
+ if zlt s.(st_stksize) Int.max_unsigned then
OK (mkfunction f.(fn_sig)
(sregs ctx f.(fn_params))
s.(st_stksize)
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index 9536141..ba61ed0 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -398,7 +398,7 @@ Inductive match_stacks (F: meminj) (m m': mem):
(AG: agree_regs F ctx rs rs')
(SP: F sp = Some(sp', ctx.(dstk)))
(PRIV: range_private F m m' sp' (ctx.(dstk) + ctx.(mstk)) f'.(fn_stacksize))
- (SSZ1: 0 <= f'.(fn_stacksize) <= Int.max_unsigned)
+ (SSZ1: 0 <= f'.(fn_stacksize) < Int.max_unsigned)
(SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize))
(RES: Ple res ctx.(mreg))
(BELOW: sp' < bound),
@@ -409,7 +409,7 @@ Inductive match_stacks (F: meminj) (m m': mem):
| match_stacks_untailcall: forall stk res f' sp' rpc rs' stk' bound ctx
(MS: match_stacks_inside F m m' stk stk' f' ctx sp' rs')
(PRIV: range_private F m m' sp' ctx.(dstk) f'.(fn_stacksize))
- (SSZ1: 0 <= f'.(fn_stacksize) <= Int.max_unsigned)
+ (SSZ1: 0 <= f'.(fn_stacksize) < Int.max_unsigned)
(SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize))
(RET: ctx.(retinfo) = Some (rpc, res))
(BELOW: sp' < bound),
@@ -775,7 +775,7 @@ Inductive match_states: state -> state -> Prop :=
(MINJ: Mem.inject F m m')
(VB: Mem.valid_block m' sp')
(PRIV: range_private F m m' sp' (ctx.(dstk) + ctx.(mstk)) f'.(fn_stacksize))
- (SSZ1: 0 <= f'.(fn_stacksize) <= Int.max_unsigned)
+ (SSZ1: 0 <= f'.(fn_stacksize) < Int.max_unsigned)
(SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize)),
match_states (State stk f (Vptr sp Int.zero) pc rs m)
(State stk' f' (Vptr sp' Int.zero) (spc ctx pc) rs' m')
@@ -796,7 +796,7 @@ Inductive match_states: state -> state -> Prop :=
(MINJ: Mem.inject F m m')
(VB: Mem.valid_block m' sp')
(PRIV: range_private F m m' sp' ctx.(dstk) f'.(fn_stacksize))
- (SSZ1: 0 <= f'.(fn_stacksize) <= Int.max_unsigned)
+ (SSZ1: 0 <= f'.(fn_stacksize) < Int.max_unsigned)
(SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize)),
match_states (Callstate stk (Internal f) vargs m)
(State stk' f' (Vptr sp' Int.zero) pc' rs' m')
@@ -814,7 +814,7 @@ Inductive match_states: state -> state -> Prop :=
(MINJ: Mem.inject F m m')
(VB: Mem.valid_block m' sp')
(PRIV: range_private F m m' sp' ctx.(dstk) f'.(fn_stacksize))
- (SSZ1: 0 <= f'.(fn_stacksize) <= Int.max_unsigned)
+ (SSZ1: 0 <= f'.(fn_stacksize) < Int.max_unsigned)
(SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize)),
match_states (Returnstate stk v m)
(State stk' f' (Vptr sp' Int.zero) pc' rs' m').
diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v
index 06826c2..82ef9cf 100644
--- a/backend/Inliningspec.v
+++ b/backend/Inliningspec.v
@@ -664,7 +664,7 @@ Inductive tr_function: function -> function -> Prop :=
f'.(fn_sig) = f.(fn_sig) ->
f'.(fn_params) = sregs ctx f.(fn_params) ->
f'.(fn_entrypoint) = spc ctx f.(fn_entrypoint) ->
- 0 <= fn_stacksize f' <= Int.max_unsigned ->
+ 0 <= fn_stacksize f' < Int.max_unsigned ->
tr_function f f'.
Lemma transf_function_spec:
@@ -672,7 +672,7 @@ Lemma transf_function_spec:
Proof.
intros. unfold transf_function in H.
destruct (expand_function fenv f initstate) as [ctx s i] eqn:?.
- destruct (zle (st_stksize s) Int.max_unsigned); inv H.
+ destruct (zlt (st_stksize s) Int.max_unsigned); inv H.
monadInv Heqr. set (ctx := initcontext x x0 (max_def_function f) (fn_stacksize f)) in *.
Opaque initstate.
destruct INCR3. inversion EQ1. inversion EQ.
diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v
index 9f5563c..c005139 100644
--- a/backend/Reloadtyping.v
+++ b/backend/Reloadtyping.v
@@ -288,8 +288,7 @@ Proof.
rewrite loc_arguments_type; auto.
destruct ros. destruct H2 as [A [B C]]. auto 10 with reloadty.
auto 10 with reloadty.
-
- destruct (ef_reloads ef) as [] eqn:?.
+ destruct (ef_reloads ef) eqn:?.
assert (arity_ok (sig_args (ef_sig ef)) = true) by intuition congruence.
assert (map mreg_type (regs_for args) = map Loc.type args).
apply wt_regs_for. apply arity_ok_enough. congruence.
@@ -297,8 +296,6 @@ Proof.
auto 10 with reloadty.
auto with reloadty.
-
-
assert (map mreg_type (regs_for args) = map Loc.type args).
eauto with reloadty.
auto with reloadty.
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 9bbf040..a61808a 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -1573,26 +1573,37 @@ Proof.
apply val_inject_val_of_optbool.
apply val_inject_val_of_optbool.
Opaque Int.add.
- unfold Val.cmpu. simpl.
- destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) eqn:?; simpl; auto.
- destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; simpl; auto.
- exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb. econstructor; eauto.
- intros V1. rewrite V1.
- exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb0. econstructor; eauto.
- intros V2. rewrite V2. simpl.
- destruct (zeq b1 b0).
+ unfold Val.cmpu. simpl.
+ destruct (zeq b1 b0); subst.
(* same blocks *)
- subst b1. rewrite H in H0; inv H0. rewrite zeq_true.
- rewrite Int.translate_cmpu. apply val_inject_val_of_optbool.
- eapply Mem.valid_pointer_inject_no_overflow; eauto.
- eapply Mem.valid_pointer_inject_no_overflow; eauto.
+ rewrite H0 in H. inv H. rewrite zeq_true.
+ fold (Mem.weak_valid_pointer m b0 (Int.unsigned ofs1)).
+ fold (Mem.weak_valid_pointer m b0 (Int.unsigned ofs0)).
+ fold (Mem.weak_valid_pointer tm b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))).
+ fold (Mem.weak_valid_pointer tm b2 (Int.unsigned (Int.add ofs0 (Int.repr delta)))).
+ destruct (Mem.weak_valid_pointer m b0 (Int.unsigned ofs1)) eqn:?; auto.
+ destruct (Mem.weak_valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; auto.
+ rewrite (Mem.weak_valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb) by eauto.
+ rewrite (Mem.weak_valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb0) by eauto.
+ rewrite Int.translate_cmpu
+ by eauto using Mem.weak_valid_pointer_inject_no_overflow.
+ apply val_inject_val_of_optbool.
(* different source blocks *)
+ destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) eqn:?; auto.
+ destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; auto.
destruct (zeq b2 b3).
- exploit Mem.different_pointers_inject; eauto. intros [A|A].
- congruence.
- destruct c; simpl; auto.
+ fold (Mem.weak_valid_pointer tm b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))).
+ fold (Mem.weak_valid_pointer tm b3 (Int.unsigned (Int.add ofs0 (Int.repr delta0)))).
+ rewrite Mem.valid_pointer_implies
+ by (eapply (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb); eauto).
+ rewrite Mem.valid_pointer_implies
+ by (eapply (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb0); eauto).
+ exploit Mem.different_pointers_inject; eauto. intros [A|A]; [congruence |].
+ destruct c; simpl; auto.
rewrite Int.eq_false. constructor. congruence.
rewrite Int.eq_false. constructor. congruence.
+ rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb) by eauto.
+ rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb0) by eauto.
apply val_inject_val_of_optbool.
(* cmpf *)
inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool.
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index 9d581b6..af7aaa8 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -714,13 +714,6 @@ Definition classify_cmp (ty1: type) (ty2: type) :=
| _ , _ => cmp_default
end.
-Function sem_cmp_mismatch (c: comparison): option val :=
- match c with
- | Ceq => Some Vfalse
- | Cne => Some Vtrue
- | _ => None
- end.
-
Function sem_cmp (c:comparison)
(v1: val) (t1: type) (v2: val) (t2: type)
(m: mem): option val :=
@@ -739,16 +732,24 @@ Function sem_cmp (c:comparison)
match v1,v2 with
| Vint n1, Vint n2 => Some (Val.of_bool (Int.cmpu c n1 n2))
| Vptr b1 ofs1, Vptr b2 ofs2 =>
- if Mem.valid_pointer m b1 (Int.unsigned ofs1)
- && Mem.valid_pointer m b2 (Int.unsigned ofs2) then
- if zeq b1 b2
+ if zeq b1 b2 then
+ if Mem.weak_valid_pointer m b1 (Int.unsigned ofs1)
+ && Mem.weak_valid_pointer m b2 (Int.unsigned ofs2)
then Some (Val.of_bool (Int.cmpu c ofs1 ofs2))
- else sem_cmp_mismatch c
- else None
+ else None
+ else
+ if Mem.valid_pointer m b1 (Int.unsigned ofs1)
+ && Mem.valid_pointer m b2 (Int.unsigned ofs2)
+ then option_map Val.of_bool (Val.cmp_different_blocks c)
+ else None
| Vptr b ofs, Vint n =>
- if Int.eq n Int.zero then sem_cmp_mismatch c else None
+ if Int.eq n Int.zero
+ then option_map Val.of_bool (Val.cmp_different_blocks c)
+ else None
| Vint n, Vptr b ofs =>
- if Int.eq n Int.zero then sem_cmp_mismatch c else None
+ if Int.eq n Int.zero
+ then option_map Val.of_bool (Val.cmp_different_blocks c)
+ else None
| _, _ => None
end
| cmp_case_ff =>
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 74a6da5..ad5ada6 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -574,7 +574,8 @@ Proof.
inversion H8. eauto with cshm.
(* pp ptr ptr *)
inversion H10. eapply eval_Ebinop; eauto with cshm.
- simpl. unfold Val.cmpu. simpl. rewrite H3. rewrite H9. auto.
+ simpl. unfold Val.cmpu. simpl. unfold Mem.weak_valid_pointer in *.
+ rewrite H3. rewrite H9. auto.
inversion H10. eapply eval_Ebinop; eauto with cshm.
simpl. unfold Val.cmpu. simpl. rewrite H3. rewrite H9.
destruct cmp; simpl in *; inv H; auto.
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index ca9c5b0..b64c309 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -380,6 +380,13 @@ Proof.
eelim Mem.perm_empty; eauto.
Qed.
+Lemma mem_empty_not_weak_valid_pointer:
+ forall b ofs, Mem.weak_valid_pointer Mem.empty b ofs = false.
+Proof.
+ intros. unfold Mem.weak_valid_pointer.
+ now rewrite !mem_empty_not_valid_pointer.
+Qed.
+
Lemma sem_cmp_match:
forall c v1 ty1 v2 ty2 m v v1' v2' v',
sem_cmp c v1 ty1 v2 ty2 Mem.empty = Some v ->
@@ -391,10 +398,12 @@ Opaque zeq.
intros. unfold sem_cmp in *.
destruct (classify_cmp ty1 ty2); try (destruct s); inv H1; inv H2; inv H; inv H0; auto with mval.
destruct (Int.eq n Int.zero); try discriminate.
- unfold sem_cmp_mismatch in *. destruct c; inv H3; inv H2; constructor.
+ unfold Val.cmp_different_blocks in *. destruct c; inv H3; inv H2; constructor.
destruct (Int.eq n Int.zero); try discriminate.
- unfold sem_cmp_mismatch in *. destruct c; inv H2; inv H1; constructor.
- rewrite (mem_empty_not_valid_pointer (Zpos id) (Int.unsigned ofs)) in H4. discriminate.
+ unfold Val.cmp_different_blocks in *. destruct c; inv H2; inv H1; constructor.
+ rewrite (mem_empty_not_valid_pointer (Zpos id) (Int.unsigned ofs)) in H4.
+ rewrite (mem_empty_not_weak_valid_pointer (Zpos id) (Int.unsigned ofs)) in H4. simpl in H4.
+ destruct (zeq (Z.pos id) (Z.pos id0)); discriminate.
Qed.
Lemma sem_binary_match:
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index c496a5e..e3aa4e2 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -1006,8 +1006,8 @@ Proof.
apply RPSRC. omega.
assert (PDST: Mem.perm m bdst (Int.unsigned odst) Cur Nonempty).
apply RPDST. omega.
- exploit Mem.address_inject. eauto. apply Mem.perm_cur_max. eexact PSRC. eauto. intros EQ1.
- exploit Mem.address_inject. eauto. apply Mem.perm_cur_max. eexact PDST. eauto. intros EQ2.
+ exploit Mem.address_inject. eauto. eexact PSRC. eauto. intros EQ1.
+ exploit Mem.address_inject. eauto. eexact PDST. eauto. intros EQ2.
exploit Mem.loadbytes_inject; eauto. intros [bytes2 [A B]].
exploit Mem.storebytes_mapped_inject; eauto. intros [tm' [C D]].
exists tm'.
@@ -1372,35 +1372,44 @@ Lemma sem_cmp_inject:
exists tv, sem_cmp cmp tv1 ty1 tv2 ty2 tm = Some tv /\ val_inject f v tv.
Proof.
unfold sem_cmp; intros.
- assert (MM: sem_cmp_mismatch cmp = Some v ->
- exists tv, sem_cmp_mismatch cmp = Some tv /\ val_inject f v tv).
+ assert (MM: option_map Val.of_bool (Val.cmp_different_blocks cmp) = Some v ->
+ exists tv, option_map Val.of_bool (Val.cmp_different_blocks cmp) = Some tv /\ val_inject f v tv).
intros. exists v; split; auto.
destruct cmp; simpl in H2; inv H2; auto.
destruct (classify_cmp ty1 ty2); try destruct s; inv H0; try discriminate; inv H1; inv H; TrivialInject.
destruct (Int.eq i Int.zero); try discriminate; auto.
destruct (Int.eq i Int.zero); try discriminate; auto.
- destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) eqn:?; try discriminate.
- destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
- simpl in H3.
- rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb).
- rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb0).
- simpl.
- destruct (zeq b1 b0). subst b1. rewrite H0 in H2; inv H2. rewrite zeq_true.
- replace (Int.cmpu cmp (Int.add ofs1 (Int.repr delta))
+
+ destruct (zeq b1 b0); subst.
+ rewrite H0 in H2. inv H2. rewrite zeq_true.
+ destruct (Mem.weak_valid_pointer m b0 (Int.unsigned ofs1)) eqn:?; try discriminate.
+ destruct (Mem.weak_valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
+ simpl H3.
+ rewrite (Mem.weak_valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb) by eauto.
+ rewrite (Mem.weak_valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb0) by eauto.
+ simpl. replace (Int.cmpu cmp (Int.add ofs1 (Int.repr delta))
(Int.add ofs0 (Int.repr delta)))
with (Int.cmpu cmp ofs1 ofs0).
inv H3; TrivialInject.
symmetry. apply Int.translate_cmpu.
- eapply Mem.valid_pointer_inject_no_overflow; eauto.
- eapply Mem.valid_pointer_inject_no_overflow; eauto.
- destruct (zeq b2 b3).
- exploit Mem.different_pointers_inject; eauto. intros [A|A]. contradiction.
+ eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
+ eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
+ destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) eqn:?; try discriminate.
+ destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
+ destruct (zeq b2 b3); subst.
+ rewrite Mem.valid_pointer_implies
+ by (eapply (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb); eauto).
+ rewrite Mem.valid_pointer_implies
+ by (eapply (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb0); eauto).
+ simpl.
+ exploit Mem.different_pointers_inject; eauto. intros [[]|A]. easy.
destruct cmp; simpl in H3; inv H3.
simpl. unfold Int.eq. rewrite zeq_false; auto.
simpl. unfold Int.eq. rewrite zeq_false; auto.
- auto.
- econstructor; eauto. econstructor; eauto.
+ rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb) by eauto.
+ rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb0) by eauto.
+ simpl in H3 |- *. auto.
Qed.
Lemma sem_binary_operation_inject:
diff --git a/common/Events.v b/common/Events.v
index fd1acd0..3f81e60 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1229,7 +1229,7 @@ Proof.
assert (Mem.range_perm m1 b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz) Cur Freeable).
eapply Mem.free_range_perm; eauto.
exploit Mem.address_inject; eauto.
- apply Mem.perm_implies with Freeable; auto with mem. apply Mem.perm_cur_max.
+ apply Mem.perm_implies with Freeable; auto with mem.
apply H0. instantiate (1 := lo). omega.
intro EQ.
assert (Mem.range_perm m1' b2 (Int.unsigned lo + delta - 4) (Int.unsigned lo + delta + Int.unsigned sz) Cur Freeable).
@@ -1357,8 +1357,8 @@ Proof.
apply RPSRC. omega.
assert (PDST: Mem.perm m1 bdst (Int.unsigned odst) Cur Nonempty).
apply RPDST. omega.
- exploit Mem.address_inject. eauto. apply Mem.perm_cur_max. eexact PSRC. eauto. intros EQ1.
- exploit Mem.address_inject. eauto. apply Mem.perm_cur_max. eexact PDST. eauto. intros EQ2.
+ exploit Mem.address_inject. eauto. eexact PSRC. eauto. intros EQ1.
+ exploit Mem.address_inject. eauto. eexact PDST. eauto. intros EQ2.
exploit Mem.loadbytes_inject; eauto. intros [bytes2 [A B]].
exploit Mem.storebytes_mapped_inject; eauto. intros [m2' [C D]].
exists f; exists Vundef; exists m2'.
diff --git a/common/Memory.v b/common/Memory.v
index 514e1e0..04a3dda 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -287,9 +287,8 @@ Proof.
right; red; intro V; inv V; contradiction.
Qed.
-(** [valid_pointer] is a boolean-valued function that says whether
- the byte at the given location is nonempty. *)
-
+(** [valid_pointer m b ofs] returns [true] if the address [b, ofs]
+ is nonempty in [m] and [false] if it is empty. *)
Definition valid_pointer (m: mem) (b: block) (ofs: Z): bool :=
perm_dec m b ofs Cur Nonempty.
@@ -313,6 +312,28 @@ Proof.
destruct H. apply H. simpl. omega.
Qed.
+(** C allows pointers one past the last element of an array. These are not
+ valid according to the previously defined [valid_pointer]. The property
+ [weak_valid_pointer m b ofs] holds if address [b, ofs] is a valid pointer
+ in [m], or a pointer one past a valid block in [m]. *)
+
+Definition weak_valid_pointer (m: mem) (b: block) (ofs: Z) :=
+ valid_pointer m b ofs || valid_pointer m b (ofs - 1).
+
+Lemma weak_valid_pointer_spec:
+ forall m b ofs,
+ weak_valid_pointer m b ofs = true <->
+ valid_pointer m b ofs = true \/ valid_pointer m b (ofs - 1) = true.
+Proof.
+ intros. unfold weak_valid_pointer. now rewrite orb_true_iff.
+Qed.
+Lemma valid_pointer_implies:
+ forall m b ofs,
+ valid_pointer m b ofs = true -> weak_valid_pointer m b ofs = true.
+Proof.
+ intros. apply weak_valid_pointer_spec. auto.
+Qed.
+
(** * Operations over memory stores *)
(** The initial store *)
@@ -2887,6 +2908,15 @@ Proof.
eapply valid_access_extends; eauto.
Qed.
+Theorem weak_valid_pointer_extends:
+ forall m1 m2 b ofs,
+ extends m1 m2 ->
+ weak_valid_pointer m1 b ofs = true -> weak_valid_pointer m2 b ofs = true.
+Proof.
+ intros until 1. unfold weak_valid_pointer. rewrite !orb_true_iff.
+ intros []; eauto using valid_pointer_extends.
+Qed.
+
(** * Memory injections *)
(** A memory state [m1] injects into another memory state [m2] via the
@@ -2899,7 +2929,8 @@ Qed.
- if [f b = Some(b', delta)], [b'] must be valid in [m2];
- distinct blocks in [m1] are mapped to non-overlapping sub-blocks in [m2];
- the sizes of [m2]'s blocks are representable with unsigned machine integers;
-- the offsets [delta] are representable with unsigned machine integers.
+- pointers that could be represented using unsigned machine integers remain
+ representable after the injection.
*)
Record inject' (f: meminj) (m1 m2: mem) : Prop :=
@@ -2913,12 +2944,11 @@ Record inject' (f: meminj) (m1 m2: mem) : Prop :=
mi_no_overlap:
meminj_no_overlap f m1;
mi_representable:
- forall b b' delta ofs k p,
+ forall b b' delta ofs,
f b = Some(b', delta) ->
- perm m1 b (Int.unsigned ofs) k p ->
+ weak_valid_pointer m1 b (Int.unsigned ofs) = true ->
delta >= 0 /\ 0 <= Int.unsigned ofs + delta <= Int.max_unsigned
}.
-
Definition inject := inject'.
Local Hint Resolve mi_mappedblocks: mem.
@@ -2987,6 +3017,18 @@ Proof.
eapply valid_access_inject; eauto.
Qed.
+Theorem weak_valid_pointer_inject:
+ forall f m1 m2 b1 ofs b2 delta,
+ f b1 = Some(b2, delta) ->
+ inject f m1 m2 ->
+ weak_valid_pointer m1 b1 ofs = true ->
+ weak_valid_pointer m2 b2 (ofs + delta) = true.
+Proof.
+ intros until 2. unfold weak_valid_pointer. rewrite !orb_true_iff.
+ replace (ofs + delta - 1) with ((ofs - 1) + delta) by omega.
+ intros []; eauto using valid_pointer_inject.
+Qed.
+
(** The following lemmas establish the absence of machine integer overflow
during address computations. *)
@@ -3006,17 +3048,19 @@ Qed.
*)
Lemma address_inject:
- forall f m1 m2 b1 ofs1 b2 delta,
+ forall f m1 m2 b1 ofs1 b2 delta p,
inject f m1 m2 ->
- perm m1 b1 (Int.unsigned ofs1) Max Nonempty ->
+ perm m1 b1 (Int.unsigned ofs1) Cur p ->
f b1 = Some (b2, delta) ->
Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta.
Proof.
- intros.
+ intros. apply (perm_implies _ _ _ _ _ Nonempty) in H0; [| constructor].
+ rewrite <-valid_pointer_nonempty_perm in H0.
+ apply valid_pointer_implies in H0.
exploit mi_representable; eauto. intros [A B].
assert (0 <= delta <= Int.max_unsigned).
generalize (Int.unsigned_range ofs1). omega.
- unfold Int.add. repeat rewrite Int.unsigned_repr; auto.
+ unfold Int.add. repeat rewrite Int.unsigned_repr; omega.
Qed.
Lemma address_inject':
@@ -3027,22 +3071,29 @@ Lemma address_inject':
Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta.
Proof.
intros. destruct H0. eapply address_inject; eauto.
- apply perm_cur_max. apply H0. generalize (size_chunk_pos chunk). omega.
+ apply H0. generalize (size_chunk_pos chunk). omega.
+Qed.
+
+Theorem weak_valid_pointer_inject_no_overflow:
+ forall f m1 m2 b ofs b' delta,
+ inject f m1 m2 ->
+ weak_valid_pointer m1 b (Int.unsigned ofs) = true ->
+ f b = Some(b', delta) ->
+ 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
+Proof.
+ intros. exploit mi_representable; eauto. intros.
+ pose proof (Int.unsigned_range ofs).
+ rewrite Int.unsigned_repr; omega.
Qed.
Theorem valid_pointer_inject_no_overflow:
- forall f m1 m2 b ofs b' x,
+ forall f m1 m2 b ofs b' delta,
inject f m1 m2 ->
valid_pointer m1 b (Int.unsigned ofs) = true ->
- f b = Some(b', x) ->
- 0 <= Int.unsigned ofs + Int.unsigned (Int.repr x) <= Int.max_unsigned.
+ f b = Some(b', delta) ->
+ 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
Proof.
- intros. rewrite valid_pointer_valid_access in H0.
- assert (perm m1 b (Int.unsigned ofs) Cur Nonempty).
- apply H0. simpl. omega.
- exploit mi_representable; eauto. intros [A B].
- rewrite Int.unsigned_repr; auto.
- generalize (Int.unsigned_range ofs). omega.
+ eauto using weak_valid_pointer_inject_no_overflow, valid_pointer_implies.
Qed.
Theorem valid_pointer_inject_val:
@@ -3058,6 +3109,19 @@ Proof.
rewrite valid_pointer_valid_access in H0. eauto.
Qed.
+Theorem weak_valid_pointer_inject_val:
+ forall f m1 m2 b ofs b' ofs',
+ inject f m1 m2 ->
+ weak_valid_pointer m1 b (Int.unsigned ofs) = true ->
+ val_inject f (Vptr b ofs) (Vptr b' ofs') ->
+ weak_valid_pointer m2 b' (Int.unsigned ofs') = true.
+Proof.
+ intros. inv H1. exploit mi_representable; try eassumption. intros.
+ pose proof (Int.unsigned_range ofs).
+ exploit weak_valid_pointer_inject; eauto.
+ unfold Int.add. repeat rewrite Int.unsigned_repr; auto; omega.
+Qed.
+
Theorem inject_no_overlap:
forall f m1 m2 b1 b2 b1' b2' delta1 delta2 ofs1 ofs2,
inject f m1 m2 ->
@@ -3213,7 +3277,10 @@ Proof.
(* no overlap *)
red; intros. eauto with mem.
(* representable *)
- eauto with mem.
+ intros. eapply mi_representable; try eassumption.
+ rewrite weak_valid_pointer_spec in *.
+ rewrite !valid_pointer_nonempty_perm in H4 |- *.
+ destruct H4; eauto with mem.
Qed.
Theorem store_unmapped_inject:
@@ -3234,7 +3301,10 @@ Proof.
(* no overlap *)
red; intros. eauto with mem.
(* representable *)
- eauto with mem.
+ intros. eapply mi_representable; try eassumption.
+ rewrite weak_valid_pointer_spec in *.
+ rewrite !valid_pointer_nonempty_perm in H3 |- *.
+ destruct H3; eauto with mem.
Qed.
Theorem store_outside_inject:
@@ -3299,7 +3369,10 @@ Proof.
(* no overlap *)
red; intros. eapply mi_no_overlap0; eauto; eapply perm_storebytes_2; eauto.
(* representable *)
- intros. eapply mi_representable0; eauto. eapply perm_storebytes_2; eauto.
+ intros. eapply mi_representable0; eauto.
+ rewrite weak_valid_pointer_spec in *.
+ rewrite !valid_pointer_nonempty_perm in H4 |- *.
+ destruct H4; eauto using perm_storebytes_2.
Qed.
Theorem storebytes_unmapped_inject:
@@ -3320,7 +3393,10 @@ Proof.
(* no overlap *)
red; intros. eapply mi_no_overlap0; eauto; eapply perm_storebytes_2; eauto.
(* representable *)
- intros. eapply mi_representable0; eauto. eapply perm_storebytes_2; eauto.
+ intros. eapply mi_representable0; eauto.
+ rewrite weak_valid_pointer_spec in *.
+ rewrite !valid_pointer_nonempty_perm in H3 |- *.
+ destruct H3; eauto using perm_storebytes_2.
Qed.
Theorem storebytes_outside_inject:
@@ -3406,8 +3482,11 @@ Proof.
exploit perm_alloc_inv. eauto. eexact H7. rewrite zeq_false; auto.
(* representable *)
unfold f'; intros.
- exploit perm_alloc_inv; eauto.
- destruct (zeq b b1). congruence. eauto with mem.
+ destruct (zeq b b1); try discriminate.
+ eapply mi_representable0; try eassumption.
+ rewrite weak_valid_pointer_spec in *.
+ rewrite !valid_pointer_nonempty_perm in H4 |- *.
+ destruct H4; eauto using perm_alloc_4.
(* incr *)
split. auto.
(* image *)
@@ -3422,7 +3501,7 @@ Theorem alloc_left_mapped_inject:
alloc m1 lo hi = (m1', b1) ->
valid_block m2 b2 ->
0 <= delta <= Int.max_unsigned ->
- (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs <= Int.max_unsigned) ->
+ (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs < Int.max_unsigned) ->
(forall ofs k p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) k p) ->
inj_offset_aligned delta (hi-lo) ->
(forall b delta' ofs k p,
@@ -3478,11 +3557,20 @@ Proof.
eapply H6; eauto. omega.
eauto.
(* representable *)
- unfold f'; intros. exploit perm_alloc_inv; eauto. destruct (zeq b b1); intros.
- inversion H9; subst b' delta0. exploit H3. apply H4 with (k := k) (p := p); eauto.
- intros [A | A]. generalize (Int.unsigned_range_2 ofs). omega.
- generalize (Int.unsigned_range_2 ofs). omega.
- eauto.
+ unfold f'; intros.
+ rewrite weak_valid_pointer_spec in *.
+ rewrite !valid_pointer_nonempty_perm in H10.
+ destruct (zeq b b1).
+ subst. injection H9; intros; subst b' delta0. destruct H10.
+ exploit perm_alloc_inv; eauto; rewrite zeq_true; intro.
+ exploit H3. apply H4 with (k := Cur) (p := Nonempty); eauto.
+ generalize (Int.unsigned_range_2 ofs). omega.
+ exploit perm_alloc_inv; eauto; rewrite zeq_true; intro.
+ exploit H3. apply H4 with (k := Cur) (p := Nonempty); eauto.
+ generalize (Int.unsigned_range_2 ofs). omega.
+ eapply mi_representable0; try eassumption.
+ rewrite !weak_valid_pointer_spec, !valid_pointer_nonempty_perm.
+ destruct H10; eauto using perm_alloc_4.
(* incr *)
split. auto.
(* image of b1 *)
@@ -3537,7 +3625,10 @@ Proof.
(* no overlap *)
red; intros. eauto with mem.
(* representable *)
- eauto with mem.
+ intros. eapply mi_representable0; try eassumption.
+ rewrite weak_valid_pointer_spec in *.
+ rewrite !valid_pointer_nonempty_perm in H2 |- *.
+ destruct H2; eauto with mem.
Qed.
Lemma free_list_left_inject:
@@ -3686,9 +3777,13 @@ Proof.
set (ofs' := Int.repr (Int.unsigned ofs + delta1)).
assert (Int.unsigned ofs' = Int.unsigned ofs + delta1).
unfold ofs'; apply Int.unsigned_repr. auto.
- exploit mi_representable1. eauto. instantiate (3 := ofs').
- rewrite H. eapply perm_inj; eauto. rewrite H. intros [C D].
- omega.
+ exploit mi_representable1. eauto. instantiate (1 := ofs').
+ rewrite H.
+ rewrite weak_valid_pointer_spec, !valid_pointer_nonempty_perm in *.
+ replace (Int.unsigned ofs + delta1 - 1) with
+ ((Int.unsigned ofs - 1) + delta1) by omega.
+ destruct H0; eauto using perm_inj.
+ rewrite H. omega.
Qed.
Lemma val_lessdef_inject_compose:
@@ -3721,7 +3816,9 @@ Proof.
(* no overlap *)
red; intros. eapply mi_no_overlap0; eauto; eapply perm_extends; eauto.
(* representable *)
- eapply mi_representable0; eauto. eapply perm_extends; eauto.
+ eapply mi_representable0; eauto.
+ rewrite weak_valid_pointer_spec, !valid_pointer_nonempty_perm in *.
+ destruct H1; eauto using perm_extends.
Qed.
Lemma inject_extends_compose:
diff --git a/common/Memtype.v b/common/Memtype.v
index a39daf4..59dc7a3 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -259,6 +259,22 @@ Axiom valid_pointer_valid_access:
forall m b ofs,
valid_pointer m b ofs = true <-> valid_access m Mint8unsigned b ofs Nonempty.
+(** C allows pointers one past the last element of an array. These are not
+ valid according to the previously defined [valid_pointer]. The property
+ [weak_valid_pointer m b ofs] holds if address [b, ofs] is a valid pointer
+ in [m], or a pointer one past a valid block in [m]. *)
+
+Definition weak_valid_pointer (m: mem) (b: block) (ofs: Z) :=
+ valid_pointer m b ofs || valid_pointer m b (ofs - 1).
+
+Axiom weak_valid_pointer_spec:
+ forall m b ofs,
+ weak_valid_pointer m b ofs = true <->
+ valid_pointer m b ofs = true \/ valid_pointer m b (ofs - 1) = true.
+Axiom valid_pointer_implies:
+ forall m b ofs,
+ valid_pointer m b ofs = true -> weak_valid_pointer m b ofs = true.
+
(** * Properties of the memory operations *)
(** ** Properties of the initial memory state. *)
@@ -899,6 +915,10 @@ Axiom valid_access_extends:
Axiom valid_pointer_extends:
forall m1 m2 b ofs,
extends m1 m2 -> valid_pointer m1 b ofs = true -> valid_pointer m2 b ofs = true.
+Axiom weak_valid_pointer_extends:
+ forall m1 m2 b ofs,
+ extends m1 m2 ->
+ weak_valid_pointer m1 b ofs = true -> weak_valid_pointer m2 b ofs = true.
(** * Memory injections *)
@@ -950,19 +970,33 @@ Axiom valid_pointer_inject:
valid_pointer m1 b1 ofs = true ->
valid_pointer m2 b2 (ofs + delta) = true.
+Axiom weak_valid_pointer_inject:
+ forall f m1 m2 b1 ofs b2 delta,
+ f b1 = Some(b2, delta) ->
+ inject f m1 m2 ->
+ weak_valid_pointer m1 b1 ofs = true ->
+ weak_valid_pointer m2 b2 (ofs + delta) = true.
+
Axiom address_inject:
- forall f m1 m2 b1 ofs1 b2 delta,
+ forall f m1 m2 b1 ofs1 b2 delta p,
inject f m1 m2 ->
- perm m1 b1 (Int.unsigned ofs1) Max Nonempty ->
+ perm m1 b1 (Int.unsigned ofs1) Cur p ->
f b1 = Some (b2, delta) ->
Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta.
Axiom valid_pointer_inject_no_overflow:
- forall f m1 m2 b ofs b' x,
+ forall f m1 m2 b ofs b' delta,
inject f m1 m2 ->
valid_pointer m1 b (Int.unsigned ofs) = true ->
- f b = Some(b', x) ->
- 0 <= Int.unsigned ofs + Int.unsigned (Int.repr x) <= Int.max_unsigned.
+ f b = Some(b', delta) ->
+ 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
+
+Axiom weak_valid_pointer_inject_no_overflow:
+ forall f m1 m2 b ofs b' delta,
+ inject f m1 m2 ->
+ weak_valid_pointer m1 b (Int.unsigned ofs) = true ->
+ f b = Some(b', delta) ->
+ 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
Axiom valid_pointer_inject_val:
forall f m1 m2 b ofs b' ofs',
@@ -971,6 +1005,13 @@ Axiom valid_pointer_inject_val:
val_inject f (Vptr b ofs) (Vptr b' ofs') ->
valid_pointer m2 b' (Int.unsigned ofs') = true.
+Axiom weak_valid_pointer_inject_val:
+ forall f m1 m2 b ofs b' ofs',
+ inject f m1 m2 ->
+ weak_valid_pointer m1 b (Int.unsigned ofs) = true ->
+ val_inject f (Vptr b ofs) (Vptr b' ofs') ->
+ weak_valid_pointer m2 b' (Int.unsigned ofs') = true.
+
Axiom inject_no_overlap:
forall f m1 m2 b1 b2 b1' b2' delta1 delta2 ofs1 ofs2,
inject f m1 m2 ->
@@ -1103,7 +1144,7 @@ Axiom alloc_left_mapped_inject:
alloc m1 lo hi = (m1', b1) ->
valid_block m2 b2 ->
0 <= delta <= Int.max_unsigned ->
- (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs <= Int.max_unsigned) ->
+ (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs < Int.max_unsigned) ->
(forall ofs k p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) k p) ->
inj_offset_aligned delta (hi-lo) ->
(forall b delta' ofs k p,
diff --git a/common/Values.v b/common/Values.v
index f02fa70..f629628 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -349,6 +349,7 @@ Definition divf (v1 v2: val): val :=
Section COMPARISONS.
Variable valid_ptr: block -> Z -> bool.
+Let weak_valid_ptr (b: block) (ofs: Z) := valid_ptr b ofs || valid_ptr b (ofs - 1).
Definition cmp_bool (c: comparison) (v1 v2: val): option bool :=
match v1, v2 with
@@ -370,11 +371,16 @@ Definition cmpu_bool (c: comparison) (v1 v2: val): option bool :=
| Vint n1, Vptr b2 ofs2 =>
if Int.eq n1 Int.zero then cmp_different_blocks c else None
| Vptr b1 ofs1, Vptr b2 ofs2 =>
- if valid_ptr b1 (Int.unsigned ofs1) && valid_ptr b2 (Int.unsigned ofs2) then
- if zeq b1 b2
+ if zeq b1 b2 then
+ if weak_valid_ptr b1 (Int.unsigned ofs1)
+ && weak_valid_ptr b2 (Int.unsigned ofs2)
then Some (Int.cmpu c ofs1 ofs2)
- else cmp_different_blocks c
- else None
+ else None
+ else
+ if valid_ptr b1 (Int.unsigned ofs1)
+ && valid_ptr b2 (Int.unsigned ofs2)
+ 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
| _, _ => None
@@ -802,8 +808,12 @@ Proof.
rewrite Int.negate_cmpu. auto.
destruct (Int.eq i Int.zero); auto.
destruct (Int.eq i0 Int.zero); auto.
+ destruct (zeq 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))).
+ rewrite Int.negate_cmpu. auto.
+ auto.
destruct (valid_ptr b (Int.unsigned i) && valid_ptr b0 (Int.unsigned i0)); auto.
- destruct (zeq b b0); auto. rewrite Int.negate_cmpu. auto.
Qed.
Lemma not_of_optbool:
@@ -821,7 +831,8 @@ Qed.
Theorem negate_cmpu:
forall valid_ptr c x y,
- cmpu valid_ptr (negate_comparison c) x y = notbool (cmpu valid_ptr c x y).
+ cmpu valid_ptr (negate_comparison c) x y =
+ notbool (cmpu valid_ptr c x y).
Proof.
intros. unfold cmpu. rewrite negate_cmpu_bool. apply not_of_optbool.
Qed.
@@ -835,7 +846,8 @@ Qed.
Theorem swap_cmpu_bool:
forall valid_ptr c x y,
- cmpu_bool valid_ptr (swap_comparison c) x y = cmpu_bool valid_ptr c y x.
+ cmpu_bool valid_ptr (swap_comparison c) x y =
+ cmpu_bool valid_ptr c y x.
Proof.
assert (forall c, cmp_different_blocks (swap_comparison c) = cmp_different_blocks c).
destruct c; auto.
@@ -843,10 +855,15 @@ Proof.
rewrite Int.swap_cmpu. auto.
case (Int.eq i Int.zero); auto.
case (Int.eq i0 Int.zero); auto.
- destruct (valid_ptr b (Int.unsigned i)); destruct (valid_ptr b0 (Int.unsigned i0)); auto.
- simpl. destruct (zeq b b0); subst.
- rewrite zeq_true. rewrite Int.swap_cmpu. auto.
- rewrite zeq_false; auto.
+ destruct (zeq b b0); subst.
+ rewrite zeq_true.
+ destruct (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1));
+ destruct (valid_ptr b0 (Int.unsigned i0) || valid_ptr b0 (Int.unsigned i0 - 1));
+ simpl; auto.
+ rewrite Int.swap_cmpu. auto.
+ rewrite zeq_false by auto.
+ destruct (valid_ptr b (Int.unsigned i));
+ destruct (valid_ptr b0 (Int.unsigned i0)); simpl; auto.
Qed.
Theorem negate_cmpf_eq:
@@ -904,25 +921,29 @@ Proof.
Qed.
Theorem cmpu_ne_0_optbool:
- forall valid_ptr ob, cmpu valid_ptr Cne (of_optbool ob) (Vint Int.zero) = of_optbool ob.
+ 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.
+ 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).
+ 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).
+ 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.
@@ -1030,9 +1051,16 @@ Proof.
destruct v1; simpl in H2; try discriminate;
destruct v2; simpl in H2; try discriminate;
inv H0; inv H1; simpl; auto.
+ destruct (zeq 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.
destruct (valid_ptr b0 (Int.unsigned i)) eqn:?; try discriminate.
destruct (valid_ptr b1 (Int.unsigned i0)) eqn:?; try discriminate.
- rewrite (H _ _ Heqb2). rewrite (H _ _ Heqb0). auto.
+ erewrite !H by eauto. auto.
Qed.
Lemma of_optbool_lessdef:
@@ -1087,14 +1115,118 @@ Inductive val_list_inject (mi: meminj): list val -> list val-> Prop:=
Hint Resolve val_nil_inject val_cons_inject.
+Section VAL_INJ_OPS.
+
+Variable f: meminj.
+
Lemma val_load_result_inject:
- forall f chunk v1 v2,
+ forall chunk v1 v2,
val_inject f v1 v2 ->
val_inject f (Val.load_result chunk v1) (Val.load_result chunk v2).
Proof.
intros. inv H; destruct chunk; simpl; econstructor; eauto.
Qed.
+Remark val_add_inject:
+ forall v1 v1' v2 v2',
+ val_inject f v1 v1' ->
+ val_inject f v2 v2' ->
+ val_inject f (Val.add v1 v2) (Val.add v1' v2').
+Proof.
+ intros. inv H; inv H0; simpl; econstructor; eauto.
+ repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+ repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+Qed.
+
+Remark val_sub_inject:
+ forall v1 v1' v2 v2',
+ val_inject f v1 v1' ->
+ val_inject f v2 v2' ->
+ val_inject f (Val.sub v1 v2) (Val.sub v1' v2').
+Proof.
+ intros. inv H; inv H0; simpl; auto.
+ econstructor; eauto. rewrite Int.sub_add_l. auto.
+ destruct (zeq b1 b0); auto. subst. rewrite H1 in H. inv H. rewrite zeq_true.
+ rewrite Int.sub_shifted. auto.
+Qed.
+
+Lemma val_cmp_bool_inject:
+ forall c v1 v2 v1' v2' b,
+ val_inject f v1 v1' ->
+ val_inject f v2 v2' ->
+ Val.cmp_bool c v1 v2 = Some b ->
+ Val.cmp_bool c v1' v2' = Some b.
+Proof.
+ intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto.
+Qed.
+
+Variable (valid_ptr1 valid_ptr2 : block -> Z -> bool).
+
+Let weak_valid_ptr1 b ofs := valid_ptr1 b ofs || valid_ptr1 b (ofs - 1).
+Let weak_valid_ptr2 b ofs := valid_ptr2 b ofs || valid_ptr2 b (ofs - 1).
+
+Hypothesis valid_ptr_inj:
+ forall b1 ofs b2 delta,
+ f b1 = Some(b2, delta) ->
+ valid_ptr1 b1 (Int.unsigned ofs) = true ->
+ valid_ptr2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+
+Hypothesis weak_valid_ptr_inj:
+ forall b1 ofs b2 delta,
+ f b1 = Some(b2, delta) ->
+ weak_valid_ptr1 b1 (Int.unsigned ofs) = true ->
+ weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+
+Hypothesis weak_valid_ptr_no_overflow:
+ forall b1 ofs b2 delta,
+ f b1 = Some(b2, delta) ->
+ weak_valid_ptr1 b1 (Int.unsigned ofs) = true ->
+ 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
+
+Hypothesis valid_different_ptrs_inj:
+ forall b1 ofs1 b2 ofs2 b1' delta1 b2' delta2,
+ b1 <> b2 ->
+ valid_ptr1 b1 (Int.unsigned ofs1) = true ->
+ valid_ptr1 b2 (Int.unsigned ofs2) = true ->
+ f b1 = Some (b1', delta1) ->
+ f b2 = Some (b2', delta2) ->
+ b1' <> b2' \/
+ Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> Int.unsigned (Int.add ofs2 (Int.repr delta2)).
+
+Lemma val_cmpu_bool_inject:
+ forall c v1 v2 v1' v2' b,
+ val_inject f v1 v1' ->
+ val_inject f v2 v2' ->
+ Val.cmpu_bool valid_ptr1 c v1 v2 = Some b ->
+ Val.cmpu_bool valid_ptr2 c v1' v2' = Some b.
+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 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)))).
+ destruct (zeq b1 b0); subst.
+ rewrite H in H2. inv H2. rewrite zeq_true.
+ destruct (weak_valid_ptr1 b0 (Int.unsigned ofs1)) eqn:?; try discriminate.
+ destruct (weak_valid_ptr1 b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
+ erewrite !weak_valid_ptr_inj by eauto. simpl.
+ rewrite <-H1. simpl. decEq. apply Int.translate_cmpu; eauto.
+ destruct (valid_ptr1 b1 (Int.unsigned ofs1)) eqn:?; try discriminate.
+ destruct (valid_ptr1 b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
+ destruct (zeq b2 b3); subst.
+ assert (valid_ptr_implies: forall b ofs, valid_ptr1 b ofs = true -> weak_valid_ptr1 b ofs = true).
+ intros. unfold weak_valid_ptr1. rewrite H0; auto.
+ erewrite !weak_valid_ptr_inj by eauto using valid_ptr_implies. simpl.
+ exploit valid_different_ptrs_inj; eauto. intros [?|?]; [congruence |].
+ destruct c; simpl in H1; inv H1.
+ simpl; decEq. rewrite Int.eq_false; auto. congruence.
+ simpl; decEq. rewrite Int.eq_false; auto. congruence.
+ now erewrite !valid_ptr_inj by eauto.
+Qed.
+
+End VAL_INJ_OPS.
+
(** Monotone evolution of a memory injection. *)
Definition inject_incr (f1 f2: meminj) : Prop :=
@@ -1185,4 +1317,3 @@ Proof.
unfold compose_meminj; rewrite H1; rewrite H3; eauto.
rewrite Int.add_assoc. decEq. unfold Int.add. apply Int.eqm_samerepr. auto with ints.
Qed.
-
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index 7a4348b..b524539 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -1110,10 +1110,11 @@ Proof.
rewrite Heqb1; reflexivity.
(* ptr ptr *)
simpl.
- destruct (Mem.valid_pointer m b0 (Int.unsigned i) &&
- Mem.valid_pointer m b1 (Int.unsigned i0)); try discriminate.
+ fold (Mem.weak_valid_pointer m b0 (Int.unsigned i)) in *.
+ fold (Mem.weak_valid_pointer m b1 (Int.unsigned i0)) in *.
destruct (zeq b0 b1).
- inversion H1.
+ destruct (Mem.weak_valid_pointer m b0 (Int.unsigned i) &&
+ Mem.weak_valid_pointer m b1 (Int.unsigned i0)); inversion H1.
destruct c; simpl; auto.
destruct (Int.eq i i0); reflexivity.
destruct (Int.eq i i0); auto.
@@ -1121,6 +1122,8 @@ Proof.
rewrite int_not_ltu. destruct (Int.ltu i i0); simpl; destruct (Int.eq i i0); auto.
rewrite (int_ltu_not i i0). destruct (Int.ltu i i0); destruct (Int.eq i i0); reflexivity.
destruct (Int.ltu i i0); reflexivity.
+ destruct (Mem.valid_pointer m b0 (Int.unsigned i) &&
+ Mem.valid_pointer m b1 (Int.unsigned i0)); try discriminate.
destruct c; simpl in *; inv H1; reflexivity.
Qed.
diff --git a/ia32/Op.v b/ia32/Op.v
index 93a867a..66ee633 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -722,10 +722,16 @@ Hypothesis valid_pointer_inj:
Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
-Hypothesis valid_pointer_no_overflow:
+Hypothesis weak_valid_pointer_inj:
forall b1 ofs b2 delta,
f b1 = Some(b2, delta) ->
- Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+ Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+ Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+
+Hypothesis weak_valid_pointer_no_overflow:
+ forall b1 ofs b2 delta,
+ f b1 = Some(b2, delta) ->
+ Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
Hypothesis valid_different_pointers_inj:
@@ -753,50 +759,17 @@ Ltac InvInject :=
| _ => idtac
end.
-Remark val_add_inj:
- forall v1 v1' v2 v2',
- val_inject f v1 v1' -> val_inject f v2 v2' -> val_inject f (Val.add v1 v2) (Val.add v1' v2').
-Proof.
- intros. inv H; inv H0; simpl; econstructor; eauto.
- repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
- repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-Qed.
-
Lemma eval_condition_inj:
forall cond vl1 vl2 b,
val_list_inject f vl1 vl2 ->
eval_condition cond vl1 m1 = Some b ->
eval_condition cond vl2 m2 = Some b.
Proof.
-Opaque Int.add.
- assert (CMPU:
- forall c v1 v2 v1' v2' b,
- val_inject f v1 v1' ->
- val_inject f v2 v2' ->
- Val.cmpu_bool (Mem.valid_pointer m1) c v1 v2 = Some b ->
- Val.cmpu_bool (Mem.valid_pointer m2) c v1' v2' = Some b).
- intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto.
- destruct (Mem.valid_pointer m1 b1 (Int.unsigned ofs1)) eqn:?; try discriminate.
- destruct (Mem.valid_pointer m1 b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
- rewrite (valid_pointer_inj _ H2 Heqb4).
- rewrite (valid_pointer_inj _ H Heqb0). simpl.
- destruct (zeq b1 b0); simpl in H1.
- inv H1. rewrite H in H2; inv H2. rewrite zeq_true.
- decEq. apply Int.translate_cmpu.
- eapply valid_pointer_no_overflow; eauto.
- eapply valid_pointer_no_overflow; eauto.
- exploit valid_different_pointers_inj; eauto. intros P.
- destruct (zeq b2 b3); auto.
- destruct P. congruence.
- destruct c; simpl in H1; inv H1.
- simpl; decEq. rewrite Int.eq_false; auto. congruence.
- simpl; decEq. rewrite Int.eq_false; auto. congruence.
-
intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto.
inv H3; inv H2; simpl in H0; inv H0; auto.
- eauto.
+ eauto 3 using val_cmpu_bool_inject, Mem.valid_pointer_implies.
inv H3; simpl in H0; inv H0; auto.
- eauto.
+ eauto 3 using val_cmpu_bool_inject, Mem.valid_pointer_implies.
inv H3; inv H2; simpl in H0; inv H0; auto.
inv H3; inv H2; simpl in H0; inv H0; auto.
Qed.
@@ -816,13 +789,13 @@ Lemma eval_addressing_inj:
exists v2, eval_addressing genv sp2 addr vl2 = Some v2 /\ val_inject f v1 v2.
Proof.
intros. destruct addr; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
- apply val_add_inj; auto.
- apply val_add_inj; auto. apply val_add_inj; auto.
- apply val_add_inj; auto. inv H4; simpl; auto.
- apply val_add_inj; auto. apply val_add_inj; auto. inv H2; simpl; auto.
- apply val_add_inj; auto.
- apply val_add_inj; auto. inv H4; simpl; auto.
- apply val_add_inj; auto.
+ apply Values.val_add_inject; auto.
+ apply Values.val_add_inject; auto. apply Values.val_add_inject; auto.
+ apply Values.val_add_inject; auto. inv H4; simpl; auto.
+ apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. inv H2; simpl; auto.
+ apply Values.val_add_inject; auto.
+ apply Values.val_add_inject; auto. inv H4; simpl; auto.
+ apply Values.val_add_inject; auto.
Qed.
Lemma eval_operation_inj:
@@ -903,10 +876,20 @@ Proof.
intros. inv H0. rewrite Int.add_zero. eapply Mem.valid_pointer_extends; eauto.
Qed.
-Remark valid_pointer_no_overflow_extends:
+Remark weak_valid_pointer_extends:
+ forall m1 m2, Mem.extends m1 m2 ->
+ forall b1 ofs b2 delta,
+ Some(b1, 0) = Some(b2, delta) ->
+ Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+ Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+Proof.
+ intros. inv H0. rewrite Int.add_zero. eapply Mem.weak_valid_pointer_extends; eauto.
+Qed.
+
+Remark weak_valid_pointer_no_overflow_extends:
forall m1 b1 ofs b2 delta,
Some(b1, 0) = Some(b2, delta) ->
- Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+ Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
Proof.
intros. inv H. rewrite Zplus_0_r. apply Int.unsigned_range_2.
@@ -934,7 +917,8 @@ Lemma eval_condition_lessdef:
Proof.
intros. eapply eval_condition_inj with (f := fun b => Some(b, 0)) (m1 := m1).
apply valid_pointer_extends; auto.
- apply valid_pointer_no_overflow_extends; auto.
+ apply weak_valid_pointer_extends; auto.
+ apply weak_valid_pointer_no_overflow_extends.
apply valid_different_pointers_extends; auto.
rewrite <- val_list_inject_lessdef. eauto. auto.
Qed.
@@ -953,7 +937,8 @@ Proof.
eapply eval_operation_inj with (m1 := m1) (sp1 := sp).
intros. rewrite <- val_inject_lessdef; auto.
apply valid_pointer_extends; auto.
- apply valid_pointer_no_overflow_extends; auto.
+ apply weak_valid_pointer_extends; auto.
+ apply weak_valid_pointer_no_overflow_extends.
apply valid_different_pointers_extends; auto.
rewrite <- val_inject_lessdef; auto.
eauto. auto.
@@ -1009,7 +994,8 @@ Lemma eval_condition_inject:
Proof.
intros. eapply eval_condition_inj with (f := f) (m1 := m1); eauto.
intros; eapply Mem.valid_pointer_inject_val; eauto.
- intros; eapply Mem.valid_pointer_inject_no_overflow; eauto.
+ intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
+ intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
intros; eapply Mem.different_pointers_inject; eauto.
Qed.
@@ -1041,9 +1027,9 @@ Proof.
eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto.
exact symbol_address_inject.
intros; eapply Mem.valid_pointer_inject_val; eauto.
- intros; eapply Mem.valid_pointer_inject_no_overflow; eauto.
+ intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
+ intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
intros; eapply Mem.different_pointers_inject; eauto.
Qed.
End EVAL_INJECT.
-
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 4a1fb62..a8936fe 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -652,10 +652,16 @@ Hypothesis valid_pointer_inj:
Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
-Hypothesis valid_pointer_no_overflow:
+Hypothesis weak_valid_pointer_inj:
forall b1 ofs b2 delta,
f b1 = Some(b2, delta) ->
- Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+ Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+ Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+
+Hypothesis weak_valid_pointer_no_overflow:
+ forall b1 ofs b2 delta,
+ f b1 = Some(b2, delta) ->
+ Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
Hypothesis valid_different_pointers_inj:
@@ -683,50 +689,17 @@ Ltac InvInject :=
| _ => idtac
end.
-Remark val_add_inj:
- forall v1 v1' v2 v2',
- val_inject f v1 v1' -> val_inject f v2 v2' -> val_inject f (Val.add v1 v2) (Val.add v1' v2').
-Proof.
- intros. inv H; inv H0; simpl; econstructor; eauto.
- repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
- repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-Qed.
-
Lemma eval_condition_inj:
forall cond vl1 vl2 b,
val_list_inject f vl1 vl2 ->
eval_condition cond vl1 m1 = Some b ->
eval_condition cond vl2 m2 = Some b.
Proof.
-Opaque Int.add.
- assert (CMPU:
- forall c v1 v2 v1' v2' b,
- val_inject f v1 v1' ->
- val_inject f v2 v2' ->
- Val.cmpu_bool (Mem.valid_pointer m1) c v1 v2 = Some b ->
- Val.cmpu_bool (Mem.valid_pointer m2) c v1' v2' = Some b).
- intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto.
- destruct (Mem.valid_pointer m1 b1 (Int.unsigned ofs1)) eqn:?; try discriminate.
- destruct (Mem.valid_pointer m1 b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
- rewrite (valid_pointer_inj _ H2 Heqb4).
- rewrite (valid_pointer_inj _ H Heqb0). simpl.
- destruct (zeq b1 b0); simpl in H1.
- inv H1. rewrite H in H2; inv H2. rewrite zeq_true.
- decEq. apply Int.translate_cmpu.
- eapply valid_pointer_no_overflow; eauto.
- eapply valid_pointer_no_overflow; eauto.
- exploit valid_different_pointers_inj; eauto. intros P.
- destruct (zeq b2 b3); auto.
- destruct P. congruence.
- destruct c; simpl in H1; inv H1.
- simpl; decEq. rewrite Int.eq_false; auto. congruence.
- simpl; decEq. rewrite Int.eq_false; auto. congruence.
-
intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto.
inv H3; inv H2; simpl in H0; inv H0; auto.
- eauto.
+ eauto 3 using val_cmpu_bool_inject, Mem.valid_pointer_implies.
inv H3; simpl in H0; inv H0; auto.
- eauto.
+ eauto 3 using val_cmpu_bool_inject, Mem.valid_pointer_implies.
inv H3; inv H2; simpl in H0; inv H0; auto.
inv H3; inv H2; simpl in H0; inv H0; auto.
Qed.
@@ -749,8 +722,8 @@ Proof.
inv H; simpl; econstructor; eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
inv H4; simpl; auto.
inv H4; simpl; auto.
- apply val_add_inj; auto.
- apply val_add_inj; auto.
+ apply Values.val_add_inject; auto.
+ apply Values.val_add_inject; auto.
inv H4; inv H2; simpl; auto. econstructor; eauto.
rewrite Int.sub_add_l. auto.
destruct (zeq b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite zeq_true.
@@ -805,11 +778,8 @@ Lemma eval_addressing_inj:
eval_addressing genv sp1 addr vl1 = Some v1 ->
exists v2, eval_addressing genv sp2 addr vl2 = Some v2 /\ val_inject f v1 v2.
Proof.
- intros. destruct addr; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
- apply val_add_inj; auto.
- apply val_add_inj; auto.
- apply val_add_inj; auto.
- apply val_add_inj; auto.
+ intros. destruct addr; simpl in H1; simpl; FuncInv; InvInject; TrivialExists;
+ auto using Values.val_add_inject.
Qed.
End EVAL_COMPAT.
@@ -831,10 +801,20 @@ Proof.
intros. inv H0. rewrite Int.add_zero. eapply Mem.valid_pointer_extends; eauto.
Qed.
-Remark valid_pointer_no_overflow_extends:
+Remark weak_valid_pointer_extends:
+ forall m1 m2, Mem.extends m1 m2 ->
+ forall b1 ofs b2 delta,
+ Some(b1, 0) = Some(b2, delta) ->
+ Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+ Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+Proof.
+ intros. inv H0. rewrite Int.add_zero. eapply Mem.weak_valid_pointer_extends; eauto.
+Qed.
+
+Remark weak_valid_pointer_no_overflow_extends:
forall m1 b1 ofs b2 delta,
Some(b1, 0) = Some(b2, delta) ->
- Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+ Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
Proof.
intros. inv H. rewrite Zplus_0_r. apply Int.unsigned_range_2.
@@ -862,7 +842,8 @@ Lemma eval_condition_lessdef:
Proof.
intros. eapply eval_condition_inj with (f := fun b => Some(b, 0)) (m1 := m1).
apply valid_pointer_extends; auto.
- apply valid_pointer_no_overflow_extends; auto.
+ apply weak_valid_pointer_extends; auto.
+ apply weak_valid_pointer_no_overflow_extends; auto.
apply valid_different_pointers_extends; auto.
rewrite <- val_list_inject_lessdef. eauto. auto.
Qed.
@@ -881,7 +862,8 @@ Proof.
eapply eval_operation_inj with (m1 := m1) (sp1 := sp).
intros. rewrite <- val_inject_lessdef; auto.
apply valid_pointer_extends; auto.
- apply valid_pointer_no_overflow_extends; auto.
+ apply weak_valid_pointer_extends; auto.
+ apply weak_valid_pointer_no_overflow_extends; auto.
apply valid_different_pointers_extends; auto.
rewrite <- val_inject_lessdef; auto.
eauto. auto.
@@ -937,7 +919,8 @@ Lemma eval_condition_inject:
Proof.
intros. eapply eval_condition_inj with (f := f) (m1 := m1); eauto.
intros; eapply Mem.valid_pointer_inject_val; eauto.
- intros; eapply Mem.valid_pointer_inject_no_overflow; eauto.
+ intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
+ intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
intros; eapply Mem.different_pointers_inject; eauto.
Qed.
@@ -969,7 +952,8 @@ Proof.
eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto.
exact symbol_address_inject.
intros; eapply Mem.valid_pointer_inject_val; eauto.
- intros; eapply Mem.valid_pointer_inject_no_overflow; eauto.
+ intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
+ intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
intros; eapply Mem.different_pointers_inject; eauto.
Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 21:05:23 +0000