summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-06-30 07:07:41 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-06-30 07:07:41 +0000
commit39528cfffaa5fd3a7e8d20874364141c694b99a7 (patch)
tree400ab6b7837cb0294d5906be5ee7a719c6d30b87
parent0827ef4107548ada564d179ed9f02a87f0a14c46 (diff)
Add "read_as_zero" property for memory areas initialized by Init_space.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2519 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r--common/Globalenvs.v120
1 files changed, 106 insertions, 14 deletions
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index 3b077e0..bd38fa3 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -723,7 +723,7 @@ Qed.
(** Data preservation properties *)
-Remark store_zeros_outside:
+Remark store_zeros_load_outside:
forall m b p n m',
store_zeros m b p n = Some m' ->
forall chunk b' p',
@@ -738,6 +738,85 @@ Proof.
discriminate.
Qed.
+Remark store_zeros_loadbytes_outside:
+ forall m b p n m',
+ store_zeros m b p n = Some m' ->
+ forall b' p' n',
+ b' <> b \/ p' + n' <= p \/ p + n <= p' ->
+ Mem.loadbytes m' b' p' n' = Mem.loadbytes m b' p' n'.
+Proof.
+ intros until n. functional induction (store_zeros m b p n); intros.
+ inv H; auto.
+ transitivity (Mem.loadbytes m' b' p' n').
+ apply IHo. auto. intuition omega.
+ eapply Mem.loadbytes_store_other; eauto. simpl. intuition omega.
+ discriminate.
+Qed.
+
+Definition read_as_zero (m: mem) (b: block) (ofs len: Z) : Prop :=
+ forall chunk p,
+ ofs <= p -> p + size_chunk chunk <= ofs + len ->
+ (align_chunk chunk | p) ->
+ Mem.load chunk m b p =
+ Some (match chunk with
+ | Mint8unsigned | Mint8signed | Mint16unsigned | Mint16signed | Mint32 => Vint Int.zero
+ | Mint64 => Vlong Int64.zero
+ | Mfloat32 | Mfloat64 => Vfloat Float.zero
+ end).
+
+Remark store_zeros_loadbytes:
+ forall m b p n m',
+ store_zeros m b p n = Some m' ->
+ forall p' n',
+ p <= p' -> p' + Z.of_nat n' <= p + n ->
+ Mem.loadbytes m' b p' (Z.of_nat n') = Some (list_repeat n' (Byte Byte.zero)).
+Proof.
+ intros until n; functional induction (store_zeros m b p n); intros.
+- destruct n'. simpl. apply Mem.loadbytes_empty. omega.
+ rewrite inj_S in H1. omegaContradiction.
+- destruct (zeq p' p).
+ + subst p'. destruct n'. simpl. apply Mem.loadbytes_empty. omega.
+ rewrite inj_S in H1. rewrite inj_S.
+ replace (Z.succ (Z.of_nat n')) with (1 + Z.of_nat n') by omega.
+ change (list_repeat (S n') (Byte Byte.zero))
+ with ((Byte Byte.zero :: nil) ++ list_repeat n' (Byte Byte.zero)).
+ apply Mem.loadbytes_concat.
+ erewrite store_zeros_loadbytes_outside; eauto.
+ change (Byte Byte.zero :: nil) with (encode_val Mint8unsigned Vzero).
+ change 1 with (size_chunk Mint8unsigned).
+ eapply Mem.loadbytes_store_same; eauto.
+ right; omega.
+ eapply IHo; eauto. omega. omega. omega. omega.
+ + eapply IHo; eauto. omega. omega.
+- discriminate.
+Qed.
+
+Lemma store_zeros_read_as_zero:
+ forall m b p n m',
+ store_zeros m b p n = Some m' ->
+ read_as_zero m' b p n.
+Proof.
+ intros; red; intros.
+ transitivity (Some(decode_val chunk (list_repeat (size_chunk_nat chunk) (Byte Byte.zero)))).
+ apply Mem.loadbytes_load; auto. rewrite size_chunk_conv.
+ eapply store_zeros_loadbytes; eauto. rewrite <- size_chunk_conv; auto.
+ f_equal. destruct chunk; reflexivity.
+Qed.
+
+Remark store_init_data_outside:
+ forall b i m p m',
+ store_init_data m b p i = Some m' ->
+ forall chunk b' q,
+ b' <> b \/ q + size_chunk chunk <= p \/ p + init_data_size i <= q ->
+ Mem.load chunk m' b' q = Mem.load chunk m b' q.
+Proof.
+ intros. destruct i; simpl in *;
+ try (eapply Mem.load_store_other; eauto; fail).
+ inv H; auto.
+ destruct (find_symbol ge i); try congruence.
+ eapply Mem.load_store_other; eauto; intuition.
+Qed.
+
Remark store_init_data_list_outside:
forall b il m p m',
store_init_data_list m b p il = Some m' ->
@@ -750,11 +829,7 @@ Proof.
intros. destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence.
transitivity (Mem.load chunk m1 b' q).
eapply IHil; eauto. generalize (init_data_size_pos a). intuition omega.
- destruct a; simpl in Heqo;
- try (eapply Mem.load_store_other; eauto; intuition; fail).
- inv Heqo. auto.
- destruct (find_symbol ge i); try congruence.
- eapply Mem.load_store_other; eauto; intuition.
+ eapply store_init_data_outside; eauto. tauto.
Qed.
Fixpoint load_store_init_data (m: mem) (b: block) (p: Z) (il: list init_data) {struct il} : Prop :=
@@ -782,26 +857,39 @@ Fixpoint load_store_init_data (m: mem) (b: block) (p: Z) (il: list init_data) {s
(exists b', find_symbol ge symb = Some b' /\ Mem.load Mint32 m b p = Some(Vptr b' ofs))
/\ load_store_init_data m b (p + 4) il'
| Init_space n :: il' =>
- load_store_init_data m b (p + Zmax n 0) il'
+ read_as_zero m b p n
+ /\ load_store_init_data m b (p + Zmax n 0) il'
end.
+Remark init_data_list_size_pos:
+ forall il, init_data_list_size il >= 0.
+Proof.
+ induction il; simpl. omega. generalize (init_data_size_pos a); omega.
+Qed.
+
Lemma store_init_data_list_charact:
forall b il m p m',
store_init_data_list m b p il = Some m' ->
+ read_as_zero m b p (init_data_list_size il) ->
load_store_init_data m' b p il.
Proof.
assert (A: forall chunk v m b p m1 il m',
Mem.store chunk m b p v = Some m1 ->
store_init_data_list m1 b (p + size_chunk chunk) il = Some m' ->
Mem.load chunk m' b p = Some(Val.load_result chunk v)).
- intros. transitivity (Mem.load chunk m1 b p).
- eapply store_init_data_list_outside; eauto. right. omega.
- eapply Mem.load_store_same; eauto.
-
+ {
+ intros. transitivity (Mem.load chunk m1 b p).
+ eapply store_init_data_list_outside; eauto. right. omega.
+ eapply Mem.load_store_same; eauto.
+ }
induction il; simpl.
auto.
intros. destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence.
- exploit IHil; eauto. intro D.
+ exploit IHil; eauto.
+ red; intros. transitivity (Mem.load chunk m b p0).
+ eapply store_init_data_outside. eauto. auto.
+ apply H0. generalize (init_data_size_pos a); omega. omega. auto.
+ intro D.
destruct a; simpl in Heqo; intuition.
eapply (A Mint8unsigned (Vint i)); eauto.
eapply (A Mint16unsigned (Vint i)); eauto.
@@ -809,6 +897,9 @@ Proof.
eapply (A Mint64 (Vlong i)); eauto.
eapply (A Mfloat32 (Vfloat f)); eauto.
eapply (A Mfloat64 (Vfloat f)); eauto.
+ inv Heqo. red; intros. transitivity (Mem.load chunk m1 b p0).
+ eapply store_init_data_list_outside; eauto. right. simpl. xomega.
+ apply H0; auto. simpl. generalize (init_data_list_size_pos il); xomega.
destruct (find_symbol ge i); try congruence. exists b0; split; auto.
eapply (A Mint32 (Vptr b0 i0)); eauto.
Qed.
@@ -838,7 +929,7 @@ Proof.
transitivity (Mem.load chunk m2 b p).
eapply store_init_data_list_outside; eauto.
transitivity (Mem.load chunk m1 b p).
- eapply store_zeros_outside; eauto.
+ eapply store_zeros_load_outside; eauto.
eapply Mem.load_alloc_unchanged; eauto.
Qed.
@@ -866,7 +957,7 @@ Remark load_store_init_data_invariant:
Proof.
induction il; intro p; simpl.
auto.
- repeat rewrite H. destruct a; intuition.
+ repeat rewrite H. destruct a; intuition. red; intros; rewrite H; auto.
Qed.
Definition variables_initialized (g: t) (m: mem) :=
@@ -931,6 +1022,7 @@ Proof.
right; right; right. unfold perm_globvar. rewrite H3.
destruct (gvar_readonly gv); auto with mem.
eapply store_init_data_list_charact; eauto.
+ eapply store_zeros_read_as_zero; eauto.
(* older var *)
exploit H1; eauto. intros [A [B C]].
assert (D: Mem.valid_block m b).