From e4723d142aa7b1229cdf5989340342d7c5ce870c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 6 Mar 2016 10:31:26 +0100 Subject: Update the back-end proofs to the new linking framework. --- backend/Deadcodeproof.v | 233 ++++++++++++++++++++++-------------------------- 1 file changed, 108 insertions(+), 125 deletions(-) (limited to 'backend/Deadcodeproof.v') diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index 6bbf0ae7..72881b94 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -12,28 +12,20 @@ (** Elimination of unneeded computations over RTL: correctness proof. *) -Require Import Coqlib. -Require Import Errors. -Require Import Maps. -Require Import IntvSets. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Events. -Require Import Smallstep. -Require Import Op. -Require Import Registers. -Require Import RTL. -Require Import Lattice. -Require Import Kildall. -Require Import ValueDomain. -Require Import ValueAnalysis. -Require Import NeedDomain. -Require Import NeedOp. -Require Import Deadcode. +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Values Memory Globalenvs Events Smallstep. +Require Import Registers Op RTL. +Require Import ValueDomain ValueAnalysis NeedDomain NeedOp Deadcode. + +Definition match_prog (prog tprog: RTL.program) := + match_program (fun cu f tf => transf_fundef (romem_for cu) f = OK tf) eq prog tprog. + +Lemma transf_program_match: + forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog. +Proof. + intros. eapply match_transform_partial_program_contextual; eauto. +Qed. (** * Relating the memory states *) @@ -378,75 +370,61 @@ Section PRESERVATION. Variable prog: program. Variable tprog: program. -Hypothesis TRANSF: transf_program prog = OK tprog. +Hypothesis TRANSF: match_prog prog tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. -Let rm := romem_for_program prog. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof. - intro. unfold ge, tge. - apply Genv.find_symbol_transf_partial with (transf_fundef rm). - exact TRANSF. -Qed. - -Lemma public_preserved: - forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. -Proof. - intro. unfold ge, tge. - apply Genv.public_symbol_transf_partial with (transf_fundef rm). - exact TRANSF. -Qed. +Proof (Genv.find_symbol_match TRANSF). -Lemma varinfo_preserved: - forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. -Proof. - intro. unfold ge, tge. - apply Genv.find_var_info_transf_partial with (transf_fundef rm). - exact TRANSF. -Qed. +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_match TRANSF). Lemma functions_translated: forall (v: val) (f: RTL.fundef), Genv.find_funct ge v = Some f -> - exists tf, - Genv.find_funct tge v = Some tf /\ transf_fundef rm f = OK tf. -Proof (Genv.find_funct_transf_partial (transf_fundef rm) _ TRANSF). + exists cu tf, + Genv.find_funct tge v = Some tf /\ transf_fundef (romem_for cu) f = OK tf /\ linkorder cu prog. +Proof (Genv.find_funct_match TRANSF). Lemma function_ptr_translated: forall (b: block) (f: RTL.fundef), Genv.find_funct_ptr ge b = Some f -> - exists tf, - Genv.find_funct_ptr tge b = Some tf /\ transf_fundef rm f = OK tf. -Proof (Genv.find_funct_ptr_transf_partial (transf_fundef rm) _ TRANSF). + exists cu tf, + Genv.find_funct_ptr tge b = Some tf /\ transf_fundef (romem_for cu) f = OK tf /\ linkorder cu prog. +Proof (Genv.find_funct_ptr_match TRANSF). Lemma sig_function_translated: - forall f tf, + forall rm f tf, transf_fundef rm f = OK tf -> funsig tf = funsig f. Proof. intros; destruct f; monadInv H. unfold transf_function in EQ. - destruct (analyze (vanalyze rm f) f); inv EQ; auto. + destruct (analyze (ValueAnalysis.analyze rm f) f); inv EQ; auto. auto. Qed. Lemma stacksize_translated: - forall f tf, + forall rm f tf, transf_function rm f = OK tf -> tf.(fn_stacksize) = f.(fn_stacksize). Proof. - unfold transf_function; intros. destruct (analyze (vanalyze rm f) f); inv H; auto. + unfold transf_function; intros. destruct (analyze (ValueAnalysis.analyze rm f) f); inv H; auto. Qed. +Definition vanalyze (cu: program) (f: function) := + ValueAnalysis.analyze (romem_for cu) f. + Lemma transf_function_at: - forall f tf an pc instr, - transf_function rm f = OK tf -> - analyze (vanalyze rm f) f = Some an -> + forall cu f tf an pc instr, + transf_function (romem_for cu) f = OK tf -> + analyze (vanalyze cu f) f = Some an -> f.(fn_code)!pc = Some instr -> - tf.(fn_code)!pc = Some(transf_instr (vanalyze rm f) an pc instr). + tf.(fn_code)!pc = Some(transf_instr (vanalyze cu f) an pc instr). Proof. - intros. unfold transf_function in H. rewrite H0 in H. inv H; simpl. + intros. unfold transf_function in H. unfold vanalyze in H0. rewrite H0 in H. inv H; simpl. rewrite PTree.gmap. rewrite H1; auto. Qed. @@ -475,7 +453,10 @@ Lemma find_function_translated: forall ros rs fd trs ne, find_function ge ros rs = Some fd -> eagree rs trs (add_ros_need_all ros ne) -> - exists tfd, find_function tge ros trs = Some tfd /\ transf_fundef rm fd = OK tfd. + exists cu tfd, + find_function tge ros trs = Some tfd + /\ transf_fundef (romem_for cu) fd = OK tfd + /\ linkorder cu prog. Proof. intros. destruct ros as [r|id]; simpl in *. - assert (LD: Val.lessdef rs#r trs#r) by eauto with na. inv LD. @@ -489,30 +470,33 @@ Qed. Inductive match_stackframes: stackframe -> stackframe -> Prop := | match_stackframes_intro: - forall res f sp pc e tf te an - (FUN: transf_function rm f = OK tf) - (ANL: analyze (vanalyze rm f) f = Some an) + forall res f sp pc e tf te cu an + (LINK: linkorder cu prog) + (FUN: transf_function (romem_for cu) f = OK tf) + (ANL: analyze (vanalyze cu f) f = Some an) (RES: forall v tv, Val.lessdef v tv -> eagree (e#res <- v) (te#res<- tv) - (fst (transfer f (vanalyze rm f) pc an!!pc))), + (fst (transfer f (vanalyze cu f) pc an!!pc))), match_stackframes (Stackframe res f (Vptr sp Int.zero) pc e) (Stackframe res tf (Vptr sp Int.zero) pc te). Inductive match_states: state -> state -> Prop := | match_regular_states: - forall s f sp pc e m ts tf te tm an + forall s f sp pc e m ts tf te tm cu an (STACKS: list_forall2 match_stackframes s ts) - (FUN: transf_function rm f = OK tf) - (ANL: analyze (vanalyze rm f) f = Some an) - (ENV: eagree e te (fst (transfer f (vanalyze rm f) pc an!!pc))) - (MEM: magree m tm (nlive ge sp (snd (transfer f (vanalyze rm f) pc an!!pc)))), + (LINK: linkorder cu prog) + (FUN: transf_function (romem_for cu) f = OK tf) + (ANL: analyze (vanalyze cu f) f = Some an) + (ENV: eagree e te (fst (transfer f (vanalyze cu f) pc an!!pc))) + (MEM: magree m tm (nlive ge sp (snd (transfer f (vanalyze cu f) pc an!!pc)))), match_states (State s f (Vptr sp Int.zero) pc e m) (State ts tf (Vptr sp Int.zero) pc te tm) | match_call_states: - forall s f args m ts tf targs tm + forall s f args m ts tf targs tm cu (STACKS: list_forall2 match_stackframes s ts) - (FUN: transf_fundef rm f = OK tf) + (LINK: linkorder cu prog) + (FUN: transf_fundef (romem_for cu) f = OK tf) (ARGS: Val.lessdef_list args targs) (MEM: Mem.extends m tm), match_states (Callstate s f args m) @@ -528,21 +512,22 @@ Inductive match_states: state -> state -> Prop := (** [match_states] and CFG successors *) Lemma analyze_successors: - forall f an pc instr pc', - analyze (vanalyze rm f) f = Some an -> + forall cu f an pc instr pc', + analyze (vanalyze cu f) f = Some an -> f.(fn_code)!pc = Some instr -> In pc' (successors_instr instr) -> - NA.ge an!!pc (transfer f (vanalyze rm f) pc' an!!pc'). + NA.ge an!!pc (transfer f (vanalyze cu f) pc' an!!pc'). Proof. intros. eapply DS.fixpoint_solution; eauto. intros. unfold transfer; rewrite H2. destruct a. apply DS.L.eq_refl. Qed. Lemma match_succ_states: - forall s f sp pc e m ts tf te tm an pc' instr ne nm + forall s f sp pc e m ts tf te tm an pc' cu instr ne nm + (LINK: linkorder cu prog) (STACKS: list_forall2 match_stackframes s ts) - (FUN: transf_function rm f = OK tf) - (ANL: analyze (vanalyze rm f) f = Some an) + (FUN: transf_function (romem_for cu) f = OK tf) + (ANL: analyze (vanalyze cu f) f = Some an) (INSTR: f.(fn_code)!pc = Some instr) (SUCC: In pc' (successors_instr instr)) (ANPC: an!!pc = (ne, nm)) @@ -720,7 +705,7 @@ Ltac TransfInstr := | [INSTR: (fn_code _)!_ = Some _, FUN: transf_function _ _ = OK _, ANL: analyze _ _ = Some _ |- _ ] => - generalize (transf_function_at _ _ _ _ _ FUN ANL INSTR); + generalize (transf_function_at _ _ _ _ _ _ FUN ANL INSTR); intro TI; unfold transf_instr in TI end. @@ -825,7 +810,7 @@ Ltac UseTransfer := - (* store *) TransfInstr; UseTransfer. - destruct (nmem_contains nm (aaddressing (vanalyze rm f) # pc addr args) + destruct (nmem_contains nm (aaddressing (vanalyze cu f) # pc addr args) (size_chunk chunk)) eqn:CONTAINS. + (* preserved *) simpl in *. @@ -854,39 +839,41 @@ Ltac UseTransfer := - (* call *) TransfInstr; UseTransfer. - exploit find_function_translated; eauto 2 with na. intros (tfd & A & B). + exploit find_function_translated; eauto 2 with na. intros (cu' & tfd & A & B & C). econstructor; split. - eapply exec_Icall; eauto. apply sig_function_translated; auto. - constructor. - constructor; auto. econstructor; eauto. + eapply exec_Icall; eauto. eapply sig_function_translated; eauto. + eapply match_call_states with (cu := cu'); eauto. + constructor; auto. eapply match_stackframes_intro with (cu := cu); eauto. intros. edestruct analyze_successors; eauto. simpl; eauto. eapply eagree_ge; eauto. rewrite ANPC. simpl. apply eagree_update; eauto with na. - auto. eauto 2 with na. eapply magree_extends; eauto. apply nlive_all. + eauto 2 with na. + eapply magree_extends; eauto. apply nlive_all. - (* tailcall *) TransfInstr; UseTransfer. - exploit find_function_translated; eauto 2 with na. intros (tfd & A & B). + exploit find_function_translated; eauto 2 with na. intros (cu' & tfd & A & B & L). exploit magree_free. eauto. eauto. instantiate (1 := nlive ge stk nmem_all). intros; eapply nlive_dead_stack; eauto. intros (tm' & C & D). econstructor; split. - eapply exec_Itailcall; eauto. apply sig_function_translated; auto. + eapply exec_Itailcall; eauto. eapply sig_function_translated; eauto. erewrite stacksize_translated by eauto. eexact C. - constructor; eauto 2 with na. eapply magree_extends; eauto. apply nlive_all. + eapply match_call_states with (cu := cu'); eauto 2 with na. + eapply magree_extends; eauto. apply nlive_all. - (* builtin *) TransfInstr; UseTransfer. revert ENV MEM TI. - functional induction (transfer_builtin (vanalyze rm f)#pc ef args res ne nm); + functional induction (transfer_builtin (vanalyze cu f)#pc ef args res ne nm); simpl in *; intros. + (* volatile load *) inv H0. inv H6. rename b1 into v1. destruct (transfer_builtin_arg All (kill_builtin_res res ne, - nmem_add nm (aaddr_arg (vanalyze rm f) # pc a1) + nmem_add nm (aaddr_arg (vanalyze cu f) # pc a1) (size_chunk chunk)) a1) as (ne1, nm1) eqn: TR. - inversion SS; subst. exploit transfer_builtin_arg_sound; eauto. + InvSoundState. exploit transfer_builtin_arg_sound; eauto. intros (tv1 & A & B & C & D). inv H1. simpl in B. inv B. assert (X: exists tvres, volatile_load ge chunk tm b ofs t tvres /\ Val.lessdef vres tvres). @@ -904,9 +891,8 @@ Ltac UseTransfer := eapply exec_Ibuiltin; eauto. apply eval_builtin_args_preserved with (ge1 := ge). exact symbols_preserved. constructor. eauto. constructor. - eapply external_call_symbols_preserved. + eapply external_call_symbols_preserved. apply senv_preserved. constructor. simpl. eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. apply eagree_set_res; auto. eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. @@ -915,7 +901,7 @@ Ltac UseTransfer := destruct (transfer_builtin_arg (store_argument chunk) (kill_builtin_res res ne, nm) a2) as (ne2, nm2) eqn: TR2. destruct (transfer_builtin_arg All (ne2, nm2) a1) as (ne1, nm1) eqn: TR1. - inversion SS; subst. + InvSoundState. exploit transfer_builtin_arg_sound. eexact H4. eauto. eauto. eauto. eauto. eauto. intros (tv1 & A1 & B1 & C1 & D1). exploit transfer_builtin_arg_sound. eexact H3. eauto. eauto. eauto. eauto. eauto. @@ -926,21 +912,21 @@ Ltac UseTransfer := eapply exec_Ibuiltin; eauto. apply eval_builtin_args_preserved with (ge1 := ge). exact symbols_preserved. constructor. eauto. constructor. eauto. constructor. - eapply external_call_symbols_preserved. simpl; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + eapply external_call_symbols_preserved. apply senv_preserved. + simpl; eauto. eapply match_succ_states; eauto. simpl; auto. apply eagree_set_res; auto. + (* memcpy *) rewrite e1 in TI. inv H0. inv H6. inv H7. rename b1 into v1. rename b0 into v2. - set (adst := aaddr_arg (vanalyze rm f) # pc dst) in *. - set (asrc := aaddr_arg (vanalyze rm f) # pc src) in *. + set (adst := aaddr_arg (vanalyze cu f) # pc dst) in *. + set (asrc := aaddr_arg (vanalyze cu f) # pc src) in *. destruct (transfer_builtin_arg All (kill_builtin_res res ne, nmem_add (nmem_remove nm adst sz) asrc sz) dst) as (ne2, nm2) eqn: TR2. destruct (transfer_builtin_arg All (ne2, nm2) src) as (ne1, nm1) eqn: TR1. - inversion SS; subst. + InvSoundState. exploit transfer_builtin_arg_sound. eexact H3. eauto. eauto. eauto. eauto. eauto. intros (tv1 & A1 & B1 & C1 & D1). exploit transfer_builtin_arg_sound. eexact H4. eauto. eauto. eauto. eauto. eauto. @@ -948,7 +934,7 @@ Ltac UseTransfer := inv H1. exploit magree_loadbytes. eauto. eauto. intros. eapply nlive_add; eauto. - unfold asrc, vanalyze, rm; rewrite AN; eapply aaddr_arg_sound_1; eauto. + unfold asrc, vanalyze; rewrite AN; eapply aaddr_arg_sound_1; eauto. intros (tbytes & P & Q). exploit magree_storebytes_parallel. eapply magree_monotone. eexact D2. @@ -957,7 +943,7 @@ Ltac UseTransfer := eauto. instantiate (1 := nlive ge sp0 nm). intros. eapply nlive_remove; eauto. - unfold adst, vanalyze, rm; rewrite AN; eapply aaddr_arg_sound_1; eauto. + unfold adst, vanalyze; rewrite AN; eapply aaddr_arg_sound_1; eauto. erewrite Mem.loadbytes_length in H1 by eauto. rewrite nat_of_Z_eq in H1 by omega. auto. eauto. @@ -966,51 +952,49 @@ Ltac UseTransfer := eapply exec_Ibuiltin; eauto. apply eval_builtin_args_preserved with (ge1 := ge). exact symbols_preserved. constructor. eauto. constructor. eauto. constructor. - eapply external_call_symbols_preserved. simpl. + eapply external_call_symbols_preserved. apply senv_preserved. simpl in B1; inv B1. simpl in B2; inv B2. econstructor; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. apply eagree_set_res; auto. + (* memcpy eliminated *) rewrite e1 in TI. inv H0. inv H6. inv H7. rename b1 into v1. rename b0 into v2. - set (adst := aaddr_arg (vanalyze rm f) # pc dst) in *. - set (asrc := aaddr_arg (vanalyze rm f) # pc src) in *. + set (adst := aaddr_arg (vanalyze cu f) # pc dst) in *. + set (asrc := aaddr_arg (vanalyze cu f) # pc src) in *. inv H1. econstructor; split. eapply exec_Inop; eauto. eapply match_succ_states; eauto. simpl; auto. destruct res; auto. apply eagree_set_undef; auto. eapply magree_storebytes_left; eauto. - exploit aaddr_arg_sound. eauto. eauto. + exploit aaddr_arg_sound; eauto. intros (bc & A & B & C). intros. eapply nlive_contains; eauto. erewrite Mem.loadbytes_length in H0 by eauto. rewrite nat_of_Z_eq in H0 by omega. auto. + (* annot *) destruct (transfer_builtin_args (kill_builtin_res res ne, nm) _x1) as (ne1, nm1) eqn:TR. - inversion SS; subst. + InvSoundState. exploit transfer_builtin_args_sound; eauto. intros (tvl & A & B & C & D). inv H1. econstructor; split. eapply exec_Ibuiltin; eauto. apply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. - eapply external_call_symbols_preserved. simpl; constructor. - eapply eventval_list_match_lessdef; eauto 2 with na. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + eapply external_call_symbols_preserved. apply senv_preserved. + constructor. eapply eventval_list_match_lessdef; eauto 2 with na. eapply match_succ_states; eauto. simpl; auto. apply eagree_set_res; auto. + (* annot val *) destruct (transfer_builtin_args (kill_builtin_res res ne, nm) _x1) as (ne1, nm1) eqn:TR. - inversion SS; subst. + InvSoundState. exploit transfer_builtin_args_sound; eauto. intros (tvl & A & B & C & D). inv H1. inv B. inv H6. econstructor; split. eapply exec_Ibuiltin; eauto. apply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. - eapply external_call_symbols_preserved. simpl; constructor. + eapply external_call_symbols_preserved. apply senv_preserved. + constructor. eapply eventval_match_lessdef; eauto 2 with na. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. apply eagree_set_res; auto. + (* debug *) @@ -1027,7 +1011,7 @@ Ltac UseTransfer := } clear y TI. destruct (transfer_builtin_args (kill_builtin_res res ne, nmem_all) _x0) as (ne1, nm1) eqn:TR. - inversion SS; subst. + InvSoundState. exploit transfer_builtin_args_sound; eauto. intros (tvl & A & B & C & D). exploit external_call_mem_extends; eauto 2 with na. eapply magree_extends; eauto. intros. apply nlive_all. @@ -1035,8 +1019,7 @@ Ltac UseTransfer := econstructor; split. eapply exec_Ibuiltin; eauto. apply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. - eapply external_call_symbols_preserved. eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + eapply external_call_symbols_preserved. apply senv_preserved. eauto. eapply match_succ_states; eauto. simpl; auto. apply eagree_set_res; auto. eapply mextends_agree; eauto. @@ -1071,8 +1054,8 @@ Ltac UseTransfer := eapply magree_extends; eauto. apply nlive_all. - (* internal function *) - monadInv FUN. generalize EQ. unfold transf_function. intros EQ'. - destruct (analyze (vanalyze rm f) f) as [an|] eqn:AN; inv EQ'. + monadInv FUN. generalize EQ. unfold transf_function. fold (vanalyze cu f). intros EQ'. + destruct (analyze (vanalyze cu f) f) as [an|] eqn:AN; inv EQ'. exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. intros (tm' & A & B). econstructor; split. @@ -1087,8 +1070,7 @@ Ltac UseTransfer := simpl in FUN. inv FUN. econstructor; split. econstructor; eauto. - eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. econstructor; eauto. - (* return *) @@ -1103,14 +1085,15 @@ Lemma transf_initial_states: exists st2, initial_state tprog st2 /\ match_states st1 st2. Proof. intros. inversion H. - exploit function_ptr_translated; eauto. intros (tf & A & B). + exploit function_ptr_translated; eauto. intros (cu & tf & A & B & C). exists (Callstate nil tf nil m0); split. econstructor; eauto. - eapply Genv.init_mem_transf_partial; eauto. - rewrite (transform_partial_program_main _ _ TRANSF). + eapply (Genv.init_mem_match TRANSF); eauto. + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. - rewrite <- H3. apply sig_function_translated; auto. - constructor. constructor. auto. constructor. apply Mem.extends_refl. + symmetry; eapply match_program_main; eauto. + rewrite <- H3. eapply sig_function_translated; eauto. + econstructor; eauto. constructor. apply Mem.extends_refl. Qed. Lemma transf_final_states: @@ -1128,7 +1111,7 @@ Proof. intros. apply forward_simulation_step with (match_states := fun s1 s2 => sound_state prog s1 /\ match_states s1 s2). -- exact public_preserved. +- apply senv_preserved. - simpl; intros. exploit transf_initial_states; eauto. intros [st2 [A B]]. exists st2; intuition. eapply sound_initial; eauto. - simpl; intros. destruct H. eapply transf_final_states; eauto. -- cgit