Partial backtracking on previous commit: the "hole in Mach stack frame"

trick prevents a future mapping of the Mach/Asm call stack as a single
block.  IA32 is fixed, PowerPC and ARM remains to be done.


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

1 files changed, 82 insertions, 55 deletions

diff --git a/backend/Mach.v b/backend/Mach.v
index 12c6c9db..0728c4df 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -115,7 +115,13 @@ semantics also make provisions for storing a back link at offset
 offset [f.(fn_retaddr_ofs)].  The latter stack location will be used
 by the Asm code generated by [Asmgen] to save the return address into
 the caller at the beginning of a function, then restore it and jump to
-it at the end of a function. *)
+it at the end of a function.  The Mach concrete semantics does not
+attach any particular meaning to the pointer stored in this reserved
+location, but makes sure that it is preserved during execution of a
+function.  The [return_address_offset] parameter is used to guess the
+value of the return address that the Asm code generated later will
+store in the reserved location.
+*)
 
 Definition chunk_of_type (ty: typ) :=
   match ty with Tint => Mint32 | Tfloat => Mfloat64al32 end.
@@ -202,16 +208,20 @@ Qed.
 
 Section RELSEM.
 
+Variable return_address_offset: function -> code -> int -> Prop.
+
 Variable ge: genv.
 
-Definition find_function (ros: mreg + ident) (rs: regset) : option fundef :=
+Definition find_function_ptr
+        (ge: genv) (ros: mreg + ident) (rs: regset) : option block :=
   match ros with
-  | inl r => Genv.find_funct ge (rs r)
-  | inr symb =>
-      match Genv.find_symbol ge symb with
-      | None => None
-      | Some b => Genv.find_funct_ptr ge b
+  | inl r =>
+      match rs r with
+      | Vptr b ofs => if Int.eq ofs Int.zero then Some b else None
+      | _ => None
       end
+  | inr symb =>
+      Genv.find_symbol ge symb
   end.
 
 (** Extract the values of the arguments to an external call. *)
@@ -242,17 +252,20 @@ Definition annot_arguments
 
 (** Mach execution states. *)
 
+(** Mach execution states. *)
+
 Inductive stackframe: Type :=
   | Stackframe:
-      forall (f: function)    (**r calling function *)
+      forall (f: block)       (**r pointer to calling function *)
              (sp: val)        (**r stack pointer in calling function *)
+             (retaddr: val)   (**r Asm return address in calling function *)
              (c: code),       (**r program point in calling function *)
       stackframe.
 
 Inductive state: Type :=
   | State:
       forall (stack: list stackframe)  (**r call stack *)
-             (f: function)             (**r current function *)
+             (f: block)                (**r pointer to current function *)
              (sp: val)                 (**r stack pointer *)
              (c: code)                 (**r current program point *)
              (rs: regset)              (**r register state *)
@@ -260,7 +273,7 @@ Inductive state: Type :=
       state
   | Callstate:
       forall (stack: list stackframe)  (**r call stack *)
-             (fd: fundef)              (**r function to call *)
+             (f: block)                (**r pointer to function to call *)
              (rs: regset)              (**r register state *)
              (m: mem),                 (**r memory state *)
       state
@@ -273,7 +286,13 @@ Inductive state: Type :=
 Definition parent_sp (s: list stackframe) : val :=
   match s with
   | nil => Vptr Mem.nullptr Int.zero
-  | Stackframe f sp c :: s' => sp
+  | Stackframe f sp ra c :: s' => sp
+  end.
+
+Definition parent_ra (s: list stackframe) : val :=
+  match s with
+  | nil => Vzero
+  | Stackframe f sp ra c :: s' => ra
   end.
 
 Inductive step: state -> trace -> state -> Prop :=
