summaryrefslogtreecommitdiff
path: root/common
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-07-28 12:51:16 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-07-28 12:51:16 +0000
commit4af1682d04244bab9f793e00eb24090153a36a0f (patch)
treea9a70d236c06a78aa9b607c6a41e09b80651aa51 /common
parentd8d1bf1aa09373f64aa1b1e6cdfb914c23a910be (diff)
Added animation of the CompCert C semantics (ccomp -interp)
test/regression: int main() so that interpretation works Revised once more implementation of __builtin_memcpy (to check for PPC & ARM) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1688 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'common')
-rw-r--r--common/Determinism.v109
-rw-r--r--common/Globalenvs.v208
2 files changed, 218 insertions, 99 deletions
diff --git a/common/Determinism.v b/common/Determinism.v
index 16e8890..29cc695 100644
--- a/common/Determinism.v
+++ b/common/Determinism.v
@@ -222,13 +222,13 @@ Qed.
Record sem_deterministic (L: semantics) := mk_deterministic {
det_step: forall s0 t1 s1 t2 s2,
- L (genv L) s0 t1 s1 -> L (genv L) s0 t2 s2 -> s1 = s2 /\ t1 = t2;
+ Step L s0 t1 s1 -> Step L s0 t2 s2 -> s1 = s2 /\ t1 = t2;
det_initial_state: forall s1 s2,
initial_state L s1 -> initial_state L s2 -> s1 = s2;
det_final_state: forall s r1 r2,
final_state L s r1 -> final_state L s r2 -> r1 = r2;
det_final_nostep: forall s r,
- final_state L s r -> nostep L (genv L) s
+ final_state L s r -> Nostep L s
}.
Section DETERM_SEM.
@@ -238,18 +238,18 @@ Hypothesis DET: sem_deterministic L.
Ltac use_step_deterministic :=
match goal with
- | [ S1: step L (genv L) _ ?t1 _, S2: step L (genv L) _ ?t2 _ |- _ ] =>
+ | [ S1: Step L _ ?t1 _, S2: Step L _ ?t2 _ |- _ ] =>
destruct (det_step L DET _ _ _ _ _ S1 S2) as [EQ1 EQ2]; subst
end.
(** Determinism for finite transition sequences. *)
Lemma star_step_diamond:
- forall s0 t1 s1, star L (genv L) s0 t1 s1 ->
- forall t2 s2, star L (genv L) s0 t2 s2 ->
+ forall s0 t1 s1, Star L s0 t1 s1 ->
+ forall t2 s2, Star L s0 t2 s2 ->
exists t,
- (star L (genv L) s1 t s2 /\ t2 = t1 ** t)
- \/ (star L (genv L) s2 t s1 /\ t1 = t2 ** t).
+ (Star L s1 t s2 /\ t2 = t1 ** t)
+ \/ (Star L s2 t s1 /\ t1 = t2 ** t).
Proof.
induction 1; intros.
exists t2; auto.
@@ -262,7 +262,7 @@ Qed.
Ltac use_star_step_diamond :=
match goal with
- | [ S1: star (step L) (genv L) _ ?t1 _, S2: star (step L) (genv L) _ ?t2 _ |- _ ] =>
+ | [ S1: Star L _ ?t1 _, S2: Star L _ ?t2 _ |- _ ] =>
let t := fresh "t" in let P := fresh "P" in let EQ := fresh "EQ" in
destruct (star_step_diamond _ _ _ S1 _ _ S2)
as [t [ [P EQ] | [P EQ] ]]; subst
@@ -270,16 +270,16 @@ Ltac use_star_step_diamond :=
Ltac use_nostep :=
match goal with
- | [ S: step L (genv L) ?s _ _, NO: nostep (step L) (genv L) ?s |- _ ] => elim (NO _ _ S)
+ | [ S: Step L ?s _ _, NO: Nostep L ?s |- _ ] => elim (NO _ _ S)
end.
Lemma star_step_triangle:
forall s0 t1 s1 t2 s2,
- star L (genv L) s0 t1 s1 ->
- star L (genv L) s0 t2 s2 ->
- nostep L (genv L) s2 ->
+ Star L s0 t1 s1 ->
+ Star L s0 t2 s2 ->
+ Nostep L s2 ->
exists t,
- star L (genv L) s1 t s2 /\ t2 = t1 ** t.
+ Star L s1 t s2 /\ t2 = t1 ** t.
Proof.
intros. use_star_step_diamond.
exists t; auto.
@@ -289,8 +289,7 @@ Qed.
Ltac use_star_step_triangle :=
match goal with
- | [ S1: star (step L) (genv L) _ ?t1 _, S2: star (step L) (genv L) _ ?t2 ?s2,
- NO: nostep (step L) (genv L) ?s2 |- _ ] =>
+ | [ S1: Star L _ ?t1 _, S2: Star L _ ?t2 ?s2, NO: Nostep L ?s2 |- _ ] =>
let t := fresh "t" in let P := fresh "P" in let EQ := fresh "EQ" in
destruct (star_step_triangle _ _ _ _ _ S1 S2 NO)
as [t [P EQ]]; subst
@@ -298,8 +297,8 @@ Ltac use_star_step_triangle :=
Lemma steps_deterministic:
forall s0 t1 s1 t2 s2,
- star L (genv L) s0 t1 s1 -> star L (genv L) s0 t2 s2 ->
- nostep L (genv L) s1 -> nostep L (genv L) s2 ->
+ Star L s0 t1 s1 -> Star L s0 t2 s2 ->
+ Nostep L s1 -> Nostep L s2 ->
t1 = t2 /\ s1 = s2.
Proof.
intros. use_star_step_triangle. inv P.
@@ -308,8 +307,8 @@ Qed.
Lemma terminates_not_goes_wrong:
forall s t1 s1 r t2 s2,
- star L (genv L) s t1 s1 -> final_state L s1 r ->
- star L (genv L) s t2 s2 -> nostep L (genv L) s2 ->
+ Star L s t1 s1 -> final_state L s1 r ->
+ Star L s t2 s2 -> Nostep L s2 ->
(forall r, ~final_state L s2 r) -> False.
Proof.
intros.
@@ -321,9 +320,9 @@ Qed.
(** Determinism for infinite transition sequences. *)
Lemma star_final_not_forever_silent:
- forall s t s', star L (genv L) s t s' ->
- nostep L (genv L) s' ->
- forever_silent L (genv L) s -> False.
+ forall s t s', Star L s t s' ->
+ Nostep L s' ->
+ Forever_silent L s -> False.
Proof.
induction 1; intros.
inv H0. use_nostep.
@@ -332,8 +331,8 @@ Qed.
Lemma star2_final_not_forever_silent:
forall s t1 s1 t2 s2,
- star L (genv L) s t1 s1 -> nostep L (genv L) s1 ->
- star L (genv L) s t2 s2 -> forever_silent L (genv L) s2 ->
+ Star L s t1 s1 -> Nostep L s1 ->
+ Star L s t2 s2 -> Forever_silent L s2 ->
False.
Proof.
intros. use_star_step_triangle.
@@ -341,8 +340,8 @@ Proof.
Qed.
Lemma star_final_not_forever_reactive:
- forall s t s', star L (genv L) s t s' ->
- forall T, nostep L (genv L) s' -> forever_reactive L (genv L) s T -> False.
+ forall s t s', Star L s t s' ->
+ forall T, Nostep L s' -> Forever_reactive L s T -> False.
Proof.
induction 1; intros.
inv H0. inv H1. congruence. use_nostep.
@@ -353,9 +352,9 @@ Proof.
Qed.
Lemma star_forever_silent_inv:
- forall s t s', star L (genv L) s t s' ->
- forever_silent L (genv L) s ->
- t = E0 /\ forever_silent L (genv L) s'.
+ forall s t s', Star L s t s' ->
+ Forever_silent L s ->
+ t = E0 /\ Forever_silent L s'.
Proof.
induction 1; intros.
auto.
@@ -364,23 +363,23 @@ Qed.
Lemma forever_silent_reactive_exclusive:
forall s T,
- forever_silent L (genv L) s -> forever_reactive L (genv L) s T -> False.
+ Forever_silent L s -> Forever_reactive L s T -> False.
Proof.
intros. inv H0. exploit star_forever_silent_inv; eauto.
intros [A B]. contradiction.
Qed.
Lemma forever_reactive_inv2:
- forall s t1 s1, star L (genv L) s t1 s1 ->
+ forall s t1 s1, Star L s t1 s1 ->
forall t2 s2 T1 T2,
- star L (genv L) s t2 s2 ->
+ Star L s t2 s2 ->
t1 <> E0 -> t2 <> E0 ->
- forever_reactive L (genv L) s1 T1 ->
- forever_reactive L (genv L) s2 T2 ->
+ Forever_reactive L s1 T1 ->
+ Forever_reactive L s2 T2 ->
exists s', exists t, exists T1', exists T2',
t <> E0 /\
- forever_reactive L (genv L) s' T1' /\
- forever_reactive L (genv L) s' T2' /\
+ Forever_reactive L s' T1' /\
+ Forever_reactive L s' T2' /\
t1 *** T1 = t *** T1' /\
t2 *** T2 = t *** T2'.
Proof.
@@ -401,8 +400,8 @@ Qed.
Lemma forever_reactive_determ':
forall s T1 T2,
- forever_reactive L (genv L) s T1 ->
- forever_reactive L (genv L) s T2 ->
+ Forever_reactive L s T1 ->
+ Forever_reactive L s T2 ->
traceinf_sim' T1 T2.
Proof.
cofix COINDHYP; intros.
@@ -415,17 +414,17 @@ Qed.
Lemma forever_reactive_determ:
forall s T1 T2,
- forever_reactive L (genv L) s T1 ->
- forever_reactive L (genv L) s T2 ->
+ Forever_reactive L s T1 ->
+ Forever_reactive L s T2 ->
traceinf_sim T1 T2.
Proof.
intros. apply traceinf_sim'_sim. eapply forever_reactive_determ'; eauto.
Qed.
Lemma star_forever_reactive_inv:
- forall s t s', star L (genv L) s t s' ->
- forall T, forever_reactive L (genv L) s T ->
- exists T', forever_reactive L (genv L) s' T' /\ T = t *** T'.
+ forall s t s', Star L s t s' ->
+ forall T, Forever_reactive L s T ->
+ exists T', Forever_reactive L s' T' /\ T = t *** T'.
Proof.
induction 1; intros.
exists T; auto.
@@ -437,8 +436,8 @@ Qed.
Lemma forever_silent_reactive_exclusive2:
forall s t s' T,
- star L (genv L) s t s' -> forever_silent L (genv L) s' ->
- forever_reactive L (genv L) s T ->
+ Star L s t s' -> Forever_silent L s' ->
+ Forever_reactive L s T ->
False.
Proof.
intros. exploit star_forever_reactive_inv; eauto.
@@ -529,28 +528,28 @@ Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
Local Open Scope pair_scope.
-Definition world_sem : semantics := @mk_semantics
+Definition world_sem : semantics := @Semantics
(state L * world)%type
(funtype L)
(vartype L)
- (fun ge s t s' => L ge s#1 t s'#1 /\ possible_trace s#2 t s'#2)
+ (fun ge s t s' => step L ge s#1 t s'#1 /\ possible_trace s#2 t s'#2)
(fun s => initial_state L s#1 /\ s#2 = initial_world)
(fun s r => final_state L s#1 r)
- (genv L).
+ (globalenv L).
(** If the original semantics is determinate, the world-aware semantics is deterministic. *)
-Hypothesis D: sem_determinate L.
+Hypothesis D: determinate L.
Theorem world_sem_deterministic: sem_deterministic world_sem.
Proof.
constructor; simpl; intros.
(* steps *)
destruct H; destruct H0.
- exploit (sd_match D). eexact H. eexact H0. intros MT.
+ exploit (sd_determ D). eexact H. eexact H0. intros [A B].
exploit match_possible_traces; eauto. intros [EQ1 EQ2]. subst t2.
- exploit (sd_determ D). eexact H. eexact H0. intros EQ3.
- split; auto. rewrite (surjective_pairing s1). rewrite (surjective_pairing s2). congruence.
+ split; auto.
+ rewrite (surjective_pairing s1). rewrite (surjective_pairing s2). intuition congruence.
(* initial states *)
destruct H; destruct H0.
rewrite (surjective_pairing s1). rewrite (surjective_pairing s2). decEq.
@@ -562,8 +561,8 @@ Proof.
red; simpl; intros. red; intros [A B]. exploit (sd_final_nostep D); eauto.
Qed.
-
-
+(*** To be updated. *)
+(***********
Variable genv: Type.
Variable state: Type.
Variable step: genv -> state -> trace -> state -> Prop.
@@ -822,6 +821,8 @@ Qed.
End INTERNAL_DET_TO_DET.
+***********)
+
End WORLD_SEM.
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index 4a57a37..a9db51e 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -33,6 +33,8 @@
place during program linking and program loading in a real operating
system. *)
+Require Recdef.
+Require Import Zwf.
Require Import Axioms.
Require Import Coqlib.
Require Import Errors.
@@ -99,6 +101,13 @@ Definition find_funct (ge: t) (v: val) : option F :=
| _ => None
end.
+(** [invert_symbol ge b] returns the name associated with the given block, if any *)
+
+Definition invert_symbol (ge: t) (b: block) : option ident :=
+ PTree.fold
+ (fun res id b' => if eq_block b b' then Some id else res)
+ ge.(genv_symb) None.
+
(** [find_var_info ge b] returns the information attached to the variable
at address [b]. *)
@@ -468,6 +477,39 @@ Proof.
intros. red; intros; subst. elim H. destruct ge. eauto.
Qed.
+Theorem invert_find_symbol:
+ forall ge id b,
+ invert_symbol ge b = Some id -> find_symbol ge id = Some b.
+Proof.
+ intros until b; unfold find_symbol, invert_symbol.
+ apply PTree_Properties.fold_rec.
+ intros. rewrite H in H0; auto.
+ congruence.
+ intros. destruct (eq_block b v). inv H2. apply PTree.gss.
+ rewrite PTree.gsspec. destruct (peq id k).
+ subst. assert (m!k = Some b) by auto. congruence.
+ auto.
+Qed.
+
+Theorem find_invert_symbol:
+ forall ge id b,
+ find_symbol ge id = Some b -> invert_symbol ge b = Some id.
+Proof.
+ intros until b.
+ assert (find_symbol ge id = Some b -> exists id', invert_symbol ge b = Some id').
+ unfold find_symbol, invert_symbol.
+ apply PTree_Properties.fold_rec.
+ intros. rewrite H in H0; auto.
+ rewrite PTree.gempty; congruence.
+ intros. destruct (eq_block b v). exists k; auto.
+ rewrite PTree.gsspec in H2. destruct (peq id k).
+ inv H2. congruence. auto.
+
+ intros; exploit H; eauto. intros [id' A].
+ assert (id = id'). eapply genv_vars_inj; eauto. apply invert_find_symbol; auto.
+ congruence.
+Qed.
+
(** * Construction of the initial memory state *)
Section INITMEM.
@@ -517,6 +559,18 @@ Fixpoint store_init_data_list (m: mem) (b: block) (p: Z) (idl: list init_data)
end
end.
+Function store_zeros (m: mem) (b: block) (n: Z) {wf (Zwf 0) n}: option mem :=
+ if zle n 0 then Some m else
+ let n' := n - 1 in
+ match Mem.store Mint8unsigned m b n' Vzero with
+ | Some m' => store_zeros m' b n'
+ | None => None
+ end.
+Proof.
+ intros. red. omega.
+ apply Zwf_well_founded.
+Qed.
+
Fixpoint init_data_list_size (il: list init_data) {struct il} : Z :=
match il with
| nil => 0
@@ -530,10 +584,15 @@ Definition perm_globvar (gv: globvar V) : permission :=
Definition alloc_variable (m: mem) (idv: ident * globvar V) : option mem :=
let init := idv#2.(gvar_init) in
- let (m', b) := Mem.alloc m 0 (init_data_list_size init) in
- match store_init_data_list m' b 0 init with
+ let sz := init_data_list_size init in
+ let (m1, b) := Mem.alloc m 0 sz in
+ match store_zeros m1 b sz with
| None => None
- | Some m'' => Mem.drop_perm m'' b 0 (init_data_list_size init) (perm_globvar idv#2)
+ | Some m2 =>
+ match store_init_data_list m2 b 0 init with
+ | None => None
+ | Some m3 => Mem.drop_perm m3 b 0 sz (perm_globvar idv#2)
+ end
end.
Fixpoint alloc_variables (m: mem) (vl: list (ident * globvar V))
@@ -561,6 +620,15 @@ Proof.
destruct (find_symbol ge i); try congruence. eapply Mem.nextblock_store; eauto.
Qed.
+Remark store_zeros_nextblock:
+ forall m b n m', store_zeros m b n = Some m' -> Mem.nextblock m' = Mem.nextblock m.
+Proof.
+ intros until n. functional induction (store_zeros m b n); intros.
+ inv H; auto.
+ rewrite IHo; eauto with mem.
+ congruence.
+Qed.
+
Remark alloc_variables_nextblock:
forall vl m m',
alloc_variables m vl = Some m' ->
@@ -571,17 +639,31 @@ Proof.
simpl length; rewrite inj_S; simpl. intros m m'.
unfold alloc_variable.
set (init := gvar_init a#2).
- caseEq (Mem.alloc m 0 (init_data_list_size init)). intros m1 b ALLOC.
- caseEq (store_init_data_list m1 b 0 init); try congruence. intros m2 STORE.
- caseEq (Mem.drop_perm m2 b 0 (init_data_list_size init) (perm_globvar a#2)); try congruence.
- intros m3 DROP REC.
+ set (sz := init_data_list_size init).
+ caseEq (Mem.alloc m 0 sz). intros m1 b ALLOC.
+ caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ.
+ caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE.
+ caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar a#2)); try congruence. intros m4 DROP REC.
rewrite (IHvl _ _ REC).
rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP).
rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
+ rewrite (store_zeros_nextblock _ _ _ STZ).
rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC).
unfold block in *; omega.
Qed.
+
+Remark store_zeros_perm:
+ forall prm b' q m b n m',
+ store_zeros m b n = Some m' ->
+ Mem.perm m b' q prm -> Mem.perm m' b' q prm.
+Proof.
+ intros until n. functional induction (store_zeros m b n); intros.
+ inv H; auto.
+ eauto with mem.
+ congruence.
+Qed.
+
Remark store_init_data_list_perm:
forall prm b' q idl b m p m',
store_init_data_list m b p idl = Some m' ->
@@ -605,17 +687,31 @@ Proof.
simpl; intros. congruence.
intros until m'. simpl. unfold alloc_variable.
set (init := gvar_init a#2).
- caseEq (Mem.alloc m 0 (init_data_list_size init)). intros m1 b ALLOC.
- caseEq (store_init_data_list m1 b 0 init); try congruence. intros m2 STORE.
- caseEq (Mem.drop_perm m2 b 0 (init_data_list_size init) (perm_globvar a#2)); try congruence.
- intros m3 DROP REC PERM.
+ set (sz := init_data_list_size init).
+ caseEq (Mem.alloc m 0 sz). intros m1 b ALLOC.
+ caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ.
+ caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE.
+ caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar a#2)); try congruence. intros m4 DROP REC PERM.
assert (b' <> b). apply Mem.valid_not_valid_diff with m; eauto with mem.
eapply IHvl; eauto.
eapply Mem.perm_drop_3; eauto.
- eapply store_init_data_list_perm; eauto.
+ eapply store_init_data_list_perm; eauto.
+ eapply store_zeros_perm; eauto.
eauto with mem.
Qed.
+Remark store_zeros_outside:
+ forall m b n m',
+ store_zeros m b n = Some m' ->
+ forall chunk b' p,
+ b' <> b -> Mem.load chunk m' b' p = Mem.load chunk m b' p.
+Proof.
+ intros until n. functional induction (store_zeros m b n); intros.
+ inv H; auto.
+ rewrite IHo; auto. eapply Mem.load_store_other; eauto.
+ inv H.
+Qed.
+
Remark store_init_data_list_outside:
forall b il m p m',
store_init_data_list m b p il = Some m' ->
@@ -699,20 +795,24 @@ Proof.
congruence.
unfold alloc_variable.
set (init := gvar_init a#2).
- caseEq (Mem.alloc m 0 (init_data_list_size init)); intros m1 b1 ALLOC.
- caseEq (store_init_data_list m1 b1 0 init); try congruence. intros m2 STO.
- caseEq (Mem.drop_perm m2 b1 0 (init_data_list_size init) (perm_globvar a#2)); try congruence.
- intros m3 DROP RED VALID.
+ set (sz := init_data_list_size init).
+ caseEq (Mem.alloc m 0 sz). intros m1 b1 ALLOC.
+ caseEq (store_zeros m1 b1 sz); try congruence. intros m2 STZ.
+ caseEq (store_init_data_list m2 b1 0 init); try congruence. intros m3 STORE.
+ caseEq (Mem.drop_perm m3 b1 0 sz (perm_globvar a#2)); try congruence. intros m4 DROP REC VALID.
assert (b <> b1). apply Mem.valid_not_valid_diff with m; eauto with mem.
- transitivity (Mem.load chunk m3 b p).
+ transitivity (Mem.load chunk m4 b p).
apply IHvl; auto. red.
rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP).
- rewrite (store_init_data_list_nextblock _ _ _ _ STO).
+ rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
+ rewrite (store_zeros_nextblock _ _ _ STZ).
change (Mem.valid_block m1 b). eauto with mem.
- transitivity (Mem.load chunk m2 b p).
+ transitivity (Mem.load chunk m3 b p).
eapply Mem.load_drop; eauto.
+ transitivity (Mem.load chunk m2 b p).
+ eapply store_init_data_list_outside; eauto.
transitivity (Mem.load chunk m1 b p).
- eapply store_init_data_list_outside; eauto.
+ eapply store_zeros_outside; eauto.
eapply Mem.load_alloc_unchanged; eauto.
Qed.
@@ -742,14 +842,15 @@ Proof.
contradiction.
intros until m'; intro NEXT.
unfold alloc_variable. destruct a as [id' gv']. simpl.
- caseEq (Mem.alloc m 0 (init_data_list_size (gvar_init gv'))); try congruence.
- intros m1 b ALLOC.
- caseEq (store_init_data_list m1 b 0 (gvar_init gv')); try congruence.
- intros m2 STORE.
- caseEq (Mem.drop_perm m2 b 0 (init_data_list_size (gvar_init gv')) (perm_globvar gv')); try congruence.
- intros m3 DROP REC NOREPET IN. inv NOREPET.
+ set (init := gvar_init gv').
+ set (sz := init_data_list_size init).
+ caseEq (Mem.alloc m 0 sz); try congruence. intros m1 b ALLOC.
+ caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ.
+ caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE.
+ caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar gv')); try congruence.
+ intros m4 DROP REC NOREPET IN. inv NOREPET.
exploit Mem.alloc_result; eauto. intro BEQ.
- destruct IN. inv H.
+ destruct IN. inversion H; subst id gv.
exists (Mem.nextblock m); split.
rewrite add_variables_same_symb; auto. unfold find_symbol; simpl.
rewrite PTree.gss. congruence.
@@ -757,23 +858,24 @@ Proof.
rewrite NEXT. apply ZMap.gss.
simpl. rewrite <- NEXT; omega.
split. red; intros.
- eapply alloc_variables_perm; eauto.
- eapply Mem.perm_drop_1; eauto.
+ rewrite <- BEQ. eapply alloc_variables_perm; eauto. eapply Mem.perm_drop_1; eauto.
intros NOVOL.
- apply load_store_init_data_invariant with m2.
- intros. transitivity (Mem.load chunk m3 (Mem.nextblock m) ofs).
+ apply load_store_init_data_invariant with m3.
+ intros. transitivity (Mem.load chunk m4 (Mem.nextblock m) ofs).
eapply load_alloc_variables; eauto.
red. rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP).
rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
- change (Mem.valid_block m1 (Mem.nextblock m)). eauto with mem.
+ rewrite (store_zeros_nextblock _ _ _ STZ).
+ change (Mem.valid_block m1 (Mem.nextblock m)). rewrite <- BEQ. eauto with mem.
eapply Mem.load_drop; eauto. repeat right.
- unfold perm_globvar. rewrite NOVOL. destruct (gvar_readonly gv); auto with mem.
- eapply store_init_data_list_charact; eauto.
+ unfold perm_globvar. rewrite NOVOL. destruct (gvar_readonly gv'); auto with mem.
+ rewrite <- BEQ. eapply store_init_data_list_charact; eauto.
- apply IHvl with m3; auto.
+ apply IHvl with m4; auto.
simpl.
rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP).
rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
+ rewrite (store_zeros_nextblock _ _ _ STZ).
rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC). unfold block in *; omega.
Qed.
@@ -861,6 +963,19 @@ Proof.
eapply IHidl. eapply store_init_data_neutral; eauto. auto. eauto.
Qed.
+Lemma store_zeros_neutral:
+ forall m b n m',
+ Mem.inject_neutral thr m ->
+ b < thr ->
+ store_zeros m b n = Some m' ->
+ Mem.inject_neutral thr m'.
+Proof.
+ intros until n. functional induction (store_zeros m b n); intros.
+ inv H1; auto.
+ apply IHo; auto. eapply Mem.store_inject_neutral; eauto. constructor.
+ inv H1.
+Qed.
+
Lemma alloc_variable_neutral:
forall id m m',
alloc_variable ge m id = Some m' ->
@@ -868,16 +983,18 @@ Lemma alloc_variable_neutral:
Mem.nextblock m < thr ->
Mem.inject_neutral thr m'.
Proof.
- intros until m'. unfold alloc_variable.
- caseEq (Mem.alloc m 0 (init_data_list_size (gvar_init id#2))); intros m1 b ALLOC.
- caseEq (store_init_data_list ge m1 b 0 (gvar_init id#2)); try congruence.
- intros m2 STORE DROP NEUTRAL NEXT.
+ intros until m'. unfold alloc_variable.
+ set (init := gvar_init id#2).
+ set (sz := init_data_list_size init).
+ caseEq (Mem.alloc m 0 sz); try congruence. intros m1 b ALLOC.
+ caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ.
+ caseEq (store_init_data_list ge m2 b 0 init); try congruence.
+ intros m3 STORE DROP NEUTRAL NEXT.
+ assert (b < thr). rewrite (Mem.alloc_result _ _ _ _ _ ALLOC). auto.
eapply Mem.drop_inject_neutral; eauto.
- eapply store_init_data_list_neutral with (b := b).
+ eapply store_init_data_list_neutral with (m := m2) (b := b); eauto.
+ eapply store_zeros_neutral with (m := m1); eauto.
eapply Mem.alloc_inject_neutral; eauto.
- rewrite (Mem.alloc_result _ _ _ _ _ ALLOC). auto.
- eauto.
- rewrite (Mem.alloc_result _ _ _ _ _ ALLOC). auto.
Qed.
Lemma alloc_variables_neutral:
@@ -1099,11 +1216,12 @@ Proof.
inv H.
unfold alloc_variable; simpl.
destruct (Mem.alloc m 0 (init_data_list_size init)).
+ destruct (store_zeros m0 b (init_data_list_size init)); auto.
rewrite store_init_data_list_match.
- destruct (store_init_data_list (globalenv p) m0 b 0 init); auto.
+ destruct (store_init_data_list (globalenv p) m1 b 0 init); auto.
change (perm_globvar (mkglobvar info2 init ro vo))
with (perm_globvar (mkglobvar info1 init ro vo)).
- destruct (Mem.drop_perm m1 b 0 (init_data_list_size init)
+ destruct (Mem.drop_perm m2 b 0 (init_data_list_size init)
(perm_globvar (mkglobvar info1 init ro vo))); auto.
Qed.