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, 72 insertions, 60 deletions

diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index d07bd08..f4d1342 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -17,7 +17,7 @@ Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Events.
 Require Import Smallstep.
 Require Import Globalenvs.
@@ -337,7 +337,7 @@ Lemma function_ptr_translated:
   exists tf,
   Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf.
 Proof
-  (Genv.find_funct_ptr_transf_partial transl_fundef TRANSL).
+  (Genv.find_funct_ptr_transf_partial transl_fundef _ TRANSL).
 
 Lemma functions_translated:
   forall (v: val) (f: CminorSel.fundef),
@@ -345,7 +345,7 @@ Lemma functions_translated:
   exists tf,
   Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf.
 Proof
-  (Genv.find_funct_transf_partial transl_fundef TRANSL).
+  (Genv.find_funct_transf_partial transl_fundef _ TRANSL).
 
 Lemma sig_transl_function:
   forall (f: CminorSel.fundef) (tf: RTL.fundef),
@@ -365,10 +365,10 @@ Qed.
 (** Correctness of the code generated by [add_move]. *)
 
 Lemma tr_move_correct:
-  forall r1 ns r2 nd cs code sp rs m,
-  tr_move code ns r1 nd r2 ->
+  forall r1 ns r2 nd cs f sp rs m,
+  tr_move f.(fn_code) ns r1 nd r2 ->
   exists rs',
