diff options
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Allocproof.v | 93 | ||||
| -rw-r--r-- | backend/LTL.v | 70 | ||||
| -rw-r--r-- | backend/LTLin.v | 12 | ||||
| -rw-r--r-- | backend/Linear.v | 34 | ||||
| -rw-r--r-- | backend/Reloadproof.v | 260 | ||||
| -rw-r--r-- | backend/Tunnelingproof.v | 2 |
6 files changed, 110 insertions, 361 deletions
diff --git a/backend/Allocproof.v b/backend/Allocproof.v index fd569ad..58ed3b6 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -35,92 +35,6 @@ Require Import Coloring. Require Import Coloringproof. Require Import Allocation. -(** * Semantic properties of calling conventions *) - -(************* -(** The value of a parameter in the called function is the same - as the value of the corresponding argument in the caller function. *) - -Lemma call_regs_param_of_arg: - forall sig ls l, - In l (loc_arguments sig) -> - LTL.call_regs ls (parameter_of_argument l) = ls l. -Proof. - intros. - generalize (loc_arguments_acceptable sig l H). - unfold LTL.call_regs; unfold parameter_of_argument. - unfold loc_argument_acceptable. - destruct l. auto. destruct s; tauto. -Qed. - -(** The return value, stored in the conventional return register, - is correctly passed from the callee back to the caller. *) - -Lemma return_regs_result: - forall sig caller callee, - LTL.return_regs caller callee (R (loc_result sig)) = - callee (R (loc_result sig)). -Proof. - intros. unfold LTL.return_regs. - case (In_dec Loc.eq (R (loc_result sig)) temporaries); intro. - auto. - case (In_dec Loc.eq (R (loc_result sig)) destroyed_at_call); intro. - auto. - elim n0. apply loc_result_caller_save. -Qed. - -(** Function arguments for a tail call are preserved by a - [return_regs] operation. *) - -Lemma return_regs_arguments: - forall sig caller callee, - tailcall_possible sig -> - map (LTL.return_regs caller callee) (loc_arguments sig) = - map callee (loc_arguments sig). -Proof. - intros. apply list_map_exten; intros. - generalize (H x H0). destruct x; intro. - unfold LTL.return_regs. - destruct (In_dec Loc.eq (R m) temporaries). auto. - destruct (In_dec Loc.eq (R m) destroyed_at_call). auto. - elim n0. eapply arguments_caller_save; eauto. - contradiction. -Qed. - -(** Acceptable locations that are not destroyed at call keep - their values across a call. *) - -Lemma return_regs_not_destroyed: - forall caller callee l, - Loc.notin l destroyed_at_call -> loc_acceptable l -> - LTL.return_regs caller callee l = caller l. -Proof. - unfold loc_acceptable, LTL.return_regs. - destruct l; auto. - intros. case (In_dec Loc.eq (R m) temporaries); intro. - contradiction. - case (In_dec Loc.eq (R m) destroyed_at_call); intro. - elim (Loc.notin_not_in _ _ H i). - auto. -Qed. - -(** Characterization of parallel assignments. *) - -Lemma parmov_spec: - forall ls srcs dsts, - Loc.norepet dsts -> List.length srcs = List.length dsts -> - List.map (LTL.parmov srcs dsts ls) dsts = List.map ls srcs /\ - (forall l, Loc.notin l dsts -> LTL.parmov srcs dsts ls l = ls l). -Proof. - induction srcs; destruct dsts; simpl; intros; try discriminate. - auto. - inv H. inv H0. destruct (IHsrcs _ H4 H1). split. - f_equal. apply Locmap.gss. rewrite <- H. apply list_map_exten; intros. - symmetry. apply Locmap.gso. eapply Loc.in_notin_diff; eauto. - intros x [A B]. rewrite Locmap.gso; auto. apply Loc.diff_sym; auto. -Qed. -****************) - (** * Properties of allocated locations *) (** We list here various properties of the locations [alloc r], @@ -256,9 +170,8 @@ Proof. red; intros. elim (Regset.empty_1 _ H4). unfold RTL.successors in H0; rewrite H2 in H0; elim H0. Qed. -
-(** Some useful special cases of [agree_increasing]. *) +(** Some useful special cases of [agree_increasing]. *) Lemma agree_reg_live: forall r live rs ls, @@ -423,7 +336,7 @@ Lemma agree_postcall: (forall r, Regset.In r live -> r <> res -> assign r <> assign res) -> agree (reg_list_live args (reg_sum_live ros (reg_dead res live))) rs ls -> - agree live (rs#res <- v) (Locmap.set (assign res) v (postcall_regs ls)). + agree live (rs#res <- v) (Locmap.set (assign res) v (postcall_locs ls)). Proof. intros. assert (agree (reg_dead res live) rs ls). @@ -433,7 +346,7 @@ Proof. subst r. rewrite Locmap.gss. auto. rewrite Locmap.gso. transitivity (ls (assign r)). apply H2. apply Regset.remove_2; auto. - unfold postcall_regs. + unfold postcall_locs. assert (~In (assign r) temporaries). apply Loc.notin_not_in. eapply regalloc_not_temporary; eauto. assert (~In (assign r) destroyed_at_call). diff --git a/backend/LTL.v b/backend/LTL.v index e39a4ec..6ee07f7 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -84,25 +84,12 @@ Fixpoint init_locs (vl: list val) (rl: list loc) {struct rl} : locset := | _, _ => Locmap.init Vundef end. - -Section RELSEM. - -(** [parmov srcs dsts ls] performs the parallel assignment - of locations [dsts] to the values of the corresponding locations - [srcs]. *) - -Fixpoint parmov (srcs dsts: list loc) (ls: locset) {struct srcs} : locset := - match srcs, dsts with - | s1 :: sl, d1 :: dl => Locmap.set d1 (ls s1) (parmov sl dl ls) - | _, _ => ls - end. - -(** [postcall_regs ls] returns the location set [ls] after a function +(** [postcall_locs ls] returns the location set [ls] after a function call. Caller-save registers and temporary registers are set to [undef], reflecting the fact that the called function can modify them freely. *) -Definition postcall_regs (ls: locset) : locset := +Definition postcall_locs (ls: locset) : locset := fun (l: loc) => match l with | R r => @@ -147,6 +134,9 @@ Inductive state : Set := (m: mem), (**r memory state *) state. + +Section RELSEM. + Variable ge: genv. Definition find_function (los: loc + ident) (rs: locset) : option fundef := @@ -159,46 +149,12 @@ Definition find_function (los: loc + ident) (rs: locset) : option fundef := end end. -(** The main difference between the LTL transition relation - and the RTL transition relation is the handling of function calls. - In RTL, arguments and results to calls are transmitted via - [vargs] and [vres] components of [Callstate] and [Returnstate], - respectively. The semantics takes care of transferring these values - between the pseudo-registers of the caller and of the callee. - - In lower-level intermediate languages (e.g [Linear], [Mach], [PPC]), - arguments and results are transmitted implicitly: the generated - code for the caller arranges for arguments to be left in conventional - registers and stack locations, as determined by the calling conventions, - where the function being called will find them. Similarly, - conventional registers will be used to pass the result value back - to the caller. - - In LTL, we take an hybrid view of argument and result passing. - The LTL code does not contain (yet) instructions for moving - arguments and results to the conventional registers. However, - the dynamic semantics "goes through the motions" of such code: -- The [exec_Lcall] transition from [State] to [Callstate] - leaves the values of arguments in the conventional locations - given by [loc_arguments]. -- The [exec_function_internal] transition from [Callstate] to [State] - changes the view of stack slots ([Outgoing] slots slide to - [Incoming] slots as per [call_regs]), then recovers the - values of parameters from the conventional locations given by - [loc_parameters]. -- The [exec_Lreturn] transition from [State] to [Returnstate] - moves the result value to the conventional location [loc_result], - then restores the values of callee-save locations from - the location state of the caller, using [return_regs]. -- The [exec_return] transition from [Returnstate] to [State] - reads the result value from the conventional location [loc_result], - then stores it in the result location for the [Lcall] instruction. - -This complicated protocol will make it much easier to prove -the correctness of the [Stacking] pass later, which inserts actual -code that performs all the shuffling of arguments and results -described above. -*) +(** The LTL transition relation is very similar to that of RTL, + with locations being used in place of pseudo-registers. + The main difference is for the [call] instruction: caller-save + registers are set to [Vundef] across the call, using the [postcall_locs] + function defined above. This forces the LTL producer to avoid + storing values live across the call in a caller-save register. *) Inductive step: state -> trace -> state -> Prop := | exec_Lnop: @@ -232,7 +188,7 @@ Inductive step: state -> trace -> state -> Prop := find_function ros rs = Some f' -> funsig f' = sig -> step (State s f sp pc rs m) - E0 (Callstate (Stackframe res f sp (postcall_regs rs) pc' :: s) + E0 (Callstate (Stackframe res f sp (postcall_locs rs) pc' :: s) f' (List.map rs args) m) | exec_Ltailcall: forall s f stk pc rs m sig ros args f', @@ -247,7 +203,7 @@ Inductive step: state -> trace -> state -> Prop := rs arg = Vint sz -> Mem.alloc m 0 (Int.signed sz) = (m', b) -> step (State s f sp pc rs m) - E0 (State s f sp pc' (Locmap.set res (Vptr b Int.zero) (postcall_regs rs)) m') + E0 (State s f sp pc' (Locmap.set res (Vptr b Int.zero) (postcall_locs rs)) m') | exec_Lcond_true: forall s f sp pc rs m cond args ifso ifnot, (fn_code f)!pc = Some(Lcond cond args ifso ifnot) -> diff --git a/backend/LTLin.v b/backend/LTLin.v index 83787ce..fae6417 100644 --- a/backend/LTLin.v +++ b/backend/LTLin.v @@ -140,14 +140,6 @@ Inductive state : Set := (m: mem), (**r memory state *) state. -(* -Definition parent_callsig (stack: list stackframe) : signature := - match stack with - | nil => mksignature nil (Some Tint) - | Stackframe sg res f sp ls pc :: stack' => sg - end. -*) - Section RELSEM. Variable ge: genv. @@ -185,7 +177,7 @@ Inductive step: state -> trace -> state -> Prop := find_function ros rs = Some f' -> sig = funsig f' -> step (State s f sp (Lcall sig ros args res :: b) rs m) - E0 (Callstate (Stackframe res f sp (postcall_regs rs) b :: s) + E0 (Callstate (Stackframe res f sp (postcall_locs rs) b :: s) f' (List.map rs args) m) | exec_Ltailcall: forall s f stk sig ros args b rs m f', @@ -198,7 +190,7 @@ Inductive step: state -> trace -> state -> Prop := rs arg = Vint sz -> Mem.alloc m 0 (Int.signed sz) = (m', blk) -> step (State s f sp (Lalloc arg res :: b) rs m) - E0 (State s f sp b (Locmap.set res (Vptr blk Int.zero) (postcall_regs rs)) m') + E0 (State s f sp b (Locmap.set res (Vptr blk Int.zero) (postcall_locs rs)) m') | exec_Llabel: forall s f sp lbl b rs m, step (State s f sp (Llabel lbl :: b) rs m) diff --git a/backend/Linear.v b/backend/Linear.v index ca1a2bc..900b6a5 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -202,6 +202,40 @@ Definition parent_locset (stack: list stackframe) : locset := | Stackframe f sp ls c :: stack' => ls end. +(** The main difference between the Linear transition relation + and the LTL transition relation is the handling of function calls. + In LTL, arguments and results to calls are transmitted via + [vargs] and [vres] components of [Callstate] and [Returnstate], + respectively. The semantics takes care of transferring these values + between the locations of the caller and of the callee. + + In Linear and lower-level languages (Mach, PPC), arguments and + results are transmitted implicitly: the generated code for the + caller arranges for arguments to be left in conventional registers + and stack locations, as determined by the calling conventions, where + the function being called will find them. Similarly, conventional + registers will be used to pass the result value back to the caller. + This is reflected in the definition of [Callstate] and [Returnstate] + above, where a whole location state [rs] is passed instead of just + the values of arguments or returns as in LTL. + + These location states passed across calls are treated in a way that + reflects the callee-save/caller-save convention: +- The [exec_Lcall] transition from [State] to [Callstate] + saves the current location state [ls] in the call stack, + and passes it to the callee. +- The [exec_function_internal] transition from [Callstate] to [State] + changes the view of stack slots ([Outgoing] slots slide to + [Incoming] slots as per [call_regs]). +- The [exec_Lreturn] transition from [State] to [Returnstate] + restores the values of callee-save locations from + the location state of the caller, using [return_regs]. + +This protocol makes it much easier to later prove the correctness of +the [Stacking] pass, which inserts actual code that performs the +saving and restoring of callee-save registers described above. +*) + Inductive step: state -> trace -> state -> Prop := | exec_Lgetstack: forall s f sp sl r b rs m, diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index 372a261..3177eaf 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'), diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index cefad10..7ad75ba 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -299,7 +299,7 @@ Proof. econstructor; eauto. (* Lalloc *) rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. - left; exists (State ts (tunnel_function f) sp (branch_target f pc') (Locmap.set res (Vptr b Integers.Int.zero) (postcall_regs rs)) m'); split. + left; exists (State ts (tunnel_function f) sp (branch_target f pc') (Locmap.set res (Vptr b Integers.Int.zero) (postcall_locs rs)) m'); split. eapply exec_Lalloc; eauto. rewrite (tunnel_function_lookup _ _ _ H); simpl; auto. econstructor; eauto. |