From 210352d90e5972aabfb253f7c8a38349f53917b3 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 22 Oct 2006 16:54:24 +0000
Subject: Lever la restriction sur les fonctions externes, restriction qui
 exigeait que tous les arguments resident en registres

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@125 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/Allocation.v     | 10 +----
 backend/Allocproof.v     |  6 +--
 backend/Alloctyping.v    |  6 +--
 backend/Conventions.v    | 23 ------------
 backend/LTLtyping.v      |  1 -
 backend/Lineartyping.v   |  1 -
 backend/Mach.v           | 22 ++++++++++-
 backend/Machabstr.v      | 24 +++++++++++-
 backend/Machabstr2mach.v | 27 +++++++++++++-
 backend/Machtyping.v     |  1 -
 backend/PPC.v            | 56 ++++++++++++++--------------
 backend/PPCgenproof.v    |  8 ++--
 backend/PPCgenproof1.v   | 97 ++++++++++++++++++++++++++++--------------------
 backend/RTLtyping.v      | 19 ----------
 backend/Stackingproof.v  | 47 ++++++++++++++++++++++-
 backend/Stackingtyping.v |  2 +-
 16 files changed, 209 insertions(+), 141 deletions(-)

(limited to 'backend')

diff --git a/backend/Allocation.v b/backend/Allocation.v
index 66c7a3c..c66d6b0 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -412,15 +412,7 @@ Definition transf_function (f: RTL.function) : option LTL.function :=
   end.
 
 Definition transf_fundef (fd: RTL.fundef) : option LTL.fundef :=
-  match fd with
-  | External ef =>
-      if type_external_function ef then Some (External ef) else None
-  | Internal f =>
-      match transf_function f with
-      | None => None
-      | Some tf => Some (Internal tf)
-      end
-  end.
+  transf_partial_fundef transf_function fd.
 
 Definition transf_program (p: RTL.program) : option LTL.program :=
   transform_partial_program transf_fundef p.
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 07c0f58..0b252d5 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -1231,9 +1231,7 @@ Proof.
   destruct (regalloc f t). 
   intro EQ; injection EQ; intro EQ1; rewrite <- EQ1; simpl; auto.
   congruence. congruence. congruence.
-  destruct (type_external_function e).
   intro EQ; inversion EQ; subst tf. reflexivity.
-  congruence.
 Qed.
 
 Lemma entrypoint_function_translated:
@@ -1780,7 +1778,7 @@ Lemma transl_function_correct:
   exec_function_prop (Internal f) args m t vres (free m2 stk).
 Proof.
   intros; red; intros until tf.
-  unfold transf_fundef, transf_function.
+  unfold transf_fundef, transf_partial_fundef, transf_function.
   caseEq (type_function f).
   intros env TRF. 
   caseEq (analyze f).
@@ -1856,7 +1854,7 @@ Lemma transl_external_function_correct:
 Proof.
   intros; red; intros.
   simpl in H0. 
-  destruct (type_external_function ef); simplify_eq H0; intro.
+  simplify_eq H0; intro.
   exists (Locmap.set (R (loc_result (funsig tf))) res ls); split.
   subst tf. eapply exec_funct_external; eauto. 
   apply Locmap.gss.
diff --git a/backend/Alloctyping.v b/backend/Alloctyping.v
index e4f9f96..4c4c4f7 100644
--- a/backend/Alloctyping.v
+++ b/backend/Alloctyping.v
@@ -420,7 +420,7 @@ Proof.
   assert (sig = tf.(fn_sig)).
     unfold sig. 
     assert (transf_fundef (Internal f) = Some (Internal tf)).
-      unfold transf_fundef; rewrite TRANSL; auto.
+      unfold transf_fundef, transf_partial_fundef. rewrite TRANSL; auto.
     generalize (Allocproof.sig_function_translated _ _ H). simpl; auto.
   assert (locs_read_ok (loc_parameters sig)).
     red; unfold loc_parameters. intros. 
@@ -542,9 +542,7 @@ Proof.
   caseEq (transf_function f). intros g TF EQ. inversion EQ.
   constructor. eapply wt_transf_function; eauto.
   congruence.
-  caseEq (type_external_function e); intros.
-  inversion H0. constructor. apply type_external_function_correct. auto.
-  congruence.
+  intros. inversion H. constructor. 
 Qed.
 
 Lemma program_typing_preserved:
