Stocker l'adresse de retour a l'offset 12 au lieu de l'offset 4 pour meilleure compatibilite avec les conventions de MacOSX

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

8 files changed, 19 insertions, 19 deletions

diff --git a/backend/Mach.v b/backend/Mach.v
index 75b5baa8..b8bf1e36 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -253,7 +253,7 @@ with exec_instrs:
 
 (** In addition to reserving the word at offset 0 in the activation 
   record for maintaining the linking of activation records,
-  we need to reserve the word at offset 4 to store the return address
+  we need to reserve the word at offset 12 to store the return address
   into the caller.  However, the return address (a pointer within
   the code of the caller) is not precisely known at this point:
   it will be determined only after the final translation to PowerPC
@@ -280,12 +280,12 @@ with exec_function_body:
                                                         = (m1, stk) ->
       let sp := Vptr stk (Int.repr (-f.(fn_framesize))) in
       store_stack m1 sp Tint (Int.repr 0) parent = Some m2 ->
-      store_stack m2 sp Tint (Int.repr 4) ra = Some m3 ->
+      store_stack m2 sp Tint (Int.repr 12) ra = Some m3 ->
       exec_instrs f sp
                   f.(fn_code) rs m3
                 t (Mreturn :: c) rs' m4 ->
       load_stack m4 sp Tint (Int.repr 0) = Some parent ->
-      load_stack m4 sp Tint (Int.repr 4) = Some ra ->
+      load_stack m4 sp Tint (Int.repr 12) = Some ra ->
       exec_function_body f parent ra rs m t rs' (Mem.free m4 stk)
 
 with exec_function:
diff --git a/backend/Machabstr.v b/backend/Machabstr.v
index 8d5d72a9..33ed93ca 100644
--- a/backend/Machabstr.v
+++ b/backend/Machabstr.v
@@ -205,7 +205,7 @@ with exec_function_body:
       forall f parent link ra rs m t rs' m1 m2 stk fr1 fr2 fr3 c,
       Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) ->
       set_slot (init_frame f) Tint 0 link fr1 ->
-      set_slot fr1 Tint 4 ra fr2 ->
+      set_slot fr1 Tint 12 ra fr2 ->
       exec_instrs f (Vptr stk (Int.repr (-f.(fn_framesize)))) parent
                   f.(fn_code) rs fr2 m1
                 t (Mreturn :: c) rs' fr3 m2 ->
@@ -347,7 +347,7 @@ Lemma exec_mutual_induction:
           (stk : block) (fr1 fr2 fr3 : frame) (c : list instruction),
         alloc m 0 (fn_stacksize f13) = (m1, stk) ->
         set_slot (init_frame f13) Tint 0 link fr1 ->
-        set_slot fr1 Tint 4 ra fr2 ->
+        set_slot fr1 Tint 12 ra fr2 ->
         exec_instrs f13 (Vptr stk (Int.repr (- fn_framesize f13))) parent
           (fn_code f13) rs fr2 m1 t (Mreturn :: c) rs' fr3 m2 ->
         P0 f13 (Vptr stk (Int.repr (- fn_framesize f13))) parent
diff --git a/backend/Machabstr2mach.v b/backend/Machabstr2mach.v
index 0513cbee..a07f64af 100644
--- a/backend/Machabstr2mach.v
+++ b/backend/Machabstr2mach.v
@@ -1091,10 +1091,10 @@ Proof.
   intros [ms2 [STORELINK [CSI2 EQ]]].
   subst stk1.
   assert (ZERO: Int.signed (Int.repr 0) = 0). reflexivity.
-  assert (FOUR: Int.signed (Int.repr 4) = 4). reflexivity.
-  assert (BND: 4 <= Int.signed (Int.repr 4)).
-    rewrite FOUR; omega.
-  rewrite <- FOUR in H1.
+  assert (TWELVE: Int.signed (Int.repr 12) = 12). reflexivity.
+  assert (BND: 4 <= Int.signed (Int.repr 12)).
+    rewrite TWELVE; omega.
+  rewrite <- TWELVE in H1.
   generalize (callstack_set_slot _ _ _ _ _ _ _ _ _ _
                CSI2 H1 BND).
   intros [ms3 [STORERA CSI3]].
@@ -1116,7 +1116,7 @@ Proof.
   eapply slot_gso; eauto. rewrite ZERO. eapply slot_gss; eauto. 
   exact I. 
   eapply callstack_get_slot. eexact CSI4.
-  apply LINKINV. rewrite FOUR. omega. eapply slot_gss; eauto. auto.
+  apply LINKINV. rewrite TWELVE. omega. eapply slot_gss; eauto. auto.
   eapply callstack_function_return; eauto.
 
   (* internal function *)
