Merge of the newmem and newextcalls branches:

- Revised memory model with concrete representation of ints & floats,
  and per-byte access permissions
- Revised Globalenvs implementation
- Matching changes in all languages and proofs.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 16 insertions, 8 deletions

diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index c79908d..5d67065 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -19,7 +19,7 @@ Require Import FSets.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Errors.
@@ -49,14 +49,14 @@ Lemma functions_translated:
   Genv.find_funct ge v = Some f ->
   exists tf,
   Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_transf_partial transf_fundef TRANSF).
+Proof (Genv.find_funct_transf_partial transf_fundef _ TRANSF).
 
 Lemma function_ptr_translated:
   forall v f,
   Genv.find_funct_ptr ge v = Some f ->
   exists tf,
   Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial transf_fundef TRANSF).
+Proof (Genv.find_funct_ptr_transf_partial transf_fundef _ TRANSF).
 
 Lemma symbols_preserved:
   forall id,
@@ -73,6 +73,14 @@ Proof.
   inv H. reflexivity.
 Qed.
 
+Lemma stacksize_preserved:
+  forall f tf,
+  transf_function f = OK tf ->
+  LTLin.fn_stacksize tf = LTL.fn_stacksize f.
+Proof.
+  intros. monadInv H. auto.
+Qed.
+
 Lemma find_function_translated:
   forall ros ls f,
   LTL.find_function ge ros ls = Some f ->
@@ -593,6 +601,7 @@ Proof.
   econstructor; split.
   apply plus_one. eapply exec_Ltailcall with (f' := tf'); eauto.
   symmetry; apply sig_preserved; auto.
+  rewrite (stacksize_preserved _ _ TRF). eauto.
   econstructor; eauto.
   destruct ros; simpl in H0.
   eapply Genv.find_funct_prop; eauto.
@@ -656,6 +665,7 @@ Proof.
   simpl in EQ. subst c.
   econstructor; split.
   apply plus_one. eapply exec_Lreturn; eauto.
+  rewrite (stacksize_preserved _ _ TRF). eauto.
   econstructor; eauto.
  
   (* internal function *)
@@ -692,16 +702,14 @@ Lemma transf_initial_states:
 Proof.
   intros. inversion H.
   exploit function_ptr_translated; eauto. intros [tf [A B]].  
-  exists (Callstate nil tf nil (Genv.init_mem tprog)); split.
-  econstructor; eauto.
+  exists (Callstate nil tf nil m0); split.
+  econstructor; eauto. eapply Genv.init_mem_transf_partial; eauto. 
   replace (prog_main tprog) with (prog_main prog).
   rewrite symbols_preserved. eauto.
   symmetry. apply (transform_partial_program_main transf_fundef _ TRANSF). 
-  rewrite <- H2. apply sig_preserved. auto.
-  replace (Genv.init_mem tprog) with (Genv.init_mem prog).
+  rewrite <- H3. apply sig_preserved. auto.
   constructor. constructor. auto.
   eapply Genv.find_funct_ptr_prop; eauto.
-  symmetry. apply Genv.init_mem_transf_partial with transf_fundef. auto.
 Qed.
 
 Lemma transf_final_states: