From 0290650b7463088bb228bc96d3143941590b54dd Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 7 Jul 2008 13:55:29 +0000 Subject: Nettoyage du traitement des signatures au return dans LTL et LTLin git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@690 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Allocproof.v | 60 +++++++++++++++++++++--------------------------- backend/LTL.v | 27 +++++++++++++--------- backend/LTLin.v | 26 +++++++++++++-------- backend/Linearizeproof.v | 16 ++++++------- backend/Reloadproof.v | 56 +++++++++++++++++--------------------------- backend/Tunnelingproof.v | 18 +++++++-------- 6 files changed, 96 insertions(+), 107 deletions(-) (limited to 'backend') diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 68d6868c..051be1e6 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -552,12 +552,13 @@ Qed. The bottom horizontal bar is the [match_states] relation. *) -Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signature -> Prop := - | match_stackframes_nil: forall ty_args, - match_stackframes nil nil (mksignature ty_args (Some Tint)) +Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> Prop := + | match_stackframes_nil: + match_stackframes nil nil | match_stackframes_cons: forall s ts sig res f sp pc rs ls env live assign, - match_stackframes s ts (RTL.fn_sig f) -> + match_stackframes s ts -> + sig_res (RTL.fn_sig f) = sig_res (parent_callsig ts) -> wt_function f env -> analyze f = Some live -> regalloc f live (live0 f live) env = Some assign -> @@ -569,13 +570,13 @@ Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signa (Locmap.set (assign res) (ls1 (R (loc_result sig))) ls1)) -> match_stackframes (RTL.Stackframe res (RTL.fn_code f) sp pc rs :: s) - (LTL.Stackframe (assign res) (transf_fun f live assign) sp ls pc :: ts) - sig. + (LTL.Stackframe sig (assign res) (transf_fun f live assign) sp ls pc :: ts). Inductive match_states: RTL.state -> LTL.state -> Prop := | match_states_intro: forall s f sp pc rs m ts ls tm live assign env - (STACKS: match_stackframes s ts (RTL.fn_sig f)) + (STACKS: match_stackframes s ts) + (SIG: sig_res(RTL.fn_sig f) = sig_res(parent_callsig ts)) (WT: wt_function f env) (ANL: analyze f = Some live) (ASG: regalloc f live (live0 f live) env = Some assign) @@ -585,7 +586,8 @@ Inductive match_states: RTL.state -> LTL.state -> Prop := (LTL.State ts (transf_fun f live assign) sp pc ls tm) | match_states_call: forall s f args m ts tf ls tm, - match_stackframes s ts (RTL.funsig f) -> + match_stackframes s ts -> + sig_res(RTL.funsig f) = sig_res(parent_callsig ts) -> transf_fundef f = OK tf -> Val.lessdef_list args (List.map ls (loc_arguments (funsig tf))) -> Mem.lessdef m tm -> @@ -593,28 +595,13 @@ Inductive match_states: RTL.state -> LTL.state -> Prop := match_states (RTL.Callstate s f args m) (LTL.Callstate ts tf ls tm) | match_states_return: - forall s v m ts sig ls tm, - match_stackframes s ts sig -> - Val.lessdef v (ls (R (loc_result sig))) -> + forall s v m ts ls tm, + match_stackframes s ts -> + Val.lessdef v (ls (R (loc_result (parent_callsig ts)))) -> Mem.lessdef m tm -> (forall l, Loc.notin l destroyed_at_call -> loc_acceptable l -> ls l = parent_locset ts l) -> match_states (RTL.Returnstate s v m) - (LTL.Returnstate ts sig ls tm). - -Remark match_stackframes_change: - forall s ts sig, - match_stackframes s ts sig -> - forall sig', - sig_res sig' = sig_res sig -> - match_stackframes s ts sig'. -Proof. - induction 1; intros. - destruct sig'. simpl in H; inv H. constructor. - assert (loc_result sig' = loc_result sig). - unfold loc_result. rewrite H4; auto. - econstructor; eauto. - rewrite H5. auto. -Qed. + (LTL.Returnstate ts ls tm). (** The simulation proof is by case analysis over the RTL transition taken in the source program. *) @@ -808,8 +795,7 @@ Proof. rewrite (sig_function_translated _ _ TF). eauto. rewrite (sig_function_translated _ _ TF). econstructor; eauto. - apply match_stackframes_change with (RTL.fn_sig f0); auto. - inv WTI. auto. + inv WTI. congruence. rewrite (sig_function_translated _ _ TF). rewrite return_regs_arguments. change Regset.elt with reg in PM1. @@ -865,13 +851,16 @@ Proof. econstructor; eauto. rewrite return_regs_result. inv WTI. destruct or; simpl in *. + replace (loc_result (parent_callsig ts)) + with (loc_result (RTL.fn_sig f)). rewrite Locmap.gss. eapply agree_eval_reg; eauto. + unfold loc_result. rewrite SIG. auto. constructor. apply free_lessdef; auto. intros. apply return_regs_not_destroyed; auto. (* internal function *) - generalize H6. simpl. unfold transf_function. + generalize H7. simpl. unfold transf_function. caseEq (type_function f); simpl; try congruence. intros env TYP. assert (WTF: wt_function f env). apply type_function_correct; auto. caseEq (analyze f); simpl; try congruence. intros live ANL. @@ -902,13 +891,16 @@ Proof. apply list_map_exten. intros. symmetry. eapply call_regs_param_of_arg; eauto. (* external function *) - injection H6; intro EQ; inv EQ. + injection H7; intro EQ; inv EQ. exploit event_match_lessdef; eauto. intros [tres [A B]]. econstructor; split. eapply exec_function_external; eauto. eapply match_states_return; eauto. + replace (loc_result (parent_callsig ts)) + with (loc_result (ef_sig ef)). rewrite Locmap.gss. auto. - intros. rewrite <- H10; auto. apply Locmap.gso. + unfold loc_result. rewrite <- H6. auto. + intros. rewrite <- H11; auto. apply Locmap.gso. apply Loc.diff_sym. eapply Loc.in_notin_diff; eauto. apply loc_result_caller_save. @@ -940,7 +932,7 @@ Proof. econstructor; eauto. rewrite symbols_preserved. rewrite (transform_partial_program_main _ _ TRANSF). auto. - constructor; auto. rewrite H2; constructor. + constructor; auto. constructor. rewrite H2; auto. Qed. Lemma transf_final_states: @@ -948,7 +940,7 @@ Lemma transf_final_states: match_states st1 st2 -> RTL.final_state st1 r -> LTL.final_state st2 r. Proof. intros. inv H0. inv H. inv H3. econstructor. - inv H4. auto. + simpl in H4. inv H4. auto. Qed. Theorem transf_program_correct: diff --git a/backend/LTL.v b/backend/LTL.v index e99e016e..a082e122 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -140,7 +140,8 @@ Definition set_result_reg (s: signature) (or: option loc) (ls: locset) := Inductive stackframe : Set := | Stackframe: - forall (res: loc) (**r where to store the result *) + forall (sig: signature) (**r signature of call *) + (res: loc) (**r where to store the result *) (f: function) (**r calling function *) (sp: val) (**r stack pointer in calling function *) (ls: locset) (**r location state in calling function *) @@ -164,7 +165,6 @@ Inductive state : Set := state | Returnstate: forall (stack: list stackframe) (**r call stack *) - (sig: signature) (**r signature of returning function *) (ls: locset) (**r location state at point of return *) (m: mem), (**r memory state *) state. @@ -172,7 +172,13 @@ Inductive state : Set := Definition parent_locset (stack: list stackframe) : locset := match stack with | nil => Locmap.init Vundef - | Stackframe res f sp ls pc :: stack' => ls + | Stackframe sg res f sp ls pc :: stack' => ls + end. + +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. Variable ge: genv. @@ -261,7 +267,7 @@ Inductive step: state -> trace -> state -> Prop := funsig f' = sig -> let rs1 := parmov args (loc_arguments sig) rs in step (State s f sp pc rs m) - E0 (Callstate (Stackframe res f sp rs1 pc' :: s) f' rs1 m) + E0 (Callstate (Stackframe sig res f sp rs1 pc' :: s) f' rs1 m) | exec_Ltailcall: forall s f stk pc rs m sig ros args f', (fn_code f)!pc = Some(Ltailcall sig ros args) -> @@ -299,7 +305,7 @@ Inductive step: state -> trace -> state -> Prop := let rs1 := set_result_reg f.(fn_sig) or rs in let rs2 := return_regs (parent_locset s) rs1 in step (State s f (Vptr stk Int.zero) pc rs m) - E0 (Returnstate s f.(fn_sig) rs2 (Mem.free m stk)) + E0 (Returnstate s rs2 (Mem.free m stk)) | exec_function_internal: forall s f rs m m' stk, Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> @@ -314,12 +320,11 @@ Inductive step: state -> trace -> state -> Prop := let rs1 := Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs in step (Callstate s (External ef) rs m) - t (Returnstate s ef.(ef_sig) rs1 m) + t (Returnstate s rs1 m) | exec_return: forall res f sp rs0 pc s sig rs m, let rs1 := Locmap.set res (rs (R (loc_result sig))) rs in - step (Returnstate (Stackframe res f sp rs0 pc :: s) - sig rs m) + step (Returnstate (Stackframe sig res f sp rs0 pc :: s) rs m) E0 (State s f sp pc rs1 m). End RELSEM. @@ -339,9 +344,9 @@ Inductive initial_state (p: program): state -> Prop := initial_state p (Callstate nil f (Locmap.init Vundef) m0). Inductive final_state: state -> int -> Prop := - | final_state_intro: forall sig rs m r, - rs (R (loc_result sig)) = Vint r -> - final_state (Returnstate nil sig rs m) r. + | final_state_intro: forall rs m r, + rs (R (loc_result (mksignature nil (Some Tint)))) = Vint r -> + final_state (Returnstate nil rs m) r. Definition exec_program (p: program) (beh: program_behavior) : Prop := program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. diff --git a/backend/LTLin.v b/backend/LTLin.v index 6cf2eb53..157b6d47 100644 --- a/backend/LTLin.v +++ b/backend/LTLin.v @@ -112,7 +112,8 @@ Fixpoint find_label (lbl: label) (c: code) {struct c} : option code := Inductive stackframe : Set := | Stackframe: - forall (res: loc) (**r where to store the result *) + forall (sig: signature) (**r signature of call *) + (res: loc) (**r where to store the result *) (f: function) (**r calling function *) (sp: val) (**r stack pointer in calling function *) (ls: locset) (**r location state in calling function *) @@ -136,7 +137,6 @@ Inductive state : Set := state | Returnstate: forall (stack: list stackframe) (**r call stack *) - (sig: signature) (**r signature of returning function *) (ls: locset) (**r location state at point of return *) (m: mem), (**r memory state *) state. @@ -144,7 +144,13 @@ Inductive state : Set := Definition parent_locset (stack: list stackframe) : locset := match stack with | nil => Locmap.init Vundef - | Stackframe res f sp ls pc :: stack' => ls + | Stackframe sg res f sp ls pc :: stack' => ls + end. + +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. @@ -185,7 +191,7 @@ Inductive step: state -> trace -> state -> Prop := sig = funsig f' -> let rs1 := parmov args (loc_arguments sig) rs in step (State s f sp (Lcall sig ros args res :: b) rs m) - E0 (Callstate (Stackframe res f sp rs1 b :: s) f' rs1 m) + E0 (Callstate (Stackframe sig res f sp rs1 b :: s) f' rs1 m) | exec_Ltailcall: forall s f stk sig ros args b rs m f', find_function ros rs = Some f' -> @@ -228,7 +234,7 @@ Inductive step: state -> trace -> state -> Prop := let rs1 := set_result_reg f.(fn_sig) or rs in let rs2 := return_regs (parent_locset s) rs1 in step (State s f (Vptr stk Int.zero) (Lreturn or :: b) rs m) - E0 (Returnstate s f.(fn_sig) rs2 (Mem.free m stk)) + E0 (Returnstate s rs2 (Mem.free m stk)) | exec_function_internal: forall s f rs m m' stk, Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> @@ -243,11 +249,11 @@ Inductive step: state -> trace -> state -> Prop := let rs1 := Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs in step (Callstate s (External ef) rs m) - t (Returnstate s ef.(ef_sig) rs1 m) + t (Returnstate s rs1 m) | exec_return: forall res f sp rs0 b s sig rs m, let rs1 := Locmap.set res (rs (R (loc_result sig))) rs in - step (Returnstate (Stackframe res f sp rs0 b :: s) sig rs m) + step (Returnstate (Stackframe sig res f sp rs0 b :: s) rs m) E0 (State s f sp b rs1 m). End RELSEM. @@ -262,9 +268,9 @@ Inductive initial_state (p: program): state -> Prop := initial_state p (Callstate nil f (Locmap.init Vundef) m0). Inductive final_state: state -> int -> Prop := - | final_state_intro: forall sig rs m r, - rs (R (loc_result sig)) = Vint r -> - final_state (Returnstate nil sig rs m) r. + | final_state_intro: forall rs m r, + rs (R (loc_result (mksignature nil (Some Tint)))) = Vint r -> + final_state (Returnstate nil rs m) r. Definition exec_program (p: program) (beh: program_behavior) : Prop := program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index a7b01861..303482e0 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -468,15 +468,15 @@ Qed. Inductive match_stackframes: LTL.stackframe -> LTLin.stackframe -> Prop := | match_stackframe_intro: - forall res f sp pc ls tf c, + forall sig res f sp pc ls tf c, transf_function f = OK tf -> (reachable f)!!pc = true -> valid_successor f pc -> is_tail c (fn_code tf) -> wt_function f -> match_stackframes - (LTL.Stackframe res f sp ls pc) - (LTLin.Stackframe res tf sp ls (add_branch pc c)). + (LTL.Stackframe sig res f sp ls pc) + (LTLin.Stackframe sig res tf sp ls (add_branch pc c)). Inductive match_states: LTL.state -> LTLin.state -> Prop := | match_states_intro: @@ -496,10 +496,10 @@ Inductive match_states: LTL.state -> LTLin.state -> Prop := match_states (LTL.Callstate s f ls m) (LTLin.Callstate ts tf ls m) | match_states_return: - forall s sig ls m ts, + forall s ls m ts, list_forall2 match_stackframes s ts -> - match_states (LTL.Returnstate s sig ls m) - (LTLin.Returnstate ts sig ls m). + match_states (LTL.Returnstate s ls m) + (LTLin.Returnstate ts ls m). Remark parent_locset_match: forall s ts, @@ -699,7 +699,7 @@ Proof. econstructor; eauto. (* return *) - inv H4. inv H1. + inv H3. inv H1. exploit find_label_lin_succ; eauto. intros [c' AT]. econstructor; split. eapply plus_left'. @@ -730,7 +730,7 @@ Lemma transf_final_states: forall st1 st2 r, match_states st1 st2 -> LTL.final_state st1 r -> LTLin.final_state st2 r. Proof. - intros. inv H0. inv H. inv H6. constructor. auto. + intros. inv H0. inv H. inv H5. constructor. auto. Qed. Theorem transf_program_correct: diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index 401ae466..f0b17e1b 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -770,26 +770,26 @@ Qed. only acceptable locations are accessed by this code. *) -Inductive match_stackframes: list LTLin.stackframe -> list Linear.stackframe -> signature -> Prop := +Inductive match_stackframes: list LTLin.stackframe -> list Linear.stackframe -> Prop := | match_stackframes_nil: - forall tyargs, - match_stackframes nil nil (mksignature tyargs (Some Tint)) + match_stackframes nil nil | match_stackframes_cons: forall res f sp c rs s s' c' ls sig, - match_stackframes s s' (LTLin.fn_sig f) -> + match_stackframes s s' -> + sig_res (LTLin.fn_sig f) = sig_res (parent_callsig s) -> c' = add_spill (loc_result sig) res (transf_code f c) -> agree rs ls -> loc_acceptable res -> wt_function f -> is_tail c (LTLin.fn_code f) -> - match_stackframes (LTLin.Stackframe res f sp rs c :: s) - (Linear.Stackframe (transf_function f) sp ls c' :: s') - sig. + match_stackframes (LTLin.Stackframe sig res f sp rs c :: s) + (Linear.Stackframe (transf_function f) sp ls c' :: s'). Inductive match_states: LTLin.state -> Linear.state -> Prop := | match_states_intro: forall s f sp c rs m s' ls - (STACKS: match_stackframes s s' (LTLin.fn_sig f)) + (STACKS: match_stackframes s s') + (SIG: sig_res (LTLin.fn_sig f) = sig_res (parent_callsig s)) (AG: agree rs ls) (WT: wt_function f) (TL: is_tail c (LTLin.fn_code f)), @@ -797,40 +797,28 @@ Inductive match_states: LTLin.state -> Linear.state -> Prop := (Linear.State s' (transf_function f) sp (transf_code f c) ls m) | match_states_call: forall s f rs m s' ls - (STACKS: match_stackframes s s' (LTLin.funsig f)) + (STACKS: match_stackframes s s') + (SIG: sig_res (LTLin.funsig f) = sig_res (parent_callsig s)) (AG: agree_arguments (LTLin.funsig f) rs ls) (WT: wt_fundef f), match_states (LTLin.Callstate s f rs m) (Linear.Callstate s' (transf_fundef f) ls m) | match_states_return: - forall s sig rs m s' ls - (STACKS: match_stackframes s s' sig) + forall s rs m s' ls + (STACKS: match_stackframes s s') (AG: agree rs ls), - match_states (LTLin.Returnstate s sig rs m) + match_states (LTLin.Returnstate s rs m) (Linear.Returnstate s' ls m). Remark parent_locset_match: - forall s s' sig, - match_stackframes s s' sig -> + forall s s', + match_stackframes s s' -> agree (LTLin.parent_locset s) (parent_locset s'). Proof. induction 1; simpl. red; intros; auto. auto. Qed. - -Remark match_stackframes_inv: - forall s ts sig, - match_stackframes s ts sig -> - forall sig', sig_res sig' = sig_res sig -> - match_stackframes s ts sig'. -Proof. - induction 1; intros. - destruct sig'. simpl in H; inv H. constructor. - assert (loc_result sig' = loc_result sig). - unfold loc_result. rewrite H5; auto. - econstructor; eauto. rewrite H6; auto. -Qed. Ltac ExploitWT := match goal with @@ -859,7 +847,7 @@ Definition measure (st: LTLin.state) : nat := match st with | LTLin.State s f sp c ls m => List.length c | LTLin.Callstate s f ls m => 0%nat - | LTLin.Returnstate s sig ls m => 0%nat + | LTLin.Returnstate s ls m => 0%nat end. Theorem transf_step_correct: @@ -995,8 +983,8 @@ Proof. eauto. traceEq. econstructor; eauto. econstructor; eauto with coqlib. - rewrite H0. auto. eapply agree_arguments_agree; eauto. + simpl. congruence. (* direct call *) destruct (parallel_move_arguments_correct tge s' (transf_function f) sp args sig @@ -1017,8 +1005,8 @@ Proof. traceEq. econstructor; eauto. econstructor; eauto with coqlib. - rewrite H0; auto. eapply agree_arguments_agree; eauto. + simpl; congruence. (* Ltailcall *) inversion MS. subst s0 f0 sp c rs0 m0 s1'. @@ -1055,8 +1043,7 @@ Proof. apply functions_translated. eauto. rewrite H0; symmetry; apply sig_preserved. eauto. traceEq. - econstructor; eauto. - eapply match_stackframes_inv; eauto. congruence. + econstructor; eauto. congruence. (* direct call *) destruct (parallel_move_arguments_correct tge s' (transf_function f) (Vptr stk Int.zero) @@ -1077,8 +1064,7 @@ Proof. apply function_ptr_translated; auto. congruence. rewrite H0. symmetry; apply sig_preserved. traceEq. - econstructor; eauto. - eapply match_stackframes_inv; eauto. congruence. + econstructor; eauto. congruence. (* Lalloc *) ExploitWT; inv WTI. @@ -1213,7 +1199,7 @@ Proof. apply function_ptr_translated; eauto. rewrite sig_preserved. auto. replace (Genv.init_mem tprog) with (Genv.init_mem prog). - econstructor; eauto. rewrite H2. constructor. + econstructor; eauto. constructor. rewrite H2; auto. red; intros. auto. eapply Genv.find_funct_ptr_prop; eauto. symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf; auto. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index d0c95462..cb0a6d83 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -190,10 +190,10 @@ Definition tunneled_code (f: function) := Inductive match_stackframes: stackframe -> stackframe -> Prop := | match_stackframes_intro: - forall res f sp ls0 pc, + forall sig res f sp ls0 pc, match_stackframes - (Stackframe res f sp ls0 pc) - (Stackframe res (tunnel_function f) sp ls0 (branch_target f pc)). + (Stackframe sig res f sp ls0 pc) + (Stackframe sig res (tunnel_function f) sp ls0 (branch_target f pc)). Inductive match_states: state -> state -> Prop := | match_states_intro: @@ -207,10 +207,10 @@ Inductive match_states: state -> state -> Prop := match_states (Callstate s f ls m) (Callstate ts (tunnel_fundef f) ls m) | match_states_return: - forall s sig ls m ts, + forall s ls m ts, list_forall2 match_stackframes s ts -> - match_states (Returnstate s sig ls m) - (Returnstate ts sig ls m). + match_states (Returnstate s ls m) + (Returnstate ts ls m). Lemma parent_locset_match: forall s ts, list_forall2 match_stackframes s ts -> parent_locset ts = parent_locset s. @@ -227,7 +227,7 @@ Definition measure (st: state) : nat := match st with | State s f sp pc ls m => count_goto f pc | Callstate s f ls m => 0%nat - | Returnstate s sig ls m => 0%nat + | Returnstate s ls m => 0%nat end. Lemma branch_target_identity: @@ -340,7 +340,7 @@ Proof. eapply exec_function_external; eauto. simpl. econstructor; eauto. (* return *) - inv H4. inv H1. + inv H3. inv H1. left; econstructor; split. eapply exec_return; eauto. fold rs1. constructor. auto. @@ -366,7 +366,7 @@ Lemma transf_final_states: forall st1 st2 r, match_states st1 st2 -> final_state st1 r -> final_state st2 r. Proof. - intros. inv H0. inv H. inv H6. constructor. auto. + intros. inv H0. inv H. inv H5. constructor. auto. Qed. Theorem transf_program_correct: -- cgit