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

1 files changed, 45 insertions, 2 deletions

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.