From cab28a5331400fee1a0dd1c5fa7d0366fa888f5f Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 27 Jul 2008 07:34:38 +0000 Subject: MAJ documentation git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@702 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Reloadproof.v | 260 +++++++++++--------------------------------------- 1 file changed, 57 insertions(+), 203 deletions(-) (limited to 'backend/Reloadproof.v') diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index 372a261b..3177eaf4 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -410,8 +410,19 @@ End LINEAR_CONSTRUCTORS. (** * Agreement between values of locations *) (** The predicate [agree] states that two location maps - give the same values to all acceptable locations, - that is, non-temporary registers and [Local] stack slots. *) + give compatible values to all acceptable locations, + that is, non-temporary registers and [Local] stack slots. + The notion of compatibility used is the [Val.lessdef] ordering, + which enables a [Vundef] value in the original program to be refined + into any value in the transformed program. + + A typical situation where this refinement of values occurs is at + function entry point. In LTLin, all registers except those + belonging to the function parameters are set to [Vundef]. In + Linear, these registers have whatever value they had in the caller + function. This difference is harmless: if the original LTLin code + does not get stuck, we know that it does not use any of these + [Vundef] values. *) Definition agree (rs1 rs2: locset) : Prop := forall l, loc_acceptable l -> Val.lessdef (rs1 l) (rs2 l). @@ -425,7 +436,8 @@ Qed. Lemma agree_locs: forall rs1 rs2 ll, - agree rs1 rs2 -> locs_acceptable ll -> Val.lessdef_list (map rs1 ll) (map rs2 ll). + agree rs1 rs2 -> locs_acceptable ll -> + Val.lessdef_list (map rs1 ll) (map rs2 ll). Proof. induction ll; simpl; intros. constructor. @@ -458,175 +470,6 @@ Proof. apply temporaries_not_acceptable; auto. Qed. -(***** -Lemma agree_return_regs: - forall rs1 ls1 rs2 ls2, - agree rs1 ls1 -> agree rs2 ls2 -> - agree (LTL.return_regs rs1 rs2) (LTL.return_regs ls1 ls2). -Proof. - intros; red; intros. unfold LTL.return_regs. - assert (~In l temporaries). - apply Loc.notin_not_in. apply temporaries_not_acceptable; auto. - destruct l. - destruct (In_dec Loc.eq (R m) temporaries). contradiction. - destruct (In_dec Loc.eq (R m) destroyed_at_call); auto. - auto. -Qed. - -Lemma agree_set_result: - forall rs1 ls1 rs2 ls2 sig res ls3, - loc_acceptable res -> agree rs1 ls1 -> agree rs2 ls2 -> - ls3 res = LTL.return_regs ls1 ls2 (R (loc_result sig)) -> - (forall l : loc, Loc.diff res l -> ls3 l = LTL.return_regs ls1 ls2 l) -> - let rs_merge := LTL.return_regs rs1 rs2 in - agree (Locmap.set res (rs_merge (R (loc_result sig))) rs_merge) ls3. -Proof. - intros. apply agree_set with (LTL.return_regs ls1 ls2); auto. - rewrite H2; unfold rs_merge. - repeat rewrite return_regs_result. apply H1. apply loc_result_acceptable. - unfold rs_merge. apply agree_return_regs; auto. -Qed. - -(** [agree_arguments] and [agree_parameters] are two stronger - variants of the predicate [agree]. They additionally demand - equality of the values of locations that are arguments or parameters - (respectively) for a call to a function of signature [sg]. *) - -Definition agree_arguments (sg: signature) (rs1 rs2: locset) : Prop := - forall l, loc_acceptable l \/ In l (loc_arguments sg) -> rs2 l = rs1 l. - -Definition agree_parameters (sg: signature) (rs1 rs2: locset) : Prop := - forall l, loc_acceptable l \/ In l (loc_parameters sg) -> rs2 l = rs1 l. - -Remark parallel_assignment: - forall (P: loc -> Prop) (rs1 rs2 ls1 ls2: locset) srcs dsts, - map rs2 dsts = map rs1 srcs -> - map ls2 dsts = map ls1 srcs -> - (forall l, In l srcs -> P l) -> - (forall l, P l -> ls1 l = rs1 l) -> - (forall l, In l dsts -> ls2 l = rs2 l). -Proof. - induction srcs; destruct dsts; simpl; intros; try congruence. - contradiction. - inv H; inv H0. elim H3; intro. subst l0. - rewrite H5; rewrite H4. auto with coqlib. - eapply IHsrcs; eauto. -Qed. - -Lemma agree_set_arguments: - forall rs1 ls1 ls2 args sg, - agree rs1 ls1 -> - List.map Loc.type args = sg.(sig_args) -> - locs_acceptable args -> - List.map ls2 (loc_arguments sg) = map ls1 args -> - (forall l : loc, - Loc.notin l (loc_arguments sg) -> - Loc.notin l temporaries -> ls2 l = ls1 l) -> - agree_arguments sg (LTL.parmov args (loc_arguments sg) rs1) ls2. -Proof. - intros. - assert (Loc.norepet (loc_arguments sg)). - apply loc_arguments_norepet. - assert (List.length args = List.length (loc_arguments sg)). - rewrite loc_arguments_length. rewrite <- H0. - symmetry. apply list_length_map. - destruct (parmov_spec rs1 _ _ H4 H5) as [A B]. - set (rs2 := LTL.parmov args (loc_arguments sg) rs1) in *. - assert (forall l, In l (loc_arguments sg) -> ls2 l = rs2 l). - intros. - eapply parallel_assignment with (P := loc_acceptable); eauto. - red; intros. - destruct (In_dec Loc.eq l (loc_arguments sg)). - auto. - assert (loc_acceptable l) by tauto. - assert (Loc.notin l (loc_arguments sg)). - eapply loc_acceptable_notin_notin; eauto. - rewrite H3; auto. rewrite B; auto. - apply temporaries_not_acceptable; auto. -Qed. - -Lemma agree_arguments_agree: - forall sg rs ls, agree_arguments sg rs ls -> agree rs ls. -Proof. - intros; red; intros; auto. -Qed. - -Lemma agree_arguments_locs: - forall sg rs1 rs2, - agree_arguments sg rs1 rs2 -> - map rs2 (loc_arguments sg) = map rs1 (loc_arguments sg). -Proof. - intros. - assert (forall ll, incl ll (loc_arguments sg) -> map rs2 ll = map rs1 ll). - induction ll; simpl; intros. auto. - f_equal. apply H. right. apply H0. auto with coqlib. - apply IHll. eapply incl_cons_inv; eauto. - apply H0. apply incl_refl. -Qed. - -Lemma agree_set_parameters: - forall rs1 ls1 ls2 sg params, - agree_parameters sg rs1 ls1 -> - List.map Loc.type params = sg.(sig_args) -> - locs_acceptable params -> - Loc.norepet params -> - List.map ls2 params = List.map ls1 (loc_parameters sg) -> - (forall l : loc, - Loc.notin l params -> - Loc.notin l temporaries -> ls2 l = ls1 l) -> - agree (LTL.parmov (loc_parameters sg) params rs1) ls2. -Proof. - intros. - assert (List.length (loc_parameters sg) = List.length params). - unfold loc_parameters. rewrite list_length_map. - rewrite loc_arguments_length. rewrite <- H0. - apply list_length_map. - destruct (parmov_spec rs1 _ _ H2 H5) as [A B]. - set (rs2 := LTL.parmov (loc_parameters sg) params rs1) in *. - red; intros. - assert (forall l, In l params -> ls2 l = rs2 l). - intros. - eapply parallel_assignment with (P := fun l => In l (loc_parameters sg)); eauto. - destruct (In_dec Loc.eq l params). - auto. - assert (Loc.notin l params). - eapply loc_acceptable_notin_notin; eauto. - rewrite B; auto. rewrite H4; auto. - apply temporaries_not_acceptable; auto. -Qed. - -Lemma agree_call_regs: - forall sg rs ls, - agree_arguments sg rs ls -> - agree_parameters sg (LTL.call_regs rs) (LTL.call_regs ls). -Proof. - intros; red; intros. elim H0. - destruct l; simpl; auto. destruct s; auto. - unfold loc_parameters. intro. - destruct (list_in_map_inv _ _ _ H1) as [r [A B]]. - subst l. generalize (loc_arguments_acceptable _ _ B). - destruct r; simpl; auto. destruct s; simpl; auto. -Qed. - -Lemma agree_arguments_return_regs: - forall sg rs1 rs2 ls1 ls2, - tailcall_possible sg -> - agree rs1 ls1 -> - agree_arguments sg rs2 ls2 -> - agree_arguments sg (LTL.return_regs rs1 rs2) (LTL.return_regs ls1 ls2). -Proof. - intros; red; intros. generalize (H1 l H2). intro. - elim H2; intro. generalize (H0 l H4); intro. - unfold LTL.return_regs. destruct l; auto. - destruct (In_dec Loc.eq (R m) temporaries); auto. - destruct (In_dec Loc.eq (R m) destroyed_at_call); auto. - generalize (H l H4). unfold LTL.return_regs; destruct l; intro. - destruct (In_dec Loc.eq (R m) temporaries); auto. - destruct (In_dec Loc.eq (R m) destroyed_at_call); auto. - contradiction. -Qed. -**********) - Lemma agree_find_funct: forall (ge: Linear.genv) rs ls r f, Genv.find_funct ge (rs r) = Some f -> @@ -643,9 +486,9 @@ Qed. Lemma agree_postcall_1: forall rs ls, agree rs ls -> - agree (LTL.postcall_regs rs) ls. + agree (LTL.postcall_locs rs) ls. Proof. - intros; red; intros. unfold LTL.postcall_regs. + intros; red; intros. unfold LTL.postcall_locs. destruct l; auto. destruct (In_dec Loc.eq (R m) temporaries). constructor. destruct (In_dec Loc.eq (R m) destroyed_at_call). constructor. @@ -654,11 +497,13 @@ Qed. Lemma agree_postcall_2: forall rs ls ls', - agree (LTL.postcall_regs rs) ls -> - (forall l, loc_acceptable l -> ~In l destroyed_at_call -> ~In l temporaries -> ls' l = ls l) -> - agree (LTL.postcall_regs rs) ls'. + agree (LTL.postcall_locs rs) ls -> + (forall l, + loc_acceptable l -> ~In l destroyed_at_call -> ~In l temporaries -> + ls' l = ls l) -> + agree (LTL.postcall_locs rs) ls'. Proof. - intros; red; intros. generalize (H l H1). unfold LTL.postcall_regs. + intros; red; intros. generalize (H l H1). unfold LTL.postcall_locs. destruct l. destruct (In_dec Loc.eq (R m) temporaries). intro; constructor. destruct (In_dec Loc.eq (R m) destroyed_at_call). intro; constructor. @@ -671,8 +516,10 @@ Qed. Lemma agree_postcall_call: forall rs ls ls' sig, agree rs ls -> - (forall l, Loc.notin l (loc_arguments sig) -> Loc.notin l temporaries -> ls' l = ls l) -> - agree (LTL.postcall_regs rs) ls'. + (forall l, + Loc.notin l (loc_arguments sig) -> Loc.notin l temporaries -> + ls' l = ls l) -> + agree (LTL.postcall_locs rs) ls'. Proof. intros. apply agree_postcall_2 with ls. apply agree_postcall_1; auto. intros. apply H0. @@ -686,7 +533,7 @@ Lemma agree_postcall_alloc: forall rs ls ls2 v, agree rs ls -> (forall l, Loc.diff (R loc_alloc_argument) l -> ls2 l = ls l) -> - agree (LTL.postcall_regs rs) (Locmap.set (R loc_alloc_result) v ls2). + agree (LTL.postcall_locs rs) (Locmap.set (R loc_alloc_result) v ls2). Proof. intros. apply agree_postcall_2 with ls. apply agree_postcall_1; auto. intros. destruct (Loc.eq l (R loc_alloc_result)). @@ -713,8 +560,7 @@ Qed. Lemma call_regs_parameters: forall ls sig, - map (call_regs ls) (loc_parameters sig) = - map ls (loc_arguments sig). + map (call_regs ls) (loc_parameters sig) = map ls (loc_arguments sig). Proof. intros. unfold loc_parameters. rewrite list_map_compose. apply list_map_exten; intros. @@ -725,12 +571,24 @@ Proof. destruct s; intros; try contradiction. auto. Qed. +Lemma return_regs_preserve: + forall ls1 ls2 l, + ~ In l temporaries -> + ~ In l destroyed_at_call -> + return_regs ls1 ls2 l = ls1 l. +Proof. + intros. unfold return_regs. destruct l; auto. + destruct (In_dec Loc.eq (R m) temporaries). contradiction. + destruct (In_dec Loc.eq (R m) destroyed_at_call). contradiction. + auto. +Qed. + Lemma return_regs_arguments: forall ls1 ls2 sig, tailcall_possible sig -> map (return_regs ls1 ls2) (loc_arguments sig) = map ls2 (loc_arguments sig). Proof. - intros. symmetry. apply list_map_exten; intros. + intros. apply list_map_exten; intros. unfold return_regs. generalize (H x H0). destruct x; intros. destruct (In_dec Loc.eq (R m) temporaries). auto. destruct (In_dec Loc.eq (R m) destroyed_at_call). auto. @@ -748,18 +606,6 @@ Proof. elim n0. apply loc_result_caller_save. Qed. -Lemma return_regs_preserve: - forall ls1 ls2 l, - ~ In l temporaries -> - ~ In l destroyed_at_call -> - return_regs ls1 ls2 l = ls1 l. -Proof. - intros. unfold return_regs. destruct l; auto. - destruct (In_dec Loc.eq (R m) temporaries). contradiction. - destruct (In_dec Loc.eq (R m) destroyed_at_call). contradiction. - auto. -Qed. - (** * Preservation of labels and gotos *) Lemma find_label_add_spill: @@ -899,13 +745,22 @@ Qed. it enforces are: - Agreement between the values of locations in the two programs, according to the [agree] or [agree_arguments] predicates. +- Agreement between the memory states of the two programs, + according to the [Mem.lessdef] predicate. - Lists of LTLin instructions appearing in the source state are always suffixes of the code for the corresponding functions. - Well-typedness of the source code, which ensures that only acceptable locations are accessed by this code. +- Agreement over return types during calls: the return type of a function + is always equal to the return type of the signature of the corresponding + call. This invariant is necessary since the conventional location + used for passing return values depend on the return type. This invariant + is enforced through the third parameter of the [match_stackframes] + predicate, which is the signature of the called function. *) -Inductive match_stackframes: list LTLin.stackframe -> list Linear.stackframe -> signature -> Prop := +Inductive match_stackframes: + list LTLin.stackframe -> list Linear.stackframe -> signature -> Prop := | match_stackframes_nil: forall sig, sig.(sig_res) = Some Tint -> @@ -914,13 +769,14 @@ Inductive match_stackframes: list LTLin.stackframe -> list Linear.stackframe -> forall res f sp c rs s s' c' ls sig, match_stackframes s s' (LTLin.fn_sig f) -> c' = add_spill (loc_result sig) res (transf_code f c) -> - agree (LTL.postcall_regs rs) ls -> + agree (LTL.postcall_locs rs) ls -> loc_acceptable res -> wt_function f -> is_tail c (LTLin.fn_code f) -> - match_stackframes (LTLin.Stackframe res f sp (LTL.postcall_regs rs) c :: s) - (Linear.Stackframe (transf_function f) sp ls c' :: s') - sig. + match_stackframes + (LTLin.Stackframe res f sp (LTL.postcall_locs rs) c :: s) + (Linear.Stackframe (transf_function f) sp ls c' :: s') + sig. Inductive match_states: LTLin.state -> Linear.state -> Prop := | match_states_intro: @@ -992,8 +848,6 @@ Definition measure (st: LTLin.state) : nat := | LTLin.Returnstate s ls m => 0%nat end. -Axiom ADMITTED: forall (P: Prop), P. - Theorem transf_step_correct: forall s1 t s2, LTLin.step ge s1 t s2 -> forall s1' (MS: match_states s1 s1'), -- cgit