-  star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs' m) /\
+  star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m) /\
   rs'#r2 = rs#r1 /\
   (forall r, r <> r2 -> rs'#r = rs#r).
 Proof.
@@ -382,13 +382,13 @@ Qed.
 (** Correctness of the code generated by [store_var] and [store_optvar]. *)
 
 Lemma tr_store_var_correct:
-  forall rs cs code map r id ns nd e sp m,
-  tr_store_var code map r id ns nd ->
+  forall rs cs f map r id ns nd e sp m,
+  tr_store_var f.(fn_code) map r id ns nd ->
   map_wf map ->
   match_env map e nil rs ->
   exists rs',
-     star step tge (State cs code sp ns rs m)
-                E0 (State cs code sp nd rs' m)
+     star step tge (State cs f sp ns rs m)
+                E0 (State cs f sp nd rs' m)
   /\ match_env map (PTree.set id rs#r e) nil rs'.
 Proof.
   intros. destruct H as [rv [A B]].
@@ -402,13 +402,13 @@ Proof.
 Qed.
 
 Lemma tr_store_optvar_correct:
-  forall rs cs code map r optid ns nd e sp m,
-  tr_store_optvar code map r optid ns nd ->
+  forall rs cs f map r optid ns nd e sp m,
+  tr_store_optvar f.(fn_code) map r optid ns nd ->
   map_wf map ->
   match_env map e nil rs ->
   exists rs',
-     star step tge (State cs code sp ns rs m)
-                E0 (State cs code sp nd rs' m)
+     star step tge (State cs f sp ns rs m)
+                E0 (State cs f sp nd rs' m)
   /\ match_env map (set_optvar optid rs#r e) nil rs'.
 Proof.
   intros. destruct optid; simpl in *.
@@ -419,15 +419,15 @@ Qed.
 (** Correctness of the translation of [switch] statements *)
 
 Lemma transl_switch_correct:
-  forall cs sp e m code map r nexits t ns,
-  tr_switch code map r nexits t ns ->
+  forall cs sp e m f map r nexits t ns,
+  tr_switch f.(fn_code) map r nexits t ns ->
   forall rs i act,
   rs#r = Vint i ->
   map_wf map ->
   match_env map e nil rs ->
   comptree_match i t = Some act ->
   exists nd, exists rs',
-  star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs' m) /\
+  star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m) /\
   nth_error nexits act = Some nd /\
   match_env map e nil rs'.
 Proof.
@@ -458,7 +458,7 @@ Proof.
   set (rs1 := rs#rt <- (Vint(Int.sub i ofs))).
   assert (ME1: match_env map e nil rs1).
     unfold rs1. eauto with rtlg.
-  assert (EX1: step tge (State cs code sp n rs m) E0 (State cs code sp n1 rs1 m)).
+  assert (EX1: step tge (State cs f sp n rs m) E0 (State cs f sp n1 rs1 m)).
     eapply exec_Iop; eauto. 
     predSpec Int.eq Int.eq_spec ofs Int.zero; simpl.
     rewrite H10. rewrite Int.sub_zero_l. congruence.
@@ -521,12 +521,12 @@ Variable m: mem.
 
 Definition transl_expr_prop 
      (le: letenv) (a: expr) (v: val) : Prop :=
-  forall cs code map pr ns nd rd rs
+  forall cs f map pr ns nd rd rs
     (MWF: map_wf map)
-    (TE: tr_expr code map pr a ns nd rd)
+    (TE: tr_expr f.(fn_code) map pr a ns nd rd)
     (ME: match_env map e le rs),
   exists rs',
-     star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs' m)
+     star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m)
   /\ match_env map e le rs'
   /\ rs'#rd = v
   /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r).
@@ -536,25 +536,25 @@ Definition transl_expr_prop
 
 Definition transl_exprlist_prop 
      (le: letenv) (al: exprlist) (vl: list val) : Prop :=
-  forall cs code map pr ns nd rl rs
+  forall cs f map pr ns nd rl rs
     (MWF: map_wf map)
-    (TE: tr_exprlist code map pr al ns nd rl)
+    (TE: tr_exprlist f.(fn_code) map pr al ns nd rl)
     (ME: match_env map e le rs),
   exists rs',
-     star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs' m)
+     star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m)
   /\ match_env map e le rs'
   /\ rs'##rl = vl
   /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r).
 
 Definition transl_condition_prop 
      (le: letenv) (a: condexpr) (vb: bool) : Prop :=
-  forall cs code map pr ns ntrue nfalse rs
+  forall cs f map pr ns ntrue nfalse rs
     (MWF: map_wf map)
-    (TE: tr_condition code map pr a ns ntrue nfalse)
+    (TE: tr_condition f.(fn_code) map pr a ns ntrue nfalse)
     (ME: match_env map e le rs),
   exists rs',
-     star step tge (State cs code sp ns rs m) E0
-                   (State cs code sp (if vb then ntrue else nfalse) rs' m)
+     star step tge (State cs f sp ns rs m) E0
+                   (State cs f sp (if vb then ntrue else nfalse) rs' m)
   /\ match_env map e le rs'
   /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r).
 
@@ -604,7 +604,7 @@ Proof.
   split. eapply star_right. eexact EX1.
   eapply exec_Iop; eauto.  
   subst vargs.
-  rewrite (@eval_operation_preserved CminorSel.fundef RTL.fundef ge tge). 
+  rewrite (@eval_operation_preserved CminorSel.fundef _ _ _ ge tge). 
   auto. 
   exact symbols_preserved. traceEq.
 (* Match-env *)
@@ -621,7 +621,7 @@ Lemma transl_expr_Eload_correct:
   eval_exprlist ge sp e m le args vargs ->
   transl_exprlist_prop le args vargs ->
   Op.eval_addressing ge sp addr vargs = Some vaddr ->
-  loadv chunk m vaddr = Some v ->
+  Mem.loadv chunk m vaddr = Some v ->
   transl_expr_prop le (Eload chunk addr args) v.
 Proof.
   intros; red; intros. inv TE.
@@ -629,7 +629,7 @@ Proof.
   exists (rs1#rd <- v).
 (* Exec *)
   split. eapply star_right. eexact EX1. eapply exec_Iload; eauto.
-  rewrite RES1. rewrite (@eval_addressing_preserved _ _ ge tge).
+  rewrite RES1. rewrite (@eval_addressing_preserved _ _ _ _ ge tge).
   exact H1. exact symbols_preserved. traceEq.
 (* Match-env *)
   split. eauto with rtlg. 
@@ -650,7 +650,7 @@ Lemma transl_expr_Econdition_correct:
 Proof.
   intros; red; intros; inv TE. 
   exploit H0; eauto. intros [rs1 [EX1 [ME1 OTHER1]]].
-  assert (tr_expr code map pr (if vcond then ifso else ifnot) (if vcond then ntrue else nfalse) nd rd).
+  assert (tr_expr f.(fn_code) map pr (if vcond then ifso else ifnot) (if vcond then ntrue else nfalse) nd rd).
     destruct vcond; auto.
   exploit H2; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
   exists rs2.
@@ -767,7 +767,7 @@ Lemma transl_condition_CEcondition_correct:
 Proof.
   intros; red; intros; inv TE. 
   exploit H0; eauto. intros [rs1 [EX1 [ME1 OTHER1]]].
-  assert (tr_condition code map pr (if vcond then ifso else ifnot)
+  assert (tr_condition f.(fn_code) map pr (if vcond then ifso else ifnot)
              (if vcond then ntrue' else nfalse') ntrue nfalse).
     destruct vcond; auto.
   exploit H2; eauto. intros [rs2 [EX2 [ME2 OTHER2]]].
@@ -977,12 +977,13 @@ Qed.
 
 *)
 
-Inductive tr_funbody (c: code) (map: mapping) (f: CminorSel.function)
+Inductive tr_fun (tf: function) (map: mapping) (f: CminorSel.function)
                      (ngoto: labelmap) (nret: node) (rret: option reg) : Prop :=
-  | tr_funbody_intro: forall nentry r,
+  | tr_fun_intro: forall nentry r,
       rret = ret_reg f.(CminorSel.fn_sig) r ->
-      tr_stmt c map f.(fn_body) nentry nret nil ngoto nret rret ->
-      tr_funbody c map f ngoto nret rret.
+      tr_stmt tf.(fn_code) map f.(fn_body) nentry nret nil ngoto nret rret ->
+      tf.(fn_stacksize) = f.(fn_stackspace) ->
+      tr_fun tf map f ngoto nret rret.
 
 Inductive tr_cont: RTL.code -> mapping -> 
                    CminorSel.cont -> node -> list node -> labelmap -> node -> option reg ->
@@ -1006,25 +1007,25 @@ Inductive tr_cont: RTL.code -> mapping ->
 with match_stacks: CminorSel.cont -> list RTL.stackframe -> Prop :=
   | match_stacks_stop:
       match_stacks Kstop nil
-  | match_stacks_call: forall optid f sp e k r c n rs cs map nexits ngoto nret rret n',
+  | match_stacks_call: forall optid f sp e k r tf n rs cs map nexits ngoto nret rret n',
       map_wf map ->
-      tr_funbody c map f ngoto nret rret ->
+      tr_fun tf map f ngoto nret rret ->
       match_env map e nil rs ->
-      tr_store_optvar c map r optid n n' ->
+      tr_store_optvar tf.(fn_code) map r optid n n' ->
       ~reg_in_map map r ->
-      tr_cont c map k n' nexits ngoto nret rret cs ->
-      match_stacks (Kcall optid f sp e k) (Stackframe r c sp n rs :: cs).
+      tr_cont tf.(fn_code) map k n' nexits ngoto nret rret cs ->
+      match_stacks (Kcall optid f sp e k) (Stackframe r tf sp n rs :: cs).
 
 Inductive match_states: CminorSel.state -> RTL.state -> Prop :=
   | match_state:
-      forall f s k sp e m cs c ns rs map ncont nexits ngoto nret rret
+      forall f s k sp e m cs tf ns rs map ncont nexits ngoto nret rret
         (MWF: map_wf map)
-        (TS: tr_stmt c map s ns ncont nexits ngoto nret rret)
-        (TF: tr_funbody c map f ngoto nret rret)
-        (TK: tr_cont c map k ncont nexits ngoto nret rret cs)
+        (TS: tr_stmt tf.(fn_code) map s ns ncont nexits ngoto nret rret)
+        (TF: tr_fun tf map f ngoto nret rret)
+        (TK: tr_cont tf.(fn_code) map k ncont nexits ngoto nret rret cs)
         (ME: match_env map e nil rs),
       match_states (CminorSel.State f s k sp e m)
-                   (RTL.State cs c sp ns rs m)
+                   (RTL.State cs tf sp ns rs m)
   | match_callstate:
       forall f args k m cs tf
         (TF: transl_fundef f = OK tf)
@@ -1109,15 +1110,19 @@ Proof.
 
   (* skip return *)
   inv TS. 
-  assert (c!ncont = Some(Ireturn rret) /\ match_stacks k cs).
-    inv TK; simpl in H; try contradiction; auto.
-  destruct H1.
+  assert ((fn_code tf)!ncont = Some(Ireturn rret)
+          /\ match_stacks k cs).
+    inv TK; simpl in H; try contradiction; auto. 
+  destruct H2.
   assert (rret = None). 
     inv TF. unfold ret_reg. rewrite H0. auto.
+  assert (fn_stacksize tf = fn_stackspace f).
+    inv TF. auto. 
   subst rret.
   econstructor; split.
   left; apply plus_one. eapply exec_Ireturn. eauto.
-  simpl. constructor; auto.
+  rewrite H5. eauto. 
+  constructor; auto.
   
   (* assign *)
   inv TS. 
@@ -1152,7 +1157,7 @@ Proof.
   intros [rs' [A [B [C D]]]].
   exploit transl_exprlist_correct; eauto.
   intros [rs'' [E [F [G J]]]].
-  exploit functions_translated; eauto. intros [tf [P Q]].
+  exploit functions_translated; eauto. intros [tf' [P Q]].
   econstructor; split.
   left; eapply plus_right. eapply star_trans. eexact A. eexact E. reflexivity.
   eapply exec_Icall; eauto. simpl. rewrite J. rewrite C. eauto. simpl; auto.
@@ -1166,12 +1171,14 @@ Proof.
   intros [rs' [A [B [C D]]]].
   exploit transl_exprlist_correct; eauto.
   intros [rs'' [E [F [G J]]]].
-  exploit functions_translated; eauto. intros [tf [P Q]].
+  exploit functions_translated; eauto. intros [tf' [P Q]].
   exploit match_stacks_call_cont; eauto. intros [U V].
+  assert (fn_stacksize tf = fn_stackspace f). inv TF; auto.
   econstructor; split.
   left; eapply plus_right. eapply star_trans. eexact A. eexact E. reflexivity.
   eapply exec_Itailcall; eauto. simpl. rewrite J. rewrite C. eauto. simpl; auto.
   apply sig_transl_function; auto.
+  rewrite H2; eauto.
   traceEq.
   rewrite G. constructor; auto.
   (* seq *)
@@ -1234,17 +1241,21 @@ Proof.
   (* return none *)
   inv TS.
   exploit match_stacks_call_cont; eauto. intros [U V].
+  inversion TF.
   econstructor; split.
   left; apply plus_one. eapply exec_Ireturn; eauto.
-  simpl. constructor; auto.
+  rewrite H2; eauto.
+  constructor; auto.
 
   (* return some *)
   inv TS.
   exploit transl_expr_correct; eauto.
   intros [rs' [A [B [C D]]]].
-  exploit match_stacks_call_cont; eauto. intros [U V].  
+  exploit match_stacks_call_cont; eauto. intros [U V].
+  inversion TF.
   econstructor; split.
-  left; eapply plus_right. eexact A. eapply exec_Ireturn; eauto. traceEq.
+  left; eapply plus_right. eexact A. eapply exec_Ireturn; eauto.
+  rewrite H4; eauto. traceEq.
   simpl. rewrite C. constructor; auto.
 
   (* label *)
@@ -1301,11 +1312,12 @@ Proof.
   induction 1.
   exploit function_ptr_translated; eauto. intros [tf [A B]].
   econstructor; split.
-  econstructor. rewrite (transform_partial_program_main _ _ TRANSL). fold tge.
-  rewrite symbols_preserved. eexact H.
+  econstructor. apply (Genv.init_mem_transf_partial _ _ TRANSL); eauto.
+  rewrite (transform_partial_program_main _ _ TRANSL). fold tge.
+  rewrite symbols_preserved. eauto.
   eexact A.
-  rewrite <- H1. apply sig_transl_function; auto.
-  rewrite (Genv.init_mem_transf_partial _ _ TRANSL). constructor. auto. constructor.
+  rewrite <- H2. apply sig_transl_function; auto.
+  constructor. auto. constructor.
 Qed.
 
 Lemma transl_final_states: