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 +-
 caml/Cil2Csyntax.ml      | 15 --------
 extraction/.depend       | 25 ++++++++-----
 lib/Coqlib.v             | 44 +++++++++++++++++++++-
 19 files changed, 267 insertions(+), 167 deletions(-)

diff --git a/backend/Allocation.v b/backend/Allocation.v
index 66c7a3c1..c66d6b08 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 07c0f58b..0b252d56 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 e4f9f964..4c4c4f76 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 5b4222df..d621e7c0 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 34508140..187c5cb8 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 3a0ee131..cbe18311 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 b8bf1e36..f61620d1 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 33ed93ca..d83ffa51 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 a07f64af..8a2b01dd 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 24f0ddb6..ad3ee886 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 3aa4ec4f..ba645d02 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 9cbbc659..f1ee9f22 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 4a9ac948..f9af3c30 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 449e837a..97d063ac 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 69a7e99f..3bc4339b 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 996ada4c..beb28e29 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.
diff --git a/caml/Cil2Csyntax.ml b/caml/Cil2Csyntax.ml
index 4012cd15..c41ddeb9 100644
--- a/caml/Cil2Csyntax.ml
+++ b/caml/Cil2Csyntax.ml
@@ -160,17 +160,6 @@ let globals_for_strings globs =
     (fun s id l -> CList.Coq_cons(global_for_string s id, l))
     stringTable globs
 
-(** Checking restrictions on external functions *)
-
-let acceptableExtFun targs =
-  let rec acceptable nint nfloat = function
-  | Tnil -> true
-  | Tcons(Tfloat _, rem) ->
-      nfloat > 0 && acceptable (nint - 2) (nfloat - 1) rem 
-  | Tcons(_, rem) ->
-      nint > 0 && acceptable (nint - 1) nfloat rem
-  in acceptable 8 10 targs
-
 (** ** Handling of stubs for variadic functions *)
 
 let stub_function_table = Hashtbl.create 47
@@ -185,8 +174,6 @@ let register_stub_function name tres targs =
   try
     (stub_name, Hashtbl.find stub_function_table stub_name)
   with Not_found ->
-    if not (acceptableExtFun targs) then
-      warning (name ^ ": too many parameters for a variadic function, will fail during Cminor -> PPC translation");
     let rec types_of_types = function
       | Tnil -> Tnil
       | Tcons(Tfloat _, tl) -> Tcons(Tfloat F64, types_of_types tl)
@@ -864,8 +851,6 @@ let convertExtFun v =
   updateLoc(v.vdecl);
   match convertTyp v.vtype with
   | Tfunction(args, res) ->
-      if not (acceptableExtFun args) then
-        warning (v.vname ^ ": too many parameters for an external function, will fail during Cminor -> PPC translation");
       let id = intern_string v.vname in
       Datatypes.Coq_pair (id, External(id, args, res))
   | _ ->
diff --git a/extraction/.depend b/extraction/.depend
index 9e201baf..f320d0dd 100644
--- a/extraction/.depend
+++ b/extraction/.depend
@@ -40,10 +40,6 @@
 ../caml/Main2.cmx: ../caml/PrintPPC.cmx ../caml/PrintCsyntax.cmx Main.cmx \
     Datatypes.cmx Csyntax.cmx ../caml/Cil2Csyntax.cmx ../caml/CMtypecheck.cmx \
     ../caml/CMparser.cmx ../caml/CMlexer.cmx 
-../caml/PrintCshm.cmo: Integers.cmi Datatypes.cmi Csharpminor.cmi \
-    ../caml/Camlcoq.cmo CList.cmi AST.cmi 
-../caml/PrintCshm.cmx: Integers.cmx Datatypes.cmx Csharpminor.cmx \
-    ../caml/Camlcoq.cmx CList.cmx AST.cmx 
 ../caml/PrintCsyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \
     CList.cmi AST.cmi 
 ../caml/PrintCsyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \
@@ -99,6 +95,7 @@ Ctyping.cmi: Specif.cmi Maps.cmi Datatypes.cmi Csyntax.cmi Coqlib.cmi \
 Floats.cmi: Specif.cmi Integers.cmi Datatypes.cmi 
 FSetAVL.cmi: Wf.cmi Specif.cmi Peano.cmi OrderedType.cmi Int.cmi \
     Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi 
