From 210352d90e5972aabfb253f7c8a38349f53917b3 Mon Sep 17 00:00:00 2001 From: xleroy 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/Stackingproof.v | 47 +++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 45 insertions(+), 2 deletions(-) (limited to 'backend/Stackingproof.v') 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. -- cgit v1.2.3