diff --git a/backend/Conventions.v b/backend/Conventions.v
index 5b4222d..d621e7c 100644
--- a/backend/Conventions.v
+++ b/backend/Conventions.v
@@ -676,29 +676,6 @@ Proof.
   intros; simpl. tauto.
 Qed.
 
-(** ** Location of arguments to external functions *)
-
-Definition loc_external_arguments (s: signature) : list mreg :=
-  List.map
-    (fun l => match l with R r => r | S _ => IT1 end)
-    (loc_arguments s).
-
-Definition sig_external_ok (s: signature) : Prop :=
-  forall sl, ~In (S sl) (loc_arguments s).
-
-Lemma loc_external_arguments_loc_arguments:
-  forall s, 
-  sig_external_ok s ->
-  loc_arguments s = List.map R (loc_external_arguments s).
-Proof.
-  intros. unfold loc_external_arguments.
-  rewrite list_map_compose.
-  transitivity (List.map (fun x => x) (loc_arguments s)).
-  symmetry; apply list_map_identity.
-  apply list_map_exten; intros.
-  destruct x. auto. elim (H _ H0).
-Qed.
-
 (** ** Location of argument and result of dynamic allocation *)
 
 Definition loc_alloc_argument := R3.
diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v
index 3450814..187c5cb 100644
--- a/backend/LTLtyping.v
+++ b/backend/LTLtyping.v
@@ -94,7 +94,6 @@ Definition wt_function (f: function) : Prop :=
 
 Inductive wt_fundef: fundef -> Prop :=
   | wt_fundef_external: forall ef,
-      Conventions.sig_external_ok ef.(ef_sig) ->
       wt_fundef (External ef)
   | wt_function_internal: forall f,
       wt_function f ->
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 3a0ee13..cbe1831 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -254,7 +254,6 @@ Definition wt_function (f: function) : Prop :=
 
 Inductive wt_fundef: fundef -> Prop :=
   | wt_fundef_external: forall ef,
-      Conventions.sig_external_ok ef.(ef_sig) ->
       wt_fundef (External ef)
   | wt_function_internal: forall f,
       wt_function f ->
diff --git a/backend/Mach.v b/backend/Mach.v
index b8bf1e3..f61620d 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -143,6 +143,26 @@ Definition find_function (ros: mreg + ident) (rs: regset) : option fundef :=
       end
   end.
 