+FSetBridge.cmi: Specif.cmi FSetInterface.cmi Datatypes.cmi CList.cmi 
 FSetFacts.cmi: Specif.cmi setoid.cmi FSetInterface.cmi Datatypes.cmi 
 FSetInterface.cmi: Specif.cmi OrderedType.cmi Datatypes.cmi CList.cmi 
 FSetList.cmi: Specif.cmi OrderedType.cmi Datatypes.cmi CList.cmi 
@@ -154,8 +151,8 @@ RTLgen.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Integers.cmi \
     Datatypes.cmi Coqlib.cmi Cminor.cmi CList.cmi BinPos.cmi AST.cmi 
 RTL.cmi: Values.cmi Registers.cmi Op.cmi Maps.cmi Integers.cmi Globalenvs.cmi \
     Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi 
-RTLtyping.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Locations.cmi \
-    Datatypes.cmi Coqlib.cmi Conventions.cmi CList.cmi AST.cmi 
+RTLtyping.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Datatypes.cmi \
+    Coqlib.cmi CList.cmi AST.cmi 
 setoid.cmi: Datatypes.cmi 
 Sets.cmi: Specif.cmi Maps.cmi Datatypes.cmi CList.cmi 
 Specif.cmi: Datatypes.cmi 
@@ -164,6 +161,7 @@ Stacking.cmi: Specif.cmi Op.cmi Mach.cmi Locations.cmi Lineartyping.cmi \
     CList.cmi BinPos.cmi BinInt.cmi AST.cmi 
 Sumbool.cmi: Specif.cmi Datatypes.cmi 
 Tunneling.cmi: Maps.cmi LTL.cmi Datatypes.cmi AST.cmi 
+union_find.cmi: Wf.cmi Specif.cmi Datatypes.cmi 
 Values.cmi: Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi \
     BinPos.cmi BinInt.cmi AST.cmi 
 ZArith_dec.cmi: Sumbool.cmi Specif.cmi Datatypes.cmi BinInt.cmi 
@@ -173,6 +171,7 @@ Zdiv.cmi: Zbool.cmi ZArith_dec.cmi Specif.cmi Datatypes.cmi BinPos.cmi \
     BinInt.cmi 
 Zeven.cmi: Specif.cmi Datatypes.cmi BinPos.cmi BinInt.cmi 
 Zmax.cmi: Datatypes.cmi BinInt.cmi 
+Zmin.cmi: Datatypes.cmi BinInt.cmi 
 Zmisc.cmi: Datatypes.cmi BinPos.cmi BinInt.cmi 
 Zpower.cmi: Zmisc.cmi Datatypes.cmi BinPos.cmi BinInt.cmi 
 Allocation.cmo: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi \
@@ -267,6 +266,10 @@ FSetAVL.cmo: Wf.cmi Specif.cmi Peano.cmi OrderedType.cmi Int.cmi FSetList.cmi \
     Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi FSetAVL.cmi 
 FSetAVL.cmx: Wf.cmx Specif.cmx Peano.cmx OrderedType.cmx Int.cmx FSetList.cmx \
     Datatypes.cmx CList.cmx BinPos.cmx BinInt.cmx FSetAVL.cmi 
+FSetBridge.cmo: Specif.cmi FSetInterface.cmi Datatypes.cmi CList.cmi \
+    FSetBridge.cmi 
+FSetBridge.cmx: Specif.cmx FSetInterface.cmx Datatypes.cmx CList.cmx \
+    FSetBridge.cmi 
 FSetFacts.cmo: Specif.cmi setoid.cmi OrderedType.cmi FSetInterface.cmi \
     Datatypes.cmi FSetFacts.cmi 
 FSetFacts.cmx: Specif.cmx setoid.cmx OrderedType.cmx FSetInterface.cmx \
@@ -400,11 +403,9 @@ RTL.cmo: Values.cmi Registers.cmi Op.cmi Maps.cmi Integers.cmi Globalenvs.cmi \
 RTL.cmx: Values.cmx Registers.cmx Op.cmx Maps.cmx Integers.cmx Globalenvs.cmx \
     Datatypes.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx RTL.cmi 
 RTLtyping.cmo: Specif.cmi Registers.cmi ../caml/RTLtypingaux.cmo RTL.cmi \
-    Op.cmi Maps.cmi Locations.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \
-    CList.cmi AST.cmi RTLtyping.cmi 
+    Op.cmi Maps.cmi Datatypes.cmi Coqlib.cmi CList.cmi AST.cmi RTLtyping.cmi 
 RTLtyping.cmx: Specif.cmx Registers.cmx ../caml/RTLtypingaux.cmx RTL.cmx \