@@ -292,11 +311,12 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State s f sp (Msetstack src ofs ty :: c) rs m)
         E0 (State s f sp c (undef_setstack rs) m')
   | exec_Mgetparam:
-      forall s f sp ofs ty dst c rs m v,
+      forall s fb f sp ofs ty dst c rs m v,
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
       load_stack m sp Tint f.(fn_link_ofs) = Some (parent_sp s) ->
       load_stack m (parent_sp s) ty ofs = Some v ->
-      step (State s f sp (Mgetparam ofs ty dst :: c) rs m)
-        E0 (State s f sp c (rs # IT1 <- Vundef # dst <- v) m)
+      step (State s fb sp (Mgetparam ofs ty dst :: c) rs m)
+        E0 (State s fb sp c (rs # IT1 <- Vundef # dst <- v) m)
   | exec_Mop:
       forall s f sp op args res c rs m v,
       eval_operation ge sp op rs##args m = Some v ->
@@ -315,19 +335,22 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State s f sp (Mstore chunk addr args src :: c) rs m)
         E0 (State s f sp c (undef_temps rs) m')
   | exec_Mcall:
-      forall s f sp sig ros c rs m fd,
-      find_function ros rs = Some fd ->
-      step (State s f sp (Mcall sig ros :: c) rs m)
-        E0 (Callstate (Stackframe f sp c :: s)
-                       fd rs m)
+      forall s fb sp sig ros c rs m f f' ra,
+      find_function_ptr ge ros rs = Some f' ->
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
+      return_address_offset f c ra ->
+      step (State s fb sp (Mcall sig ros :: c) rs m)
+        E0 (Callstate (Stackframe fb sp (Vptr fb ra) c :: s)
+                       f' rs m)
   | exec_Mtailcall:
-      forall s f stk soff sig ros c rs m fd m' m'',
-      find_function ros rs = Some fd ->
+      forall s fb stk soff sig ros c rs m f f' m',
+      find_function_ptr ge ros rs = Some f' ->
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
       load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
-      Mem.free m stk 0 (Int.unsigned f.(fn_retaddr_ofs)) = Some m' ->
-      Mem.free m' stk (Int.unsigned f.(fn_retaddr_ofs) + 4) f.(fn_stacksize) = Some m'' ->
-      step (State s f (Vptr stk soff) (Mtailcall sig ros :: c) rs m)
-        E0 (Callstate s fd rs m'')
+      load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
+      step (State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs m)
+        E0 (Callstate s f' rs m')
   | exec_Mbuiltin:
       forall s f sp rs m ef args res b t v m',
       external_call ef ge rs##args m t v m' ->
@@ -340,70 +363,74 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State s f sp (Mannot ef args :: b) rs m)
          t (State s f sp b rs m')
   | exec_Mgoto:
-      forall s f sp lbl c rs m c',
+      forall s fb f sp lbl c rs m c',
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
       find_label lbl f.(fn_code) = Some c' ->
-      step (State s f sp (Mgoto lbl :: c) rs m)
-        E0 (State s f sp c' rs m)
+      step (State s fb sp (Mgoto lbl :: c) rs m)
+        E0 (State s fb sp c' rs m)
   | exec_Mcond_true:
-      forall s f sp cond args lbl c rs m c',
+      forall s fb f sp cond args lbl c rs m c',
       eval_condition cond rs##args m = Some true ->
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
       find_label lbl f.(fn_code) = Some c' ->
-      step (State s f sp (Mcond cond args lbl :: c) rs m)
-        E0 (State s f sp c' (undef_temps rs) m)
+      step (State s fb sp (Mcond cond args lbl :: c) rs m)
+        E0 (State s fb sp c' (undef_temps rs) m)
   | exec_Mcond_false:
       forall s f sp cond args lbl c rs m,
       eval_condition cond rs##args m = Some false ->
       step (State s f sp (Mcond cond args lbl :: c) rs m)
         E0 (State s f sp c (undef_temps rs) m)
   | exec_Mjumptable:
-      forall s f sp arg tbl c rs m n lbl c',
+      forall s fb f sp arg tbl c rs m n lbl c',
       rs arg = Vint n ->
       list_nth_z tbl (Int.unsigned n) = Some lbl ->
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
       find_label lbl f.(fn_code) = Some c' ->
-      step (State s f sp (Mjumptable arg tbl :: c) rs m)
-        E0 (State s f sp c' (undef_temps rs) m)
+      step (State s fb sp (Mjumptable arg tbl :: c) rs m)
+        E0 (State s fb sp c' (undef_temps rs) m)
   | exec_Mreturn:
-      forall s f stk soff c rs m m' m'',
+      forall s fb stk soff c rs m f m',
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
       load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
-      Mem.free m stk 0 (Int.unsigned f.(fn_retaddr_ofs)) = Some m' ->
-      Mem.free m' stk (Int.unsigned f.(fn_retaddr_ofs) + 4) f.(fn_stacksize) = Some m'' ->
-      step (State s f (Vptr stk soff) (Mreturn :: c) rs m)
-        E0 (Returnstate s rs m'')
+      load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
+      step (State s fb (Vptr stk soff) (Mreturn :: c) rs m)
+        E0 (Returnstate s rs m')
   | exec_function_internal:
-      forall s f rs m m1 m2 m3 stk,
+      forall s fb rs m f m1 m2 m3 stk,
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
       Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) ->
-      Mem.free m1 stk (Int.unsigned f.(fn_retaddr_ofs)) (Int.unsigned f.(fn_retaddr_ofs) + 4) = Some m2 ->
       let sp := Vptr stk Int.zero in
-      store_stack m2 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m3 ->
-      (4 | Int.unsigned f.(fn_retaddr_ofs)) ->
-      step (Callstate s (Internal f) rs m)
-        E0 (State s f sp f.(fn_code) (undef_temps rs) m3)
+      store_stack m1 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m2 ->
+      store_stack m2 sp Tint f.(fn_retaddr_ofs) (parent_ra s) = Some m3 ->
+      step (Callstate s fb rs m)
+        E0 (State s fb sp f.(fn_code) (undef_temps rs) m3)
   | exec_function_external:
-      forall s ef rs m t rs' args res m',
+      forall s fb rs m t rs' ef args res m',
+      Genv.find_funct_ptr ge fb = Some (External ef) ->
       external_call ef ge args m t res m' ->
       extcall_arguments rs m (parent_sp s) (ef_sig ef) args ->
       rs' = (rs#(loc_result (ef_sig ef)) <- res) ->
-      step (Callstate s (External ef) rs m)
+      step (Callstate s fb rs m)
          t (Returnstate s rs' m')
   | exec_return:
-      forall s f sp c rs m,
-      step (Returnstate (Stackframe f sp c :: s) rs m)
+      forall s f sp ra c rs m,
+      step (Returnstate (Stackframe f sp ra c :: s) rs m)
         E0 (State s f sp c rs m).
 
 End RELSEM.
 
 Inductive initial_state (p: program): state -> Prop :=
-  | initial_state_intro: forall b fd m0,
+  | initial_state_intro: forall fb m0,
       let ge := Genv.globalenv p in
       Genv.init_mem p = Some m0 ->
-      Genv.find_symbol ge p.(prog_main) = Some b ->
-      Genv.find_funct_ptr ge b = Some fd ->
-      initial_state p (Callstate nil fd (Regmap.init Vundef) m0).
+      Genv.find_symbol ge p.(prog_main) = Some fb ->
+      initial_state p (Callstate nil fb (Regmap.init Vundef) m0).
 
 Inductive final_state: state -> int -> Prop :=
   | final_state_intro: forall rs m r,
       rs (loc_result (mksignature nil (Some Tint))) = Vint r ->
       final_state (Returnstate nil rs m) r.
 
-Definition semantics (p: program) :=
-  Semantics step (initial_state p) final_state (Genv.globalenv p).
+Definition semantics (rao: function -> code -> int -> Prop) (p: program) :=
+  Semantics (step rao) (initial_state p) final_state (Genv.globalenv p).