From 4af1682d04244bab9f793e00eb24090153a36a0f Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 28 Jul 2011 12:51:16 +0000
Subject: 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
---
 common/Determinism.v | 109 ++++++++++++++-------------
 common/Globalenvs.v  | 208 ++++++++++++++++++++++++++++++++++++++++-----------
 2 files changed, 218 insertions(+), 99 deletions(-)

(limited to 'common')

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.
 
-- 
cgit v1.2.3