From 39528cfffaa5fd3a7e8d20874364141c694b99a7 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 30 Jun 2014 07:07:41 +0000 Subject: 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 --- common/Globalenvs.v | 120 ++++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 106 insertions(+), 14 deletions(-) (limited to 'common') 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). -- cgit v1.2.3