+(** Extract the values of the arguments of an external call. *)
+
+Inductive extcall_arg: regset -> mem -> val -> loc -> val -> Prop :=
+  | extcall_arg_reg: forall rs m sp r,
+      extcall_arg rs m sp (R r) (rs r)
+  | extcall_arg_stack: forall rs m sp ofs ty v,
+      load_stack m sp ty (Int.repr (4 * ofs)) = Some v ->
+      extcall_arg rs m sp (S (Outgoing ofs ty)) v.
+
+Inductive extcall_args: regset -> mem -> val -> list loc -> list val -> Prop :=
+  | extcall_args_nil: forall rs m sp,
+      extcall_args rs m sp nil nil
+  | extcall_args_cons: forall rs m sp l1 ll v1 vl,
+      extcall_arg rs m sp l1 v1 -> extcall_args rs m sp ll vl ->
+      extcall_args rs m sp (l1 :: ll) (v1 :: vl).
+
+Definition extcall_arguments
+   (rs: regset) (m: mem) (sp: val) (sg: signature) (args: list val) : Prop :=
+  extcall_args rs m sp (Conventions.loc_arguments sg) args.
+
 (** [exec_instr ge f sp c rs m c' rs' m'] reflects the execution of
   the first instruction in the current instruction sequence [c].  
   [c'] is the current instruction sequence after this execution.
@@ -299,7 +319,7 @@ with exec_function:
   | exec_funct_external:
       forall ef parent args res rs1 rs2 m t,
       event_match ef args t res ->
-      args = rs1##(Conventions.loc_external_arguments ef.(ef_sig)) ->
+      extcall_arguments rs1 m parent ef.(ef_sig) args ->
       rs2 = (rs1#(Conventions.loc_result ef.(ef_sig)) <- res) ->
       exec_function (External ef) parent rs1 m t rs2 m.
 
diff --git a/backend/Machabstr.v b/backend/Machabstr.v
index 33ed93c..d83ffa5 100644
--- a/backend/Machabstr.v
+++ b/backend/Machabstr.v
@@ -88,6 +88,26 @@ Inductive set_slot: frame -> typ -> Z -> val -> frame -> Prop :=
 Definition init_frame (f: function) :=
   empty_block (- f.(fn_framesize)) 0.
 
+(** Extract the values of the arguments of an external call. *)
+
+Inductive extcall_arg: regset -> frame -> loc -> val -> Prop :=
+  | extcall_arg_reg: forall rs fr r,
+      extcall_arg rs fr (R r) (rs r)
+  | extcall_arg_stack: forall rs fr ofs ty v,
+      get_slot fr ty (Int.signed (Int.repr (4 * ofs))) v ->
+      extcall_arg rs fr (S (Outgoing ofs ty)) v.
+
+Inductive extcall_args: regset -> frame -> list loc -> list val -> Prop :=
+  | extcall_args_nil: forall rs fr,
+      extcall_args rs fr nil nil
+  | extcall_args_cons: forall rs fr l1 ll v1 vl,
+      extcall_arg rs fr l1 v1 -> extcall_args rs fr ll vl ->
+      extcall_args rs fr (l1 :: ll) (v1 :: vl).
+
+Definition extcall_arguments
+   (rs: regset) (fr: frame) (sg: signature) (args: list val) : Prop :=
+  extcall_args rs fr (Conventions.loc_arguments sg) args.
+    
 Section RELSEM.
 
 Variable ge: genv.
@@ -223,7 +243,7 @@ with exec_function:
   | exec_funct_external:
       forall ef parent args res rs1 rs2 m t,
       event_match ef args t res ->
-      args = rs1##(Conventions.loc_external_arguments ef.(ef_sig)) ->
+      extcall_arguments rs1 parent ef.(ef_sig) args ->
       rs2 = (rs1#(Conventions.loc_result ef.(ef_sig)) <- res) ->
       exec_function (External ef) parent rs1 m t rs2 m.
 
@@ -367,7 +387,7 @@ Lemma exec_mutual_induction:
           (res : val) (rs1 : mreg -> val) (rs2 : RegEq.t -> val) (m : mem)
           (t0 : trace),
         event_match ef args t0 res ->
-        args = rs1 ## (Conventions.loc_external_arguments (ef_sig ef)) ->
+        extcall_arguments rs1 parent ef.(ef_sig) args ->
         rs2 = rs1 # (Conventions.loc_result (ef_sig ef)) <- res ->
         P2 (External ef) parent rs1 m t0 rs2 m) ->
       (forall (f16 : function) (v : val) (f17 : frame) (c : code)
diff --git a/backend/Machabstr2mach.v b/backend/Machabstr2mach.v
index a07f64a..8a2b01d 100644
--- a/backend/Machabstr2mach.v
+++ b/backend/Machabstr2mach.v
@@ -906,6 +906,29 @@ Proof.
   constructor. exact A. constructor.
 Qed.
 
+(** Preservation of arguments to external functions. *)
+
+Lemma transl_extcall_arguments:
+  forall rs fr sg args stk base cs m ms,
+  Machabstr.extcall_arguments rs fr sg args ->
+  callstack_invariant ((fr, stk, base) :: cs) m ms ->
+  wt_frame fr ->
+  extcall_arguments rs ms (Vptr stk base) sg args.
+Proof.
+  unfold Machabstr.extcall_arguments, extcall_arguments; intros.
+  assert (forall locs vals,
+    Machabstr.extcall_args rs fr locs vals ->
+    extcall_args rs ms (Vptr stk base) locs vals).
+  induction locs; intros; inversion H2; subst; clear H2.
+  constructor.
+  constructor; auto.
+  inversion H7; subst; clear H7. 
+  constructor.
+  constructor. eapply callstack_get_slot; eauto. 
+  eapply wt_get_slot; eauto. 
+  auto.
+Qed.
+
 (** * The proof of simulation *)
 
 Section SIMULATION.
@@ -1132,7 +1155,9 @@ Proof.
   auto.
 
   (* external function *)
-  exists ms; split. econstructor; eauto. auto.
+  exists ms; split. econstructor; eauto. 
+  eapply transl_extcall_arguments; eauto.
+  auto.
 Qed.  
 
 End SIMULATION.
diff --git a/backend/Machtyping.v b/backend/Machtyping.v
index 24f0ddb..ad3ee88 100644
--- a/backend/Machtyping.v
+++ b/backend/Machtyping.v
@@ -83,7 +83,6 @@ Record wt_function (f: function) : Prop := mk_wt_function {
 
 Inductive wt_fundef: fundef -> Prop :=
   | wt_fundef_external: forall ef,
-      Conventions.sig_external_ok ef.(ef_sig) ->
       wt_fundef (External ef)
   | wt_function_internal: forall f,
       wt_function f ->
diff --git a/backend/PPC.v b/backend/PPC.v
index 3aa4ec4..ba645d0 100644
--- a/backend/PPC.v
+++ b/backend/PPC.v
@@ -756,32 +756,34 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
     the calling conventions in module [Conventions], except that
     we use PPC registers instead of locations. *)
 
-Fixpoint loc_external_arguments_rec
-    (tyl: list typ) (iregl: list ireg) (fregl: list freg)
-    {struct tyl} : list preg :=
-  match tyl with
-  | nil => nil
-  | Tint :: tys =>
-      match iregl with
-      | nil => IR GPR11 (* should not happen *)
-      | ireg :: _ => IR ireg
-      end ::
-      loc_external_arguments_rec tys (list_drop1 iregl) fregl
-  | Tfloat :: tys =>
-      match fregl with
-      | nil => IR GPR11 (* should not happen *)
-      | freg :: _ => FR freg
-      end ::
-      loc_external_arguments_rec tys (list_drop2 iregl) (list_drop1 fregl)
-  end.
-
-Definition int_param_regs :=
-  GPR3 :: GPR4 :: GPR5 :: GPR6 :: GPR7 :: GPR8 :: GPR9 :: GPR10 :: nil.
-Definition float_param_regs :=
-  FPR1 :: FPR2 :: FPR3 :: FPR4 :: FPR5 :: FPR6 :: FPR7 :: FPR8 :: FPR9 :: FPR10 :: nil.
-
-Definition loc_external_arguments (s: signature) : list preg :=
-  loc_external_arguments_rec s.(sig_args) int_param_regs float_param_regs.
+Inductive extcall_args (rs: regset) (m: mem):
+      list typ -> list ireg -> list freg -> Z -> list val -> Prop :=
+  | extcall_args_nil: forall irl frl ofs,
+      extcall_args rs m nil irl frl ofs nil
+  | extcall_args_int_reg: forall tyl ir1 irl frl ofs v1 vl,
+      v1 = rs (IR ir1) ->
+      extcall_args rs m tyl irl frl (ofs + 4) vl ->
+      extcall_args rs m (Tint :: tyl) (ir1 :: irl) frl ofs (v1 :: vl)
+  | extcall_args_int_stack: forall tyl frl ofs v1 vl,
+      Mem.loadv Mint32 m (Val.add (rs (IR GPR1)) (Vint (Int.repr ofs))) = Some v1 ->
+      extcall_args rs m tyl nil frl (ofs + 4) vl ->
+      extcall_args rs m (Tint :: tyl) nil frl ofs (v1 :: vl)
+  | extcall_args_float_reg: forall tyl irl fr1 frl ofs v1 vl,
+      v1 = rs (FR fr1) ->
+      extcall_args rs m tyl (list_drop2 irl) frl (ofs + 8) vl ->
+      extcall_args rs m (Tfloat :: tyl) irl (fr1 :: frl) ofs (v1 :: vl)
+  | extcall_args_float_stack: forall tyl irl ofs v1 vl,
+      Mem.loadv Mfloat64 m (Val.add (rs (IR GPR1)) (Vint (Int.repr ofs))) = Some v1 ->
+      extcall_args rs m tyl (list_drop2 irl) nil (ofs + 8) vl ->
+      extcall_args rs m (Tfloat :: tyl) irl nil ofs (v1 :: vl).
+
+Definition extcall_arguments
+    (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop :=
+  extcall_args rs m
+    sg.(sig_args)
+    (GPR3 :: GPR4 :: GPR5 :: GPR6 :: GPR7 :: GPR8 :: GPR9 :: GPR10 :: nil)
+    (FPR1 :: FPR2 :: FPR3 :: FPR4 :: FPR5 :: FPR6 :: FPR7 :: FPR8 :: FPR9 :: FPR10 :: nil)
+    24 args.
 
 Definition loc_external_result (s: signature) : preg :=
   match s.(sig_res) with
@@ -805,7 +807,7 @@ Inductive exec_step: regset -> mem -> trace -> regset -> mem -> Prop :=
       rs PC = Vptr b Int.zero ->
       Genv.find_funct_ptr ge b = Some (External ef) ->
       event_match ef args t res ->
-      args = List.map (fun r => rs#r) (loc_external_arguments ef.(ef_sig)) ->
+      extcall_arguments rs m ef.(ef_sig) args ->
       rs' = (rs#(loc_external_result ef.(ef_sig)) <- res
                #PC <- (rs LR)) ->
       exec_step rs m t rs' m.
diff --git a/backend/PPCgenproof.v b/backend/PPCgenproof.v
index 9cbbc65..f1ee9f2 100644
--- a/backend/PPCgenproof.v
+++ b/backend/PPCgenproof.v
@@ -1185,7 +1185,7 @@ Lemma exec_function_external_prop:
          (res : val) (ms1 ms2: Mach.regset) (m : mem)
          (t : trace),
   event_match ef args t res ->
-  args = ms1 ## (Conventions.loc_external_arguments (ef_sig ef)) ->
+  Mach.extcall_arguments ms1 m parent ef.(ef_sig) args ->
   ms2 = Regmap.set (Conventions.loc_result (ef_sig ef)) res ms1 ->
   exec_function_prop (External ef) parent ms1 m t ms2 m.
 Proof.
@@ -1197,10 +1197,8 @@ Proof.
   split. apply exec_one. eapply exec_step_external; eauto.
   destruct (functions_translated _ _ AT) as [tf [A B]].
   simpl in B. congruence.
-  rewrite H0. rewrite loc_external_arguments_match. 
-  rewrite list_map_compose. apply list_map_exten; intros.
-  symmetry; eapply preg_val; eauto. 
-  reflexivity.
+  eapply extcall_arguments_match; eauto.
+  reflexivity. 
 Qed.
 
 (** We then conclude by induction on the structure of the Mach
diff --git a/backend/PPCgenproof1.v b/backend/PPCgenproof1.v
index 4a9ac94..f9af3c3 100644
--- a/backend/PPCgenproof1.v
+++ b/backend/PPCgenproof1.v
@@ -442,40 +442,54 @@ Proof.
   destruct sres. destruct t; reflexivity. reflexivity.
 Qed.
 
-Remark list_map_drop1:
-  forall (A B: Set) (f: A -> B) (l: list A), list_drop1 (map f l) = map f (list_drop1 l).
-Proof.
-  intros; destruct l; reflexivity.
-Qed.
-
-Remark list_map_drop2:
-  forall (A B: Set) (f: A -> B) (l: list A), list_drop2 (map f l) = map f (list_drop2 l).
-Proof.
-  intros; destruct l. reflexivity. destruct l; reflexivity.
-Qed.
-
-Lemma loc_external_arguments_rec_match:
-  forall tyl iregl fregl ofs,
+Lemma extcall_args_match:
+  forall ms m sp rs,
+  agree ms sp rs ->
+  forall tyl iregl fregl ofs args,
   (forall r, In r iregl -> mreg_type r = Tint) ->
   (forall r, In r fregl -> mreg_type r = Tfloat) ->
-  PPC.loc_external_arguments_rec tyl (map ireg_of iregl) (map freg_of fregl) =
-  List.map
-    (fun l => preg_of (match l with R r => r | S _ => IT1 end))
-    (Conventions.loc_arguments_rec tyl iregl fregl ofs).
-Proof.
-  induction tyl; intros; simpl.
-  auto.
-  destruct a; simpl; apply (f_equal2 (@cons preg)). 
-  destruct iregl; simpl. 
-  reflexivity. unfold preg_of; rewrite (H m); auto with coqlib.
-  rewrite list_map_drop1. apply IHtyl. 
-  intros; apply H; apply list_drop1_incl; auto. 
-  assumption.
-  destruct fregl; simpl. 
-  reflexivity. unfold preg_of; rewrite (H0 m); auto with coqlib.
-  rewrite list_map_drop1. rewrite list_map_drop2. apply IHtyl. 
-  intros; apply H; apply list_drop2_incl; auto. 
-  intros; apply H0; apply list_drop1_incl; auto. 
+  Mach.extcall_args ms m sp (Conventions.loc_arguments_rec tyl iregl fregl ofs) args ->
+  PPC.extcall_args rs m tyl (List.map ireg_of iregl) (List.map freg_of fregl) (4 * ofs) args.
+Proof.
+  induction tyl; intros.
+  inversion H2; constructor.
+  destruct a. 
+  (* integer case *)
+  destruct iregl as [ | ir1 irl]. 
+  (* stack *)
+  inversion H2; subst; clear H2. inversion H8; subst; clear H8.
+  constructor. replace (rs GPR1) with sp. assumption. 
+  eapply sp_val; eauto. 
+  change (@nil ireg) with (ireg_of ## nil). 
+  replace (4 * ofs + 4) with (4 * (ofs + 1)) by omega. 
+  apply IHtyl; auto. 
+  (* register *)
+  inversion H2; subst; clear H2. inversion H8; subst; clear H8.
+  simpl map. econstructor. eapply ireg_val; eauto.
+  apply H0; simpl; auto. 
+  replace (4 * ofs + 4) with (4 * (ofs + 1)) by omega. 
+  apply IHtyl; auto. 
+  intros; apply H0; simpl; auto.
+  (* float case *)
+  destruct fregl as [ | fr1 frl]. 
+  (* stack *)
+  inversion H2; subst; clear H2. inversion H8; subst; clear H8.
+  constructor. replace (rs GPR1) with sp. assumption. 
+  eapply sp_val; eauto. 
+  change (@nil freg) with (freg_of ## nil). 
+  replace (4 * ofs + 8) with (4 * (ofs + 2)) by omega. 
+  rewrite list_map_drop2. 
+  apply IHtyl; auto. 
+  intros. apply H0. apply list_drop2_incl. auto. 
+  (* register *)
+  inversion H2; subst; clear H2. inversion H8; subst; clear H8.
+  simpl map. econstructor. eapply freg_val; eauto.
+  apply H1; simpl; auto. 
+  replace (4 * ofs + 8) with (4 * (ofs + 2)) by omega. 
+  rewrite list_map_drop2.
+  apply IHtyl; auto. 
+  intros; apply H0. apply list_drop2_incl. auto.
+  intros; apply H1; simpl; auto.
 Qed.
 
 Ltac ElimOrEq :=
@@ -488,14 +502,17 @@ Ltac ElimOrEq :=
        let H := fresh in (intro H; contradiction)
   end.
 
-Lemma loc_external_arguments_match:
-  forall sg,
-  PPC.loc_external_arguments sg = List.map preg_of (Conventions.loc_external_arguments sg).
-Proof.
-  intros. destruct sg as [sgargs sgres]; unfold loc_external_arguments, Conventions.loc_external_arguments.
-  rewrite list_map_compose. unfold Conventions.loc_arguments.
-  rewrite <- loc_external_arguments_rec_match.
-  reflexivity.
+Lemma extcall_arguments_match:
+  forall ms m sp rs sg args,
+  agree ms sp rs ->
+  Mach.extcall_arguments ms m sp sg args ->
+  PPC.extcall_arguments rs m sg args.
+Proof.
+  unfold Mach.extcall_arguments, PPC.extcall_arguments; intros.
+  change (extcall_args rs m sg.(sig_args)
+    (List.map ireg_of Conventions.int_param_regs)
+    (List.map freg_of Conventions.float_param_regs) (4 * 6) args).
+  eapply extcall_args_match; eauto. 
   intro; simpl; ElimOrEq; reflexivity.  
   intro; simpl; ElimOrEq; reflexivity.  
 Qed.
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 449e837..97d063a 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -105,7 +105,6 @@ Record wt_function (f: function) (env: regenv): Prop :=
 
 Inductive wt_fundef: fundef -> Prop :=
   | wt_fundef_external: forall ef,
-      Conventions.sig_external_ok ef.(ef_sig) ->
       wt_fundef (External ef)
   | wt_function_internal: forall f env,
       wt_function f env ->
@@ -300,11 +299,6 @@ Definition type_function (f: function): option regenv :=
       then Some env else None
   end.
 
-Definition type_external_function (ef: external_function): bool :=
-  List.fold_right
-    (fun l b => match l with Locations.S _ => false | Locations.R _ => b end)
-    true (Conventions.loc_arguments ef.(ef_sig)).
-
 Lemma type_function_correct:
   forall f env,
   type_function f = Some env ->
@@ -327,19 +321,6 @@ Proof.
   congruence.
 Qed.
 
-Lemma type_external_function_correct:
-  forall ef,
-  type_external_function ef = true ->
-  Conventions.sig_external_ok ef.(ef_sig).
-Proof.
-  intro ef. unfold type_external_function, Conventions.sig_external_ok.
-  generalize (Conventions.loc_arguments (ef_sig ef)).
-  induction l; simpl.
-  tauto.
-  destruct a. intros. firstorder congruence.
-  congruence.
-Qed.
-
 (** * Type preservation during evaluation *)
 
 (** The type system for RTL is not sound in that it does not guarantee
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 69a7e99..3bc4339 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -1272,6 +1272,50 @@ Proof.
   apply shift_offset_sp; auto.
 Qed.
 
+(** Preservation of the arguments to an external call. *)
+
+Section EXTERNAL_ARGUMENTS.
+
+Variable ls: locset.
+Variable fr: frame.
+Variable rs: regset.
+Variable sg: signature.
+Hypothesis AG1: forall r, rs r = ls (R r).
+Hypothesis AG2: forall (ofs : Z) (ty : typ),
+      6 <= ofs ->
+      ofs + typesize ty <= size_arguments sg ->
+      get_slot fr ty (Int.signed (Int.repr (4 * ofs)))
+                     (ls (S (Outgoing ofs ty))).
+
+Lemma transl_external_arguments_rec:
+  forall locs,
+  (forall l, In l locs -> loc_argument_acceptable l) ->
+  (forall ofs ty, In (S (Outgoing ofs ty)) locs ->
+                  ofs + typesize ty <= size_arguments sg) ->
+  extcall_args rs fr locs ls##locs.
+Proof.
+  induction locs; simpl; intros.
+  constructor.
+  constructor. 
+  assert (loc_argument_acceptable a). apply H; auto.
+  destruct a; red in H1.
+  rewrite <- AG1. constructor. 
+  destruct s; try contradiction.
+  constructor. apply AG2. omega. apply H0. auto.
+  apply IHlocs; auto.
+Qed.
+
+Lemma transl_external_arguments:
+  extcall_arguments rs fr sg (ls ## (loc_arguments sg)).
+Proof.
+  unfold extcall_arguments. 
+  apply transl_external_arguments_rec. 
+  exact (Conventions.loc_arguments_acceptable sg).
+  exact (Conventions.loc_arguments_bounded sg).
+Qed.
+
+End EXTERNAL_ARGUMENTS.
+
 (** The proof of semantic preservation relies on simulation diagrams
   of the following form:
 <<
@@ -1594,8 +1638,7 @@ Proof.
   inversion WTF. subst ef0. set (sg := ef_sig ef) in *.
   exists (rs#(loc_result sg) <- res). 
   split. econstructor. eauto. 
-  fold sg. rewrite H0. rewrite Conventions.loc_external_arguments_loc_arguments; auto.
-  rewrite list_map_compose. apply list_map_exten; intros. auto. 
+  fold sg. rewrite H0. apply transl_external_arguments; assumption.
   reflexivity.
   split; intros. rewrite H1. 
   unfold Regmap.set. case (RegEq.eq r (loc_result sg)); intro.
diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v
index 996ada4..beb28e2 100644
--- a/backend/Stackingtyping.v
+++ b/backend/Stackingtyping.v
@@ -217,7 +217,7 @@ Lemma wt_transf_fundef:
   wt_fundef tf.
 Proof.
   intros f tf WT. inversion WT; subst.
-  simpl; intros; inversion H0. constructor; auto.
+  simpl; intros; inversion H. constructor.
   unfold transf_fundef, transf_partial_fundef.
   caseEq (transf_function f0); try congruence.
   intros tfn TRANSF EQ. inversion EQ; subst tf.
-- 
cgit v1.2.3