-    Op.cmx Maps.cmx Locations.cmx Datatypes.cmx Coqlib.cmx Conventions.cmx \
-    CList.cmx AST.cmx RTLtyping.cmi 
+    Op.cmx Maps.cmx Datatypes.cmx Coqlib.cmx CList.cmx AST.cmx RTLtyping.cmi 
 setoid.cmo: Datatypes.cmi setoid.cmi 
 setoid.cmx: Datatypes.cmx setoid.cmi 
 Sets.cmo: Specif.cmi Maps.cmi Datatypes.cmi CList.cmi Sets.cmi 
@@ -421,6 +422,8 @@ Sumbool.cmo: Specif.cmi Datatypes.cmi Sumbool.cmi
 Sumbool.cmx: Specif.cmx Datatypes.cmx Sumbool.cmi 
 Tunneling.cmo: Maps.cmi LTL.cmi Datatypes.cmi AST.cmi Tunneling.cmi 
 Tunneling.cmx: Maps.cmx LTL.cmx Datatypes.cmx AST.cmx Tunneling.cmi 
+union_find.cmo: Wf.cmi Specif.cmi Datatypes.cmi union_find.cmi 
+union_find.cmx: Wf.cmx Specif.cmx Datatypes.cmx union_find.cmi 
 Values.cmo: Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi \
     BinPos.cmi BinInt.cmi AST.cmi Values.cmi 
 Values.cmx: Specif.cmx Integers.cmx Floats.cmx Datatypes.cmx Coqlib.cmx \
@@ -443,6 +446,8 @@ Zeven.cmo: Specif.cmi Datatypes.cmi BinPos.cmi BinInt.cmi Zeven.cmi
 Zeven.cmx: Specif.cmx Datatypes.cmx BinPos.cmx BinInt.cmx Zeven.cmi 
 Zmax.cmo: Datatypes.cmi BinInt.cmi Zmax.cmi 
 Zmax.cmx: Datatypes.cmx BinInt.cmx Zmax.cmi 
+Zmin.cmo: Datatypes.cmi BinInt.cmi Zmin.cmi 
+Zmin.cmx: Datatypes.cmx BinInt.cmx Zmin.cmi 
 Zmisc.cmo: Datatypes.cmi BinPos.cmi BinInt.cmi Zmisc.cmi 
 Zmisc.cmx: Datatypes.cmx BinPos.cmx BinInt.cmx Zmisc.cmi 
 Zpower.cmo: Zmisc.cmi Datatypes.cmi BinPos.cmi BinInt.cmi Zpower.cmi 
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 3bcc8a69..b5d59b86 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -637,6 +637,21 @@ Proof.
   apply sym_not_equal. apply H; auto.
 Qed.
 
+Lemma list_disjoint_dec:
+  forall (A: Set) (eqA_dec: forall (x y: A), {x=y} + {x<>y}) (l1 l2: list A),
+  {list_disjoint l1 l2} + {~list_disjoint l1 l2}.
+Proof.
+  induction l1; intros.
+  left; red; intros. elim H.
+  case (In_dec eqA_dec a l2); intro.
+  right; red; intro. apply (H a a); auto with coqlib. 
+  case (IHl1 l2); intro.
+  left; red; intros. elim H; intro. 
+    red; intro; subst a y. contradiction.
+    apply l; auto.
+  right; red; intros. elim n0. eapply list_disjoint_cons_left; eauto.
+Defined.
+
 (** [list_norepet l] holds iff the list [l] contains no repetitions,
   i.e. no element occurs twice. *)
 
@@ -658,7 +673,7 @@ Proof.
   right. red; intro. inversion H. contradiction. 
   left. constructor; auto.
   right. red; intro. inversion H. contradiction.
-Qed.
+Defined.
 
 Lemma list_map_norepet:
   forall (A B: Set) (f: A -> B) (l: list A),
@@ -803,3 +818,30 @@ Proof.
   destruct l; simpl. constructor. inversion H. inversion H3. auto.
 Qed.
 
+Lemma 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.
+
+Lemma 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.
+
+(** * Definitions and theorems over boolean types *)
+
+Definition proj_sumbool (P Q: Prop) (a: {P} + {Q}) : bool :=
+  if a then true else false.
+
+Implicit Arguments proj_sumbool [P Q].
+
+Coercion proj_sumbool: sumbool >-> bool.
+
+Lemma proj_sumbool_true:
+  forall (P Q: Prop) (a: {P}+{Q}), proj_sumbool a = true -> P.
+Proof.
+  intros P Q a. destruct a; simpl. auto. congruence.
+Qed.
+
-- 
cgit