diff --git a/backend/Machtyping.v b/backend/Machtyping.v
index 92f283b6..24f0ddb6 100644
--- a/backend/Machtyping.v
+++ b/backend/Machtyping.v
@@ -335,7 +335,7 @@ End SUBJECT_REDUCTION.
 (** We now show another result useful for the proof of implication
     between the two Mach semantics: well-typed functions do not
     change the values of the back link and return address fields
-    of the frame slot (at offsets 0 and 4) during their execution.
+    of the frame slot (at offsets 0 and 12) during their execution.
     Actually, we show that the whole reserved part of the frame
     (between offsets 0 and 24) does not change. *)
 
diff --git a/backend/PPCgen.v b/backend/PPCgen.v
index 6cf06991..ba8ea285 100644
--- a/backend/PPCgen.v
+++ b/backend/PPCgen.v
@@ -485,7 +485,7 @@ Definition transl_instr (i: Mach.instruction) (k: code) :=
       transl_cond cond args
         (if (snd p) then Pbt (fst p) lbl :: k else Pbf (fst p) lbl :: k)
   | Mreturn =>
-      Plwz GPR2 (Cint (Int.repr 4)) GPR1 ::
+      Plwz GPR2 (Cint (Int.repr 12)) GPR1 ::
       Pmtlr GPR2 :: Pfreeframe :: Pblr :: k
   end.
 
@@ -501,7 +501,7 @@ Definition transl_function (f: Mach.function) :=
   Pallocframe (- f.(fn_framesize))
               (align_16_top (-f.(fn_framesize)) f.(fn_stacksize)) ::
   Pmflr GPR2 ::
-  Pstw GPR2 (Cint (Int.repr 4)) GPR1 ::
+  Pstw GPR2 (Cint (Int.repr 12)) GPR1 ::
   transl_code f.(fn_code).
 
 Fixpoint code_size (c: code) : Z :=
diff --git a/backend/PPCgenproof.v b/backend/PPCgenproof.v
index 32649998..9cbbc659 100644
--- a/backend/PPCgenproof.v
+++ b/backend/PPCgenproof.v
@@ -1061,11 +1061,11 @@ Lemma exec_function_body_prop_:
       (align_16_top (- fn_framesize f) (fn_stacksize f)) = (m1, stk) ->
    let sp := Vptr stk (Int.repr (- fn_framesize f)) in
    store_stack m1 sp Tint (Int.repr 0) parent = Some m2 ->
-   store_stack m2 sp Tint (Int.repr 4) ra = Some m3 ->
+   store_stack m2 sp Tint (Int.repr 12) ra = Some m3 ->
    exec_instrs ge f sp (fn_code f) ms m3 t (Mreturn :: c) ms' m4 ->
    exec_instr_prop f sp (fn_code f) ms m3 t (Mreturn :: c) ms' m4 ->
    load_stack m4 sp Tint (Int.repr 0) = Some parent ->
-   load_stack m4 sp Tint (Int.repr 4) = Some ra ->
+   load_stack m4 sp Tint (Int.repr 12) = Some ra ->
    exec_function_body_prop f parent ra ms m t ms' (free m4 stk).
 Proof.
   intros; red; intros.
diff --git a/backend/Stacking.v b/backend/Stacking.v
index 85ac9335..de350dc1 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -17,9 +17,9 @@ Require Import Conventions.
 (** The general shape of activation records is as follows,
   from bottom (lowest offsets) to top:
 - 24 reserved bytes.  The first 4 bytes hold the back pointer to the
-  activation record of the caller.  The next 4 bytes will be used
-  to store the return address.  The remaining 16 bytes are unused
-  but reserved in accordance with the PowerPC application binary interface.
+  activation record of the caller.  We use the 4 bytes at offset 12
+  to store the return address.  (These are reserved by the PowerPC
+  application binary interface.)  The remaining bytes are unused.
 - Space for outgoing arguments to function calls.
 - Local stack slots of integer type.
 - Saved values of integer callee-save registers used by the function.
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 96926707..69a7e99f 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -1533,7 +1533,7 @@ Proof.
     inversion SET1. reflexivity.
   assert (low fr1 = -fe.(fe_size)).
     inversion SET1. rewrite <- H2. reflexivity.
-  assert (exists fr2, set_slot fr1 Tint 4 ra fr2).
+  assert (exists fr2, set_slot fr1 Tint 12 ra fr2).
     apply set_slot_ok. auto. omega. rewrite H4. generalize (size_pos f). 
     unfold fe. simpl typesize. omega.
   elim H5; intros fr2 SET2; clear H5.