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/Allocation.v | 23 +- backend/Allocproof.v | 86 ++-- backend/CSE.v | 28 +- backend/CSEproof.v | 141 +++--- backend/CleanupLabels.v | 6 +- backend/CleanupLabelsproof.v | 83 ++-- backend/Constprop.v | 22 +- backend/Constpropproof.v | 264 +++++----- backend/Deadcode.v | 27 +- backend/Deadcodeproof.v | 233 ++++----- backend/Debugvar.v | 15 +- backend/Debugvarproof.v | 81 ++- backend/Inlining.v | 12 +- backend/Inliningproof.v | 243 +++++---- backend/Inliningspec.v | 122 ++--- backend/Linearize.v | 16 +- backend/Linearizeproof.v | 61 +-- backend/RTLgenproof.v | 69 ++- backend/Renumberproof.v | 56 +-- backend/SelectLongproof.v | 56 ++- backend/Selection.v | 68 ++- backend/Selectionproof.v | 560 ++++++++++++--------- backend/Stacking.v | 16 +- backend/Stackingproof.v | 92 ++-- backend/Tailcall.v | 11 +- backend/Tailcallproof.v | 104 ++-- backend/Tunneling.v | 4 +- backend/Tunnelingproof.v | 58 +-- backend/Unusedglob.v | 56 +-- backend/Unusedglobproof.v | 1120 +++++++++++++++++++++++------------------- backend/ValueAnalysis.v | 249 ++++++---- backend/ValueDomain.v | 24 +- 32 files changed, 1996 insertions(+), 2010 deletions(-) (limited to 'backend') diff --git a/backend/Allocation.v b/backend/Allocation.v index 7534e23f..6a6c1eb6 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -12,26 +12,11 @@ (** Register allocation by external oracle and a posteriori validation. *) -Require Import FSets. -Require FSetAVLplus. +Require Import FSets FSetAVLplus. +Require Import Coqlib Ordered Maps Errors Integers Floats. +Require Import AST Lattice Kildall Memdata. Require Archi. -Require Import Coqlib. -Require Import Ordered. -Require Import Errors. -Require Import Maps. -Require Import Lattice. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Memdata. -Require Import Op. -Require Import Registers. -Require Import RTL. -Require Import Kildall. -Require Import Locations. -Require Import Conventions. -Require Import RTLtyping. -Require Import LTL. +Require Import Op Registers RTL Locations Conventions RTLtyping LTL. (** The validation algorithm used here is described in "Validating register allocation and spilling", diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 2bcc038c..84d4bdd5 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -14,29 +14,22 @@ RTL to LTL). *) Require Import FSets. +Require Import Coqlib Ordered Maps Errors Integers Floats. +Require Import AST Linking Lattice Kildall. +Require Import Values Memory Globalenvs Events Smallstep. Require Archi. -Require Import Coqlib. -Require Import Ordered. -Require Import Errors. -Require Import Maps. -Require Import Lattice. -Require Import AST. -Require Import Integers. -Require Import Values. -Require Import Memory. -Require Import Events. -Require Import Globalenvs. -Require Import Smallstep. -Require Import Op. -Require Import Registers. -Require Import RTL. -Require Import RTLtyping. -Require Import Kildall. -Require Import Locations. -Require Import Conventions. -Require Import LTL. +Require Import Op Registers RTL Locations Conventions RTLtyping LTL. Require Import Allocation. +Definition match_prog (p: RTL.program) (tp: LTL.program) := + match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. + +Lemma transf_program_match: + forall p tp, transf_program p = OK tp -> match_prog p tp. +Proof. + intros. eapply match_transform_partial_program; eauto. +Qed. + (** * Soundness of structural checks *) Definition expand_move (sd: loc * loc) : instruction := @@ -1608,48 +1601,32 @@ Section PRESERVATION. Variable prog: RTL.program. Variable tprog: LTL.program. -Hypothesis TRANSF: transf_program prog = OK tprog. +Hypothesis TRANSF: match_prog prog tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. 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. - exact TRANSF. -Qed. +Proof (Genv.find_symbol_match TRANSF). -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. - exact TRANSF. -Qed. - -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. - 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 f = OK tf. -Proof (Genv.find_funct_transf_partial transf_fundef _ TRANSF). +Proof (Genv.find_funct_transf_partial 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 f = OK tf. -Proof (Genv.find_funct_ptr_transf_partial transf_fundef _ TRANSF). +Proof (Genv.find_funct_ptr_transf_partial TRANSF). Lemma sig_function_translated: forall f tf, @@ -2185,8 +2162,7 @@ Proof. eapply star_trans. eexact A1. eapply star_left. econstructor. eapply 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. instantiate (1 := ls2); auto. eapply star_right. eexact A3. econstructor. @@ -2278,8 +2254,7 @@ Proof. econstructor; split. apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved' with (ge1 := ge). - econstructor; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + econstructor; eauto. apply senv_preserved. econstructor; eauto. simpl. replace (map (Locmap.setlist (map R (loc_result (ef_sig ef))) @@ -2314,9 +2289,9 @@ Proof. exploit sig_function_translated; eauto. intros SIG. exists (LTL.Callstate nil tf (Locmap.init Vundef) m0); split. econstructor; eauto. - eapply Genv.init_mem_transf_partial; eauto. + eapply (Genv.init_mem_transf_partial TRANSF); eauto. rewrite symbols_preserved. - rewrite (transform_partial_program_main _ _ TRANSF). auto. + rewrite (match_program_main TRANSF). auto. congruence. constructor; auto. constructor. rewrite SIG; rewrite H3; auto. @@ -2334,12 +2309,15 @@ Proof. econstructor. simpl; reflexivity. unfold loc_result in RES; rewrite H in RES. simpl in RES. inv RES. inv H3; auto. Qed. - + Lemma wt_prog: wt_program prog. Proof. - red; intros. exploit transform_partial_program_succeeds; eauto. - intros [tfd TF]. destruct f; simpl in *. -- monadInv TF. unfold transf_function in EQ. + red; intros. + exploit list_forall2_in_left. eexact (proj1 TRANSF). eauto. + intros ([i' gd] & A & B & C). simpl in *; subst i'. + inv C. destruct f; simpl in *. +- monadInv H2. + unfold transf_function in EQ. destruct (type_function f) as [env|] eqn:TF; try discriminate. econstructor. eapply type_function_correct; eauto. - constructor. @@ -2350,7 +2328,7 @@ Theorem transf_program_correct: Proof. set (ms := fun s s' => wt_state s /\ match_states s s'). eapply forward_simulation_plus with (match_states := ms). -- exact public_preserved. +- apply senv_preserved. - intros. exploit initial_states_simulation; eauto. intros [st2 [A B]]. exists st2; split; auto. split; auto. apply wt_initial_state with (p := prog); auto. exact wt_prog. diff --git a/backend/CSE.v b/backend/CSE.v index 63dadbc7..d6b89557 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -13,22 +13,11 @@ (** Common subexpression elimination over RTL. This optimization proceeds by value numbering over extended basic blocks. *) -Require Import Coqlib. -Require Import Maps. -Require Import Errors. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Op. -Require Import Registers. -Require Import RTL. -Require Import ValueDomain. -Require Import ValueAnalysis. -Require Import CSEdomain. -Require Import Kildall. -Require Import CombineOp. +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Values Memory. +Require Import Op Registers RTL. +Require Import ValueDomain ValueAnalysis CSEdomain CombineOp. (** The idea behind value numbering algorithms is to associate abstract identifiers (``value numbers'') to the contents of registers @@ -451,7 +440,8 @@ Module Solver := BBlock_solver(Numbering). For builtin invocations [Ibuiltin], we have three strategies: - Forget all equations. This is appropriate for builtins that can be - turned into function calls ([EF_external], [EF_malloc], [EF_free]). + turned into function calls + ([EF_external], [EF_runtime], [EF_malloc], [EF_free]). - Forget equations involving loads but keep equations over registers. This is appropriate for builtins that can modify memory, e.g. volatile stores, or [EF_builtin] @@ -481,7 +471,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb empty_numbering | Ibuiltin ef args res s => match ef with - | EF_external _ _ | EF_malloc | EF_free | EF_inline_asm _ _ _ => + | EF_external _ _ | EF_runtime _ _ | EF_malloc | EF_free | EF_inline_asm _ _ _ => empty_numbering | EF_builtin _ _ | EF_vstore _ => set_res_unknown (kill_all_loads before) res @@ -582,5 +572,5 @@ Definition transf_fundef (rm: romem) (f: fundef) : res fundef := AST.transf_partial_fundef (transf_function rm) f. Definition transf_program (p: program) : res program := - transform_partial_program (transf_fundef (romem_for_program p)) p. + transform_partial_program (transf_fundef (romem_for p)) p. diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 07c7008d..2c144249 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -12,28 +12,21 @@ (** Correctness proof for common subexpression elimination. *) -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Errors. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Events. -Require Import Globalenvs. -Require Import Smallstep. -Require Import Op. -Require Import Registers. -Require Import RTL. -Require Import Kildall. -Require Import ValueDomain. -Require Import ValueAOp. -Require Import ValueAnalysis. -Require Import CSEdomain. -Require Import CombineOp. -Require Import CombineOpproof. -Require Import CSE. +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Values Memory Events Globalenvs Smallstep. +Require Import Op Registers RTL. +Require Import ValueDomain ValueAOp ValueAnalysis. +Require Import CSEdomain CombineOp CombineOpproof CSE. + +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. (** * Soundness of operations over value numberings *) @@ -809,37 +802,32 @@ 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 (Genv.find_symbol_transf_partial (transf_fundef rm) prog TRANSF). +Proof (Genv.find_symbol_match TRANSF). -Lemma public_preserved: - forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. -Proof (Genv.public_symbol_transf_partial (transf_fundef rm) prog TRANSF). - -Lemma varinfo_preserved: - forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. -Proof (Genv.find_var_info_transf_partial (transf_fundef rm) prog TRANSF). +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) prog 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 funct_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) prog 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_preserved: - forall f tf, transf_fundef rm f = OK tf -> funsig tf = funsig f. + forall rm f tf, transf_fundef rm f = OK tf -> funsig tf = funsig f. Proof. unfold transf_fundef; intros. destruct f; monadInv H; auto. unfold transf_function in EQ. @@ -887,7 +875,9 @@ Lemma find_function_translated: forall ros rs fd rs', find_function ge ros rs = Some fd -> regs_lessdef rs rs' -> - exists tfd, find_function tge ros rs' = Some tfd /\ transf_fundef rm fd = OK tfd. + exists cu tfd, find_function tge ros rs' = Some tfd + /\ transf_fundef (romem_for cu) fd = OK tfd + /\ linkorder cu prog. Proof. unfold find_function; intros; destruct ros. - specialize (H0 r). inv H0. @@ -914,12 +904,16 @@ Qed. the numbering at [pc] (returned by the static analysis) is satisfiable. *) +Definition analyze (cu: program) (f: function) := + CSE.analyze f (vanalyze (romem_for cu) f). + Inductive match_stackframes: list stackframe -> list stackframe -> Prop := | match_stackframes_nil: match_stackframes nil nil | match_stackframes_cons: - forall res sp pc rs f approx s rs' s' - (ANALYZE: analyze f (vanalyze rm f) = Some approx) + forall res sp pc rs f s rs' s' cu approx + (LINK: linkorder cu prog) + (ANALYZE: analyze cu f = Some approx) (SAT: forall v m, exists valu, numbering_holds valu ge sp (rs#res <- v) m approx!!pc) (RLD: regs_lessdef rs rs') (STACKS: match_stackframes s s'), @@ -929,8 +923,9 @@ Inductive match_stackframes: list stackframe -> list stackframe -> Prop := Inductive match_states: state -> state -> Prop := | match_states_intro: - forall s sp pc rs m s' rs' m' f approx - (ANALYZE: analyze f (vanalyze rm f) = Some approx) + forall s sp pc rs m s' rs' m' f cu approx + (LINK: linkorder cu prog) + (ANALYZE: analyze cu f = Some approx) (SAT: exists valu, numbering_holds valu ge sp rs m approx!!pc) (RLD: regs_lessdef rs rs') (MEXT: Mem.extends m m') @@ -938,18 +933,19 @@ Inductive match_states: state -> state -> Prop := match_states (State s f sp pc rs m) (State s' (transf_function' f approx) sp pc rs' m') | match_states_call: - forall s f tf args m s' args' m', - match_stackframes s s' -> - transf_fundef rm f = OK tf -> - Val.lessdef_list args args' -> - Mem.extends m m' -> + forall s f tf args m s' args' m' cu + (LINK: linkorder cu prog) + (STACKS: match_stackframes s s') + (TFD: transf_fundef (romem_for cu) f = OK tf) + (ARGS: Val.lessdef_list args args') + (MEXT: Mem.extends m m'), match_states (Callstate s f args m) (Callstate s' tf args' m') | match_states_return: - forall s s' v v' m m', - match_stackframes s s' -> - Val.lessdef v v' -> - Mem.extends m m' -> + forall s s' v v' m m' + (STACK: match_stackframes s s') + (RES: Val.lessdef v v') + (MEXT: Mem.extends m m'), match_states (Returnstate s v m) (Returnstate s' v' m'). @@ -1076,28 +1072,28 @@ Proof. econstructor; eauto. eapply analysis_correct_1; eauto. simpl; auto. unfold transfer; rewrite H. - inv SOUND. + InvSoundState. eapply add_store_result_hold; eauto. eapply kill_loads_after_store_holds; eauto. - (* Icall *) - exploit find_function_translated; eauto. intros [tf [FIND' TRANSF']]. + exploit find_function_translated; eauto. intros (cu' & tf & FIND' & TRANSF' & LINK'). econstructor; split. eapply exec_Icall; eauto. - apply sig_preserved; auto. - econstructor; eauto. + eapply sig_preserved; eauto. econstructor; eauto. + eapply match_stackframes_cons with (cu := cu); eauto. intros. eapply analysis_correct_1; eauto. simpl; auto. unfold transfer; rewrite H. exists (fun _ => Vundef); apply empty_numbering_holds. apply regs_lessdef_regs; auto. - (* Itailcall *) - exploit find_function_translated; eauto. intros [tf [FIND' TRANSF']]. + exploit find_function_translated; eauto. intros (cu' & tf & FIND' & TRANSF' & LINK'). exploit Mem.free_parallel_extends; eauto. intros [m'' [A B]]. econstructor; split. eapply exec_Itailcall; eauto. - apply sig_preserved; auto. + eapply sig_preserved; eauto. econstructor; eauto. apply regs_lessdef_regs; auto. @@ -1109,8 +1105,7 @@ Proof. econstructor; split. eapply exec_Ibuiltin; eauto. eapply 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; eauto. apply senv_preserved. econstructor; eauto. eapply analysis_correct_1; eauto. simpl; auto. * unfold transfer; rewrite H. @@ -1125,6 +1120,7 @@ Proof. destruct ef. + apply CASE1. + apply CASE3. + + apply CASE1. + apply CASE2; inv H1; auto. + apply CASE3. + apply CASE1. @@ -1133,7 +1129,7 @@ Proof. simpl in H1. inv H1. exists valu. apply set_res_unknown_holds. - inv SOUND. unfold vanalyze, rm; rewrite AN. + InvSoundState. unfold vanalyze; rewrite AN. assert (pmatch bc bsrc osrc (aaddr_arg (VA.State ae am) a0)) by (eapply aaddr_arg_sound_1; eauto). assert (pmatch bc bdst odst (aaddr_arg (VA.State ae am) a1)) @@ -1179,8 +1175,8 @@ Proof. destruct or; simpl; auto. - (* internal function *) - monadInv H6. unfold transf_function in EQ. - destruct (analyze f (vanalyze rm f)) as [approx|] eqn:?; inv EQ. + monadInv TFD. unfold transf_function in EQ. fold (analyze cu f) in EQ. + destruct (analyze cu f) as [approx|] eqn:?; inv EQ. exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. intros (m'' & A & B). econstructor; split. @@ -1190,17 +1186,16 @@ Proof. apply init_regs_lessdef; auto. - (* external function *) - monadInv H6. + monadInv TFD. exploit external_call_mem_extends; eauto. intros (v' & m1' & P & Q & R & S). econstructor; split. eapply exec_function_external; 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 *) - inv H2. + inv STACK. econstructor; split. eapply exec_return; eauto. econstructor; eauto. @@ -1212,22 +1207,22 @@ Lemma transf_initial_states: exists st2, initial_state tprog st2 /\ match_states st1 st2. Proof. intros. inversion H. - exploit funct_ptr_translated; eauto. intros [tf [A B]]. + exploit funct_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. + eapply (Genv.init_mem_match TRANSF); eauto. replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. - symmetry. eapply transform_partial_program_main; eauto. - rewrite <- H3. apply sig_preserved; auto. - constructor. constructor. auto. auto. apply Mem.extends_refl. + symmetry. eapply match_program_main; eauto. + rewrite <- H3. eapply sig_preserved; eauto. + econstructor. eauto. constructor. auto. auto. apply Mem.extends_refl. Qed. 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 H5. inv H3. constructor. + intros. inv H0. inv H. inv RES. inv STACK. constructor. Qed. Theorem transf_program_correct: @@ -1235,7 +1230,7 @@ Theorem transf_program_correct: Proof. eapply forward_simulation_step with (match_states := fun s1 s2 => sound_state prog s1 /\ match_states s1 s2). -- eexact public_preserved. +- apply senv_preserved. - intros. exploit transf_initial_states; eauto. intros [s2 [A B]]. exists s2. split. auto. split. apply sound_initial; auto. auto. - intros. destruct H. eapply transf_final_states; eauto. diff --git a/backend/CleanupLabels.v b/backend/CleanupLabels.v index 759201b2..303fcb64 100644 --- a/backend/CleanupLabels.v +++ b/backend/CleanupLabels.v @@ -20,10 +20,8 @@ better-looking, the present pass removes labels that cannot be branched to. *) -Require Import FSets. -Require FSetAVL. -Require Import Coqlib. -Require Import Ordered. +Require Import FSets FSetAVL. +Require Import Coqlib Ordered. Require Import Linear. Module Labelset := FSetAVL.Make(OrderedPositive). diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v index 6f33c9c2..a498a654 100644 --- a/backend/CleanupLabelsproof.v +++ b/backend/CleanupLabelsproof.v @@ -12,68 +12,51 @@ (** Correctness proof for clean-up of labels *) -Require Import Coqlib. -Require Import Ordered. Require Import FSets. -Require Import AST. -Require Import Integers. -Require Import Values. -Require Import Memory. -Require Import Events. -Require Import Globalenvs. -Require Import Smallstep. -Require Import Op. -Require Import Locations. -Require Import Linear. +Require Import Coqlib Ordered Integers. +Require Import AST Linking. +Require Import Values Memory Events Globalenvs Smallstep. +Require Import Op Locations Linear. Require Import CleanupLabels. Module LabelsetFacts := FSetFacts.Facts(Labelset). +Definition match_prog (p tp: Linear.program) := + match_program (fun ctx f tf => tf = transf_fundef f) eq p tp. + +Lemma transf_program_match: + forall p, match_prog p (transf_program p). +Proof. + intros. eapply match_transform_program; eauto. +Qed. + Section CLEANUP. -Variable prog: program. -Let tprog := transf_program prog. +Variables prog tprog: program. +Hypothesis TRANSL: match_prog prog tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. Lemma symbols_preserved: - forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof. - intros; unfold ge, tge, tprog, transf_program. - apply Genv.find_symbol_transf. -Qed. + forall id, + Genv.find_symbol tge id = Genv.find_symbol ge id. +Proof (Genv.find_symbol_transf TRANSL). -Lemma public_preserved: - forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. -Proof. - intros; unfold ge, tge, tprog, transf_program. - apply Genv.public_symbol_transf. -Qed. - -Lemma varinfo_preserved: - forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. -Proof. - intros; unfold ge, tge, tprog, transf_program. - apply Genv.find_var_info_transf. -Qed. +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_transf TRANSL). Lemma functions_translated: - forall (v: val) (f: fundef), + forall v f, Genv.find_funct ge v = Some f -> Genv.find_funct tge v = Some (transf_fundef f). -Proof. - intros. - exact (Genv.find_funct_transf transf_fundef _ _ H). -Qed. +Proof (Genv.find_funct_transf TRANSL). Lemma function_ptr_translated: - forall (b: block) (f: fundef), - Genv.find_funct_ptr ge b = Some f -> - Genv.find_funct_ptr tge b = Some (transf_fundef f). -Proof. - intros. - exact (Genv.find_funct_ptr_transf transf_fundef _ _ H). -Qed. + forall v f, + Genv.find_funct_ptr ge v = Some f -> + Genv.find_funct_ptr tge v = Some (transf_fundef f). +Proof (Genv.find_funct_ptr_transf TRANSL). Lemma sig_function_translated: forall f, @@ -293,8 +276,7 @@ Proof. left; econstructor; split. econstructor. eapply 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; eauto. apply senv_preserved. eauto. econstructor; eauto with coqlib. (* Llabel *) @@ -333,8 +315,7 @@ Proof. econstructor; eauto with coqlib. (* external function *) left; econstructor; split. - econstructor; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + econstructor; eauto. eapply external_call_symbols_preserved'; eauto. apply senv_preserved. econstructor; eauto with coqlib. (* return *) inv H3. inv H1. left; econstructor; split. @@ -349,8 +330,8 @@ Proof. intros. inv H. econstructor; split. eapply initial_state_intro with (f := transf_fundef f). - eapply Genv.init_mem_transf; eauto. - rewrite symbols_preserved; eauto. + eapply (Genv.init_mem_transf TRANSL); eauto. + rewrite (match_program_main TRANSL), symbols_preserved; eauto. apply function_ptr_translated; auto. rewrite sig_function_translated. auto. constructor; auto. constructor. @@ -367,7 +348,7 @@ Theorem transf_program_correct: forward_simulation (Linear.semantics prog) (Linear.semantics tprog). Proof. eapply forward_simulation_opt. - eexact public_preserved. + apply senv_preserved. eexact transf_initial_states. eexact transf_final_states. eexact transf_step_correct. diff --git a/backend/Constprop.v b/backend/Constprop.v index 5ca69183..4de80b7a 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -14,21 +14,11 @@ performed at RTL level. It proceeds by a standard dataflow analysis and the corresponding code rewriting. *) -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Op. -Require Machregs. -Require Import Registers. -Require Import RTL. -Require Import Lattice. -Require Import Kildall. -Require Import Liveness. -Require Import ValueDomain. -Require Import ValueAOp. -Require Import ValueAnalysis. +Require Import Coqlib Maps Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Compopts Machregs. +Require Import Op Registers RTL. +Require Import Liveness ValueDomain ValueAOp ValueAnalysis. Require Import ConstpropOp. (** The code transformation builds on the results of the static analysis @@ -231,5 +221,5 @@ Definition transf_fundef (rm: romem) (fd: fundef) : fundef := AST.transf_fundef (transf_function rm) fd. Definition transf_program (p: program) : program := - let rm := romem_for_program p in + let rm := romem_for p in transform_program (transf_fundef rm) p. diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index ad9068ab..4e76c641 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -12,35 +12,30 @@ (** Correctness proof for constant propagation. *) -Require Import Coqlib. -Require Import Maps. -Require Compopts. -Require Import AST. -Require Import Integers. -Require Import Values. -Require Import Events. -Require Import Memory. -Require Import Globalenvs. -Require Import Smallstep. -Require Import Op. -Require Import Registers. -Require Import RTL. -Require Import Lattice. -Require Import Kildall. -Require Import ValueDomain. -Require Import ValueAOp. -Require Import ValueAnalysis. -Require Import ConstpropOp. -Require Import Constprop. -Require Import ConstpropOpproof. +Require Import Coqlib Maps Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Values Events Memory Globalenvs Smallstep. +Require Compopts Machregs. +Require Import Op Registers RTL. +Require Import Liveness ValueDomain ValueAOp ValueAnalysis. +Require Import ConstpropOp ConstpropOpproof Constprop. + +Definition match_prog (prog tprog: program) := + match_program (fun cu f tf => tf = transf_fundef (romem_for cu) f) eq prog tprog. + +Lemma transf_program_match: + forall prog, match_prog prog (transf_program prog). +Proof. + intros. eapply match_transform_program_contextual. auto. +Qed. Section PRESERVATION. Variable prog: program. -Let tprog := transf_program prog. +Variable tprog: program. +Hypothesis TRANSL: match_prog prog tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. -Let rm := romem_for_program prog. (** * Correctness of the code transformation *) @@ -49,45 +44,32 @@ Let rm := romem_for_program prog. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof. - intros; unfold ge, tge, tprog, transf_program. - apply Genv.find_symbol_transf. -Qed. - -Lemma public_preserved: - forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. -Proof. - intros; unfold ge, tge, tprog, transf_program. - apply Genv.public_symbol_transf. -Qed. +Proof (Genv.find_symbol_match TRANSL). -Lemma varinfo_preserved: - forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. -Proof. - intros; unfold ge, tge, tprog, transf_program. - apply Genv.find_var_info_transf. -Qed. +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_match TRANSL). Lemma functions_translated: forall (v: val) (f: fundef), Genv.find_funct ge v = Some f -> - Genv.find_funct tge v = Some (transf_fundef rm f). + exists cunit, Genv.find_funct tge v = Some (transf_fundef (romem_for cunit) f) /\ linkorder cunit prog. Proof. - intros. - exact (Genv.find_funct_transf (transf_fundef rm) _ _ H). + intros. exploit (Genv.find_funct_match TRANSL); eauto. + intros (cu & tf & A & B & C). subst tf. exists cu; auto. Qed. Lemma function_ptr_translated: forall (b: block) (f: fundef), Genv.find_funct_ptr ge b = Some f -> - Genv.find_funct_ptr tge b = Some (transf_fundef rm f). + exists cunit, Genv.find_funct_ptr tge b = Some (transf_fundef (romem_for cunit) f) /\ linkorder cunit prog. Proof. - intros. - exact (Genv.find_funct_ptr_transf (transf_fundef rm) _ _ H). + intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto. + intros (cu & tf & A & B & C). subst tf. exists cu; auto. Qed. Lemma sig_function_translated: - forall f, + forall rm f, funsig (transf_fundef rm f) = funsig f. Proof. intros. destruct f; reflexivity. @@ -110,12 +92,17 @@ Lemma transf_ros_correct: ematch bc rs ae -> find_function ge ros rs = Some f -> regs_lessdef rs rs' -> - find_function tge (transf_ros ae ros) rs' = Some (transf_fundef rm f). + exists cunit, + find_function tge (transf_ros ae ros) rs' = Some (transf_fundef (romem_for cunit) f) + /\ linkorder cunit prog. Proof. intros until rs'; intros GE EM FF RLD. destruct ros; simpl in *. - (* function pointer *) generalize (EM r); fold (areg ae r); intro VM. generalize (RLD r); intro LD. - assert (DEFAULT: find_function tge (inl _ r) rs' = Some (transf_fundef rm f)). + assert (DEFAULT: + exists cunit, + find_function tge (inl _ r) rs' = Some (transf_fundef (romem_for cunit) f) + /\ linkorder cunit prog). { simpl. inv LD. apply functions_translated; auto. rewrite <- H0 in FF; discriminate. } @@ -162,35 +149,45 @@ Proof. eapply vmatch_ptr_stk; eauto. Qed. -Inductive match_pc (f: function) (ae: AE.t): nat -> node -> node -> Prop := +Inductive match_pc (f: function) (rs: regset) (m: mem): nat -> node -> node -> Prop := | match_pc_base: forall n pc, - match_pc f ae n pc pc + match_pc f rs m n pc pc | match_pc_nop: forall n pc s pcx, f.(fn_code)!pc = Some (Inop s) -> - match_pc f ae n s pcx -> - match_pc f ae (S n) pc pcx - | match_pc_cond: forall n pc cond args s1 s2 b pcx, + match_pc f rs m n s pcx -> + match_pc f rs m (S n) pc pcx + | match_pc_cond: forall n pc cond args s1 s2 pcx, f.(fn_code)!pc = Some (Icond cond args s1 s2) -> - resolve_branch (eval_static_condition cond (aregs ae args)) = Some b -> - match_pc f ae n (if b then s1 else s2) pcx -> - match_pc f ae (S n) pc pcx. + (forall b, + eval_condition cond rs##args m = Some b -> + match_pc f rs m n (if b then s1 else s2) pcx) -> + match_pc f rs m (S n) pc pcx. Lemma match_successor_rec: - forall f ae n pc, match_pc f ae n pc (successor_rec n f ae pc). + forall f rs m bc ae, + ematch bc rs ae -> + forall n pc, + match_pc f rs m n pc (successor_rec n f ae pc). Proof. induction n; simpl; intros. - apply match_pc_base. - destruct (fn_code f)!pc as [[]|] eqn:INSTR; try apply match_pc_base. - eapply match_pc_nop; eauto. - destruct (resolve_branch (eval_static_condition c (aregs ae l))) as [b|] eqn:COND. - eapply match_pc_cond; eauto. - apply match_pc_base. ++ eapply match_pc_nop; eauto. ++ destruct (resolve_branch (eval_static_condition c (aregs ae l))) as [b|] eqn:STATIC; + try apply match_pc_base. + eapply match_pc_cond; eauto. intros b' DYNAMIC. + assert (b = b'). + { eapply resolve_branch_sound; eauto. + rewrite <- DYNAMIC. apply eval_static_condition_sound with bc. + apply aregs_sound; auto. } + subst b'. apply IHn. Qed. Lemma match_successor: - forall f ae pc, match_pc f ae num_iter pc (successor f ae pc). + forall f rs m bc ae pc, + ematch bc rs ae -> match_pc f rs m num_iter pc (successor f ae pc). Proof. - unfold successor; intros. apply match_successor_rec. + intros. eapply match_successor_rec; eauto. Qed. Lemma builtin_arg_reduction_correct: @@ -300,29 +297,31 @@ Qed. Inductive match_stackframes: stackframe -> stackframe -> Prop := match_stackframe_intro: - forall res sp pc rs f rs', + forall res sp pc rs f rs' cu, + linkorder cu prog -> regs_lessdef rs rs' -> match_stackframes (Stackframe res f sp pc rs) - (Stackframe res (transf_function rm f) sp pc rs'). + (Stackframe res (transf_function (romem_for cu) f) sp pc rs'). Inductive match_states: nat -> state -> state -> Prop := | match_states_intro: - forall s sp pc rs m f s' pc' rs' m' bc ae n - (MATCH: ematch bc rs ae) + forall s sp pc rs m f s' pc' rs' m' cu n + (LINK: linkorder cu prog) (STACKS: list_forall2 match_stackframes s s') - (PC: match_pc f ae n pc pc') + (PC: match_pc f rs m n pc pc') (REGS: regs_lessdef rs rs') (MEM: Mem.extends m m'), match_states n (State s f sp pc rs m) - (State s' (transf_function rm f) sp pc' rs' m') + (State s' (transf_function (romem_for cu) f) sp pc' rs' m') | match_states_call: - forall s f args m s' args' m' + forall s f args m s' args' m' cu + (LINK: linkorder cu prog) (STACKS: list_forall2 match_stackframes s s') (ARGS: Val.lessdef_list args args') (MEM: Mem.extends m m'), match_states O (Callstate s f args m) - (Callstate s' (transf_fundef rm f) args' m') + (Callstate s' (transf_fundef (romem_for cu) f) args' m') | match_states_return: forall s v m s' v' m' (STACKS: list_forall2 match_stackframes s s') @@ -333,21 +332,19 @@ Inductive match_states: nat -> state -> state -> Prop := (Returnstate s' v' m'). Lemma match_states_succ: - forall s f sp pc rs m s' rs' m', - sound_state prog (State s f sp pc rs m) -> + forall s f sp pc rs m s' rs' m' cu, + linkorder cu prog -> list_forall2 match_stackframes s s' -> regs_lessdef rs rs' -> Mem.extends m m' -> match_states O (State s f sp pc rs m) - (State s' (transf_function rm f) sp pc rs' m'). + (State s' (transf_function (romem_for cu) f) sp pc rs' m'). Proof. - intros. inv H. - apply match_states_intro with (bc := bc) (ae := ae); auto. - constructor. + intros. apply match_states_intro; auto. constructor. Qed. Lemma transf_instr_at: - forall f pc i, + forall rm f pc i, f.(fn_code)!pc = Some i -> (transf_function rm f).(fn_code)!pc = Some(transf_instr f (analyze rm f) rm pc i). Proof. @@ -357,8 +354,8 @@ Qed. Ltac TransfInstr := match goal with | H1: (PTree.get ?pc (fn_code ?f) = Some ?instr), - H2: (analyze (romem_for_program prog) ?f)#?pc = VA.State ?ae ?am |- _ => - fold rm in H2; generalize (transf_instr_at _ _ _ H1); unfold transf_instr; rewrite H2 + H2: (analyze ?rm ?f)#?pc = VA.State ?ae ?am |- _ => + generalize (transf_instr_at rm _ _ _ H1); unfold transf_instr; rewrite H2 end. (** The proof of simulation proceeds by case analysis on the transition @@ -367,38 +364,38 @@ Ltac TransfInstr := Lemma transf_step_correct: forall s1 t s2, step ge s1 t s2 -> - forall n1 s1' (SS1: sound_state prog s1) (SS2: sound_state prog s2) (MS: match_states n1 s1 s1'), + forall n1 s1' (SS: sound_state prog s1) (MS: match_states n1 s1 s1'), (exists n2, exists s2', step tge s1' t s2' /\ match_states n2 s2 s2') \/ (exists n2, n2 < n1 /\ t = E0 /\ match_states n2 s2 s1')%nat. Proof. - induction 1; intros; inv SS1; inv MS; try (inv PC; try congruence). + induction 1; intros; inv MS; try InvSoundState; try (inv PC; try congruence). - (* Inop, preserved *) +- (* Inop, preserved *) rename pc'0 into pc. TransfInstr; intros. left; econstructor; econstructor; split. eapply exec_Inop; eauto. eapply match_states_succ; eauto. - (* Inop, skipped over *) +- (* Inop, skipped over *) assert (s0 = pc') by congruence. subst s0. right; exists n; split. omega. split. auto. - apply match_states_intro with bc0 ae0; auto. + apply match_states_intro; auto. - (* Iop *) +- (* Iop *) rename pc'0 into pc. TransfInstr. set (a := eval_static_operation op (aregs ae args)). set (ae' := AE.set res a ae). assert (VMATCH: vmatch bc v a) by (eapply eval_static_operation_sound; eauto with va). assert (MATCH': ematch bc (rs#res <- v) ae') by (eapply ematch_update; eauto). destruct (const_for_result a) as [cop|] eqn:?; intros. - (* constant is propagated *) ++ (* constant is propagated *) exploit const_for_result_correct; eauto. intros (v' & A & B). left; econstructor; econstructor; split. eapply exec_Iop; eauto. - apply match_states_intro with bc ae'; auto. - apply match_successor. + apply match_states_intro; auto. + eapply match_successor; eauto. apply set_reg_lessdef; auto. - (* operator is strength-reduced *) ++ (* operator is strength-reduced *) assert(OP: let (op', args') := op_strength_reduction op args (aregs ae args) in exists v', @@ -413,24 +410,24 @@ Proof. left; econstructor; econstructor; split. eapply exec_Iop; eauto. erewrite eval_operation_preserved. eexact EV''. exact symbols_preserved. - apply match_states_intro with bc ae'; auto. - apply match_successor. + apply match_states_intro; auto. + eapply match_successor; eauto. apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto. - (* Iload *) +- (* Iload *) rename pc'0 into pc. TransfInstr. set (aa := eval_static_addressing addr (aregs ae args)). assert (VM1: vmatch bc a aa) by (eapply eval_static_addressing_sound; eauto with va). - set (av := loadv chunk rm am aa). + set (av := loadv chunk (romem_for cu) am aa). assert (VM2: vmatch bc v av) by (eapply loadv_sound; eauto). destruct (const_for_result av) as [cop|] eqn:?; intros. - (* constant-propagated *) ++ (* constant-propagated *) exploit const_for_result_correct; eauto. intros (v' & A & B). left; econstructor; econstructor; split. eapply exec_Iop; eauto. eapply match_states_succ; eauto. apply set_reg_lessdef; auto. - (* strength-reduced *) ++ (* strength-reduced *) assert (ADDR: let (addr', args') := addr_strength_reduction addr args (aregs ae args) in exists a', @@ -449,7 +446,7 @@ Proof. eapply exec_Iload; eauto. eapply match_states_succ; eauto. apply set_reg_lessdef; auto. - (* Istore *) +- (* Istore *) rename pc'0 into pc. TransfInstr. assert (ADDR: let (addr', args') := addr_strength_reduction addr args (aregs ae args) in @@ -469,9 +466,9 @@ Proof. eapply exec_Istore; eauto. eapply match_states_succ; eauto. - (* Icall *) +- (* Icall *) rename pc'0 into pc. - exploit transf_ros_correct; eauto. intro FIND'. + exploit transf_ros_correct; eauto. intros (cu' & FIND & LINK'). TransfInstr; intro. left; econstructor; econstructor; split. eapply exec_Icall; eauto. apply sig_function_translated; auto. @@ -479,17 +476,17 @@ Proof. econstructor; eauto. apply regs_lessdef_regs; auto. - (* Itailcall *) +- (* Itailcall *) exploit Mem.free_parallel_extends; eauto. intros [m2' [A B]]. - exploit transf_ros_correct; eauto. intros FIND'. + exploit transf_ros_correct; eauto. intros (cu' & FIND & LINK'). TransfInstr; intro. left; econstructor; econstructor; split. eapply exec_Itailcall; eauto. apply sig_function_translated; auto. constructor; auto. apply regs_lessdef_regs; auto. - (* Ibuiltin *) - rename pc'0 into pc. clear MATCH. TransfInstr; intros. +- (* Ibuiltin *) + rename pc'0 into pc. TransfInstr; intros. Opaque builtin_strength_reduction. exploit builtin_strength_reduction_correct; eauto. intros (vargs' & P & Q). exploit (@eval_builtin_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)). @@ -500,13 +497,12 @@ Opaque builtin_strength_reduction. left; econstructor; econstructor; split. eapply exec_Ibuiltin; eauto. eapply eval_builtin_args_preserved. eexact symbols_preserved. 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. eapply match_states_succ; eauto. apply set_res_lessdef; auto. - (* Icond, preserved *) - rename pc' into pc. TransfInstr. +- (* Icond, preserved *) + rename pc'0 into pc. TransfInstr. set (ac := eval_static_condition cond (aregs ae args)). assert (C: cmatch (eval_condition cond rs ## args m) ac) by (eapply eval_static_condition_sound; eauto with va). @@ -514,7 +510,7 @@ Opaque builtin_strength_reduction. generalize (cond_strength_reduction_correct bc ae rs m EM cond args (aregs ae args) (refl_equal _)). destruct (cond_strength_reduction cond args (aregs ae args)) as [cond' args']. intros EV1 TCODE. - left; exists O; exists (State s' (transf_function rm f) (Vptr sp0 Int.zero) (if b then ifso else ifnot) rs' m'); split. + left; exists O; exists (State s' (transf_function (romem_for cu) f) (Vptr sp0 Int.zero) (if b then ifso else ifnot) rs' m'); split. destruct (resolve_branch ac) eqn: RB. assert (b0 = b) by (eapply resolve_branch_sound; eauto). subst b0. destruct b; eapply exec_Inop; eauto. @@ -522,20 +518,15 @@ Opaque builtin_strength_reduction. eapply eval_condition_lessdef with (vl1 := rs##args'); eauto. eapply regs_lessdef_regs; eauto. congruence. eapply match_states_succ; eauto. - (* Icond, skipped over *) +- (* Icond, skipped over *) rewrite H1 in H; inv H. - set (ac := eval_static_condition cond (aregs ae0 args)) in *. - assert (C: cmatch (eval_condition cond rs ## args m) ac) - by (eapply eval_static_condition_sound; eauto with va). - rewrite H0 in C. - assert (b0 = b) by (eapply resolve_branch_sound; eauto). subst b0. - right; exists n; split. omega. split. auto. + right; exists n; split. omega. split. auto. econstructor; eauto. - (* Ijumptable *) +- (* Ijumptable *) rename pc'0 into pc. - assert (A: (fn_code (transf_function rm f))!pc = Some(Ijumptable arg tbl) - \/ (fn_code (transf_function rm f))!pc = Some(Inop pc')). + assert (A: (fn_code (transf_function (romem_for cu) f))!pc = Some(Ijumptable arg tbl) + \/ (fn_code (transf_function (romem_for cu) f))!pc = Some(Inop pc')). { TransfInstr. destruct (areg ae arg) eqn:A; auto. generalize (EM arg). fold (areg ae arg); rewrite A. @@ -543,23 +534,20 @@ Opaque builtin_strength_reduction. rewrite H1. auto. } assert (rs'#arg = Vint n). { generalize (REGS arg). rewrite H0. intros LD; inv LD; auto. } - left; exists O; exists (State s' (transf_function rm f) (Vptr sp0 Int.zero) pc' rs' m'); split. + left; exists O; exists (State s' (transf_function (romem_for cu) f) (Vptr sp0 Int.zero) pc' rs' m'); split. destruct A. eapply exec_Ijumptable; eauto. eapply exec_Inop; eauto. eapply match_states_succ; eauto. - (* Ireturn *) +- (* Ireturn *) exploit Mem.free_parallel_extends; eauto. intros [m2' [A B]]. left; exists O; exists (Returnstate s' (regmap_optget or Vundef rs') m2'); split. eapply exec_Ireturn; eauto. TransfInstr; auto. constructor; auto. destruct or; simpl; auto. - (* internal function *) +- (* internal function *) exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. intros [m2' [A B]]. - assert (X: exists bc ae, ematch bc (init_regs args (fn_params f)) ae). - { inv SS2. exists bc0; exists ae; auto. } - destruct X as (bc1 & ae1 & MATCH). simpl. unfold transf_function. left; exists O; econstructor; split. eapply exec_function_internal; simpl; eauto. @@ -567,19 +555,15 @@ Opaque builtin_strength_reduction. constructor. apply init_regs_lessdef; auto. - (* external function *) +- (* external function *) exploit external_call_mem_extends; eauto. intros [v' [m2' [A [B [C D]]]]]. simpl. left; econstructor; econstructor; split. eapply exec_function_external; 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. constructor; auto. - (* return *) - assert (X: exists bc ae, ematch bc (rs#res <- vres) ae). - { inv SS2. exists bc0; exists ae; auto. } - destruct X as (bc1 & ae1 & MATCH). +- (* return *) inv H4. inv H1. left; exists O; econstructor; split. eapply exec_return; eauto. @@ -591,15 +575,15 @@ Lemma transf_initial_states: exists n, exists st2, initial_state tprog st2 /\ match_states n st1 st2. Proof. intros. inversion H. - exploit function_ptr_translated; eauto. intro FIND. - exists O; exists (Callstate nil (transf_fundef rm f) nil m0); split. + exploit function_ptr_translated; eauto. intros (cu & FIND & LINK). + exists O; exists (Callstate nil (transf_fundef (romem_for cu) f) nil m0); split. econstructor; eauto. - apply Genv.init_mem_transf; auto. + apply (Genv.init_mem_match TRANSL); auto. replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. - reflexivity. + symmetry; eapply match_program_main; eauto. rewrite <- H3. apply sig_function_translated. - constructor. constructor. constructor. apply Mem.extends_refl. + constructor. auto. constructor. constructor. apply Mem.extends_refl. Qed. Lemma transf_final_states: @@ -615,9 +599,7 @@ Qed. Theorem transf_program_correct: forward_simulation (RTL.semantics prog) (RTL.semantics tprog). Proof. - apply Forward_simulation with - (fsim_order := lt) - (fsim_match_states := fun n s1 s2 => sound_state prog s1 /\ match_states n s1 s2). + apply Forward_simulation with lt (fun n s1 s2 => sound_state prog s1 /\ match_states n s1 s2); constructor. - apply lt_wf. - simpl; intros. exploit transf_initial_states; eauto. intros (n & st2 & A & B). exists n, st2; intuition. eapply sound_initial; eauto. @@ -629,7 +611,7 @@ Proof. intros [ [n2 [s2' [A B]]] | [n2 [A [B C]]]]. exists n2; exists s2'; split; auto. left; apply plus_one; auto. exists n2; exists s2; split; auto. right; split; auto. subst t; apply star_refl. -- eexact public_preserved. +- apply senv_preserved. Qed. End PRESERVATION. diff --git a/backend/Deadcode.v b/backend/Deadcode.v index fa99915d..e5b2ce3a 100644 --- a/backend/Deadcode.v +++ b/backend/Deadcode.v @@ -12,22 +12,10 @@ (** Elimination of unneeded computations over RTL. *) -Require Import Coqlib. -Require Import Errors. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Memory. -Require Import Registers. -Require Import Op. -Require Import RTL. -Require Import Lattice. -Require Import Kildall. -Require Import ValueDomain. -Require Import ValueAnalysis. -Require Import NeedDomain. -Require Import NeedOp. +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL. +Require Import ValueDomain ValueAnalysis NeedDomain NeedOp. (** * Part 1: the static analysis *) @@ -205,10 +193,8 @@ Definition transf_instr (approx: PMap.t VA.t) (an: PMap.t NA.t) instr end. -Definition vanalyze := ValueAnalysis.analyze. - Definition transf_function (rm: romem) (f: function) : res function := - let approx := vanalyze rm f in + let approx := ValueAnalysis.analyze rm f in match analyze approx f with | Some an => OK {| fn_sig := f.(fn_sig); @@ -220,10 +206,9 @@ Definition transf_function (rm: romem) (f: function) : res function := Error (msg "Neededness analysis failed") end. - Definition transf_fundef (rm: romem) (fd: fundef) : res fundef := AST.transf_partial_fundef (transf_function rm) fd. Definition transf_program (p: program) : res program := - transform_partial_program (transf_fundef (romem_for_program p)) p. + transform_partial_program (transf_fundef (romem_for p)) p. 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. diff --git a/backend/Debugvar.v b/backend/Debugvar.v index dcc4327a..5d31831a 100644 --- a/backend/Debugvar.v +++ b/backend/Debugvar.v @@ -13,18 +13,9 @@ (** Computation of live ranges for local variables that carry debugging information. *) -Require Import Coqlib. -Require Import Axioms. -Require Import Maps. -Require Import Iteration. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Errors. -Require Import Machregs. -Require Import Locations. -Require Import Conventions. -Require Import Linear. +Require Import Axioms Coqlib Maps Iteration Errors. +Require Import Integers Floats AST. +Require Import Machregs Locations Conventions Linear. (** A debug info is a [builtin_arg loc] expression that safely evaluates in any context. *) diff --git a/backend/Debugvarproof.v b/backend/Debugvarproof.v index 73e32103..110c0f26 100644 --- a/backend/Debugvarproof.v +++ b/backend/Debugvarproof.v @@ -12,28 +12,23 @@ (** Correctness proof for the [Debugvar] pass. *) -Require Import Coqlib. -Require Import Axioms. -Require Import Maps. -Require Import Iteration. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Events. -Require Import Globalenvs. -Require Import Smallstep. -Require Import Op. -Require Import Errors. -Require Import Machregs. -Require Import Locations. -Require Import Conventions. -Require Import Linear. +Require Import Axioms Coqlib Maps Iteration Errors. +Require Import Integers Floats AST Linking. +Require Import Values Memory Events Globalenvs Smallstep. +Require Import Machregs Locations Conventions Op Linear. Require Import Debugvar. (** * Relational characterization of the transformation *) +Definition match_prog (p tp: program) := + match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. + +Lemma transf_program_match: + forall p tp, transf_program p = OK tp -> match_prog p tp. +Proof. + intros. eapply match_transform_partial_program; eauto. +Qed. + Inductive match_code: code -> code -> Prop := | match_code_nil: match_code nil nil @@ -294,38 +289,32 @@ 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. +Lemma symbols_preserved: + forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof (Genv.find_symbol_match TRANSF). + +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_match TRANSF). + Lemma functions_translated: - forall v f, + forall (v: val) (f: fundef), Genv.find_funct ge v = Some f -> exists tf, Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf. -Proof (Genv.find_funct_transf_partial transf_fundef _ TRANSF). +Proof (Genv.find_funct_transf_partial TRANSF). Lemma function_ptr_translated: - forall v f, - Genv.find_funct_ptr ge v = Some f -> + forall (b: block) (f: fundef), + Genv.find_funct_ptr ge b = Some f -> exists tf, - Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf. -Proof (Genv.find_funct_ptr_transf_partial transf_fundef _ TRANSF). - -Lemma symbols_preserved: - forall id, - Genv.find_symbol tge id = Genv.find_symbol ge id. -Proof (Genv.find_symbol_transf_partial transf_fundef _ TRANSF). - -Lemma public_preserved: - forall id, - Genv.public_symbol tge id = Genv.public_symbol ge id. -Proof (Genv.public_symbol_transf_partial transf_fundef _ TRANSF). - -Lemma varinfo_preserved: - forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. -Proof (Genv.find_var_info_transf_partial transf_fundef _ TRANSF). + Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf. +Proof (Genv.find_funct_ptr_transf_partial TRANSF). Lemma sig_preserved: forall f tf, @@ -488,8 +477,7 @@ Proof. eapply plus_left. econstructor; eauto. eapply 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; eauto. apply senv_preserved. apply eval_add_delta_ranges. traceEq. constructor; auto. - (* label *) @@ -530,8 +518,7 @@ Proof. - (* external function *) monadInv H8. econstructor; split. apply plus_one. 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. constructor; auto. - (* return *) inv H3. inv H1. @@ -547,10 +534,8 @@ Proof. intros. inversion H. exploit function_ptr_translated; eauto. intros [tf [A B]]. exists (Callstate nil tf (Locmap.init Vundef) m0); split. - econstructor; eauto. eapply Genv.init_mem_transf_partial; eauto. - replace (prog_main tprog) with (prog_main prog). - rewrite symbols_preserved. eauto. - symmetry. apply (transform_partial_program_main transf_fundef _ TRANSF). + econstructor; eauto. eapply (Genv.init_mem_transf_partial TRANSF); eauto. + rewrite (match_program_main TRANSF), symbols_preserved. auto. rewrite <- H3. apply sig_preserved. auto. constructor. constructor. auto. Qed. @@ -566,7 +551,7 @@ Theorem transf_program_correct: forward_simulation (semantics prog) (semantics tprog). Proof. eapply forward_simulation_plus. - eexact public_preserved. + apply senv_preserved. eexact transf_initial_states. eexact transf_final_states. eexact transf_step_correct. diff --git a/backend/Inlining.v b/backend/Inlining.v index 566ab27c..5c8f4419 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -12,15 +12,9 @@ (** RTL function inlining *) -Require Import Coqlib. -Require Import Wfsimpl. -Require Import Errors. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Op. -Require Import Registers. -Require Import RTL. +Require Import Coqlib Wfsimpl Maps Errors Integers. +Require Import AST Linking. +Require Import Op Registers RTL. (** ** Environment of inlinable functions *) diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index ad861543..91f4a3f5 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -12,63 +12,50 @@ (** RTL function inlining: semantic preservation *) -Require Import Coqlib. -Require Import Errors. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Events. -Require Import Smallstep. -Require Import Op. -Require Import Registers. -Require Import Inlining. -Require Import Inliningspec. -Require Import RTL. +Require Import Coqlib Wfsimpl Maps Errors Integers. +Require Import AST Linking Values Memory Globalenvs Events Smallstep. +Require Import Op Registers RTL. +Require Import Inlining Inliningspec. + +Definition match_prog (prog tprog: program) := + match_program (fun cunit f tf => transf_fundef (funenv_program cunit) 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. Section INLINING. 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 fenv := funenv_program prog. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof. - intros. apply Genv.find_symbol_transf_partial with (transf_fundef fenv); auto. -Qed. +Proof (Genv.find_symbol_match TRANSF). -Lemma public_preserved: - forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. -Proof. - intros. apply Genv.public_symbol_transf_partial with (transf_fundef fenv); auto. -Qed. - -Lemma varinfo_preserved: - forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. -Proof. - intros. apply Genv.find_var_info_transf_partial with (transf_fundef fenv); auto. -Qed. +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_match TRANSF). Lemma functions_translated: forall (v: val) (f: fundef), Genv.find_funct ge v = Some f -> - exists f', Genv.find_funct tge v = Some f' /\ transf_fundef fenv f = OK f'. -Proof (Genv.find_funct_transf_partial (transf_fundef fenv) _ TRANSF). + exists cu f', Genv.find_funct tge v = Some f' /\ transf_fundef (funenv_program cu) f = OK f' /\ linkorder cu prog. +Proof (Genv.find_funct_match TRANSF). Lemma function_ptr_translated: forall (b: block) (f: fundef), Genv.find_funct_ptr ge b = Some f -> - exists f', Genv.find_funct_ptr tge b = Some f' /\ transf_fundef fenv f = OK f'. -Proof (Genv.find_funct_ptr_transf_partial (transf_fundef fenv) _ TRANSF). + exists cu f', Genv.find_funct_ptr tge b = Some f' /\ transf_fundef (funenv_program cu) f = OK f' /\ linkorder cu prog. +Proof (Genv.find_funct_ptr_match TRANSF). Lemma sig_function_translated: - forall f f', transf_fundef fenv f = OK f' -> funsig f' = funsig f. + forall cu f f', transf_fundef (funenv_program cu) f = OK f' -> funsig f' = funsig f. Proof. intros. destruct f; Errors.monadInv H. exploit transf_function_spec; eauto. intros SP; inv SP. auto. @@ -382,24 +369,39 @@ Lemma find_function_agree: find_function ge ros rs = Some fd -> agree_regs F ctx rs rs' -> match_globalenvs F bound -> - exists fd', - find_function tge (sros ctx ros) rs' = Some fd' /\ transf_fundef fenv fd = OK fd'. + exists cu fd', + find_function tge (sros ctx ros) rs' = Some fd' /\ transf_fundef (funenv_program cu) fd = OK fd' /\ linkorder cu prog. Proof. intros. destruct ros as [r | id]; simpl in *. - (* register *) - assert (rs'#(sreg ctx r) = rs#r). - exploit Genv.find_funct_inv; eauto. intros [b EQ]. +- (* register *) + assert (EQ: rs'#(sreg ctx r) = rs#r). + { exploit Genv.find_funct_inv; eauto. intros [b EQ]. assert (A: Val.inject F rs#r rs'#(sreg ctx r)). eapply agree_val_reg; eauto. rewrite EQ in A; inv A. inv H1. rewrite DOMAIN in H5. inv H5. auto. apply FUNCTIONS with fd. rewrite EQ in H; rewrite Genv.find_funct_find_funct_ptr in H. auto. - rewrite H2. eapply functions_translated; eauto. - (* symbol *) + } + rewrite EQ. eapply functions_translated; eauto. +- (* symbol *) rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try discriminate. eapply function_ptr_translated; eauto. Qed. +Lemma find_inlined_function: + forall fenv id rs fd f, + fenv_compat prog fenv -> + find_function ge (inr id) rs = Some fd -> + fenv!id = Some f -> + fd = Internal f. +Proof. + intros. + apply H in H1. apply Genv.find_def_symbol in H1. destruct H1 as (b & A & B). + simpl in H0. unfold ge, fundef in H0. rewrite A in H0. + rewrite <- Genv.find_funct_ptr_iff in B. + congruence. +Qed. + (** Translation of builtin arguments. *) Lemma tr_builtin_arg: @@ -465,8 +467,9 @@ Inductive match_stacks (F: meminj) (m m': mem): (MG: match_globalenvs F bound1) (BELOW: Ple bound1 bound), match_stacks F m m' nil nil bound - | match_stacks_cons: forall res f sp pc rs stk f' sp' rs' stk' bound ctx + | match_stacks_cons: forall res f sp pc rs stk f' sp' rs' stk' bound fenv ctx (MS: match_stacks_inside F m m' stk stk' f' ctx sp' rs') + (COMPAT: fenv_compat prog fenv) (FB: tr_funbody fenv f'.(fn_stacksize) ctx f f'.(fn_code)) (AG: agree_regs F ctx rs rs') (SP: F sp = Some(sp', ctx.(dstk))) @@ -498,8 +501,9 @@ with match_stacks_inside (F: meminj) (m m': mem): (RET: ctx.(retinfo) = None) (DSTK: ctx.(dstk) = 0), match_stacks_inside F m m' stk stk' f' ctx sp' rs' - | match_stacks_inside_inlined: forall res f sp pc rs stk stk' f' ctx sp' rs' ctx' + | match_stacks_inside_inlined: forall res f sp pc rs stk stk' f' fenv ctx sp' rs' ctx' (MS: match_stacks_inside F m m' stk stk' f' ctx' sp' rs') + (COMPAT: fenv_compat prog fenv) (FB: tr_funbody fenv f'.(fn_stacksize) ctx' f f'.(fn_code)) (AG: agree_regs F ctx' rs rs') (SP: F sp = Some(sp', ctx'.(dstk))) @@ -597,7 +601,7 @@ Proof. intros. apply IMAGE with delta. eapply INJ; eauto. eapply Plt_le_trans; eauto. auto. auto. (* cons *) - apply match_stacks_cons with (ctx := ctx); auto. + apply match_stacks_cons with (fenv := fenv) (ctx := ctx); auto. eapply match_stacks_inside_invariant; eauto. intros; eapply INJ; eauto; xomega. intros; eapply PERM1; eauto; xomega. @@ -623,7 +627,7 @@ Proof. intros; eapply PERM2; eauto; xomega. intros; eapply PERM3; eauto; xomega. (* inlined *) - apply match_stacks_inside_inlined with (ctx' := ctx'); auto. + apply match_stacks_inside_inlined with (fenv := fenv) (ctx' := ctx'); auto. apply IHmatch_stacks_inside; auto. intros. apply RS. red in BELOW. xomega. apply agree_regs_incr with F; auto. @@ -825,7 +829,7 @@ Proof. Qed. Lemma match_stacks_inside_inlined_tailcall: - forall F m m' stk stk' f' ctx sp' rs' ctx' f, + forall fenv F m m' stk stk' f' ctx sp' rs' ctx' f, match_stacks_inside F m m' stk stk' f' ctx sp' rs' -> context_below ctx ctx' -> context_stack_tailcall ctx f ctx' -> @@ -849,9 +853,10 @@ Qed. (** ** Relating states *) -Inductive match_states: state -> state -> Prop := - | match_regular_states: forall stk f sp pc rs m stk' f' sp' rs' m' F ctx +Inductive match_states: RTL.state -> RTL.state -> Prop := + | match_regular_states: forall stk f sp pc rs m stk' f' sp' rs' m' F fenv ctx (MS: match_stacks_inside F m m' stk stk' f' ctx sp' rs') + (COMPAT: fenv_compat prog fenv) (FB: tr_funbody fenv f'.(fn_stacksize) ctx f f'.(fn_code)) (AG: agree_regs F ctx rs rs') (SP: F sp = Some(sp', ctx.(dstk))) @@ -862,15 +867,17 @@ Inductive match_states: state -> state -> Prop := (SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize)), match_states (State stk f (Vptr sp Int.zero) pc rs m) (State stk' f' (Vptr sp' Int.zero) (spc ctx pc) rs' m') - | match_call_states: forall stk fd args m stk' fd' args' m' F + | match_call_states: forall stk fd args m stk' fd' args' m' cunit F (MS: match_stacks F m m' stk stk' (Mem.nextblock m')) - (FD: transf_fundef fenv fd = OK fd') + (LINK: linkorder cunit prog) + (FD: transf_fundef (funenv_program cunit) fd = OK fd') (VINJ: Val.inject_list F args args') (MINJ: Mem.inject F m m'), match_states (Callstate stk fd args m) (Callstate stk' fd' args' m') - | match_call_regular_states: forall stk f vargs m stk' f' sp' rs' m' F ctx ctx' pc' pc1' rargs + | match_call_regular_states: forall stk f vargs m stk' f' sp' rs' m' F fenv ctx ctx' pc' pc1' rargs (MS: match_stacks_inside F m m' stk stk' f' ctx sp' rs') + (COMPAT: fenv_compat prog fenv) (FB: tr_funbody fenv f'.(fn_stacksize) ctx f f'.(fn_code)) (BELOW: context_below ctx' ctx) (NOP: f'.(fn_code)!pc' = Some(Inop pc1')) @@ -904,7 +911,7 @@ Inductive match_states: state -> state -> Prop := (** ** Forward simulation *) -Definition measure (S: state) : nat := +Definition measure (S: RTL.state) : nat := match S with | State _ _ _ _ _ _ => 1%nat | Callstate _ _ _ _ => 0%nat @@ -912,7 +919,7 @@ Definition measure (S: state) : nat := end. Lemma tr_funbody_inv: - forall sz cts f c pc i, + forall fenv sz cts f c pc i, tr_funbody fenv sz cts f c -> f.(fn_code)!pc = Some i -> tr_instr fenv sz cts pc i c. Proof. intros. inv H. eauto. @@ -927,13 +934,13 @@ Theorem step_simulation: Proof. induction 1; intros; inv MS. -(* nop *) +- (* nop *) exploit tr_funbody_inv; eauto. intros TR; inv TR. left; econstructor; split. eapply plus_one. eapply exec_Inop; eauto. econstructor; eauto. -(* op *) +- (* op *) exploit tr_funbody_inv; eauto. intros TR; inv TR. exploit eval_operation_inject. eapply match_stacks_inside_globals; eauto. @@ -948,7 +955,7 @@ Proof. apply match_stacks_inside_set_reg; auto. apply agree_set_reg; auto. -(* load *) +- (* load *) exploit tr_funbody_inv; eauto. intros TR; inv TR. exploit eval_addressing_inject. eapply match_stacks_inside_globals; eauto. @@ -965,7 +972,7 @@ Proof. apply match_stacks_inside_set_reg; auto. apply agree_set_reg; auto. -(* store *) +- (* store *) exploit tr_funbody_inv; eauto. intros TR; inv TR. exploit eval_addressing_inject. eapply match_stacks_inside_globals; eauto. @@ -989,22 +996,19 @@ Proof. intros; eapply Mem.perm_store_1; eauto. intros. eapply SSZ2. eapply Mem.perm_store_2; eauto. -(* call *) +- (* call *) exploit match_stacks_inside_globalenvs; eauto. intros [bound G]. - exploit find_function_agree; eauto. intros [fd' [A B]]. + exploit find_function_agree; eauto. intros (cu & fd' & A & B & C). exploit tr_funbody_inv; eauto. intros TR; inv TR. -(* not inlined *) ++ (* not inlined *) left; econstructor; split. eapply plus_one. eapply exec_Icall; eauto. eapply sig_function_translated; eauto. econstructor; eauto. eapply match_stacks_cons; eauto. eapply agree_val_regs; eauto. -(* inlined *) - assert (fd = Internal f0). - simpl in H0. destruct (Genv.find_symbol ge id) as [b|] eqn:?; try discriminate. - exploit (funenv_program_compat prog); eauto. intros. - unfold ge in H0. congruence. ++ (* inlined *) + assert (EQ: fd = Internal f0) by (eapply find_inlined_function; eauto). subst fd. right; split. simpl; omega. split. auto. econstructor; eauto. @@ -1013,13 +1017,13 @@ Proof. apply agree_val_regs_gen; auto. red; intros; apply PRIV. destruct H16. omega. -(* tailcall *) +- (* tailcall *) exploit match_stacks_inside_globalenvs; eauto. intros [bound G]. - exploit find_function_agree; eauto. intros [fd' [A B]]. + exploit find_function_agree; eauto. intros (cu & fd' & A & B & C). assert (PRIV': range_private F m' m'0 sp' (dstk ctx) f'.(fn_stacksize)). - eapply range_private_free_left; eauto. inv FB. rewrite <- H4. auto. + { eapply range_private_free_left; eauto. inv FB. rewrite <- H4. auto. } exploit tr_funbody_inv; eauto. intros TR; inv TR. -(* within the original function *) ++ (* within the original function *) inv MS0; try congruence. assert (X: { m1' | Mem.free m'0 sp' 0 (fn_stacksize f') = Some m1'}). apply Mem.range_perm_free. red; intros. @@ -1044,7 +1048,7 @@ Proof. intros. rewrite DSTK in PRIV'. exploit (PRIV' (ofs + delta)). omega. intros [P Q]. eelim Q; eauto. replace (ofs + delta - delta) with ofs by omega. apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem. -(* turned into a call *) ++ (* turned into a call *) left; econstructor; split. eapply plus_one. eapply exec_Icall; eauto. eapply sig_function_translated; eauto. @@ -1054,11 +1058,8 @@ Proof. intros. eapply Mem.perm_free_3; eauto. eapply agree_val_regs; eauto. eapply Mem.free_left_inject; eauto. -(* inlined *) - assert (fd = Internal f0). - simpl in H0. destruct (Genv.find_symbol ge id) as [b|] eqn:?; try discriminate. - exploit (funenv_program_compat prog); eauto. intros. - unfold ge in H0. congruence. ++ (* inlined *) + assert (EQ: fd = Internal f0) by (eapply find_inlined_function; eauto). subst fd. right; split. simpl; omega. split. auto. econstructor; eauto. @@ -1071,7 +1072,7 @@ Proof. assert (dstk ctx <= dstk ctx'). red in H14; rewrite H14. apply align_le. apply min_alignment_pos. omega. -(* builtin *) +- (* builtin *) exploit tr_funbody_inv; eauto. intros TR; inv TR. exploit match_stacks_inside_globalenvs; eauto. intros [bound MG]. exploit tr_builtin_args; eauto. intros (vargs' & P & Q). @@ -1080,14 +1081,13 @@ Proof. intros [F1 [v1 [m1' [A [B [C [D [E [J K]]]]]]]]]. left; econstructor; split. eapply plus_one. eapply exec_Ibuiltin; 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. eapply match_stacks_inside_set_res. eapply match_stacks_inside_extcall with (F1 := F) (F2 := F1) (m1 := m) (m1' := m'0); eauto. intros; eapply external_call_max_perm; eauto. intros; eapply external_call_max_perm; eauto. - auto. + auto. eauto. auto. destruct res; simpl; [apply agree_set_reg;auto|idtac|idtac]; eapply agree_regs_incr; eauto. auto. auto. eapply external_call_valid_block; eauto. @@ -1096,7 +1096,7 @@ Proof. auto. intros. apply SSZ2. eapply external_call_max_perm; eauto. -(* cond *) +- (* cond *) exploit tr_funbody_inv; eauto. intros TR; inv TR. assert (eval_condition cond rs'##(sregs ctx args) m' = Some b). eapply eval_condition_inject; eauto. eapply agree_val_regs; eauto. @@ -1104,7 +1104,7 @@ Proof. eapply plus_one. eapply exec_Icond; eauto. destruct b; econstructor; eauto. -(* jumptable *) +- (* jumptable *) exploit tr_funbody_inv; eauto. intros TR; inv TR. assert (Val.inject F rs#arg rs'#(sreg ctx arg)). eapply agree_val_reg; eauto. rewrite H0 in H2; inv H2. @@ -1113,9 +1113,9 @@ Proof. rewrite list_nth_z_map. rewrite H1. simpl; reflexivity. econstructor; eauto. -(* return *) +- (* return *) exploit tr_funbody_inv; eauto. intros TR; inv TR. - (* not inlined *) ++ (* not inlined *) inv MS0; try congruence. assert (X: { m1' | Mem.free m'0 sp' 0 (fn_stacksize f') = Some m1'}). apply Mem.range_perm_free. red; intros. @@ -1144,7 +1144,7 @@ Proof. eelim B; eauto. replace (ofs + delta - delta) with ofs by omega. apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem. - (* inlined *) ++ (* inlined *) right. split. simpl. omega. split. auto. econstructor; eauto. eapply match_stacks_inside_invariant; eauto. @@ -1153,42 +1153,45 @@ Proof. eapply Mem.free_left_inject; eauto. inv FB. rewrite H4 in PRIV. eapply range_private_free_left; eauto. -(* internal function, not inlined *) - assert (A: exists f', tr_function fenv f f' /\ fd' = Internal f'). - Errors.monadInv FD. exists x. split; auto. eapply transf_function_spec; eauto. - destruct A as [f' [TR EQ]]. inversion TR; subst. +- (* internal function, not inlined *) + assert (A: exists f', tr_function cunit f f' /\ fd' = Internal f'). + { Errors.monadInv FD. exists x. split; auto. eapply transf_function_spec; eauto. } + destruct A as [f' [TR1 EQ]]. + assert (TR: tr_function prog f f'). + { eapply tr_function_linkorder; eauto. } + inversion TR; subst. exploit Mem.alloc_parallel_inject. eauto. eauto. apply Zle_refl. - instantiate (1 := fn_stacksize f'). inv H0. xomega. + instantiate (1 := fn_stacksize f'). inv H1. xomega. intros [F' [m1' [sp' [A [B [C [D E]]]]]]]. left; econstructor; split. eapply plus_one. eapply exec_function_internal; eauto. - rewrite H5. econstructor. + rewrite H6. econstructor. instantiate (1 := F'). apply match_stacks_inside_base. assert (SP: sp' = Mem.nextblock m'0) by (eapply Mem.alloc_result; eauto). rewrite <- SP in MS0. eapply match_stacks_invariant; eauto. intros. destruct (eq_block b1 stk). - subst b1. rewrite D in H7; inv H7. subst b2. eelim Plt_strict; eauto. - rewrite E in H7; auto. + subst b1. rewrite D in H8; inv H8. subst b2. eelim Plt_strict; eauto. + rewrite E in H8; auto. intros. exploit Mem.perm_alloc_inv. eexact H. eauto. destruct (eq_block b1 stk); intros; auto. - subst b1. rewrite D in H7; inv H7. subst b2. eelim Plt_strict; eauto. + subst b1. rewrite D in H8; inv H8. subst b2. eelim Plt_strict; eauto. intros. eapply Mem.perm_alloc_1; eauto. intros. exploit Mem.perm_alloc_inv. eexact A. eauto. rewrite dec_eq_false; auto. - auto. auto. auto. - rewrite H4. apply agree_regs_init_regs. eauto. auto. inv H0; auto. congruence. auto. + auto. auto. auto. eauto. auto. + rewrite H5. apply agree_regs_init_regs. eauto. auto. inv H1; auto. congruence. auto. eapply Mem.valid_new_block; eauto. red; intros. split. - eapply Mem.perm_alloc_2; eauto. inv H0; xomega. + eapply Mem.perm_alloc_2; eauto. inv H1; xomega. intros; red; intros. exploit Mem.perm_alloc_inv. eexact H. eauto. destruct (eq_block b stk); intros. - subst. rewrite D in H8; inv H8. inv H0; xomega. - rewrite E in H8; auto. eelim Mem.fresh_block_alloc. eexact A. eapply Mem.mi_mappedblocks; eauto. + subst. rewrite D in H9; inv H9. inv H1; xomega. + rewrite E in H9; auto. eelim Mem.fresh_block_alloc. eexact A. eapply Mem.mi_mappedblocks; eauto. auto. intros. exploit Mem.perm_alloc_inv; eauto. rewrite dec_eq_true. omega. -(* internal function, inlined *) +- (* internal function, inlined *) inversion FB; subst. exploit Mem.alloc_left_mapped_inject. eauto. @@ -1218,13 +1221,13 @@ Proof. eapply match_stacks_inside_alloc_left; eauto. eapply match_stacks_inside_invariant; eauto. omega. - auto. + eauto. auto. apply agree_regs_incr with F; auto. auto. auto. auto. rewrite H2. eapply range_private_alloc_left; eauto. auto. auto. -(* external function *) +- (* external function *) exploit match_stacks_globalenvs; eauto. intros [bound MG]. exploit external_call_mem_inject; eauto. eapply match_globalenvs_preserves_globals; eauto. @@ -1232,8 +1235,7 @@ Proof. simpl in FD. inv FD. left; econstructor; split. eapply plus_one. eapply exec_function_external; 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. eapply match_stacks_bound with (Mem.nextblock m'0). eapply match_stacks_extcall with (F1 := F) (F2 := F1) (m1 := m) (m1' := m'0); eauto. @@ -1243,43 +1245,38 @@ Proof. eapply external_call_nextblock; eauto. auto. auto. -(* return fron noninlined function *) +- (* return fron noninlined function *) inv MS0. - (* normal case *) ++ (* normal case *) left; econstructor; split. eapply plus_one. eapply exec_return. econstructor; eauto. apply match_stacks_inside_set_reg; auto. apply agree_set_reg; auto. - (* untailcall case *) ++ (* untailcall case *) inv MS; try congruence. rewrite RET in RET0; inv RET0. -(* - assert (rpc = pc). unfold spc in H0; unfold node in *; xomega. - assert (res0 = res). unfold sreg in H1; unfold reg in *; xomega. - subst rpc res0. -*) left; econstructor; split. eapply plus_one. eapply exec_return. eapply match_regular_states. eapply match_stacks_inside_set_reg; eauto. - auto. + eauto. auto. apply agree_set_reg; auto. auto. auto. auto. red; intros. destruct (zlt ofs (dstk ctx)). apply PAD; omega. apply PRIV; omega. auto. auto. -(* return from inlined function *) +- (* return from inlined function *) inv MS0; try congruence. rewrite RET0 in RET; inv RET. unfold inline_return in AT. assert (PRIV': range_private F m m' sp' (dstk ctx' + mstk ctx') f'.(fn_stacksize)). red; intros. destruct (zlt ofs (dstk ctx)). apply PAD. omega. apply PRIV. omega. destruct or. - (* with a result *) ++ (* with a result *) left; econstructor; split. eapply plus_one. eapply exec_Iop; eauto. simpl. reflexivity. econstructor; eauto. apply match_stacks_inside_set_reg; auto. apply agree_set_reg; auto. - (* without a result *) ++ (* without a result *) left; econstructor; split. eapply plus_one. eapply exec_Inop; eauto. econstructor; eauto. subst vres. apply agree_set_reg_undef'; auto. @@ -1289,13 +1286,13 @@ Lemma transf_initial_states: forall st1, initial_state prog st1 -> exists st2, initial_state tprog st2 /\ match_states st1 st2. Proof. intros. inv H. - exploit function_ptr_translated; eauto. intros [tf [FIND TR]]. + exploit function_ptr_translated; eauto. intros (cu & tf & FIND & TR & LINK). exists (Callstate nil tf nil m0); split. econstructor; eauto. - unfold transf_program in TRANSF. eapply Genv.init_mem_transf_partial; eauto. - rewrite symbols_preserved. - rewrite (transform_partial_program_main _ _ TRANSF). auto. - rewrite <- H3. apply sig_function_translated; auto. + eapply (Genv.init_mem_match TRANSF); eauto. + rewrite symbols_preserved. replace (prog_main tprog) with (prog_main prog). auto. + symmetry; eapply match_program_main; eauto. + rewrite <- H3. eapply sig_function_translated; eauto. econstructor; eauto. instantiate (1 := Mem.flat_inj (Mem.nextblock m0)). apply match_stacks_nil with (Mem.nextblock m0). @@ -1322,7 +1319,7 @@ Theorem transf_program_correct: forward_simulation (semantics prog) (semantics tprog). Proof. eapply forward_simulation_star. - eexact public_preserved. + apply senv_preserved. eexact transf_initial_states. eexact transf_final_states. eexact step_simulation. diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index ba62313f..23770cb7 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -12,64 +12,60 @@ (** RTL function inlining: relational specification *) -Require Import Coqlib. -Require Import Wfsimpl. -Require Import Errors. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Globalenvs. -Require Import Op. -Require Import Registers. -Require Import RTL. +Require Import Coqlib Wfsimpl Maps Errors Integers. +Require Import AST Linking. +Require Import Op Registers RTL. Require Import Inlining. (** ** Soundness of function environments. *) -(** A (compile-time) function environment is compatible with a - (run-time) global environment if the following condition holds. *) +(** A compile-time function environment is compatible with a whole + program if the following condition holds. *) -Definition fenv_compat (ge: genv) (fenv: funenv) : Prop := - forall id b f, - fenv!id = Some f -> Genv.find_symbol ge id = Some b -> - Genv.find_funct_ptr ge b = Some (Internal f). +Definition fenv_compat (p: program) (fenv: funenv) : Prop := + forall id f, + fenv!id = Some f -> (prog_defmap p)!id = Some (Gfun (Internal f)). -Remark add_globdef_compat: - forall ge fenv idg, - fenv_compat ge fenv -> - fenv_compat (Genv.add_global ge idg) (Inlining.add_globdef fenv idg). +Lemma funenv_program_compat: + forall p, fenv_compat p (funenv_program p). Proof. - intros. destruct idg as [id gd]. red; simpl; intros. - unfold Genv.find_symbol in H1; simpl in H1. - unfold Genv.find_funct_ptr; simpl. - rewrite PTree.gsspec in H1. destruct (peq id0 id). - (* same *) - subst id0. inv H1. destruct gd. destruct f0. - destruct (should_inline id f0). - rewrite PTree.gss in H0. rewrite PTree.gss. inv H0; auto. - rewrite PTree.grs in H0; discriminate. - rewrite PTree.grs in H0; discriminate. - rewrite PTree.grs in H0; discriminate. - (* different *) - destruct gd. rewrite PTree.gso. eapply H; eauto. - destruct f0. destruct (should_inline id f0). - rewrite PTree.gso in H0; auto. - rewrite PTree.gro in H0; auto. - rewrite PTree.gro in H0; auto. - red; intros; subst b. eelim Plt_strict. eapply Genv.genv_symb_range; eauto. - rewrite PTree.gro in H0; auto. eapply H; eauto. + set (P := fun (dm: PTree.t (globdef fundef unit)) (fenv: funenv) => + forall id f, + fenv!id = Some f -> dm!id = Some (Gfun (Internal f))). + assert (REMOVE: forall dm fenv id g, + P dm fenv -> + P (PTree.set id g dm) (PTree.remove id fenv)). + { unfold P; intros. rewrite PTree.grspec in H0. destruct (PTree.elt_eq id0 id). + discriminate. + rewrite PTree.gso; auto. + } + assert (ADD: forall dm fenv idg, + P dm fenv -> + P (PTree.set (fst idg) (snd idg) dm) (add_globdef fenv idg)). + { intros dm fenv [id g]; simpl; intros. + destruct g as [ [f|ef] | v]; auto. + destruct (should_inline id f); auto. + red; intros. rewrite ! PTree.gsspec in *. + destruct (peq id0 id); auto. inv H0; auto. + } + assert (REC: forall l dm fenv, + P dm fenv -> + P (fold_left (fun x idg => PTree.set (fst idg) (snd idg) x) l dm) + (fold_left add_globdef l fenv)). + { induction l; simpl; intros. + - auto. + - apply IHl. apply ADD; auto. + } + intros. apply REC. red; intros. rewrite PTree.gempty in H; discriminate. Qed. -Lemma funenv_program_compat: - forall p, fenv_compat (Genv.globalenv p) (funenv_program p). +Lemma fenv_compat_linkorder: + forall cunit prog fenv, + linkorder cunit prog -> fenv_compat cunit fenv -> fenv_compat prog fenv. Proof. - intros. - unfold Genv.globalenv, funenv_program. - assert (forall gl ge fenv, - fenv_compat ge fenv -> - fenv_compat (Genv.add_globals ge gl) (fold_left add_globdef gl fenv)). - induction gl; simpl; intros. auto. apply IHgl. apply add_globdef_compat; auto. - apply H. red; intros. rewrite PTree.gempty in H0; discriminate. + intros; red; intros. apply H0 in H1. + destruct (prog_defmap_linkorder _ _ _ _ H H1) as (gd' & P & Q). + inv Q. inv H3. auto. Qed. (** ** Properties of shifting *) @@ -684,29 +680,45 @@ Qed. End INLINING_BODY_SPEC. +End INLINING_SPEC. + (** ** Relational specification of the translation of a function *) -Inductive tr_function: function -> function -> Prop := - | tr_function_intro: forall f f' ctx, - tr_funbody f'.(fn_stacksize) ctx f f'.(fn_code) -> +Inductive tr_function: program -> function -> function -> Prop := + | tr_function_intro: forall p fenv f f' ctx, + fenv_compat p fenv -> + tr_funbody fenv f'.(fn_stacksize) ctx f f'.(fn_code) -> ctx.(dstk) = 0 -> ctx.(retinfo) = None -> f'.(fn_sig) = f.(fn_sig) -> f'.(fn_params) = sregs ctx f.(fn_params) -> f'.(fn_entrypoint) = spc ctx f.(fn_entrypoint) -> 0 <= fn_stacksize f' < Int.max_unsigned -> - tr_function f f'. + tr_function p f f'. + +Lemma tr_function_linkorder: + forall cunit prog f f', + linkorder cunit prog -> + tr_function cunit f f' -> + tr_function prog f f'. +Proof. + intros. inv H0. econstructor; eauto. eapply fenv_compat_linkorder; eauto. +Qed. Lemma transf_function_spec: - forall f f', transf_function fenv f = OK f' -> tr_function f f'. + forall cunit f f', + transf_function (funenv_program cunit) f = OK f' -> + tr_function cunit f f'. Proof. intros. unfold transf_function in H. + set (fenv := funenv_program cunit) in *. destruct (expand_function fenv f initstate) as [ctx s i] eqn:?. destruct (zlt (st_stksize s) Int.max_unsigned); inv H. monadInv Heqr. set (ctx := initcontext x x0 (max_reg_function f) (fn_stacksize f)) in *. Opaque initstate. destruct INCR3. inversion EQ1. inversion EQ. - apply tr_function_intro with ctx; auto. + apply tr_function_intro with fenv ctx; auto. + apply funenv_program_compat. eapply expand_cfg_spec with (fe := fenv); eauto. red; auto. unfold ctx; rewrite <- H1; rewrite <- H2; rewrite <- H3; simpl. xomega. @@ -718,5 +730,3 @@ Opaque initstate. simpl. split; auto. destruct INCR2. destruct INCR1. destruct INCR0. destruct INCR. simpl. change 0 with (st_stksize initstate). omega. Qed. - -End INLINING_SPEC. diff --git a/backend/Linearize.v b/backend/Linearize.v index 68c2b32f..2cfa4d3c 100644 --- a/backend/Linearize.v +++ b/backend/Linearize.v @@ -12,19 +12,9 @@ (** Linearization of the control-flow graph: translation from LTL to Linear *) -Require Import Coqlib. -Require Import Maps. -Require Import Ordered. -Require Import FSets. -Require FSetAVL. -Require Import AST. -Require Import Errors. -Require Import Op. -Require Import Locations. -Require Import LTL. -Require Import Linear. -Require Import Kildall. -Require Import Lattice. +Require Import FSets FSetAVL. +Require Import Coqlib Maps Ordered Errors Lattice Kildall. +Require Import AST Op Locations LTL Linear. Open Scope error_monad_scope. diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index 65258b2d..16717365 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -13,32 +13,29 @@ (** Correctness proof for code linearization *) Require Import FSets. -Require Import Coqlib. -Require Import Maps. -Require Import Ordered. -Require Import Lattice. -Require Import AST. -Require Import Integers. -Require Import Values. -Require Import Memory. -Require Import Events. -Require Import Globalenvs. -Require Import Errors. -Require Import Smallstep. -Require Import Op. -Require Import Locations. -Require Import LTL. -Require Import Linear. +Require Import Coqlib Maps Ordered Errors Lattice Kildall Integers. +Require Import AST Linking. +Require Import Values Memory Events Globalenvs Smallstep. +Require Import Op Locations LTL Linear. Require Import Linearize. Module NodesetFacts := FSetFacts.Facts(Nodeset). +Definition match_prog (p: LTL.program) (tp: Linear.program) := + match_program (fun ctx f tf => transf_fundef f = OK tf) eq p tp. + +Lemma transf_program_match: + forall p tp, transf_program p = OK tp -> match_prog p tp. +Proof. + intros. eapply match_transform_partial_program; eauto. +Qed. + Section LINEARIZATION. Variable prog: LTL.program. Variable tprog: Linear.program. -Hypothesis TRANSF: transf_program prog = OK tprog. +Hypothesis TRANSF: match_prog prog tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. @@ -48,28 +45,23 @@ Lemma functions_translated: Genv.find_funct ge v = Some f -> exists tf, Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf. -Proof (Genv.find_funct_transf_partial transf_fundef _ TRANSF). +Proof (Genv.find_funct_transf_partial TRANSF). Lemma function_ptr_translated: forall v f, Genv.find_funct_ptr ge v = Some f -> exists tf, Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf. -Proof (Genv.find_funct_ptr_transf_partial transf_fundef _ TRANSF). +Proof (Genv.find_funct_ptr_transf_partial TRANSF). Lemma symbols_preserved: forall id, Genv.find_symbol tge id = Genv.find_symbol ge id. -Proof (Genv.find_symbol_transf_partial transf_fundef _ TRANSF). - -Lemma public_preserved: - forall id, - Genv.public_symbol tge id = Genv.public_symbol ge id. -Proof (Genv.public_symbol_transf_partial transf_fundef _ TRANSF). +Proof (Genv.find_symbol_transf_partial TRANSF). -Lemma varinfo_preserved: - forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. -Proof (Genv.find_var_info_transf_partial transf_fundef _ TRANSF). +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_transf_partial TRANSF). Lemma sig_preserved: forall f tf, @@ -645,8 +637,7 @@ Proof. left; econstructor; split. simpl. apply plus_one. eapply exec_Lbuiltin; eauto. eapply 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; eauto. apply senv_preserved. econstructor; eauto. (* Lbranch *) @@ -703,8 +694,7 @@ Proof. (* external function *) monadInv H8. left; econstructor; split. apply plus_one. eapply exec_function_external; 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 *) @@ -721,10 +711,9 @@ Proof. intros. inversion H. exploit function_ptr_translated; eauto. intros [tf [A B]]. exists (Callstate nil tf (Locmap.init Vundef) m0); split. - econstructor; eauto. eapply Genv.init_mem_transf_partial; eauto. - replace (prog_main tprog) with (prog_main prog). + econstructor; eauto. eapply (Genv.init_mem_transf_partial TRANSF); eauto. + rewrite (match_program_main TRANSF). rewrite symbols_preserved. eauto. - symmetry. apply (transform_partial_program_main transf_fundef _ TRANSF). rewrite <- H3. apply sig_preserved. auto. constructor. constructor. auto. Qed. @@ -740,7 +729,7 @@ Theorem transf_program_correct: forward_simulation (LTL.semantics prog) (Linear.semantics tprog). Proof. eapply forward_simulation_star. - eexact public_preserved. + apply senv_preserved. eexact transf_initial_states. eexact transf_final_states. eexact transf_step_correct. diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index f458de8b..ace822fd 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -12,23 +12,10 @@ (** Correctness proof for RTL generation. *) -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Values. -Require Import Memory. -Require Import Events. -Require Import Smallstep. -Require Import Globalenvs. -Require Import Switch. -Require Import Registers. -Require Import Cminor. -Require Import Op. -Require Import CminorSel. -Require Import RTL. -Require Import RTLgen. -Require Import RTLgenspec. +Require Import Coqlib Maps AST Linking. +Require Import Integers Values Memory Events Smallstep Globalenvs. +Require Import Switch Registers Cminor Op CminorSel RTL. +Require Import RTLgen RTLgenspec. (** * Correspondence between Cminor environments and RTL register sets *) @@ -361,11 +348,20 @@ Qed. Require Import Errors. +Definition match_prog (p: CminorSel.program) (tp: RTL.program) := + match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp. + +Lemma transf_program_match: + forall p tp, transl_program p = OK tp -> match_prog p tp. +Proof. + intros. apply match_transform_partial_program; auto. +Qed. + Section CORRECTNESS. Variable prog: CminorSel.program. Variable tprog: RTL.program. -Hypothesis TRANSL: transl_program prog = OK tprog. +Hypothesis TRANSL: match_prog prog tprog. Let ge : CminorSel.genv := Genv.globalenv prog. Let tge : RTL.genv := Genv.globalenv tprog. @@ -376,12 +372,7 @@ Let tge : RTL.genv := Genv.globalenv tprog. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof - (Genv.find_symbol_transf_partial transl_fundef _ TRANSL). - -Lemma public_preserved: - forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. -Proof - (Genv.public_symbol_transf_partial transl_fundef _ TRANSL). + (Genv.find_symbol_transf_partial TRANSL). Lemma function_ptr_translated: forall (b: block) (f: CminorSel.fundef), @@ -389,7 +380,7 @@ Lemma function_ptr_translated: exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf. Proof - (Genv.find_funct_ptr_transf_partial transl_fundef _ TRANSL). + (Genv.find_funct_ptr_transf_partial TRANSL). Lemma functions_translated: forall (v: val) (f: CminorSel.fundef), @@ -397,7 +388,7 @@ Lemma functions_translated: exists tf, Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf. Proof - (Genv.find_funct_transf_partial transl_fundef _ TRANSL). + (Genv.find_funct_transf_partial TRANSL). Lemma sig_transl_function: forall (f: CminorSel.fundef) (tf: RTL.fundef), @@ -414,10 +405,10 @@ Proof. intro. inversion H. reflexivity. Qed. -Lemma varinfo_preserved: - forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. +Lemma senv_preserved: + Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). Proof - (Genv.find_var_info_transf_partial transl_fundef _ TRANSL). + (Genv.senv_transf_partial TRANSL). (** Correctness of the code generated by [add_move]. *) @@ -720,8 +711,7 @@ Proof. change (rs1#rd <- v') with (regmap_setres (BR rd) v' rs1). eapply exec_Ibuiltin; eauto. eapply eval_builtin_args_trivial. - eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. reflexivity. (* Match-env *) split. eauto with rtlg. @@ -754,8 +744,7 @@ Proof. eapply star_left. eapply exec_Icall; eauto. simpl. rewrite symbols_preserved. rewrite H. eauto. auto. eapply star_left. eapply exec_function_external. - eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. apply star_one. apply exec_return. reflexivity. reflexivity. reflexivity. (* Match-env *) @@ -1422,8 +1411,7 @@ Proof. left. eapply plus_right. eexact E. eapply exec_Ibuiltin. eauto. eapply 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. traceEq. econstructor; eauto. constructor. eapply match_env_update_res; eauto. @@ -1540,8 +1528,7 @@ Proof. edestruct external_call_mem_extends as [tvres [tm' [A [B [C D]]]]]; eauto. econstructor; split. left; apply plus_one. eapply exec_function_external; 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. constructor; auto. (* return *) @@ -1559,9 +1546,9 @@ Proof. induction 1. exploit function_ptr_translated; eauto. intros [tf [A B]]. econstructor; split. - econstructor. apply (Genv.init_mem_transf_partial _ _ TRANSL); eauto. - rewrite (transform_partial_program_main _ _ TRANSL). fold tge. - rewrite symbols_preserved. eauto. + econstructor. apply (Genv.init_mem_transf_partial TRANSL); eauto. + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved; eauto. + symmetry; eapply match_program_main; eauto. eexact A. rewrite <- H2. apply sig_transl_function; auto. constructor. auto. constructor. @@ -1579,7 +1566,7 @@ Theorem transf_program_correct: forward_simulation (CminorSel.semantics prog) (RTL.semantics tprog). Proof. eapply forward_simulation_star_wf with (order := lt_state). - eexact public_preserved. + apply senv_preserved. eexact transl_initial_states. eexact transl_final_states. apply lt_state_wf. diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v index f4d9cca3..7cda9425 100644 --- a/backend/Renumberproof.v +++ b/backend/Renumberproof.v @@ -12,21 +12,24 @@ (** Postorder renumbering of RTL control-flow graphs. *) -Require Import Coqlib. -Require Import Maps. -Require Import Postorder. -Require Import Events. -Require Import Globalenvs. -Require Import Smallstep. -Require Import Op. -Require Import Registers. -Require Import RTL. -Require Import Renumber. +Require Import Coqlib Maps Postorder. +Require Import AST Linking. +Require Import Values Memory Globalenvs Events Smallstep. +Require Import Op Registers RTL Renumber. + +Definition match_prog (p tp: RTL.program) := + match_program (fun ctx f tf => tf = transf_fundef f) eq p tp. + +Lemma transf_program_match: + forall p, match_prog p (transf_program p). +Proof. + intros. eapply match_transform_program; eauto. +Qed. Section PRESERVATION. -Variable prog: program. -Let tprog := transf_program prog. +Variables prog tprog: program. +Hypothesis TRANSL: match_prog prog tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. @@ -34,27 +37,22 @@ Lemma functions_translated: forall v f, Genv.find_funct ge v = Some f -> Genv.find_funct tge v = Some (transf_fundef f). -Proof (@Genv.find_funct_transf _ _ _ transf_fundef prog). +Proof (Genv.find_funct_transf TRANSL). Lemma function_ptr_translated: forall v f, Genv.find_funct_ptr ge v = Some f -> Genv.find_funct_ptr tge v = Some (transf_fundef f). -Proof (@Genv.find_funct_ptr_transf _ _ _ transf_fundef prog). +Proof (Genv.find_funct_ptr_transf TRANSL). Lemma symbols_preserved: forall id, Genv.find_symbol tge id = Genv.find_symbol ge id. -Proof (@Genv.find_symbol_transf _ _ _ transf_fundef prog). - -Lemma public_preserved: - forall id, - Genv.public_symbol tge id = Genv.public_symbol ge id. -Proof (@Genv.public_symbol_transf _ _ _ transf_fundef prog). +Proof (Genv.find_symbol_transf TRANSL). -Lemma varinfo_preserved: - forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. -Proof (@Genv.find_var_info_transf _ _ _ transf_fundef prog). +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_transf TRANSL). Lemma sig_preserved: forall f, funsig (transf_fundef f) = funsig f. @@ -199,8 +197,7 @@ Proof. econstructor; split. eapply exec_Ibuiltin; eauto. eapply 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; eauto. apply senv_preserved. constructor; auto. eapply reach_succ; eauto. simpl; auto. (* cond *) econstructor; split. @@ -224,8 +221,7 @@ Proof. (* external function *) econstructor; split. eapply exec_function_external; 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. constructor; auto. (* return *) inv STACKS. inv H1. @@ -240,8 +236,8 @@ Lemma transf_initial_states: Proof. intros. inv H. econstructor; split. econstructor. - eapply Genv.init_mem_transf; eauto. - simpl. rewrite symbols_preserved. eauto. + eapply (Genv.init_mem_transf TRANSL); eauto. + rewrite symbols_preserved. rewrite (match_program_main TRANSL). eauto. eapply function_ptr_translated; eauto. rewrite <- H3; apply sig_preserved. constructor. constructor. @@ -257,7 +253,7 @@ Theorem transf_program_correct: forward_simulation (RTL.semantics prog) (RTL.semantics tprog). Proof. eapply forward_simulation_step. - eexact public_preserved. + apply senv_preserved. eexact transf_initial_states. eexact transf_final_states. exact step_simulation. diff --git a/backend/SelectLongproof.v b/backend/SelectLongproof.v index 35d53215..f15015e8 100644 --- a/backend/SelectLongproof.v +++ b/backend/SelectLongproof.v @@ -14,6 +14,7 @@ Require Import String. Require Import Coqlib. +Require Import Maps. Require Import AST. Require Import Errors. Require Import Integers. @@ -36,7 +37,7 @@ Open Local Scope string_scope. Definition external_implements (name: string) (sg: signature) (vargs: list val) (vres: val) : Prop := forall F V (ge: Genv.t F V) m, - external_call (EF_external name sg) ge vargs m E0 vres m. + external_call (EF_runtime name sg) ge vargs m E0 vres m. Definition builtin_implements (name: string) (sg: signature) (vargs: list val) (vres: val) : Prop := forall F V (ge: Genv.t F V) m, @@ -61,32 +62,32 @@ Axiom i64_helpers_correct : /\ (forall x y, external_implements "__i64_shr" sig_li_l (x::y::nil) (Val.shrlu x y)) /\ (forall x y, external_implements "__i64_sar" sig_li_l (x::y::nil) (Val.shrl x y)). -Definition helper_declared {F V: Type} (ge: Genv.t (AST.fundef F) V) (id: ident) (name: string) (sg: signature) : Prop := - exists b, Genv.find_symbol ge id = Some b - /\ Genv.find_funct_ptr ge b = Some (External (EF_external name sg)). - -Definition helper_functions_declared {F V: Type} (ge: Genv.t (AST.fundef F) V) (hf: helper_functions) : Prop := - helper_declared ge hf.(i64_dtos) "__i64_dtos" sig_f_l - /\ helper_declared ge hf.(i64_dtou) "__i64_dtou" sig_f_l - /\ helper_declared ge hf.(i64_stod) "__i64_stod" sig_l_f - /\ helper_declared ge hf.(i64_utod) "__i64_utod" sig_l_f - /\ helper_declared ge hf.(i64_stof) "__i64_stof" sig_l_s - /\ helper_declared ge hf.(i64_utof) "__i64_utof" sig_l_s - /\ helper_declared ge hf.(i64_sdiv) "__i64_sdiv" sig_ll_l - /\ helper_declared ge hf.(i64_udiv) "__i64_udiv" sig_ll_l - /\ helper_declared ge hf.(i64_smod) "__i64_smod" sig_ll_l - /\ helper_declared ge hf.(i64_umod) "__i64_umod" sig_ll_l - /\ helper_declared ge hf.(i64_shl) "__i64_shl" sig_li_l - /\ helper_declared ge hf.(i64_shr) "__i64_shr" sig_li_l - /\ helper_declared ge hf.(i64_sar) "__i64_sar" sig_li_l. +Definition helper_declared {F V: Type} (p: AST.program (AST.fundef F) V) (id: ident) (name: string) (sg: signature) : Prop := + (prog_defmap p)!id = Some (Gfun (External (EF_runtime name sg))). + +Definition helper_functions_declared {F V: Type} (p: AST.program (AST.fundef F) V) (hf: helper_functions) : Prop := + helper_declared p hf.(i64_dtos) "__i64_dtos" sig_f_l + /\ helper_declared p hf.(i64_dtou) "__i64_dtou" sig_f_l + /\ helper_declared p hf.(i64_stod) "__i64_stod" sig_l_f + /\ helper_declared p hf.(i64_utod) "__i64_utod" sig_l_f + /\ helper_declared p hf.(i64_stof) "__i64_stof" sig_l_s + /\ helper_declared p hf.(i64_utof) "__i64_utof" sig_l_s + /\ helper_declared p hf.(i64_sdiv) "__i64_sdiv" sig_ll_l + /\ helper_declared p hf.(i64_udiv) "__i64_udiv" sig_ll_l + /\ helper_declared p hf.(i64_smod) "__i64_smod" sig_ll_l + /\ helper_declared p hf.(i64_umod) "__i64_umod" sig_ll_l + /\ helper_declared p hf.(i64_shl) "__i64_shl" sig_li_l + /\ helper_declared p hf.(i64_shr) "__i64_shr" sig_li_l + /\ helper_declared p hf.(i64_sar) "__i64_sar" sig_li_l. (** * Correctness of the instruction selection functions for 64-bit operators *) Section CMCONSTR. -Variable ge: genv. +Variable prog: program. Variable hf: helper_functions. -Hypothesis HELPERS: helper_functions_declared ge hf. +Hypothesis HELPERS: helper_functions_declared prog hf. +Let ge := Genv.globalenv prog. Variable sp: val. Variable e: env. Variable m: mem. @@ -97,17 +98,20 @@ Ltac DeclHelper := red in HELPERS; decompose [Logic.and] HELPERS; eauto. Lemma eval_helper: forall le id name sg args vargs vres, eval_exprlist ge sp e m le args vargs -> - helper_declared ge id name sg -> + helper_declared prog id name sg -> external_implements name sg vargs vres -> eval_expr ge sp e m le (Eexternal id sg args) vres. Proof. - intros. destruct H0 as (b & P & Q). econstructor; eauto. + intros. + red in H0. apply Genv.find_def_symbol in H0. destruct H0 as (b & P & Q). + rewrite <- Genv.find_funct_ptr_iff in Q. + econstructor; eauto. Qed. Corollary eval_helper_1: forall le id name sg arg1 varg1 vres, eval_expr ge sp e m le arg1 varg1 -> - helper_declared ge id name sg -> + helper_declared prog id name sg -> external_implements name sg (varg1::nil) vres -> eval_expr ge sp e m le (Eexternal id sg (arg1 ::: Enil)) vres. Proof. @@ -118,7 +122,7 @@ Corollary eval_helper_2: forall le id name sg arg1 arg2 varg1 varg2 vres, eval_expr ge sp e m le arg1 varg1 -> eval_expr ge sp e m le arg2 varg2 -> - helper_declared ge id name sg -> + helper_declared prog id name sg -> external_implements name sg (varg1::varg2::nil) vres -> eval_expr ge sp e m le (Eexternal id sg (arg1 ::: arg2 ::: Enil)) vres. Proof. @@ -845,7 +849,7 @@ Qed. Lemma eval_binop_long: forall id name sem le a b x y z, (forall p q, x = Vlong p -> y = Vlong q -> z = Vlong (sem p q)) -> - helper_declared ge id name sig_ll_l -> + helper_declared prog id name sig_ll_l -> external_implements name sig_ll_l (x::y::nil) z -> eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> diff --git a/backend/Selection.v b/backend/Selection.v index dcefdd1c..02b37c48 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -69,6 +69,8 @@ Definition store (chunk: memory_chunk) (e1 e2: expr) := Section SELECTION. +Definition globdef := AST.globdef Cminor.fundef unit. +Variable defmap: PTree.t globdef. Variable hf: helper_functions. Definition sel_constant (cst: Cminor.constant) : expr := @@ -194,17 +196,13 @@ Definition expr_is_addrof_ident (e: Cminor.expr) : option ident := | _ => None end. -Definition classify_call (ge: Cminor.genv) (e: Cminor.expr) : call_kind := +Definition classify_call (e: Cminor.expr) : call_kind := match expr_is_addrof_ident e with | None => Call_default | Some id => - match Genv.find_symbol ge id with - | None => Call_imm id - | Some b => - match Genv.find_funct_ptr ge b with - | Some(External ef) => if ef_inline ef then Call_builtin ef else Call_imm id - | _ => Call_imm id - end + match defmap!id with + | Some(Gfun(External ef)) => if ef_inline ef then Call_builtin ef else Call_imm id + | _ => Call_imm id end end. @@ -279,13 +277,13 @@ Definition sel_switch_long := (** Conversion from Cminor statements to Cminorsel statements. *) -Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : res stmt := +Fixpoint sel_stmt (s: Cminor.stmt) : res stmt := match s with | Cminor.Sskip => OK Sskip | Cminor.Sassign id e => OK (Sassign id (sel_expr e)) | Cminor.Sstore chunk addr rhs => OK (store chunk (sel_expr addr) (sel_expr rhs)) | Cminor.Scall optid sg fn args => - OK (match classify_call ge fn with + OK (match classify_call fn with | Call_default => Scall optid sg (inl _ (sel_expr fn)) (sel_exprlist args) | Call_imm id => Scall optid sg (inr _ id) (sel_exprlist args) | Call_builtin ef => Sbuiltin (sel_builtin_res optid) ef @@ -296,20 +294,20 @@ Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : res stmt := OK (Sbuiltin (sel_builtin_res optid) ef (sel_builtin_args args (Machregs.builtin_constraints ef))) | Cminor.Stailcall sg fn args => - OK (match classify_call ge fn with + OK (match classify_call fn with | Call_imm id => Stailcall sg (inr _ id) (sel_exprlist args) | _ => Stailcall sg (inl _ (sel_expr fn)) (sel_exprlist args) end) | Cminor.Sseq s1 s2 => - do s1' <- sel_stmt ge s1; do s2' <- sel_stmt ge s2; + do s1' <- sel_stmt s1; do s2' <- sel_stmt s2; OK (Sseq s1' s2') | Cminor.Sifthenelse e ifso ifnot => - do ifso' <- sel_stmt ge ifso; do ifnot' <- sel_stmt ge ifnot; + do ifso' <- sel_stmt ifso; do ifnot' <- sel_stmt ifnot; OK (Sifthenelse (condexpr_of_expr (sel_expr e)) ifso' ifnot') | Cminor.Sloop body => - do body' <- sel_stmt ge body; OK (Sloop body') + do body' <- sel_stmt body; OK (Sloop body') | Cminor.Sblock body => - do body' <- sel_stmt ge body; OK (Sblock body') + do body' <- sel_stmt body; OK (Sblock body') | Cminor.Sexit n => OK (Sexit n) | Cminor.Sswitch false e cases dfl => let t := compile_switch Int.modulus dfl cases in @@ -324,14 +322,14 @@ Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : res stmt := | Cminor.Sreturn None => OK (Sreturn None) | Cminor.Sreturn (Some e) => OK (Sreturn (Some (sel_expr e))) | Cminor.Slabel lbl body => - do body' <- sel_stmt ge body; OK (Slabel lbl body') + do body' <- sel_stmt body; OK (Slabel lbl body') | Cminor.Sgoto lbl => OK (Sgoto lbl) end. (** Conversion of functions. *) -Definition sel_function (ge: Cminor.genv) (f: Cminor.function) : res function := - do body' <- sel_stmt ge f.(Cminor.fn_body); +Definition sel_function (f: Cminor.function) : res function := + do body' <- sel_stmt f.(Cminor.fn_body); OK (mkfunction f.(Cminor.fn_sig) f.(Cminor.fn_params) @@ -339,41 +337,36 @@ Definition sel_function (ge: Cminor.genv) (f: Cminor.function) : res function := f.(Cminor.fn_stackspace) body'). -Definition sel_fundef (ge: Cminor.genv) (f: Cminor.fundef) : res fundef := - transf_partial_fundef (sel_function ge) f. +Definition sel_fundef (f: Cminor.fundef) : res fundef := + transf_partial_fundef sel_function f. End SELECTION. (** Setting up the helper functions. *) -Definition globdef := AST.globdef Cminor.fundef unit. - (** We build a partial mapping from global identifiers to their definitions, restricting ourselves to the globals we are interested in, namely - the external function declarations whose name starts with "__i64_". + the external function declarations that are marked as runtime library + helpers. This ensures that the mapping remains small and that [lookup_helper] below is efficient. *) Definition globdef_of_interest (gd: globdef) : bool := match gd with - | Gfun (External (EF_external name sg)) => String.prefix "__i64_" name + | Gfun (External (EF_runtime name sg)) => true | _ => false end. -Definition record_globdef (globs: PTree.t globdef) (id_gd: ident * globdef) := - let (id, gd) := id_gd in - if globdef_of_interest gd - then PTree.set id gd globs - else PTree.remove id globs. - -Definition record_globdefs (p: Cminor.program) : PTree.t globdef := - List.fold_left record_globdef p.(prog_defs) (PTree.empty _). +Definition record_globdefs (defmap: PTree.t globdef) : PTree.t globdef := + PTree.fold + (fun m id gd => if globdef_of_interest gd then PTree.set id gd m else m) + defmap (PTree.empty globdef). Definition lookup_helper_aux (name: String.string) (sg: signature) (res: option ident) (id: ident) (gd: globdef) := match gd with - | Gfun (External (EF_external name' sg')) => + | Gfun (External (EF_runtime name' sg')) => if String.string_dec name name' && signature_eq sg sg' then Some id else res @@ -389,8 +382,8 @@ Definition lookup_helper (globs: PTree.t globdef) Local Open Scope string_scope. -Definition get_helpers (p: Cminor.program) : res helper_functions := - let globs := record_globdefs p in +Definition get_helpers (defmap: PTree.t globdef) : res helper_functions := + let globs := record_globdefs defmap in do i64_dtos <- lookup_helper globs "__i64_dtos" sig_f_l ; do i64_dtou <- lookup_helper globs "__i64_dtou" sig_f_l ; do i64_stod <- lookup_helper globs "__i64_stod" sig_l_f ; @@ -412,6 +405,7 @@ Definition get_helpers (p: Cminor.program) : res helper_functions := (** Conversion of programs. *) Definition sel_program (p: Cminor.program) : res program := - do hf <- get_helpers p; - transform_partial_program (sel_fundef hf (Genv.globalenv p)) p. + let dm := prog_defmap p in + do hf <- get_helpers dm; + transform_partial_program (sel_fundef dm hf) p. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 8051df59..aad3add4 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -15,6 +15,7 @@ Require Import Coqlib. Require Import Maps. Require Import AST. +Require Import Linking. Require Import Errors. Require Import Integers. Require Import Values. @@ -37,6 +38,92 @@ Require Import SelectLongproof. Local Open Scope cminorsel_scope. Local Open Scope error_monad_scope. +(** * Relational specification of instruction selection *) + +Definition match_fundef (cunit: Cminor.program) (f: Cminor.fundef) (tf: CminorSel.fundef) : Prop := + exists hf, helper_functions_declared cunit hf /\ sel_fundef (prog_defmap cunit) hf f = OK tf. + +Definition match_prog (p: Cminor.program) (tp: CminorSel.program) := + match_program match_fundef eq p tp. + +(** Processing of helper functions *) + +Lemma record_globdefs_sound: + forall dm id gd, (record_globdefs dm)!id = Some gd -> dm!id = Some gd. +Proof. + intros. + set (f := fun m id gd => if globdef_of_interest gd then PTree.set id gd m else m) in *. + set (P := fun m m' => m'!id = Some gd -> m!id = Some gd). + assert (X: P dm (PTree.fold f dm (PTree.empty _))). + { apply PTree_Properties.fold_rec. + - unfold P; intros. rewrite <- H0; auto. + - red. rewrite ! PTree.gempty. auto. + - unfold P; intros. rewrite PTree.gsspec. unfold f in H3. + destruct (globdef_of_interest v). + + rewrite PTree.gsspec in H3. destruct (peq id k); auto. + + apply H2 in H3. destruct (peq id k). congruence. auto. } + apply X. auto. +Qed. + +Lemma lookup_helper_correct_1: + forall globs name sg id, + lookup_helper globs name sg = OK id -> + globs!id = Some (Gfun (External (EF_runtime name sg))). +Proof. + intros. + set (P := fun (m: PTree.t globdef) res => res = Some id -> m!id = Some(Gfun(External (EF_runtime name sg)))). + assert (P globs (PTree.fold (lookup_helper_aux name sg) globs None)). + { apply PTree_Properties.fold_rec; red; intros. + - rewrite <- H0. apply H1; auto. + - discriminate. + - assert (EITHER: k = id /\ v = Gfun (External (EF_runtime name sg)) + \/ a = Some id). + { unfold lookup_helper_aux in H3. destruct v; auto. destruct f; auto. destruct e; auto. + destruct (String.string_dec name name0); auto. + destruct (signature_eq sg sg0); auto. + inversion H3. left; split; auto. repeat f_equal; auto. } + destruct EITHER as [[X Y] | X]. + subst k v. apply PTree.gss. + apply H2 in X. rewrite PTree.gso by congruence. auto. + } + red in H0. unfold lookup_helper in H. + destruct (PTree.fold (lookup_helper_aux name sg) globs None); inv H. auto. +Qed. + +Lemma lookup_helper_correct: + forall p name sg id, + lookup_helper (record_globdefs (prog_defmap p)) name sg = OK id -> + helper_declared p id name sg. +Proof. + intros. apply lookup_helper_correct_1 in H. apply record_globdefs_sound in H. auto. +Qed. + +Lemma get_helpers_correct: + forall p hf, + get_helpers (prog_defmap p) = OK hf -> helper_functions_declared p hf. +Proof. + intros. monadInv H. red; simpl. auto 20 using lookup_helper_correct. +Qed. + +Theorem transf_program_match: + forall p tp, sel_program p = OK tp -> match_prog p tp. +Proof. + intros. monadInv H. + eapply match_transform_partial_program_contextual. eexact EQ0. + intros. exists x; split; auto. apply get_helpers_correct; auto. +Qed. + +Lemma helper_functions_declared_linkorder: + forall (p p': Cminor.program) hf, + helper_functions_declared p hf -> linkorder p p' -> helper_functions_declared p' hf. +Proof. + intros. + assert (X: forall id name sg, helper_declared p id name sg -> helper_declared p' id name sg). + { unfold helper_declared; intros. + destruct (prog_defmap_linkorder _ _ _ _ H0 H1) as (gd & P & Q). + inv Q. inv H3. auto. } + red in H. decompose [Logic.and] H; clear H. red; auto 20. +Qed. (** * Correctness of the instruction selection functions for expressions *) @@ -46,75 +133,68 @@ Variable prog: Cminor.program. Variable tprog: CminorSel.program. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. -Variable hf: helper_functions. -Hypothesis HELPERS: helper_functions_declared ge hf. -Hypothesis TRANSFPROG: transform_partial_program (sel_fundef hf ge) prog = OK tprog. +Hypothesis TRANSF: match_prog prog tprog. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof. - intros. eapply Genv.find_symbol_transf_partial; eauto. -Qed. +Proof (Genv.find_symbol_match TRANSF). -Lemma public_preserved: - forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. -Proof. - intros. eapply Genv.public_symbol_transf_partial; eauto. -Qed. +Lemma senv_preserved: + Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). +Proof (Genv.senv_match TRANSF). Lemma function_ptr_translated: forall (b: block) (f: Cminor.fundef), Genv.find_funct_ptr ge b = Some f -> - exists tf, Genv.find_funct_ptr tge b = Some tf /\ sel_fundef hf ge f = OK tf. -Proof. - intros. eapply Genv.find_funct_ptr_transf_partial; eauto. -Qed. + exists cu tf, Genv.find_funct_ptr tge b = Some tf /\ match_fundef cu f tf /\ linkorder cu prog. +Proof (Genv.find_funct_ptr_match TRANSF). Lemma functions_translated: forall (v v': val) (f: Cminor.fundef), Genv.find_funct ge v = Some f -> Val.lessdef v v' -> - exists tf, Genv.find_funct tge v' = Some tf /\ sel_fundef hf ge f = OK tf. + exists cu tf, Genv.find_funct tge v' = Some tf /\ match_fundef cu f tf /\ linkorder cu prog. Proof. intros. inv H0. - eapply Genv.find_funct_transf_partial; eauto. - simpl in H. discriminate. + eapply Genv.find_funct_match; eauto. + discriminate. Qed. Lemma sig_function_translated: - forall f tf, sel_fundef hf ge f = OK tf -> funsig tf = Cminor.funsig f. + forall cu f tf, match_fundef cu f tf -> funsig tf = Cminor.funsig f. Proof. - intros. destruct f; monadInv H; auto. monadInv EQ. auto. + intros. destruct H as (hf & P & Q). destruct f; monadInv Q; auto. monadInv EQ; auto. Qed. Lemma stackspace_function_translated: - forall f tf, sel_function hf ge f = OK tf -> fn_stackspace tf = Cminor.fn_stackspace f. + forall dm hf f tf, sel_function dm hf f = OK tf -> fn_stackspace tf = Cminor.fn_stackspace f. Proof. intros. monadInv H. auto. Qed. -Lemma varinfo_preserved: - forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. +Lemma helper_functions_preserved: + forall hf, helper_functions_declared prog hf -> helper_functions_declared tprog hf. Proof. - intros; eapply Genv.find_var_info_transf_partial; eauto. + assert (X: forall id name sg, helper_declared prog id name sg -> helper_declared tprog id name sg). + { unfold helper_declared; intros. + generalize (match_program_defmap _ _ _ _ _ TRANSF id). + unfold Cminor.fundef; rewrite H; intros R; inv R. inv H2. + destruct H4 as (cu & A & B). monadInv B. auto. } + unfold helper_functions_declared; intros. decompose [Logic.and] H; clear H. auto 20. Qed. -Lemma helper_declared_preserved: - forall id name sg, helper_declared ge id name sg -> helper_declared tge id name sg. -Proof. - intros id name sg (b & A & B). - exploit function_ptr_translated; eauto. simpl. intros (tf & P & Q). inv Q. - exists b; split; auto. rewrite symbols_preserved. auto. -Qed. +Section CMCONSTR. + +Variable cunit: Cminor.program. +Variable hf: helper_functions. +Hypothesis LINK: linkorder cunit prog. +Hypothesis HF: helper_functions_declared cunit hf. -Let HELPERS': helper_functions_declared tge hf. +Let HF': helper_functions_declared tprog hf. Proof. - red in HELPERS; decompose [Logic.and] HELPERS. - red. auto 20 using helper_declared_preserved. + apply helper_functions_preserved. eapply helper_functions_declared_linkorder; eauto. Qed. -Section CMCONSTR. - Variable sp: val. Variable e: env. Variable m: mem. @@ -172,6 +252,7 @@ Lemma eval_sel_unop: forall le op a1 v1 v, eval_expr tge sp e m le a1 v1 -> eval_unop op v1 = Some v -> + exists v', eval_expr tge sp e m le (sel_unop hf op a1) v' /\ Val.lessdef v v'. Proof. destruct op; simpl; intros; FuncInv; try subst v. @@ -276,26 +357,30 @@ Proof. Qed. Lemma classify_call_correct: - forall sp e m a v fd, + forall unit sp e m a v fd, + linkorder unit prog -> Cminor.eval_expr ge sp e m a v -> Genv.find_funct ge v = Some fd -> - match classify_call ge a with + match classify_call (prog_defmap unit) a with | Call_default => True | Call_imm id => exists b, Genv.find_symbol ge id = Some b /\ v = Vptr b Int.zero | Call_builtin ef => fd = External ef end. Proof. unfold classify_call; intros. - destruct (expr_is_addrof_ident a) as [id|] eqn:?. + destruct (expr_is_addrof_ident a) as [id|] eqn:EA; auto. exploit expr_is_addrof_ident_correct; eauto. intros EQ; subst a. - inv H. inv H2. - destruct (Genv.find_symbol ge id) as [b|] eqn:?. - rewrite Genv.find_funct_find_funct_ptr in H0. - rewrite H0. - destruct fd. exists b; auto. - destruct (ef_inline e0). auto. exists b; auto. - simpl in H0. discriminate. - auto. + inv H0. inv H3. + destruct (Genv.find_symbol ge id) as [b|] eqn:FS; try discriminate. + rewrite Genv.find_funct_find_funct_ptr in H1. + assert (DFL: exists b1, Genv.find_symbol ge id = Some b1 /\ Vptr b Int.zero = Vptr b1 Int.zero) by (exists b; auto). + unfold globdef; destruct (prog_defmap unit)!id as [[[f|ef] |gv] |] eqn:G; auto. + destruct (ef_inline ef) eqn:INLINE; auto. + destruct (prog_defmap_linkorder _ _ _ _ H G) as (gd & P & Q). + inv Q. inv H2. +- apply Genv.find_def_symbol in P. destruct P as (b' & X & Y). fold ge in X, Y. + rewrite <- Genv.find_funct_ptr_iff in Y. congruence. +- simpl in INLINE. discriminate. Qed. (** Translation of [switch] statements *) @@ -547,6 +632,13 @@ Qed. (** Semantic preservation for expressions. *) +Section EXPRESSIONS. + +Variable cunit: Cminor.program. +Variable hf: helper_functions. +Hypothesis LINK: linkorder cunit prog. +Hypothesis HF: helper_functions_declared cunit hf. + Lemma sel_expr_correct: forall sp e m a v, Cminor.eval_expr ge sp e m a v -> @@ -576,7 +668,7 @@ Proof. exploit IHeval_expr1; eauto. intros [v1' [A B]]. exploit IHeval_expr2; eauto. intros [v2' [C D]]. exploit eval_binop_lessdef; eauto. intros [v' [E F]]. - exploit eval_sel_binop. eexact A. eexact C. eauto. intros [v'' [P Q]]. + exploit eval_sel_binop. eexact LINK. eexact HF. eexact A. eexact C. eauto. intros [v'' [P Q]]. exists v''; split; eauto. eapply Val.lessdef_trans; eauto. (* Eload *) exploit IHeval_expr; eauto. intros [vaddr' [A B]]. @@ -641,51 +733,89 @@ Proof. intros. destruct oid; simpl; auto. apply set_var_lessdef; auto. Qed. +End EXPRESSIONS. + (** Semantic preservation for functions and statements. *) -Inductive match_cont: Cminor.cont -> CminorSel.cont -> Prop := - | match_cont_stop: - match_cont Cminor.Kstop Kstop - | match_cont_seq: forall s s' k k', - sel_stmt hf ge s = OK s' -> - match_cont k k' -> - match_cont (Cminor.Kseq s k) (Kseq s' k') - | match_cont_block: forall k k', - match_cont k k' -> - match_cont (Cminor.Kblock k) (Kblock k') - | match_cont_call: forall id f sp e k f' e' k', - sel_function hf ge f = OK f' -> - match_cont k k' -> env_lessdef e e' -> - match_cont (Cminor.Kcall id f sp e k) (Kcall id f' sp e' k'). +(* +Inductive match_call_cont: Cminor.cont -> CminorSel.cont -> Prop := + | match_call_cont_stop: + match_call_cont Cminor.Kstop Kstop + | match_call_cont_call: forall cunit hf id f sp e k f' e' k', + linkorder cunit prog -> + helper_functions_declared cunit hf -> + sel_function (prog_defmap cunit) hf f = OK f' -> + match_cont cunit hf k k' -> env_lessdef e e' -> + match_call_cont (Cminor.Kcall id f sp e k) (Kcall id f' sp e' k') + +with match_cont: Cminor.program -> helper_functions -> Cminor.cont -> CminorSel.cont -> Prop := + | match_cont_stop: forall cunit hf, + match_cont cunit hf Cminor.Kstop Kstop + | match_cont_seq: forall cunit hf s s' k k', + sel_stmt (prog_defmap cunit) hf s = OK s' -> + match_cont cunit hf k k' -> + match_cont cunit hf (Cminor.Kseq s k) (Kseq s' k') + | match_cont_block: forall cunit hf k k', + match_cont cunit hf k k' -> + match_cont cunit hf (Cminor.Kblock k) (Kblock k') + | match_cont_call: forall cunit hf id f sp e k f' e' k', + match_call_cont (Cminor.Kcall id f sp e k) (Kcall id f' sp e' k') -> + match_cont cunit hf (Cminor.Kcall id f sp e k) (Kcall id f' sp e' k'). +*) + +Inductive match_cont: Cminor.program -> helper_functions -> Cminor.cont -> CminorSel.cont -> Prop := + | match_cont_stop: forall cunit hf, + match_cont cunit hf Cminor.Kstop Kstop + | match_cont_seq: forall cunit hf s s' k k', + sel_stmt (prog_defmap cunit) hf s = OK s' -> + match_cont cunit hf k k' -> + match_cont cunit hf (Cminor.Kseq s k) (Kseq s' k') + | match_cont_block: forall cunit hf k k', + match_cont cunit hf k k' -> + match_cont cunit hf (Cminor.Kblock k) (Kblock k') + | match_cont_call: forall cunit' hf' cunit hf id f sp e k f' e' k', + linkorder cunit prog -> + helper_functions_declared cunit hf -> + sel_function (prog_defmap cunit) hf f = OK f' -> + match_cont cunit hf k k' -> env_lessdef e e' -> + match_cont cunit' hf' (Cminor.Kcall id f sp e k) (Kcall id f' sp e' k'). + +Definition match_call_cont (k: Cminor.cont) (k': CminorSel.cont) : Prop := + forall cunit hf, match_cont cunit hf k k'. Inductive match_states: Cminor.state -> CminorSel.state -> Prop := - | match_state: forall f f' s k s' k' sp e m e' m' - (TF: sel_function hf ge f = OK f') - (TS: sel_stmt hf ge s = OK s') - (MC: match_cont k k') + | match_state: forall cunit hf f f' s k s' k' sp e m e' m' + (LINK: linkorder cunit prog) + (HF: helper_functions_declared cunit hf) + (TF: sel_function (prog_defmap cunit) hf f = OK f') + (TS: sel_stmt (prog_defmap cunit) hf s = OK s') + (MC: match_cont cunit hf k k') (LD: env_lessdef e e') (ME: Mem.extends m m'), match_states (Cminor.State f s k sp e m) (State f' s' k' sp e' m') - | match_callstate: forall f f' args args' k k' m m' - (TF: sel_fundef hf ge f = OK f') - (MC: match_cont k k') + | match_callstate: forall cunit f f' args args' k k' m m' + (LINK: linkorder cunit prog) + (TF: match_fundef cunit f f') + (MC: match_call_cont k k') (LD: Val.lessdef_list args args') (ME: Mem.extends m m'), match_states (Cminor.Callstate f args k m) (Callstate f' args' k' m') | match_returnstate: forall v v' k k' m m' - (MC: match_cont k k') + (MC: match_call_cont k k') (LD: Val.lessdef v v') (ME: Mem.extends m m'), match_states (Cminor.Returnstate v k m) (Returnstate v' k' m') - | match_builtin_1: forall ef args args' optid f sp e k m al f' e' k' m' - (TF: sel_function hf ge f = OK f') - (MC: match_cont k k') + | match_builtin_1: forall cunit hf ef args args' optid f sp e k m al f' e' k' m' + (LINK: linkorder cunit prog) + (HF: helper_functions_declared cunit hf) + (TF: sel_function (prog_defmap cunit) hf f = OK f') + (MC: match_cont cunit hf k k') (LDA: Val.lessdef_list args args') (LDE: env_lessdef e e') (ME: Mem.extends m m') @@ -693,9 +823,11 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop := match_states (Cminor.Callstate (External ef) args (Cminor.Kcall optid f sp e k) m) (State f' (Sbuiltin (sel_builtin_res optid) ef al) k' sp e' m') - | match_builtin_2: forall v v' optid f sp e k m f' e' m' k' - (TF: sel_function hf ge f = OK f') - (MC: match_cont k k') + | match_builtin_2: forall cunit hf v v' optid f sp e k m f' e' m' k' + (LINK: linkorder cunit prog) + (HF: helper_functions_declared cunit hf) + (TF: sel_function (prog_defmap cunit) hf f = OK f') + (MC: match_cont cunit hf k k') (LDV: Val.lessdef v v') (LDE: env_lessdef e e') (ME: Mem.extends m m'), @@ -703,19 +835,50 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop := (Cminor.Returnstate v (Cminor.Kcall optid f sp e k) m) (State f' Sskip k' sp (set_builtin_res (sel_builtin_res optid) v' e') m'). +(* +Remark call_cont_commut_1: + forall cunit hf k k', match_cont cunit hf k k' -> + forall cunit' hf', match_cont cunit' hf' (Cminor.call_cont k) (call_cont k'). +Proof. + induction 1; simpl; auto; intros; econstructor; eauto. +Qed. + +Remark call_cont_commut_2: + forall cunit hf k k', match_cont cunit hf k k' -> match_cont cunit hf (Cminor.call_cont k) (call_cont k'). +Proof. + intros. eapply call_cont_commut_1; eauto. +Qed. +*) + Remark call_cont_commut: - forall k k', match_cont k k' -> match_cont (Cminor.call_cont k) (call_cont k'). + forall cunit hf k k', match_cont cunit hf k k' -> match_call_cont (Cminor.call_cont k) (call_cont k'). Proof. - induction 1; simpl; auto. constructor. constructor; auto. + induction 1; simpl; auto; red; intros; econstructor; eauto. +Qed. + +Remark match_is_call_cont: + forall cunit hf k k', match_cont cunit hf k k' -> Cminor.is_call_cont k -> match_call_cont k k'. +Proof. + destruct 1; intros; try contradiction; red; intros; econstructor; eauto. +Qed. + +Remark match_call_cont_cont: + forall k k', match_call_cont k k' -> exists cunit hf, match_cont cunit hf k k'. +Proof. + intros. refine (let cunit : Cminor.program := _ in _). + econstructor. apply nil. apply nil. apply xH. + refine (let hf : helper_functions := _ in _). + econstructor; apply xH. + exists cunit, hf; auto. Qed. Remark find_label_commut: - forall lbl s k s' k', - match_cont k k' -> - sel_stmt hf ge s = OK s' -> + forall cunit hf lbl s k s' k', + match_cont cunit hf k k' -> + sel_stmt (prog_defmap cunit) hf s = OK s' -> match Cminor.find_label lbl s k, find_label lbl s' k' with | None, None => True - | Some(s1, k1), Some(s1', k1') => sel_stmt hf ge s1 = OK s1' /\ match_cont k1 k1' + | Some(s1, k1), Some(s1', k1') => sel_stmt (prog_defmap cunit) hf s1 = OK s1' /\ match_cont cunit hf k1 k1' | _, _ => False end. Proof. @@ -723,9 +886,9 @@ Proof. (* store *) unfold store. destruct (addressing m (sel_expr hf e)); simpl; auto. (* call *) - destruct (classify_call ge e); simpl; auto. + destruct (classify_call (prog_defmap cunit) e); simpl; auto. (* tailcall *) - destruct (classify_call ge e); simpl; auto. + destruct (classify_call (prog_defmap cunit) e); simpl; auto. (* seq *) exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. eauto. destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)) as [[sx kx] | ]; @@ -767,48 +930,50 @@ Lemma sel_step_correct: Proof. induction 1; intros T1 ME; inv ME; try (monadInv TS). - (* skip seq *) - inv MC. left; econstructor; split. econstructor. constructor; auto. + inv MC. left; econstructor; split. econstructor. econstructor; eauto. - (* skip block *) - inv MC. left; econstructor; split. econstructor. constructor; auto. + inv MC. left; econstructor; split. econstructor. econstructor; eauto. - (* skip call *) exploit Mem.free_parallel_extends; eauto. intros [m2' [A B]]. left; econstructor; split. econstructor. inv MC; simpl in H; simpl; auto. eauto. erewrite stackspace_function_translated; eauto. - constructor; auto. + econstructor; eauto. eapply match_is_call_cont; eauto. - (* assign *) exploit sel_expr_correct; eauto. intros [v' [A B]]. left; econstructor; split. econstructor; eauto. - constructor; auto. apply set_var_lessdef; auto. + econstructor; eauto. apply set_var_lessdef; auto. - (* store *) - exploit sel_expr_correct. eexact H. eauto. eauto. intros [vaddr' [A B]]. - exploit sel_expr_correct. eexact H0. eauto. eauto. intros [v' [C D]]. + exploit sel_expr_correct. eauto. eauto. eexact H. eauto. eauto. intros [vaddr' [A B]]. + exploit sel_expr_correct. eauto. eauto. eexact H0. eauto. eauto. intros [v' [C D]]. exploit Mem.storev_extends; eauto. intros [m2' [P Q]]. left; econstructor; split. eapply eval_store; eauto. - constructor; auto. + econstructor; eauto. - (* Scall *) exploit classify_call_correct; eauto. - destruct (classify_call ge a) as [ | id | ef]. + destruct (classify_call (prog_defmap cunit) a) as [ | id | ef]. + (* indirect *) exploit sel_expr_correct; eauto. intros [vf' [A B]]. exploit sel_exprlist_correct; eauto. intros [vargs' [C D]]. - exploit functions_translated; eauto. intros (fd' & U & V). + exploit functions_translated; eauto. intros (cunit' & fd' & U & V & W). left; econstructor; split. econstructor; eauto. econstructor; eauto. - apply sig_function_translated; auto. - constructor; auto. constructor; auto. + eapply sig_function_translated; eauto. + eapply match_callstate with (cunit := cunit'); eauto. + red; intros. eapply match_cont_call with (cunit := cunit); eauto. + (* direct *) intros [b [U V]]. exploit sel_exprlist_correct; eauto. intros [vargs' [C D]]. - exploit functions_translated; eauto. intros (fd' & X & Y). + exploit functions_translated; eauto. intros (cunit' & fd' & X & Y & Z). left; econstructor; split. econstructor; eauto. subst vf. econstructor; eauto. rewrite symbols_preserved; eauto. - apply sig_function_translated; auto. - constructor; auto. constructor; auto. + eapply sig_function_translated; eauto. + eapply match_callstate with (cunit := cunit'); eauto. + red; intros; eapply match_cont_call with (cunit := cunit); eauto. + (* turned into Sbuiltin *) intros EQ. subst fd. exploit sel_builtin_args_correct; eauto. intros [vargs' [C D]]. @@ -819,43 +984,44 @@ Proof. erewrite <- stackspace_function_translated in P by eauto. exploit sel_expr_correct; eauto. intros [vf' [A B]]. exploit sel_exprlist_correct; eauto. intros [vargs' [C D]]. - exploit functions_translated; eauto. intros [fd' [E F]]. + exploit functions_translated; eauto. intros (cunit' & fd' & E & F & G). left; econstructor; split. - exploit classify_call_correct; eauto. - destruct (classify_call ge a) as [ | id | ef]; intros. - econstructor; eauto. econstructor; eauto. apply sig_function_translated; auto. + exploit classify_call_correct. eexact LINK. eauto. eauto. + destruct (classify_call (prog_defmap cunit)) as [ | id | ef]; intros. + econstructor; eauto. econstructor; eauto. eapply sig_function_translated; eauto. destruct H2 as [b [U V]]. subst vf. inv B. - econstructor; eauto. econstructor; eauto. rewrite symbols_preserved; eauto. apply sig_function_translated; auto. - econstructor; eauto. econstructor; eauto. apply sig_function_translated; auto. - constructor; auto. apply call_cont_commut; auto. + econstructor; eauto. econstructor; eauto. rewrite symbols_preserved; eauto. eapply sig_function_translated; eauto. + econstructor; eauto. econstructor; eauto. eapply sig_function_translated; eauto. + eapply match_callstate with (cunit := cunit'); eauto. + eapply call_cont_commut; eauto. - (* Sbuiltin *) exploit sel_builtin_args_correct; eauto. intros [vargs' [P Q]]. exploit external_call_mem_extends; eauto. intros [vres' [m2 [A [B [C D]]]]]. left; econstructor; split. - econstructor. eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - constructor; auto. apply sel_builtin_res_correct; auto. + econstructor. eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved. + econstructor; eauto. apply sel_builtin_res_correct; auto. - (* Seq *) left; econstructor; split. - constructor. constructor; auto. constructor; auto. + constructor. + econstructor; eauto. constructor; auto. - (* Sifthenelse *) exploit sel_expr_correct; eauto. intros [v' [A B]]. assert (Val.bool_of_val v' b). inv B. auto. inv H0. left; exists (State f' (if b then x else x0) k' sp e' m'); split. econstructor; eauto. eapply eval_condexpr_of_expr; eauto. - constructor; auto. destruct b; auto. + econstructor; eauto. destruct b; auto. - (* Sloop *) - left; econstructor; split. constructor. constructor; auto. + left; econstructor; split. constructor. econstructor; eauto. constructor; auto. simpl; rewrite EQ; auto. - (* Sblock *) - left; econstructor; split. constructor. constructor; auto. constructor; auto. + left; econstructor; split. constructor. econstructor; eauto. constructor; auto. - (* Sexit seq *) - inv MC. left; econstructor; split. constructor. constructor; auto. + inv MC. left; econstructor; split. constructor. econstructor; eauto. - (* Sexit0 block *) - inv MC. left; econstructor; split. constructor. constructor; auto. + inv MC. left; econstructor; split. constructor. econstructor; eauto. - (* SexitS block *) - inv MC. left; econstructor; split. constructor. constructor; auto. + inv MC. left; econstructor; split. constructor. econstructor; eauto. - (* Sswitch *) inv H0; simpl in TS. + set (ct := compile_switch Int.modulus default cases) in *. @@ -863,69 +1029,70 @@ Proof. exploit sel_expr_correct; eauto. intros [v' [A B]]. inv B. left; econstructor; split. econstructor. eapply sel_switch_int_correct; eauto. - constructor; auto. + econstructor; eauto. + set (ct := compile_switch Int64.modulus default cases) in *. destruct (validate_switch Int64.modulus default cases ct) eqn:VALID; inv TS. exploit sel_expr_correct; eauto. intros [v' [A B]]. inv B. left; econstructor; split. econstructor. eapply sel_switch_long_correct; eauto. - constructor; auto. + econstructor; eauto. - (* Sreturn None *) exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]]. erewrite <- stackspace_function_translated in P by eauto. left; econstructor; split. econstructor. simpl; eauto. - constructor; auto. apply call_cont_commut; auto. + econstructor; eauto. eapply call_cont_commut; eauto. - (* Sreturn Some *) exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]]. erewrite <- stackspace_function_translated in P by eauto. exploit sel_expr_correct; eauto. intros [v' [A B]]. left; econstructor; split. econstructor; eauto. - constructor; auto. apply call_cont_commut; auto. + econstructor; eauto. eapply call_cont_commut; eauto. - (* Slabel *) - left; econstructor; split. constructor. constructor; auto. + left; econstructor; split. constructor. econstructor; eauto. - (* Sgoto *) - assert (sel_stmt hf ge (Cminor.fn_body f) = OK (fn_body f')). + assert (sel_stmt (prog_defmap cunit) hf (Cminor.fn_body f) = OK (fn_body f')). { monadInv TF; simpl; auto. } - exploit (find_label_commut lbl (Cminor.fn_body f) (Cminor.call_cont k)). - apply call_cont_commut; eauto. eauto. + exploit (find_label_commut cunit hf lbl (Cminor.fn_body f) (Cminor.call_cont k)). + eapply call_cont_commut; eauto. eauto. rewrite H. destruct (find_label lbl (fn_body f') (call_cont k'0)) as [[s'' k'']|] eqn:?; intros; try contradiction. destruct H1. left; econstructor; split. econstructor; eauto. - constructor; auto. + econstructor; eauto. - (* internal function *) + destruct TF as (hf & HF & TF). specialize (MC cunit hf). monadInv TF. generalize EQ; intros TF; monadInv TF. exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. intros [m2' [A B]]. left; econstructor; split. econstructor; simpl; eauto. - constructor; simpl; auto. apply set_locals_lessdef. apply set_params_lessdef; auto. + econstructor; simpl; eauto. apply set_locals_lessdef. apply set_params_lessdef; auto. - (* external call *) + destruct TF as (hf & HF & TF). monadInv TF. exploit external_call_mem_extends; eauto. intros [vres' [m2 [A [B [C D]]]]]. left; econstructor; split. - econstructor. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - constructor; auto. + econstructor. eapply external_call_symbols_preserved; eauto. apply senv_preserved. + econstructor; eauto. - (* external call turned into a Sbuiltin *) exploit external_call_mem_extends; eauto. intros [vres' [m2 [A [B [C D]]]]]. left; econstructor; split. - econstructor. eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - constructor; auto. + econstructor. eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved. + econstructor; eauto. - (* return *) + apply match_call_cont_cont in MC. destruct MC as (cunit0 & hf0 & MC). inv MC. left; econstructor; split. econstructor. - constructor; auto. destruct optid; simpl; auto. apply set_var_lessdef; auto. + econstructor; eauto. destruct optid; simpl; auto. apply set_var_lessdef; auto. - (* return of an external call turned into a Sbuiltin *) - right; split. simpl; omega. split. auto. constructor; auto. + right; split. simpl; omega. split. auto. econstructor; eauto. apply sel_builtin_res_correct; auto. Qed. @@ -933,118 +1100,49 @@ Lemma sel_initial_states: forall S, Cminor.initial_state prog S -> exists R, initial_state tprog R /\ match_states S R. Proof. - induction 1. - exploit function_ptr_translated; eauto. intros (f' & A & B). + destruct 1. + exploit function_ptr_translated; eauto. intros (cu & f' & A & B & C). econstructor; split. econstructor. - eapply Genv.init_mem_transf_partial; eauto. - simpl. fold tge. rewrite symbols_preserved. - erewrite transform_partial_program_main by eauto. eexact H0. - eauto. - rewrite <- H2. apply sig_function_translated; auto. - constructor; auto. constructor. apply Mem.extends_refl. + eapply (Genv.init_mem_match TRANSF); eauto. + rewrite (match_program_main TRANSF). fold tge. rewrite symbols_preserved. eauto. + eexact A. + rewrite <- H2. eapply sig_function_translated; eauto. + econstructor; eauto. red; intros; constructor. apply Mem.extends_refl. Qed. Lemma sel_final_states: forall S R r, match_states S R -> Cminor.final_state S r -> final_state R r. Proof. - intros. inv H0. inv H. inv MC. inv LD. constructor. -Qed. - -End PRESERVATION. - -(** Processing of helper functions *) - -Lemma record_globdefs_sound: - forall p id fd, - (record_globdefs p)!id = Some (Gfun fd) -> - exists b, Genv.find_symbol (Genv.globalenv p) id = Some b - /\ Genv.find_funct_ptr (Genv.globalenv p) b = Some fd. -Proof. - intros until fd. - set (P := fun (m: PTree.t globdef) (ge: Genv.t Cminor.fundef unit) => - m!id = Some (Gfun fd) -> - exists b, Genv.find_symbol ge id = Some b - /\ Genv.find_funct_ptr ge b = Some fd). - assert (REC: forall gl m ge, - P m ge -> - P (fold_left record_globdef gl m) (Genv.add_globals ge gl)). - { - induction gl; simpl; intros. - - auto. - - apply IHgl. red. destruct a as [id1 gd1]; simpl; intros. - unfold Genv.find_symbol; simpl. rewrite PTree.gsspec. destruct (peq id id1). - + subst id1. exists (Genv.genv_next ge); split; auto. - replace gd1 with (@Gfun Cminor.fundef unit fd). - unfold Genv.find_funct_ptr; simpl. apply PTree.gss. - destruct (globdef_of_interest gd1). - rewrite PTree.gss in H0; congruence. - rewrite PTree.grs in H0; congruence. - + assert (m!id = Some (Gfun fd)). - { destruct (globdef_of_interest gd1). - rewrite PTree.gso in H0; auto. - rewrite PTree.gro in H0; auto. } - exploit H; eauto. intros (b & A & B). - exists b; split; auto. unfold Genv.find_funct_ptr; simpl. - destruct gd1; auto. rewrite PTree.gso; auto. - apply Plt_ne. eapply Genv.genv_symb_range; eauto. - } - eapply REC. red; intros. rewrite PTree.gempty in H; discriminate. -Qed. - -Lemma lookup_helper_correct_1: - forall globs name sg id, - lookup_helper globs name sg = OK id -> - globs!id = Some (Gfun (External (EF_external name sg))). -Proof. - intros. - set (P := fun (m: PTree.t globdef) res => res = Some id -> m!id = Some(Gfun(External (EF_external name sg)))). - assert (P globs (PTree.fold (lookup_helper_aux name sg) globs None)). - { apply PTree_Properties.fold_rec; red; intros. - - rewrite <- H0. apply H1; auto. - - discriminate. - - assert (EITHER: k = id /\ v = Gfun (External (EF_external name sg)) - \/ a = Some id). - { unfold lookup_helper_aux in H3. destruct v; auto. destruct f; auto. destruct e; auto. - destruct (String.string_dec name name0); auto. - destruct (signature_eq sg sg0); auto. - inversion H3. left; split; auto. repeat f_equal; auto. } - destruct EITHER as [[X Y] | X]. - subst k v. apply PTree.gss. - apply H2 in X. rewrite PTree.gso by congruence. auto. - } - red in H0. unfold lookup_helper in H. - destruct (PTree.fold (lookup_helper_aux name sg) globs None); inv H. auto. + intros. inv H0. inv H. + apply match_call_cont_cont in MC. destruct MC as (cunit0 & hf0 & MC). + inv MC. inv LD. constructor. Qed. -Lemma lookup_helper_correct: - forall p name sg id, - lookup_helper (record_globdefs p) name sg = OK id -> - helper_declared (Genv.globalenv p) id name sg. +Theorem transf_program_correct: + forward_simulation (Cminor.semantics prog) (CminorSel.semantics tprog). Proof. - intros. apply lookup_helper_correct_1 in H. apply record_globdefs_sound in H. auto. + apply forward_simulation_opt with (match_states := match_states) (measure := measure). + apply senv_preserved. + apply sel_initial_states; auto. + apply sel_final_states; auto. + apply sel_step_correct; auto. Qed. -Theorem get_helpers_correct: - forall p hf, - get_helpers p = OK hf -> helper_functions_declared (Genv.globalenv p) hf. -Proof. - intros. monadInv H. red; simpl. auto 20 using lookup_helper_correct. -Qed. +End PRESERVATION. -(** All together *) +(** ** Commutation with linking *) -Theorem transf_program_correct: - forall prog tprog, - sel_program prog = OK tprog -> - forward_simulation (Cminor.semantics prog) (CminorSel.semantics tprog). +Instance TransfSelectionLink : TransfLink match_prog. Proof. - intros. unfold sel_program in H. - destruct (get_helpers prog) as [hf|] eqn:G; simpl in H; try discriminate. - apply forward_simulation_opt with (match_states := match_states prog tprog hf) (measure := measure). - eapply public_preserved; eauto. - apply sel_initial_states; auto. - apply sel_final_states; auto. - apply sel_step_correct; auto. eapply get_helpers_correct; eauto. + red; intros. destruct (link_linkorder _ _ _ H) as [LO1 LO2]. + eapply link_match_program; eauto. + intros. elim H3; intros hf1 [A1 B1]. elim H4; intros hf2 [A2 B2]. +Local Transparent Linker_fundef. + simpl in *. destruct f1, f2; simpl in *; monadInv B1; monadInv B2; simpl. +- discriminate. +- destruct e; inv H2. econstructor; eauto. +- destruct e; inv H2. econstructor; eauto. +- destruct (external_function_eq e e0); inv H2. econstructor; eauto. Qed. diff --git a/backend/Stacking.v b/backend/Stacking.v index ab67e213..cf797a11 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -12,18 +12,10 @@ (** Layout of activation records; translation from Linear to Mach. *) -Require Import Coqlib. -Require Import Errors. -Require Import AST. -Require Import Integers. -Require Import Op. -Require Import Locations. -Require Import Linear. -Require Import Bounds. -Require Import Mach. -Require Import Conventions. -Require Import Stacklayout. -Require Import Lineartyping. +Require Import Coqlib Errors. +Require Import Integers AST. +Require Import Op Locations Linear Mach. +Require Import Bounds Conventions Stacklayout Lineartyping. (** * Layout of activation records *) diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 8becb773..a76fdbba 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -14,26 +14,22 @@ (** This file proves semantic preservation for the [Stacking] pass. *) -Require Import Coqlib. -Require Import Errors. -Require Import AST. -Require Import Integers. -Require Import Values. -Require Import Op. -Require Import Memory. -Require Import Events. -Require Import Globalenvs. -Require Import Smallstep. -Require Import Locations. -Require Import LTL. -Require Import Linear. -Require Import Lineartyping. -Require Import Mach. -Require Import Bounds. -Require Import Conventions. -Require Import Stacklayout. +Require Import Coqlib Errors. +Require Import Integers AST Linking. +Require Import Values Memory Events Globalenvs Smallstep. +Require Import LTL Op Locations Linear Mach. +Require Import Bounds Conventions Stacklayout Lineartyping. Require Import Stacking. +Definition match_prog (p: Linear.program) (tp: Mach.program) := + match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. + +Lemma transf_program_match: + forall p tp, transf_program p = OK tp -> match_prog p tp. +Proof. + intros. eapply match_transform_partial_program; eauto. +Qed. + (** * Properties of frame offsets *) Lemma typesize_typesize: @@ -61,11 +57,10 @@ Let step := Mach.step return_address_offset. Variable prog: Linear.program. Variable tprog: Mach.program. -Hypothesis TRANSF: transf_program prog = OK tprog. +Hypothesis TRANSF: match_prog prog tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. - Section FRAME_PROPERTIES. Variable f: Linear.function. @@ -2261,44 +2256,26 @@ Qed. (** Preservation / translation of global symbols and functions. *) Lemma symbols_preserved: - forall id, Genv.find_symbol tge id = Genv.find_symbol ge id. -Proof. - intros. unfold ge, tge. - apply Genv.find_symbol_transf_partial with transf_fundef. - exact TRANSF. -Qed. + forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof (Genv.find_symbol_match TRANSF). -Lemma public_preserved: - forall id, Genv.public_symbol tge id = Genv.public_symbol ge id. -Proof. - intros. unfold ge, tge. - apply Genv.public_symbol_transf_partial with transf_fundef. - exact TRANSF. -Qed. - -Lemma varinfo_preserved: - forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. -Proof. - intros. unfold ge, tge. - apply Genv.find_var_info_transf_partial with transf_fundef. - exact TRANSF. -Qed. +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_match TRANSF). Lemma functions_translated: forall v f, Genv.find_funct ge v = Some f -> exists tf, Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf. -Proof - (Genv.find_funct_transf_partial transf_fundef _ TRANSF). +Proof (Genv.find_funct_transf_partial TRANSF). Lemma function_ptr_translated: - forall v f, - Genv.find_funct_ptr ge v = Some f -> + forall b f, + Genv.find_funct_ptr ge b = Some f -> exists tf, - Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf. -Proof - (Genv.find_funct_ptr_transf_partial transf_fundef _ TRANSF). + Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf. +Proof (Genv.find_funct_ptr_transf_partial TRANSF). Lemma sig_preserved: forall f tf, transf_fundef f = OK tf -> Mach.funsig tf = Linear.funsig f. @@ -2749,8 +2726,7 @@ Proof. econstructor; split. apply plus_one. econstructor; eauto. eapply 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; eauto. apply senv_preserved. econstructor; eauto with coqlib. eapply match_stack_change_extcall; eauto. apply Plt_Ple. change (Mem.valid_block m sp0). eapply agree_valid_linear; eauto. @@ -2858,8 +2834,7 @@ Proof. intros [j' [res' [m1' [A [B [C [D [E [F G]]]]]]]]]. econstructor; split. apply plus_one. eapply exec_function_external; 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. apply match_stacks_change_bounds with (Mem.nextblock m) (Mem.nextblock m'0). inv H0; inv A. eapply match_stack_change_extcall; eauto. apply Ple_refl. apply Ple_refl. @@ -2884,8 +2859,8 @@ Proof. exploit function_ptr_translated; eauto. intros [tf [FIND TR]]. econstructor; split. econstructor. - eapply Genv.init_mem_transf_partial; eauto. - rewrite (transform_partial_program_main _ _ TRANSF). + eapply (Genv.init_mem_transf_partial TRANSF); eauto. + rewrite (match_program_main TRANSF). rewrite symbols_preserved. eauto. econstructor; eauto. eapply Genv.initmem_inject; eauto. @@ -2913,9 +2888,10 @@ Qed. Lemma wt_prog: forall i fd, In (i, Gfun fd) prog.(prog_defs) -> wt_fundef fd. Proof. - intros. exploit transform_partial_program_succeeds; eauto. - intros [tfd TF]. destruct fd; simpl in *. -- monadInv TF. unfold transf_function in EQ. + intros. + exploit list_forall2_in_left. eexact (proj1 TRANSF). eauto. + intros ([i' g] & P & Q & R). simpl in *. inv R. destruct fd; simpl in *. +- monadInv H2. unfold transf_function in EQ. destruct (wt_function f). auto. discriminate. - auto. Qed. @@ -2925,7 +2901,7 @@ Theorem transf_program_correct: Proof. set (ms := fun s s' => wt_state s /\ match_states s s'). eapply forward_simulation_plus with (match_states := ms). -- exact public_preserved. +- apply senv_preserved. - intros. exploit transf_initial_states; eauto. intros [st2 [A B]]. exists st2; split; auto. split; auto. apply wt_initial_state with (prog := prog); auto. exact wt_prog. diff --git a/backend/Tailcall.v b/backend/Tailcall.v index e8ce9e25..939abeea 100644 --- a/backend/Tailcall.v +++ b/backend/Tailcall.v @@ -12,13 +12,7 @@ (** Recognition of tail calls. *) -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Registers. -Require Import Op. -Require Import RTL. -Require Import Conventions. +Require Import Coqlib Maps AST Registers Op RTL Conventions. (** An [Icall] instruction that stores its result in register [rreg] can be turned into a tail call if: @@ -95,8 +89,7 @@ Definition transf_instr (f: function) (pc: node) (instr: instruction) := end. (** A function is transformed only if its stack block is empty, - as explained above. Moreover, we can turn tail calls off - using a compilation option. *) + as explained above. *) Definition transf_function (f: function) : function := if zeq f.(fn_stacksize) 0 diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 7e7b7b53..793dc861 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -12,20 +12,9 @@ (** Recognition of tail calls: correctness proof *) -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Values. -Require Import Memory. -Require Import Op. -Require Import Events. -Require Import Globalenvs. -Require Import Smallstep. -Require Import Registers. -Require Import RTL. -Require Import Conventions. -Require Import Tailcall. +Require Import Coqlib Maps Integers AST Linking. +Require Import Values Memory Events Globalenvs Smallstep. +Require Import Op Registers RTL Conventions Tailcall. (** * Syntactic properties of the code transformation *) @@ -212,36 +201,42 @@ Qed. (** * Proof of semantic preservation *) +Definition match_prog (p tp: RTL.program) := + match_program (fun cu f tf => tf = transf_fundef f) eq p tp. + +Lemma transf_program_match: + forall p, match_prog p (transf_program p). +Proof. + intros. apply match_transform_program; auto. +Qed. + Section PRESERVATION. -Variable prog: program. -Let tprog := transf_program prog. +Variable prog tprog: program. +Hypothesis TRANSL: match_prog prog tprog. + Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof (Genv.find_symbol_transf transf_fundef prog). - -Lemma public_preserved: - forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. -Proof (Genv.public_symbol_transf transf_fundef prog). - -Lemma varinfo_preserved: - forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. -Proof (Genv.find_var_info_transf transf_fundef prog). +Proof (Genv.find_symbol_transf TRANSL). Lemma functions_translated: forall (v: val) (f: RTL.fundef), Genv.find_funct ge v = Some f -> Genv.find_funct tge v = Some (transf_fundef f). -Proof (@Genv.find_funct_transf _ _ _ transf_fundef prog). +Proof (Genv.find_funct_transf TRANSL). Lemma funct_ptr_translated: forall (b: block) (f: RTL.fundef), Genv.find_funct_ptr ge b = Some f -> Genv.find_funct_ptr tge b = Some (transf_fundef f). -Proof (@Genv.find_funct_ptr_transf _ _ _ transf_fundef prog). +Proof (Genv.find_funct_ptr_transf TRANSL). + +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_transf TRANSL). Lemma sig_preserved: forall f, funsig (transf_fundef f) = funsig f. @@ -409,15 +404,15 @@ Lemma transf_step_correct: Proof. induction 1; intros; inv MS; EliminatedInstr. -(* nop *) +- (* nop *) TransfInstr. left. econstructor; split. eapply exec_Inop; eauto. constructor; auto. -(* eliminated nop *) +- (* eliminated nop *) assert (s0 = pc') by congruence. subst s0. right. split. simpl. omega. split. auto. econstructor; eauto. -(* op *) +- (* op *) TransfInstr. assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto. exploit eval_operation_lessdef; eauto. @@ -426,12 +421,12 @@ Proof. eapply exec_Iop; eauto. rewrite <- EVAL'. apply eval_operation_preserved. exact symbols_preserved. econstructor; eauto. apply set_reg_lessdef; auto. -(* eliminated move *) +- (* eliminated move *) rewrite H1 in H. clear H1. inv H. right. split. simpl. omega. split. auto. econstructor; eauto. simpl in H0. rewrite PMap.gss. congruence. -(* load *) +- (* load *) TransfInstr. assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto. exploit eval_addressing_lessdef; eauto. @@ -443,7 +438,7 @@ Proof. apply eval_addressing_preserved. exact symbols_preserved. eauto. econstructor; eauto. apply set_reg_lessdef; auto. -(* store *) +- (* store *) TransfInstr. assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto. exploit eval_addressing_lessdef; eauto. @@ -456,10 +451,10 @@ Proof. destruct a; simpl in H1; try discriminate. econstructor; eauto. -(* call *) +- (* call *) exploit find_function_translated; eauto. intro FIND'. TransfInstr. -(* call turned tailcall *) ++ (* call turned tailcall *) assert ({ m'' | Mem.free m' sp0 0 (fn_stacksize (transf_function f)) = Some m''}). apply Mem.range_perm_free. rewrite stacksize_preserved. rewrite H7. red; intros; omegaContradiction. @@ -469,13 +464,13 @@ Proof. constructor. eapply match_stackframes_tail; eauto. apply regs_lessdef_regs; auto. eapply Mem.free_right_extends; eauto. rewrite stacksize_preserved. rewrite H7. intros. omegaContradiction. -(* call that remains a call *) ++ (* call that remains a call *) left. exists (Callstate (Stackframe res (transf_function f) (Vptr sp0 Int.zero) pc' rs' :: s') (transf_fundef fd) (rs'##args) m'); split. eapply exec_Icall; eauto. apply sig_preserved. constructor. constructor; auto. apply regs_lessdef_regs; auto. auto. -(* tailcall *) +- (* tailcall *) exploit find_function_translated; eauto. intro FIND'. exploit Mem.free_parallel_extends; eauto. intros [m'1 [FREE EXT]]. TransfInstr. @@ -484,7 +479,7 @@ Proof. rewrite stacksize_preserved; auto. constructor. auto. apply regs_lessdef_regs; auto. auto. -(* builtin *) +- (* builtin *) TransfInstr. exploit (@eval_builtin_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)); eauto. intros (vargs' & P & Q). @@ -493,25 +488,24 @@ Proof. left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' (regmap_setres res v' rs') m'1); split. eapply exec_Ibuiltin; eauto. eapply 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; eauto. apply senv_preserved. econstructor; eauto. apply set_res_lessdef; auto. -(* cond *) +- (* cond *) TransfInstr. left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) (if b then ifso else ifnot) rs' m'); split. eapply exec_Icond; eauto. apply eval_condition_lessdef with (rs##args) m; auto. apply regs_lessdef_regs; auto. constructor; auto. -(* jumptable *) +- (* jumptable *) TransfInstr. left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' rs' m'); split. eapply exec_Ijumptable; eauto. generalize (RLD arg). rewrite H0. intro. inv H2. auto. constructor; auto. -(* return *) +- (* return *) exploit Mem.free_parallel_extends; eauto. intros [m'1 [FREE EXT]]. TransfInstr. left. exists (Returnstate s' (regmap_optget or Vundef rs') m'1); split. @@ -520,21 +514,21 @@ Proof. destruct or; simpl. apply RLD. constructor. auto. -(* eliminated return None *) +- (* eliminated return None *) assert (or = None) by congruence. subst or. right. split. simpl. omega. split. auto. constructor. auto. simpl. constructor. eapply Mem.free_left_extends; eauto. -(* eliminated return Some *) +- (* eliminated return Some *) assert (or = Some r) by congruence. subst or. right. split. simpl. omega. split. auto. constructor. auto. simpl. auto. eapply Mem.free_left_extends; eauto. -(* internal call *) +- (* internal call *) exploit Mem.alloc_extends; eauto. instantiate (1 := 0). omega. instantiate (1 := fn_stacksize f). omega. @@ -549,22 +543,21 @@ Proof. rewrite EQ2. rewrite EQ3. constructor; auto. apply regs_lessdef_init_regs. auto. -(* external call *) +- (* external call *) exploit external_call_mem_extends; eauto. intros [res' [m2' [A [B [C D]]]]]. left. exists (Returnstate s' res' m2'); split. simpl. 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. constructor; auto. -(* returnstate *) +- (* returnstate *) inv H2. -(* synchronous return in both programs *) ++ (* synchronous return in both programs *) left. econstructor; split. apply exec_return. constructor; auto. apply set_reg_lessdef; auto. -(* return instr in source program, eliminated because of tailcall *) ++ (* return instr in source program, eliminated because of tailcall *) right. split. unfold measure. simpl length. change (S (length s) * (niter + 2))%nat with ((niter + 2) + (length s) * (niter + 2))%nat. @@ -581,10 +574,10 @@ Proof. intros. inv H. exploit funct_ptr_translated; eauto. intro FIND. exists (Callstate nil (transf_fundef f) nil m0); split. - econstructor; eauto. apply Genv.init_mem_transf. auto. + econstructor; eauto. apply (Genv.init_mem_transf TRANSL). auto. replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. - reflexivity. + symmetry; eapply match_program_main; eauto. rewrite <- H3. apply sig_preserved. constructor. constructor. constructor. apply Mem.extends_refl. Qed. @@ -604,7 +597,7 @@ Theorem transf_program_correct: forward_simulation (RTL.semantics prog) (RTL.semantics tprog). Proof. eapply forward_simulation_opt with (measure := measure); eauto. - eexact public_preserved. + apply senv_preserved. eexact transf_initial_states. eexact transf_final_states. exact transf_step_correct. @@ -612,4 +605,3 @@ Qed. End PRESERVATION. - diff --git a/backend/Tunneling.v b/backend/Tunneling.v index fa7ff787..3374d5b4 100644 --- a/backend/Tunneling.v +++ b/backend/Tunneling.v @@ -12,9 +12,7 @@ (** Branch tunneling (optimization of branches to branches). *) -Require Import Coqlib. -Require Import Maps. -Require Import UnionFind. +Require Import Coqlib Maps UnionFind. Require Import AST. Require Import LTL. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 22f0521e..4f1f8143 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -12,20 +12,21 @@ (** Correctness proof for the branch tunneling optimization. *) -Require Import Coqlib. -Require Import Maps. -Require Import UnionFind. -Require Import AST. -Require Import Values. -Require Import Memory. -Require Import Events. -Require Import Globalenvs. -Require Import Smallstep. -Require Import Op. -Require Import Locations. -Require Import LTL. +Require Import Coqlib Maps UnionFind. +Require Import AST Linking. +Require Import Values Memory Events Globalenvs Smallstep. +Require Import Op Locations LTL. Require Import Tunneling. +Definition match_prog (p tp: program) := + match_program (fun ctx f tf => tf = tunnel_fundef f) eq p tp. + +Lemma transf_program_match: + forall p, match_prog p (tunnel_program p). +Proof. + intros. eapply match_transform_program; eauto. +Qed. + (** * Properties of the branch map computed using union-find. *) (** A variant of [record_goto] that also incrementally computes a measure [f: node -> nat] @@ -138,8 +139,8 @@ Qed. Section PRESERVATION. -Variable prog: program. -Let tprog := tunnel_program prog. +Variables prog tprog: program. +Hypothesis TRANSL: match_prog prog tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. @@ -147,27 +148,22 @@ Lemma functions_translated: forall v f, Genv.find_funct ge v = Some f -> Genv.find_funct tge v = Some (tunnel_fundef f). -Proof (@Genv.find_funct_transf _ _ _ tunnel_fundef prog). +Proof (Genv.find_funct_transf TRANSL). Lemma function_ptr_translated: forall v f, Genv.find_funct_ptr ge v = Some f -> Genv.find_funct_ptr tge v = Some (tunnel_fundef f). -Proof (@Genv.find_funct_ptr_transf _ _ _ tunnel_fundef prog). +Proof (Genv.find_funct_ptr_transf TRANSL). Lemma symbols_preserved: forall id, Genv.find_symbol tge id = Genv.find_symbol ge id. -Proof (@Genv.find_symbol_transf _ _ _ tunnel_fundef prog). - -Lemma public_preserved: - forall id, - Genv.public_symbol tge id = Genv.public_symbol ge id. -Proof (@Genv.public_symbol_transf _ _ _ tunnel_fundef prog). +Proof (Genv.find_symbol_transf TRANSL). -Lemma varinfo_preserved: - forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. -Proof (@Genv.find_var_info_transf _ _ _ tunnel_fundef prog). +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_transf TRANSL). Lemma sig_preserved: forall f, funsig (tunnel_fundef f) = funsig f. @@ -340,8 +336,7 @@ Proof. left; simpl; econstructor; split. eapply exec_Lbuiltin; eauto. eapply 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. econstructor; eauto. (* Lbranch (preserved) *) @@ -372,8 +367,7 @@ Proof. (* external function *) left; simpl; econstructor; split. eapply exec_function_external; 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. simpl. econstructor; eauto. (* return *) inv H3. inv H1. @@ -389,8 +383,8 @@ Proof. intros. inversion H. exists (Callstate nil (tunnel_fundef f) (Locmap.init Vundef) m0); split. econstructor; eauto. - apply Genv.init_mem_transf; auto. - change (prog_main tprog) with (prog_main prog). + apply (Genv.init_mem_transf TRANSL); auto. + rewrite (match_program_main TRANSL). rewrite symbols_preserved. eauto. apply function_ptr_translated; auto. rewrite <- H3. apply sig_preserved. @@ -408,7 +402,7 @@ Theorem transf_program_correct: forward_simulation (LTL.semantics prog) (LTL.semantics tprog). Proof. eapply forward_simulation_opt. - eexact public_preserved. + apply senv_preserved. eexact transf_initial_states. eexact transf_final_states. eexact tunnel_step_correct. diff --git a/backend/Unusedglob.v b/backend/Unusedglob.v index 8725c9af..916e111b 100644 --- a/backend/Unusedglob.v +++ b/backend/Unusedglob.v @@ -12,16 +12,9 @@ (** Elimination of unreferenced static definitions *) -Require Import FSets. -Require Import Coqlib. -Require Import Ordered. -Require Import Maps. -Require Import Iteration. -Require Import AST. -Require Import Errors. -Require Import Op. -Require Import Registers. -Require Import RTL. +Require Import FSets Coqlib Maps Ordered Iteration Errors. +Require Import AST Linking. +Require Import Op Registers RTL. Local Open Scope string_scope. @@ -90,6 +83,15 @@ Definition add_ref_definition (pm: prog_map) (id: ident) (w: workset): workset : | Some (Gvar gv) => add_ref_globvar gv w end. +(** The initial workset is composed of all public definitions of the compilation unit, + plus the "main" entry point. *) + +Definition initial_workset (p: program): workset := + add_workset p.(prog_main) + (List.fold_left (fun w id => add_workset id w) + p.(prog_public) + {| w_seen := IS.empty; w_todo := nil |}). + (** Traversal of the dependency graph. *) Definition iter_step (pm: prog_map) (w: workset) : IS.t + workset := @@ -100,20 +102,7 @@ Definition iter_step (pm: prog_map) (w: workset) : IS.t + workset := inr _ (add_ref_definition pm id {| w_seen := w.(w_seen); w_todo := rem |}) end. -Definition initial_workset (p: program): workset := - add_workset p.(prog_main) - (List.fold_left (fun w id => add_workset id w) - p.(prog_public) - {| w_seen := IS.empty; w_todo := nil |}). - -Definition add_def_prog_map (pm: prog_map) (id_df: ident * globdef fundef unit) : prog_map := - PTree.set (fst id_df) (snd id_df) pm. - -Definition program_map (p: program) : prog_map := - List.fold_left add_def_prog_map p.(prog_defs) (PTree.empty _). - -Definition used_globals (p: program) : option IS.t := - let pm := program_map p in +Definition used_globals (p: program) (pm: prog_map) : option IS.t := PrimIter.iterate _ _ (iter_step pm) (initial_workset p). (** * Elimination of unreferenced global definitions *) @@ -130,12 +119,23 @@ Fixpoint filter_globdefs (used: IS.t) (accu defs: list (ident * globdef fundef u else filter_globdefs used accu defs' end. +(** To ensure compatibility with linking, we must ensure that all the + global names referenced are defined in the compilation unit, with + the possible exception of the [prog_main] name. *) + +Definition global_defined (p: program) (pm: prog_map) (id: ident) : bool := + match pm!id with Some _ => true | None => ident_eq id (prog_main p) end. + Definition transform_program (p: program) : res program := - match used_globals p with + let pm := prog_defmap p in + match used_globals p pm with | None => Error (msg "Unusedglob: analysis failed") | Some used => - OK {| prog_defs := filter_globdefs used nil (List.rev p.(prog_defs)); - prog_public := p.(prog_public); - prog_main := p.(prog_main) |} + if IS.for_all (global_defined p pm) used then + OK {| prog_defs := filter_globdefs used nil (List.rev p.(prog_defs)); + prog_public := p.(prog_public); + prog_main := p.(prog_main) |} + else + Error (msg "Unusedglob: reference to undefined global") end. diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index 7c1b60a9..bb40a2d3 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -12,28 +12,67 @@ (** Elimination of unreferenced static definitions *) -Require Import FSets. -Require Import Coqlib. -Require Import Ordered. -Require Import Maps. -Require Import Iteration. -Require Import AST. -Require Import Errors. -Require Import Integers. -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 FSets Coqlib Maps Ordered Iteration Errors. +Require Import AST Linking. +Require Import Integers Values Memory Globalenvs Events Smallstep. +Require Import Op Registers RTL. Require Import Unusedglob. Module ISF := FSetFacts.Facts(IS). Module ISP := FSetProperties.Properties(IS). -(** * Properties of the analysis *) +(** * Relational specification of the transformation *) + +(** The transformed program is obtained from the original program + by keeping only the global definitions that belong to a given + set [u] of names. *) + +Record match_prog_1 (u: IS.t) (p tp: program) : Prop := { + match_prog_main: + tp.(prog_main) = p.(prog_main); + match_prog_public: + tp.(prog_public) = p.(prog_public); + match_prog_def: + forall id, + (prog_defmap tp)!id = if IS.mem id u then (prog_defmap p)!id else None; + match_prog_unique: + list_norepet (prog_defs_names tp) +}. + +(** This set [u] (as "used") must be closed under references, and + contain the entry point and the public identifiers of the program. *) + +Definition ref_function (f: function) (id: ident) : Prop := + exists pc i, f.(fn_code)!pc = Some i /\ In id (ref_instruction i). + +Definition ref_fundef (fd: fundef) (id: ident) : Prop := + match fd with Internal f => ref_function f id | External ef => False end. + +Definition ref_init (il: list init_data) (id: ident) : Prop := + exists ofs, In (Init_addrof id ofs) il. + +Definition ref_def (gd: globdef fundef unit) (id: ident) : Prop := + match gd with + | Gfun fd => ref_fundef fd id + | Gvar gv => ref_init gv.(gvar_init) id + end. + +Record valid_used_set (p: program) (u: IS.t) : Prop := { + used_closed: forall id gd id', + IS.In id u -> (prog_defmap p)!id = Some gd -> ref_def gd id' -> + IS.In id' u; + used_main: + IS.In p.(prog_main) u; + used_public: forall id, + In id p.(prog_public) -> IS.In id u; + used_defined: forall id, + IS.In id u -> In id (prog_defs_names p) \/ id = p.(prog_main) +}. + +Definition match_prog (p tp: program) : Prop := + exists u: IS.t, valid_used_set p u /\ match_prog_1 u p tp. + +(** * Properties of the static analysis *) (** Monotonic evolution of the workset. *) @@ -123,7 +162,7 @@ Proof. eapply workset_incl_trans. 2: apply add_workset_incl. generalize {| w_seen := IS.empty; w_todo := nil |}. induction (prog_public p); simpl; intros. apply workset_incl_refl. - eapply workset_incl_trans. eapply add_workset_incl. eapply IHl. + eapply workset_incl_trans. apply add_workset_incl. apply IHl. Qed. (** Soundness properties for functions that add identifiers to the workset *) @@ -148,9 +187,6 @@ Proof. apply IHl; auto. Qed. -Definition ref_function (f: function) (id: ident) : Prop := - exists pc i, f.(fn_code)!pc = Some i /\ In id (ref_instruction i). - Lemma seen_add_ref_function: forall id f w, ref_function f id -> IS.In id (add_ref_function f w). @@ -164,15 +200,6 @@ Proof. apply H1. exists pc, i; auto. Qed. -Definition ref_fundef (fd: fundef) (id: ident) : Prop := - match fd with Internal f => ref_function f id | External ef => False end. - -Definition ref_def (gd: globdef fundef unit) (id: ident) : Prop := - match gd with - | Gfun fd => ref_fundef fd id - | Gvar gv => exists ofs, List.In (Init_addrof id ofs) gv.(gvar_init) - end. - Lemma seen_add_ref_definition: forall pm id gd id' w, pm!id = Some gd -> ref_def gd id' -> IS.In id' (add_ref_definition pm id w). @@ -198,7 +225,7 @@ Qed. Lemma seen_main_initial_workset: forall p, IS.In p.(prog_main) (initial_workset p). Proof. - unfold initial_workset; intros. apply seen_add_workset. + intros. apply seen_add_workset. Qed. Lemma seen_public_initial_workset: @@ -217,19 +244,14 @@ Proof. apply H0. auto. Qed. -(** * Semantic preservation *) +(** * Correctness of the transformation with respect to the relational specification *) -Section SOUNDNESS. -Variable p: program. -Variable tp: program. -Hypothesis TRANSF: transform_program p = OK tp. -Let ge := Genv.globalenv p. -Let tge := Genv.globalenv tp. - -Let pm := program_map p. +(** Correctness of the dependency graph traversal. *) +Section ANALYSIS. -(** Correctness of the dependency graph traversal. *) +Variable p: program. +Let pm := prog_defmap p. Definition workset_invariant (w: workset) : Prop := forall id gd id', @@ -264,7 +286,7 @@ Proof. Qed. Theorem used_globals_sound: - forall u, used_globals p = Some u -> used_set_closed u. + forall u, used_globals p pm = Some u -> used_set_closed u. Proof. unfold used_globals; intros. eapply PrimIter.iterate_prop with (P := workset_invariant); eauto. - intros. apply iter_step_invariant; auto. @@ -275,7 +297,7 @@ Proof. Qed. Theorem used_globals_incl: - forall u, used_globals p = Some u -> IS.Subset (initial_workset p) u. + forall u, used_globals p pm = Some u -> IS.Subset (initial_workset p) u. Proof. unfold used_globals; intros. eapply PrimIter.iterate_prop with (P := fun (w: workset) => IS.Subset (initial_workset p) w); eauto. @@ -286,35 +308,34 @@ Proof. - red; auto. Qed. -Definition used: IS.t := - match used_globals p with Some u => u | None => IS.empty end. - -Remark USED_GLOBALS: used_globals p = Some used. +Corollary used_globals_valid: + forall u, + used_globals p pm = Some u -> + IS.for_all (global_defined p pm) u = true -> + valid_used_set p u. Proof. - unfold used. unfold transform_program in TRANSF. destruct (used_globals p). auto. discriminate. + intros. constructor. +- intros. eapply used_globals_sound; eauto. +- eapply used_globals_incl; eauto. apply seen_main_initial_workset. +- intros. eapply used_globals_incl; eauto. apply seen_public_initial_workset; auto. +- intros. apply ISF.for_all_iff in H0. ++ red in H0. apply H0 in H1. unfold global_defined in H1. + destruct pm!id as [g|] eqn:E. +* left. change id with (fst (id,g)). apply in_map. apply in_prog_defmap; auto. +* InvBooleans; auto. ++ hnf. simpl; intros; congruence. Qed. -Definition kept (id: ident) : Prop := IS.In id used. +End ANALYSIS. -Theorem kept_closed: - forall id gd id', - kept id -> pm!id = Some gd -> ref_def gd id' -> kept id'. -Proof. - intros. assert (UC: used_set_closed used) by (apply used_globals_sound; apply USED_GLOBALS). - eapply UC; eauto. -Qed. +(** Properties of the elimination of unused global definitions. *) -Theorem kept_main: - kept p.(prog_main). -Proof. - unfold kept. eapply used_globals_incl; eauto. apply USED_GLOBALS. apply seen_main_initial_workset. -Qed. +Section TRANSFORMATION. -Theorem kept_public: - forall id, In id p.(prog_public) -> kept id. -Proof. - intros. unfold kept. eapply used_globals_incl; eauto. apply USED_GLOBALS. apply seen_public_initial_workset; auto. -Qed. +Variable p: program. +Variable used: IS.t. + +Let add_def (m: prog_map) idg := PTree.set (fst idg) (snd idg) m. Remark filter_globdefs_accu: forall defs accu1 accu2 u, @@ -333,98 +354,154 @@ Proof. intros. rewrite <- filter_globdefs_accu. auto. Qed. -Theorem transform_program_charact: - forall id, (program_map tp)!id = if IS.mem id used then pm!id else None. +Lemma filter_globdefs_map_1: + forall id l u m1, + IS.mem id u = false -> + m1!id = None -> + (fold_left add_def (filter_globdefs u nil l) m1)!id = None. Proof. - intros. - assert (X: forall l u m1 m2, - IS.In id u -> - m1!id = m2!id -> - (fold_left add_def_prog_map (filter_globdefs u nil l) m1)!id = - (fold_left add_def_prog_map (List.rev l) m2)!id). - { - induction l; simpl; intros. - auto. - destruct a as [id1 gd1]. rewrite fold_left_app. simpl. - destruct (IS.mem id1 u) eqn:MEM. - rewrite filter_globdefs_nil. rewrite fold_left_app. simpl. - unfold add_def_prog_map at 1 3. simpl. - rewrite ! PTree.gsspec. destruct (peq id id1). auto. - apply IHl; auto. apply IS.remove_2; auto. - unfold add_def_prog_map at 2. simpl. rewrite PTree.gso. apply IHl; auto. - red; intros; subst id1. - assert (IS.mem id u = true) by (apply IS.mem_1; auto). congruence. - } - assert (Y: forall l u m1, - IS.mem id u = false -> - m1!id = None -> - (fold_left add_def_prog_map (filter_globdefs u nil l) m1)!id = None). - { - induction l; simpl; intros. - auto. - destruct a as [id1 gd1]. - destruct (IS.mem id1 u) eqn:MEM. - rewrite filter_globdefs_nil. rewrite fold_left_app. simpl. - unfold add_def_prog_map at 1. simpl. rewrite PTree.gso by congruence. eapply IHl; eauto. - rewrite ISF.remove_b. rewrite H; auto. - eapply IHl; eauto. - } - unfold pm, program_map. - unfold transform_program in TRANSF; rewrite USED_GLOBALS in TRANSF. inversion TRANSF. - simpl. destruct (IS.mem id used) eqn: MEM. - erewrite X. rewrite List.rev_involutive. eauto. apply IS.mem_2; auto. auto. - apply Y. auto. apply PTree.gempty. -Qed. - -(** Program map and Genv operations *) - -Definition genv_progmap_match (ge: genv) (pm: prog_map) : Prop := - forall id, - match Genv.find_symbol ge id with - | None => pm!id = None - | Some b => - match pm!id with - | None => False - | Some (Gfun fd) => Genv.find_funct_ptr ge b = Some fd - | Some (Gvar gv) => Genv.find_var_info ge b = Some gv - end - end. + induction l as [ | [id1 gd1] l]; simpl; intros. +- auto. +- destruct (IS.mem id1 u) eqn:MEM. ++ rewrite filter_globdefs_nil. rewrite fold_left_app. simpl. + unfold add_def at 1. simpl. rewrite PTree.gso by congruence. eapply IHl; eauto. + rewrite ISF.remove_b. rewrite H; auto. ++ eapply IHl; eauto. +Qed. -Lemma genv_program_map: - forall p, genv_progmap_match (Genv.globalenv p) (program_map p). +Lemma filter_globdefs_map_2: + forall id l u m1 m2, + IS.mem id u = true -> + m1!id = m2!id -> + (fold_left add_def (filter_globdefs u nil l) m1)!id = (fold_left add_def (List.rev l) m2)!id. Proof. - intros. unfold Genv.globalenv, program_map. - assert (REC: forall defs g m, - genv_progmap_match g m -> - genv_progmap_match (Genv.add_globals g defs) (fold_left add_def_prog_map defs m)). - { - induction defs; simpl; intros. - auto. - apply IHdefs. red; intros. specialize (H id). - destruct a as [id1 [fd|gv]]; - unfold Genv.add_global, Genv.find_symbol, Genv.find_funct_ptr, Genv.find_var_info, add_def_prog_map in *; - simpl. - - rewrite PTree.gsspec. destruct (peq id id1); subst. - + rewrite ! PTree.gss. auto. - + destruct (Genv.genv_symb g)!id as [b|] eqn:S; rewrite PTree.gso by auto. - * rewrite PTree.gso. auto. apply Plt_ne. eapply Genv.genv_symb_range; eauto. - * auto. - - rewrite PTree.gsspec. destruct (peq id id1); subst. - + rewrite ! PTree.gss. auto. - + destruct (Genv.genv_symb g)!id as [b|] eqn:S; rewrite PTree.gso by auto. - * rewrite PTree.gso. auto. apply Plt_ne. eapply Genv.genv_symb_range; eauto. - * auto. - } - apply REC. red; intros. unfold Genv.find_symbol, Genv.empty_genv; simpl. rewrite ! PTree.gempty; auto. + induction l as [ | [id1 gd1] l]; simpl; intros. +- auto. +- rewrite fold_left_app. simpl. + destruct (IS.mem id1 u) eqn:MEM. ++ rewrite filter_globdefs_nil. rewrite fold_left_app. simpl. + unfold add_def at 1 3. simpl. + rewrite ! PTree.gsspec. destruct (peq id id1). auto. + apply IHl; auto. + apply IS.mem_1. apply IS.remove_2; auto. apply IS.mem_2; auto. ++ unfold add_def at 2. simpl. rewrite PTree.gso by congruence. apply IHl; auto. Qed. -Lemma transform_program_kept: - forall id b, Genv.find_symbol tge id = Some b -> kept id. +Lemma filter_globdefs_map: + forall id u defs, + (PTree_Properties.of_list (filter_globdefs u nil (List.rev defs)))! id = + if IS.mem id u then (PTree_Properties.of_list defs)!id else None. Proof. - intros. generalize (genv_program_map tp id). fold tge; rewrite H. - rewrite transform_program_charact. intros. destruct (IS.mem id used) eqn:U. - unfold kept; apply IS.mem_2; auto. - contradiction. + intros. unfold PTree_Properties.of_list. fold prog_map. unfold PTree.elt. fold add_def. + destruct (IS.mem id u) eqn:MEM. +- erewrite filter_globdefs_map_2. rewrite List.rev_involutive. reflexivity. + auto. auto. +- apply filter_globdefs_map_1. auto. apply PTree.gempty. +Qed. + +Lemma filter_globdefs_domain: + forall id l u, + In id (map fst (filter_globdefs u nil l)) -> IS.In id u /\ In id (map fst l). +Proof. + induction l as [ | [id1 gd1] l]; simpl; intros. +- tauto. +- destruct (IS.mem id1 u) eqn:MEM. ++ rewrite filter_globdefs_nil, map_app, in_app_iff in H. destruct H. + apply IHl in H. rewrite ISF.remove_iff in H. tauto. + simpl in H. destruct H; try tauto. subst id1. split; auto. apply IS.mem_2; auto. ++ apply IHl in H. tauto. +Qed. + +Lemma filter_globdefs_unique_names: + forall l u, list_norepet (map fst (filter_globdefs u nil l)). +Proof. + induction l as [ | [id1 gd1] l]; simpl; intros. +- constructor. +- destruct (IS.mem id1 u) eqn:MEM; auto. + rewrite filter_globdefs_nil, map_app. simpl. + apply list_norepet_append; auto. + constructor. simpl; tauto. constructor. + red; simpl; intros. destruct H0; try tauto. subst y. + apply filter_globdefs_domain in H. rewrite ISF.remove_iff in H. intuition. +Qed. + +End TRANSFORMATION. + +Theorem transf_program_match: + forall p tp, transform_program p = OK tp -> match_prog p tp. +Proof. + unfold transform_program; intros p tp TR. set (pm := prog_defmap p) in *. + destruct (used_globals p pm) as [u|] eqn:U; try discriminate. + destruct (IS.for_all (global_defined p pm) u) eqn:DEF; inv TR. + exists u; split. + apply used_globals_valid; auto. + constructor; simpl; auto. + intros. unfold prog_defmap; simpl. apply filter_globdefs_map. + apply filter_globdefs_unique_names. +Qed. + +(** * Semantic preservation *) + +Section SOUNDNESS. + +Variable p: program. +Variable tp: program. +Variable used: IS.t. +Hypothesis USED_VALID: valid_used_set p used. +Hypothesis TRANSF: match_prog_1 used p tp. +Let ge := Genv.globalenv p. +Let tge := Genv.globalenv tp. +Let pm := prog_defmap p. + +Definition kept (id: ident) : Prop := IS.In id used. + +Lemma kept_closed: + forall id gd id', + kept id -> pm!id = Some gd -> ref_def gd id' -> kept id'. +Proof. + intros. eapply used_closed; eauto. +Qed. + +Lemma kept_main: + kept p.(prog_main). +Proof. + eapply used_main; eauto. +Qed. + +Lemma kept_public: + forall id, In id p.(prog_public) -> kept id. +Proof. + intros. eapply used_public; eauto. +Qed. + +(** Relating [Genv.find_symbol] operations in the original and transformed program *) + +Lemma transform_find_symbol_1: + forall id b, + Genv.find_symbol ge id = Some b -> kept id -> exists b', Genv.find_symbol tge id = Some b'. +Proof. + intros. + assert (A: exists g, (prog_defmap p)!id = Some g). + { apply prog_defmap_dom. eapply Genv.find_symbol_inversion; eauto. } + destruct A as (g & P). + apply Genv.find_symbol_exists with g. + apply in_prog_defmap. + erewrite match_prog_def by eauto. rewrite IS.mem_1 by auto. auto. +Qed. + +Lemma transform_find_symbol_2: + forall id b, + Genv.find_symbol tge id = Some b -> kept id /\ exists b', Genv.find_symbol ge id = Some b'. +Proof. + intros. + assert (A: exists g, (prog_defmap tp)!id = Some g). + { apply prog_defmap_dom. eapply Genv.find_symbol_inversion; eauto. } + destruct A as (g & P). + erewrite match_prog_def in P by eauto. + destruct (IS.mem id used) eqn:U; try discriminate. + split. apply IS.mem_2; auto. + apply Genv.find_symbol_exists with g. + apply in_prog_defmap. auto. Qed. (** Injections that preserve used globals. *) @@ -439,16 +516,13 @@ Record meminj_preserves_globals (f: meminj) : Prop := { symbols_inject_3: forall id b', Genv.find_symbol tge id = Some b' -> exists b, Genv.find_symbol ge id = Some b /\ f b = Some(b', 0); - funct_ptr_inject: forall b b' delta fd, - f b = Some(b', delta) -> Genv.find_funct_ptr ge b = Some fd -> - Genv.find_funct_ptr tge b' = Some fd /\ delta = 0 /\ - (forall id, ref_fundef fd id -> kept id); - var_info_inject: forall b b' delta gv, - f b = Some(b', delta) -> Genv.find_var_info ge b = Some gv -> - Genv.find_var_info tge b' = Some gv /\ delta = 0; - var_info_rev_inject: forall b b' delta gv, - f b = Some(b', delta) -> Genv.find_var_info tge b' = Some gv -> - Genv.find_var_info ge b = Some gv /\ delta = 0 + defs_inject: forall b b' delta gd, + f b = Some(b', delta) -> Genv.find_def ge b = Some gd -> + Genv.find_def tge b' = Some gd /\ delta = 0 /\ + (forall id, ref_def gd id -> kept id); + defs_rev_inject: forall b b' delta gd, + f b = Some(b', delta) -> Genv.find_def tge b' = Some gd -> + Genv.find_def ge b = Some gd /\ delta = 0 }. Definition init_meminj : meminj := @@ -462,6 +536,14 @@ Definition init_meminj : meminj := | None => None end. +Remark init_meminj_eq: + forall id b b', + Genv.find_symbol ge id = Some b -> Genv.find_symbol tge id = Some b' -> + init_meminj b = Some(b', 0). +Proof. + intros. unfold init_meminj. erewrite Genv.find_invert_symbol by eauto. rewrite H0. auto. +Qed. + Remark init_meminj_invert: forall b b' delta, init_meminj b = Some(b', delta) -> @@ -480,44 +562,26 @@ Proof. - exploit init_meminj_invert; eauto. intros (A & id1 & B & C). assert (id1 = id) by (eapply (Genv.genv_vars_inj ge); eauto). subst id1. auto. -- unfold init_meminj. erewrite Genv.find_invert_symbol by eauto. apply IS.mem_1 in H. - generalize (genv_program_map p id) (genv_program_map tp id). fold ge; fold tge; fold pm. - rewrite transform_program_charact. rewrite H, H0. - destruct (Genv.find_symbol tge id) as [b'|]; intros. - exists b'; auto. rewrite H2 in H1; contradiction. -- generalize (genv_program_map tp id). fold tge. rewrite H. intros. - destruct (program_map tp)!id as [gd|] eqn:PM; try contradiction. - generalize (transform_program_charact id). rewrite PM. - destruct (IS.mem id used) eqn:USED; intros; try discriminate. - generalize (genv_program_map p id). fold ge; fold pm. - destruct (Genv.find_symbol ge id) as [b|] eqn:FS; intros; try congruence. - exists b; split; auto. unfold init_meminj. - erewrite Genv.find_invert_symbol by eauto. rewrite H. auto. +- exploit transform_find_symbol_1; eauto. intros (b' & F). exists b'; split; auto. + eapply init_meminj_eq; eauto. +- exploit transform_find_symbol_2; eauto. intros (K & b & F). + exists b; split; auto. eapply init_meminj_eq; eauto. +- exploit init_meminj_invert; eauto. intros (A & id & B & C). + assert (kept id) by (eapply transform_find_symbol_2; eauto). + assert (pm!id = Some gd). + { unfold pm; rewrite Genv.find_def_symbol. exists b; auto. } + assert ((prog_defmap tp)!id = Some gd). + { erewrite match_prog_def by eauto. rewrite IS.mem_1 by auto. auto. } + rewrite Genv.find_def_symbol in H3. destruct H3 as (b1 & P & Q). + fold tge in P. replace b' with b1 by congruence. split; auto. split; auto. + intros. eapply kept_closed; eauto. - exploit init_meminj_invert; eauto. intros (A & id & B & C). - generalize (genv_program_map p id) (genv_program_map tp id). fold ge; fold tge; fold pm. - rewrite transform_program_charact. rewrite B, C. intros. - destruct (IS.mem id used) eqn:KEPT; try contradiction. - destruct (pm!id) as [gd|] eqn:PM; try contradiction. - destruct gd as [fd'|gv']. - + assert (fd' = fd) by congruence. subst fd'. split. auto. split. auto. - intros. eapply kept_closed; eauto. red; apply IS.mem_2; auto. - + assert (b <> b) by (eapply Genv.genv_funs_vars; eassumption). congruence. -- exploit init_meminj_invert; eauto. intros (A & id & B & C). split; auto. - generalize (genv_program_map p id) (genv_program_map tp id). fold ge; fold tge; fold pm. - rewrite transform_program_charact. rewrite B, C. intros. - destruct (IS.mem id used); try contradiction. - destruct (pm!id) as [gd|]; try contradiction. - destruct gd as [fd'|gv']. - + assert (b <> b) by (eapply Genv.genv_funs_vars; eassumption). congruence. - + congruence. -- exploit init_meminj_invert; eauto. intros (A & id & B & C). split; auto. - generalize (genv_program_map p id) (genv_program_map tp id). fold ge; fold tge; fold pm. - rewrite transform_program_charact. rewrite B, C. intros. - destruct (IS.mem id used); try contradiction. - destruct (pm!id) as [gd|]; try contradiction. - destruct gd as [fd'|gv']. - + assert (b' <> b') by (eapply Genv.genv_funs_vars; eassumption). congruence. - + congruence. + assert ((prog_defmap tp)!id = Some gd). + { rewrite Genv.find_def_symbol. exists b'; auto. } + erewrite match_prog_def in H1 by eauto. + destruct (IS.mem id used); try discriminate. + rewrite Genv.find_def_symbol in H1. destruct H1 as (b1 & P & Q). + fold ge in P. replace b with b1 by congruence. auto. Qed. Lemma globals_symbols_inject: @@ -527,28 +591,33 @@ Proof. assert (E1: Genv.genv_public ge = p.(prog_public)). { apply Genv.globalenv_public. } assert (E2: Genv.genv_public tge = p.(prog_public)). - { unfold tge; rewrite Genv.globalenv_public. - unfold transform_program in TRANSF. rewrite USED_GLOBALS in TRANSF. inversion TRANSF. auto. } + { unfold tge; rewrite Genv.globalenv_public. eapply match_prog_public; eauto. } split; [|split;[|split]]; intros. + simpl; unfold Genv.public_symbol; rewrite E1, E2. destruct (Genv.find_symbol tge id) as [b'|] eqn:TFS. exploit symbols_inject_3; eauto. intros (b & FS & INJ). rewrite FS. auto. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto. destruct (in_dec ident_eq id (prog_public p)); simpl; auto. - exploit symbols_inject_2; eauto. apply kept_public; auto. + exploit symbols_inject_2; eauto. + eapply kept_public; eauto. intros (b' & TFS' & INJ). congruence. + eapply symbols_inject_1; eauto. + simpl in *; unfold Genv.public_symbol in H0. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; try discriminate. rewrite E1 in H0. destruct (in_dec ident_eq id (prog_public p)); try discriminate. inv H1. - exploit symbols_inject_2; eauto. apply kept_public; auto. + exploit symbols_inject_2; eauto. + eapply kept_public; eauto. intros (b' & A & B); exists b'; auto. + simpl. unfold Genv.block_is_volatile. destruct (Genv.find_var_info ge b1) as [gv|] eqn:V1. - exploit var_info_inject; eauto. intros [A B]. rewrite A. auto. + rewrite Genv.find_var_info_iff in V1. + exploit defs_inject; eauto. intros (A & B & C). + rewrite <- Genv.find_var_info_iff in A. rewrite A; auto. destruct (Genv.find_var_info tge b2) as [gv|] eqn:V2; auto. - exploit var_info_rev_inject; eauto. intros [A B]. congruence. + rewrite Genv.find_var_info_iff in V2. + exploit defs_rev_inject; eauto. intros (A & B). + rewrite <- Genv.find_var_info_iff in A. congruence. Qed. Lemma symbol_address_inject: @@ -661,12 +730,10 @@ Proof. exists b'; auto. + exploit symbols_inject_3; eauto. intros (b & A & B). exists b; auto. - + eapply funct_ptr_inject; eauto. apply SAME; auto. - eapply Genv.genv_funs_range; eauto. - + eapply var_info_inject; eauto. apply SAME; auto. - eapply Genv.genv_vars_range; eauto. - + eapply var_info_rev_inject; eauto. apply SAME'; auto. - eapply Genv.genv_vars_range; eauto. + + eapply defs_inject; eauto. apply SAME; auto. + eapply Genv.genv_defs_range; eauto. + + eapply defs_rev_inject; eauto. apply SAME'; auto. + eapply Genv.genv_defs_range; eauto. - econstructor; eauto. apply IHmatch_stacks. intros. exploit H1; eauto. intros [A B]. split; eapply Ple_trans; eauto. @@ -738,11 +805,15 @@ Proof. - exploit Genv.find_funct_inv; eauto. intros (b & R). rewrite R in H0. rewrite Genv.find_funct_find_funct_ptr in H0. specialize (H1 r). rewrite R in H1. inv H1. - exploit funct_ptr_inject; eauto. intros (A & B & C). + rewrite Genv.find_funct_ptr_iff in H0. + exploit defs_inject; eauto. intros (A & B & C). + rewrite <- Genv.find_funct_ptr_iff in A. rewrite B; auto. - destruct (Genv.find_symbol ge id) as [b|] eqn:FS; try discriminate. exploit symbols_inject_2; eauto. intros (tb & P & Q). rewrite P. - exploit funct_ptr_inject; eauto. intros (A & B & C). + rewrite Genv.find_funct_ptr_iff in H0. + exploit defs_inject; eauto. intros (A & B & C). + rewrite <- Genv.find_funct_ptr_iff in A. auto. Qed. @@ -973,285 +1044,159 @@ Qed. (** Relating initial memory states *) -Remark init_meminj_no_overlap: - forall m, Mem.meminj_no_overlap init_meminj m. +(* +Remark genv_find_def_exists: + forall (F V: Type) (p: AST.program F V) b, + Plt b (Genv.genv_next (Genv.globalenv p)) -> + exists gd, Genv.find_def (Genv.globalenv p) b = Some gd. Proof. - intros; red; intros. - exploit init_meminj_invert. eexact H0. intros (A1 & id1 & B1 & C1). - exploit init_meminj_invert. eexact H1. intros (A2 & id2 & B2 & C2). - left; red; intros; subst b2'. - assert (id1 = id2) by (eapply Genv.genv_vars_inj; eauto). - congruence. + intros until b. + set (P := fun (g: Genv.t F V) => + Plt b (Genv.genv_next g) -> exists gd, (Genv.genv_defs g)!b = Some gd). + assert (forall l g, P g -> P (Genv.add_globals g l)). + { induction l as [ | [id1 g1] l]; simpl; intros. + - auto. + - apply IHl. unfold Genv.add_global, P; simpl. intros LT. apply Plt_succ_inv in LT. destruct LT. + + rewrite PTree.gso. apply H; auto. apply Plt_ne; auto. + + rewrite H0. rewrite PTree.gss. exists g1; auto. } + apply H. red; simpl; intros. exfalso; xomega. Qed. +*) -Lemma store_zeros_unmapped_inj: - forall m1 b1 i n m1', - store_zeros m1 b1 i n = Some m1' -> - forall m2, - Mem.mem_inj init_meminj m1 m2 -> - init_meminj b1 = None -> - Mem.mem_inj init_meminj m1' m2. -Proof. - intros until m1'. functional induction (store_zeros m1 b1 i n); intros. - inv H. auto. - eapply IHo; eauto. eapply Mem.store_unmapped_inj; eauto. - discriminate. -Qed. - -Lemma store_zeros_mapped_inj: - forall m1 b1 i n m1', - store_zeros m1 b1 i n = Some m1' -> - forall m2 b2, - Mem.mem_inj init_meminj m1 m2 -> - init_meminj b1 = Some(b2, 0) -> - exists m2', store_zeros m2 b2 i n = Some m2' /\ Mem.mem_inj init_meminj m1' m2'. -Proof. - intros until m1'. functional induction (store_zeros m1 b1 i n); intros. - inv H. exists m2; split; auto. rewrite store_zeros_equation, e; auto. - exploit Mem.store_mapped_inj; eauto. apply init_meminj_no_overlap. instantiate (1 := Vzero); constructor. - intros (m2' & A & B). rewrite Zplus_0_r in A. - exploit IHo; eauto. intros (m3' & C & D). - exists m3'; split; auto. rewrite store_zeros_equation, e, A, C; auto. - discriminate. -Qed. - -Lemma store_init_data_unmapped_inj: - forall m1 b1 i id m1' m2, - Genv.store_init_data ge m1 b1 i id = Some m1' -> - Mem.mem_inj init_meminj m1 m2 -> - init_meminj b1 = None -> - Mem.mem_inj init_meminj m1' m2. -Proof. - intros. destruct id; simpl in H; try (eapply Mem.store_unmapped_inj; now eauto). - inv H; auto. - destruct (Genv.find_symbol ge i0); try discriminate. eapply Mem.store_unmapped_inj; now eauto. -Qed. - -Lemma store_init_data_mapped_inj: - forall m1 b1 i init m1' b2 m2, - Genv.store_init_data ge m1 b1 i init = Some m1' -> - Mem.mem_inj init_meminj m1 m2 -> - init_meminj b1 = Some(b2, 0) -> - (forall id ofs, init = Init_addrof id ofs -> kept id) -> - exists m2', Genv.store_init_data tge m2 b2 i init = Some m2' /\ Mem.mem_inj init_meminj m1' m2'. -Proof. - intros. replace i with (i + 0) by omega. pose proof (init_meminj_no_overlap m1). - destruct init; simpl in *; try (eapply Mem.store_mapped_inj; now eauto). - inv H. exists m2; auto. - destruct (Genv.find_symbol ge i0) as [bi|] eqn:FS1; try discriminate. - exploit symbols_inject_2. eapply init_meminj_preserves_globals. eapply H2; eauto. eauto. - intros (bi' & A & B). rewrite A. eapply Mem.store_mapped_inj; eauto. - econstructor; eauto. rewrite Int.add_zero; auto. +Lemma init_meminj_invert_strong: + forall b b' delta, + init_meminj b = Some(b', delta) -> + delta = 0 /\ + exists id gd, + Genv.find_symbol ge id = Some b + /\ Genv.find_symbol tge id = Some b' + /\ Genv.find_def ge b = Some gd + /\ Genv.find_def tge b' = Some gd + /\ (forall i, ref_def gd i -> kept i). +Proof. + intros. exploit init_meminj_invert; eauto. intros (A & id & B & C). + assert (exists gd, (prog_defmap p)!id = Some gd). + { apply prog_defmap_dom. eapply Genv.find_symbol_inversion; eauto. } + destruct H0 as [gd DM]. rewrite Genv.find_def_symbol in DM. + destruct DM as (b'' & P & Q). fold ge in P. rewrite P in B; inv B. + fold ge in Q. exploit defs_inject. apply init_meminj_preserves_globals. + eauto. eauto. intros (X & _ & Y). + split. auto. exists id, gd; auto. Qed. - Lemma store_init_data_list_unmapped_inj: - forall initlist m1 b1 i m1' m2, - Genv.store_init_data_list ge m1 b1 i initlist = Some m1' -> - Mem.mem_inj init_meminj m1 m2 -> - init_meminj b1 = None -> - Mem.mem_inj init_meminj m1' m2. -Proof. - induction initlist; simpl; intros. -- inv H; auto. -- destruct (Genv.store_init_data ge m1 b1 i a) as [m1''|] eqn:ST; try discriminate. - eapply IHinitlist; eauto. eapply store_init_data_unmapped_inj; eauto. -Qed. - -Lemma store_init_data_list_mapped_inj: - forall initlist m1 b1 i m1' b2 m2, - Genv.store_init_data_list ge m1 b1 i initlist = Some m1' -> - Mem.mem_inj init_meminj m1 m2 -> - init_meminj b1 = Some(b2, 0) -> - (forall id ofs, In (Init_addrof id ofs) initlist -> kept id) -> - exists m2', Genv.store_init_data_list tge m2 b2 i initlist = Some m2' /\ Mem.mem_inj init_meminj m1' m2'. -Proof. - induction initlist; simpl; intros. -- inv H. exists m2; auto. -- destruct (Genv.store_init_data ge m1 b1 i a) as [m1''|] eqn:ST; try discriminate. - exploit store_init_data_mapped_inj; eauto. intros (m2'' & A & B). - exploit IHinitlist; eauto. intros (m2' & C & D). - exists m2'; split; auto. rewrite A; auto. -Qed. - -Lemma alloc_global_unmapped_inj: - forall m1 id g m1' m2, - Genv.alloc_global ge m1 (id, g) = Some m1' -> - Mem.mem_inj init_meminj m1 m2 -> - init_meminj (Mem.nextblock m1) = None -> - Mem.mem_inj init_meminj m1' m2. -Proof. - unfold Genv.alloc_global; intros. destruct g as [fd|gv]. -- destruct (Mem.alloc m1 0 1) as (m1a, b) eqn:ALLOC. - exploit Mem.alloc_result; eauto. intros EQ. rewrite <- EQ in H1. - eapply Mem.drop_unmapped_inj with (m1 := m1a); eauto. - eapply Mem.alloc_left_unmapped_inj; eauto. -- set (sz := Genv.init_data_list_size (gvar_init gv)) in *. - destruct (Mem.alloc m1 0 sz) as (m1a, b) eqn:ALLOC. - destruct (store_zeros m1a b 0 sz) as [m1b|] eqn: STZ; try discriminate. - destruct (Genv.store_init_data_list ge m1b b 0 (gvar_init gv)) as [m1c|] eqn:ST; try discriminate. - exploit Mem.alloc_result; eauto. intros EQ. rewrite <- EQ in H1. - eapply Mem.drop_unmapped_inj with (m1 := m1c); eauto. - eapply store_init_data_list_unmapped_inj with (m1 := m1b); eauto. - eapply store_zeros_unmapped_inj with (m1 := m1a); eauto. - eapply Mem.alloc_left_unmapped_inj; eauto. -Qed. - -Lemma alloc_global_mapped_inj: - forall m1 id g m1' m2, - Genv.alloc_global ge m1 (id, g) = Some m1' -> - Mem.mem_inj init_meminj m1 m2 -> - init_meminj (Mem.nextblock m1) = Some(Mem.nextblock m2, 0) -> - (forall id, ref_def g id -> kept id) -> - exists m2', - Genv.alloc_global tge m2 (id, g) = Some m2' /\ Mem.mem_inj init_meminj m1' m2'. -Proof. - unfold Genv.alloc_global; intros. destruct g as [fd|gv]. -- destruct (Mem.alloc m1 0 1) as (m1a, b1) eqn:ALLOC. - exploit Mem.alloc_result; eauto. intros EQ. rewrite <- EQ in H1. - destruct (Mem.alloc m2 0 1) as (m2a, b2) eqn:ALLOC2. - exploit Mem.alloc_result; eauto. intros EQ2. rewrite <- EQ2 in H1. - assert (Mem.mem_inj init_meminj m1a m2a). - { eapply Mem.alloc_left_mapped_inj with (b1 := b1) (b2 := b2) (delta := 0). - eapply Mem.alloc_right_inj; eauto. - eauto. - eauto with mem. - red; intros; apply Z.divide_0_r. - intros. apply Mem.perm_implies with Freeable; auto with mem. - eapply Mem.perm_alloc_2; eauto. omega. - auto. - } - exploit Mem.drop_mapped_inj; eauto. apply init_meminj_no_overlap. -- set (sz := Genv.init_data_list_size (gvar_init gv)) in *. - destruct (Mem.alloc m1 0 sz) as (m1a, b1) eqn:ALLOC. - destruct (store_zeros m1a b1 0 sz) as [m1b|] eqn: STZ; try discriminate. - destruct (Genv.store_init_data_list ge m1b b1 0 (gvar_init gv)) as [m1c|] eqn:ST; try discriminate. - exploit Mem.alloc_result; eauto. intros EQ. rewrite <- EQ in H1. - destruct (Mem.alloc m2 0 sz) as (m2a, b2) eqn:ALLOC2. - exploit Mem.alloc_result; eauto. intros EQ2. rewrite <- EQ2 in H1. - assert (Mem.mem_inj init_meminj m1a m2a). - { eapply Mem.alloc_left_mapped_inj with (b1 := b1) (b2 := b2) (delta := 0). - eapply Mem.alloc_right_inj; eauto. - eauto. - eauto with mem. - red; intros; apply Z.divide_0_r. - intros. apply Mem.perm_implies with Freeable; auto with mem. - eapply Mem.perm_alloc_2; eauto. omega. - auto. - } - exploit store_zeros_mapped_inj; eauto. intros (m2b & A & B). - exploit store_init_data_list_mapped_inj; eauto. - intros. apply H2. red. exists ofs; auto. intros (m2c & C & D). - exploit Mem.drop_mapped_inj; eauto. apply init_meminj_no_overlap. intros (m2' & E & F). - exists m2'; split; auto. rewrite ! Zplus_0_r in E. rewrite A, C, E. auto. -Qed. - -Lemma alloc_globals_app: - forall F V (g: Genv.t F V) defs1 m defs2, - Genv.alloc_globals g m (defs1 ++ defs2) = - match Genv.alloc_globals g m defs1 with - | None => None - | Some m1 => Genv.alloc_globals g m1 defs2 - end. +Section INIT_MEM. + +Variables m tm: mem. +Hypothesis IM: Genv.init_mem p = Some m. +Hypothesis TIM: Genv.init_mem tp = Some tm. + +Lemma bytes_of_init_inject: + forall il, + (forall id, ref_init il id -> kept id) -> + list_forall2 (memval_inject init_meminj) (Genv.bytes_of_init_data_list ge il) (Genv.bytes_of_init_data_list tge il). Proof. - induction defs1; simpl; intros. auto. - destruct (Genv.alloc_global g m a); auto. + induction il as [ | i1 il]; simpl; intros. +- constructor. +- apply list_forall2_app. ++ destruct i1; simpl; try (apply inj_bytes_inject). + induction (Z.to_nat z); simpl; constructor. constructor. auto. + destruct (Genv.find_symbol ge i) as [b|] eqn:FS. + assert (kept i). { apply H. red. exists i0; auto with coqlib. } + exploit symbols_inject_2. apply init_meminj_preserves_globals. eauto. eauto. + intros (b' & A & B). rewrite A. apply inj_value_inject. + econstructor; eauto. symmetry; apply Int.add_zero. + destruct (Genv.find_symbol tge i) as [b'|] eqn:FS'. + exploit symbols_inject_3. apply init_meminj_preserves_globals. eauto. + intros (b & A & B). congruence. + apply repeat_Undef_inject_self with (n := 4%nat). ++ apply IHil. intros id [ofs IN]. apply H. exists ofs; auto with coqlib. Qed. -Lemma alloc_globals_snoc: - forall F V (g: Genv.t F V) m defs1 id_def, - Genv.alloc_globals g m (defs1 ++ id_def :: nil) = - match Genv.alloc_globals g m defs1 with - | None => None - | Some m1 => Genv.alloc_global g m1 id_def - end. +Lemma Mem_getN_forall2: + forall (P: memval -> memval -> Prop) c1 c2 i n p, + list_forall2 P (Mem.getN n p c1) (Mem.getN n p c2) -> + p <= i -> i < p + Z.of_nat n -> + P (ZMap.get i c1) (ZMap.get i c2). Proof. - intros. rewrite alloc_globals_app. - destruct (Genv.alloc_globals g m defs1); auto. unfold Genv.alloc_globals. - destruct (Genv.alloc_global g m0 id_def); auto. -Qed. - -Lemma alloc_globals_inj: - forall pubs defs m1 u g1 g2, - Genv.alloc_globals ge Mem.empty (List.rev defs) = Some m1 -> - g1 = Genv.add_globals (Genv.empty_genv _ _ pubs) (List.rev defs) -> - g2 = Genv.add_globals (Genv.empty_genv _ _ pubs) (filter_globdefs u nil defs) -> - Mem.nextblock m1 = Genv.genv_next g1 -> - (forall id, IS.In id u -> Genv.find_symbol g1 id = Genv.find_symbol ge id) -> - (forall id, IS.In id u -> Genv.find_symbol g2 id = Genv.find_symbol tge id) -> - (forall b id, Genv.find_symbol ge id = Some b -> Plt b (Mem.nextblock m1) -> kept id -> IS.In id u) -> - (forall id, IS.In id u -> (fold_left add_def_prog_map (List.rev defs) (PTree.empty _))!id = pm!id) -> - exists m2, - Genv.alloc_globals tge Mem.empty (filter_globdefs u nil defs) = Some m2 - /\ Mem.nextblock m2 = Genv.genv_next g2 - /\ Mem.mem_inj init_meminj m1 m2. -Proof. - induction defs; simpl; intros until g2; intros ALLOC GE1 GE2 NEXT1 SYMB1 SYMB2 SYMB3 PROGMAP. -- inv ALLOC. exists Mem.empty. intuition auto. constructor; intros. - eelim Mem.perm_empty; eauto. - exploit init_meminj_invert; eauto. intros [A B]. subst delta. apply Z.divide_0_r. - eelim Mem.perm_empty; eauto. -- rewrite Genv.add_globals_app in GE1. simpl in GE1. - set (g1' := Genv.add_globals (Genv.empty_genv fundef unit pubs) (rev defs)) in *. - rewrite alloc_globals_snoc in ALLOC. - destruct (Genv.alloc_globals ge Mem.empty (rev defs)) as [m1'|] eqn:ALLOC1'; try discriminate. - exploit Genv.alloc_global_nextblock; eauto. intros NEXTBLOCK1. - assert (NEXTGE1: Genv.genv_next g1 = Pos.succ (Genv.genv_next g1')) by (rewrite GE1; reflexivity). - assert (NEXT1': Mem.nextblock m1' = Genv.genv_next g1') by (unfold block in *; xomega). - rewrite fold_left_app in PROGMAP. simpl in PROGMAP. - destruct a as [id gd]. unfold add_def_prog_map at 1 in PROGMAP. simpl in PROGMAP. - destruct (IS.mem id u) eqn:MEM. - + rewrite filter_globdefs_nil in *. rewrite alloc_globals_snoc. - rewrite Genv.add_globals_app in GE2. simpl in GE2. - set (g2' := Genv.add_globals (Genv.empty_genv fundef unit pubs) (filter_globdefs (IS.remove id u) nil defs)) in *. - assert (NEXTGE2: Genv.genv_next g2 = Pos.succ (Genv.genv_next g2')) by (rewrite GE2; reflexivity). - assert (FS1: Genv.find_symbol ge id = Some (Mem.nextblock m1')). - { rewrite <- SYMB1 by (apply IS.mem_2; auto). - rewrite GE1. unfold Genv.find_symbol; simpl. rewrite PTree.gss. congruence. } - exploit (IHdefs m1' (IS.remove id u) g1' g2'); eauto. - intros. rewrite ISF.remove_iff in H; destruct H. - rewrite <- SYMB1 by auto. rewrite GE1. unfold Genv.find_symbol; simpl. - rewrite PTree.gso; auto. - intros. rewrite ISF.remove_iff in H; destruct H. - rewrite <- SYMB2 by auto. rewrite GE2. unfold Genv.find_symbol; simpl. - rewrite PTree.gso; auto. - intros. rewrite ISF.remove_iff. destruct (ident_eq id id0). - subst id0. rewrite FS1 in H. inv H. eelim Plt_strict; eauto. - exploit SYMB3. eexact H. unfold block in *; xomega. auto. tauto. - intros. rewrite ISF.remove_iff in H; destruct H. - rewrite <- PROGMAP by auto. rewrite PTree.gso by auto. auto. - intros (m2' & A & B & C). fold g2' in B. - assert (FS2: Genv.find_symbol tge id = Some (Mem.nextblock m2')). - { rewrite <- SYMB2 by (apply IS.mem_2; auto). - rewrite GE2. unfold Genv.find_symbol; simpl. rewrite PTree.gss. congruence. } - assert (INJ: init_meminj (Mem.nextblock m1') = Some (Mem.nextblock m2', 0)). - { apply Genv.find_invert_symbol in FS1. unfold init_meminj. rewrite FS1, FS2. auto. } - exploit alloc_global_mapped_inj. eexact ALLOC. eexact C. exact INJ. - intros. apply kept_closed with id gd. eapply transform_program_kept; eauto. - rewrite <- PROGMAP by (apply IS.mem_2; auto). apply PTree.gss. auto. - intros (m2 & D & E). - exploit Genv.alloc_global_nextblock; eauto. intros NEXTBLOCK2. - exists m2; split. rewrite A, D. auto. - split. unfold block in *; xomega. - auto. - + exploit (IHdefs m1' u g1' g2); auto. - intros. rewrite <- SYMB1 by auto. rewrite GE1. - unfold Genv.find_symbol; simpl. rewrite PTree.gso; auto. - red; intros; subst id0. apply IS.mem_1 in H. congruence. - intros. eapply SYMB3; eauto. unfold block in *; xomega. - intros. rewrite <- PROGMAP by auto. rewrite PTree.gso; auto. - apply IS.mem_1 in H. congruence. - intros (m2 & A & B & C). - assert (NOTINJ: init_meminj (Mem.nextblock m1') = None). - { destruct (init_meminj (Mem.nextblock m1')) as [[b' delta]|] eqn:J; auto. - exploit init_meminj_invert; eauto. intros (U & id1 & V & W). - exploit SYMB3; eauto. unfold block in *; xomega. - eapply transform_program_kept; eauto. - intros P. - revert V. rewrite <- SYMB1, GE1 by auto. unfold Genv.find_symbol; simpl. - rewrite PTree.gsspec. rewrite NEXT1'. destruct (peq id1 id); intros Q. - subst id1. apply IS.mem_1 in P. congruence. - eelim Plt_strict. eapply Genv.genv_symb_range; eauto. } - exists m2; intuition auto. eapply alloc_global_unmapped_inj; eauto. + induction n; simpl Mem.getN; intros. +- simpl in H1. omegaContradiction. +- inv H. rewrite inj_S in H1. destruct (zeq i p0). ++ congruence. ++ apply IHn with (p0 + 1); auto. omega. omega. +Qed. + +Lemma init_mem_inj_1: + Mem.mem_inj init_meminj m tm. +Proof. + intros; constructor; intros. +- exploit init_meminj_invert_strong; eauto. intros (A & id & gd & B & C & D & E & F). + exploit (Genv.init_mem_characterization_gen p); eauto. + exploit (Genv.init_mem_characterization_gen tp); eauto. + destruct gd as [f|v]. ++ intros (P2 & Q2) (P1 & Q1). + apply Q1 in H0. destruct H0. subst. + apply Mem.perm_cur. auto. ++ intros (P2 & Q2 & R2 & S2) (P1 & Q1 & R1 & S1). + apply Q1 in H0. destruct H0. subst. + apply Mem.perm_cur. eapply Mem.perm_implies; eauto. + apply P2. omega. +- exploit init_meminj_invert; eauto. intros (A & id & B & C). + subst delta. apply Zdivide_0. +- exploit init_meminj_invert_strong; eauto. intros (A & id & gd & B & C & D & E & F). + exploit (Genv.init_mem_characterization_gen p); eauto. + exploit (Genv.init_mem_characterization_gen tp); eauto. + destruct gd as [f|v]. ++ intros (P2 & Q2) (P1 & Q1). + apply Q1 in H0. destruct H0; discriminate. ++ intros (P2 & Q2 & R2 & S2) (P1 & Q1 & R1 & S1). + apply Q1 in H0. destruct H0. + assert (NO: gvar_volatile v = false). + { unfold Genv.perm_globvar in H1. destruct (gvar_volatile v); auto. inv H1. } +Local Transparent Mem.loadbytes. + generalize (S1 NO). unfold Mem.loadbytes. destruct Mem.range_perm_dec; intros E1; inv E1. + generalize (S2 NO). unfold Mem.loadbytes. destruct Mem.range_perm_dec; intros E2; inv E2. + rewrite Zplus_0_r. + apply Mem_getN_forall2 with (p := 0) (n := nat_of_Z (init_data_list_size (gvar_init v))). + rewrite H3, H4. apply bytes_of_init_inject. auto. + omega. + rewrite nat_of_Z_eq by (apply init_data_list_size_pos). omega. +Qed. + +Lemma init_mem_inj_2: + Mem.inject init_meminj m tm. +Proof. + constructor; intros. +- apply init_mem_inj_1. +- destruct (init_meminj b) as [[b' delta]|] eqn:INJ; auto. + elim H. exploit init_meminj_invert; eauto. intros (A & id & B & C). + eapply Genv.find_symbol_not_fresh; eauto. +- exploit init_meminj_invert; eauto. intros (A & id & B & C). + eapply Genv.find_symbol_not_fresh; eauto. +- red; intros. + exploit init_meminj_invert. eexact H0. intros (A1 & id1 & B1 & C1). + exploit init_meminj_invert. eexact H1. intros (A2 & id2 & B2 & C2). + destruct (ident_eq id1 id2). congruence. left; eapply Genv.global_addresses_distinct; eauto. +- exploit init_meminj_invert; eauto. intros (A & id & B & C). subst delta. + split. omega. generalize (Int.unsigned_range_2 ofs). omega. +Qed. + +End INIT_MEM. + +Lemma init_mem_exists: + forall m, Genv.init_mem p = Some m -> + exists tm, Genv.init_mem tp = Some tm. +Proof. + intros. apply Genv.init_mem_exists. + intros. + assert (P: (prog_defmap tp)!id = Some (Gvar v)). + { eapply prog_defmap_norepet; eauto. eapply match_prog_unique; eauto. } + rewrite (match_prog_def _ _ _ TRANSF) in P. destruct (IS.mem id used) eqn:U; try discriminate. + exploit Genv.init_mem_inversion; eauto. apply in_prog_defmap; eauto. intros [AL FV]. + split. auto. + intros. exploit FV; eauto. intros (b & FS). + apply transform_find_symbol_1 with b; auto. + apply kept_closed with id (Gvar v). + apply IS.mem_2; auto. auto. red. red. exists o; auto. Qed. Theorem init_mem_inject: @@ -1260,40 +1205,25 @@ Theorem init_mem_inject: exists f tm, Genv.init_mem tp = Some tm /\ Mem.inject f m tm /\ meminj_preserves_globals f. Proof. intros. - unfold transform_program in TRANSF; rewrite USED_GLOBALS in TRANSF; injection TRANSF. intros EQ. - destruct (alloc_globals_inj (prog_public p) (List.rev (prog_defs p)) m used ge tge) as (tm & A & B & C). - rewrite rev_involutive; auto. - rewrite rev_involutive; auto. - unfold tge; rewrite <- EQ; auto. - symmetry. apply Genv.init_mem_genv_next; auto. - auto. auto. auto. - intros. rewrite rev_involutive. auto. - assert (D: Genv.init_mem tp = Some tm). - { unfold Genv.init_mem. fold tge. rewrite <- EQ. exact A. } - pose proof (init_meminj_preserves_globals). - exists init_meminj, tm; intuition auto. - constructor; intros. - + auto. - + destruct (init_meminj b) as [[b1 delta1]|] eqn:INJ; auto. - exploit init_meminj_invert; eauto. intros (P & id & Q & R). - elim H1. eapply Genv.find_symbol_not_fresh; eauto. - + exploit init_meminj_invert; eauto. intros (P & id & Q & R). - eapply Genv.find_symbol_not_fresh; eauto. - + apply init_meminj_no_overlap. - + exploit init_meminj_invert; eauto. intros (P & id & Q & R). - split. omega. generalize (Int.unsigned_range_2 ofs). omega. + exploit init_mem_exists; eauto. intros [tm INIT]. + exists init_meminj, tm. + split. auto. + split. eapply init_mem_inj_2; eauto. + apply init_meminj_preserves_globals. Qed. Lemma transf_initial_states: forall S1, initial_state p S1 -> exists S2, initial_state tp S2 /\ match_states S1 S2. Proof. intros. inv H. exploit init_mem_inject; eauto. intros (j & tm & A & B & C). - exploit symbols_inject_2. eauto. apply kept_main. eexact H1. intros (tb & P & Q). - exploit funct_ptr_inject. eauto. eexact Q. exact H2. + exploit symbols_inject_2. eauto. eapply kept_main. eexact H1. intros (tb & P & Q). + rewrite Genv.find_funct_ptr_iff in H2. + exploit defs_inject. eauto. eexact Q. exact H2. intros (R & S & T). + rewrite <- Genv.find_funct_ptr_iff in R. exists (Callstate nil f nil tm); split. econstructor; eauto. - fold tge. unfold transform_program in TRANSF; rewrite USED_GLOBALS in TRANSF; inversion TRANSF; auto. + fold tge. erewrite match_prog_main by eauto. auto. econstructor; eauto. constructor. auto. erewrite <- Genv.init_mem_genv_next by eauto. apply Ple_refl. @@ -1307,7 +1237,7 @@ Proof. intros. inv H0. inv H. inv STACKS. inv RESINJ. constructor. Qed. -Theorem transf_program_correct: +Lemma transf_program_correct_1: forward_simulation (semantics p) (semantics tp). Proof. intros. @@ -1319,3 +1249,175 @@ Proof. Qed. End SOUNDNESS. + +Theorem transf_program_correct: + forall p tp, match_prog p tp -> forward_simulation (semantics p) (semantics tp). +Proof. + intros p tp (used & A & B). apply transf_program_correct_1 with used; auto. +Qed. + +(** * Commutation with linking *) + +Remark link_def_either: + forall (gd1 gd2 gd: globdef fundef unit), + link_def gd1 gd2 = Some gd -> gd = gd1 \/ gd = gd2. +Proof with (try discriminate). + intros until gd. +Local Transparent Linker_def Linker_fundef Linker_varinit Linker_vardef Linker_unit. + destruct gd1 as [f1|v1], gd2 as [f2|v2]... +(* Two fundefs *) + destruct f1 as [f1|ef1], f2 as [f2|ef2]; simpl... + destruct ef2; intuition congruence. + destruct ef1; intuition congruence. + destruct (external_function_eq ef1 ef2); intuition congruence. +(* Two vardefs *) + simpl. unfold link_vardef. destruct v1 as [info1 init1 ro1 vo1], v2 as [info2 init2 ro2 vo2]; simpl. + destruct (link_varinit init1 init2) as [init|] eqn:LI... + destruct (eqb ro1 ro2) eqn:RO... + destruct (eqb vo1 vo2) eqn:VO... + simpl. + destruct info1, info2. + assert (EITHER: init = init1 \/ init = init2). + { revert LI. unfold link_varinit. + destruct (classify_init init1), (classify_init init2); intro EQ; inv EQ; auto. + destruct (zeq sz (Z.max sz0 0 + 0)); inv H0; auto. + destruct (zeq sz (init_data_list_size il)); inv H0; auto. + destruct (zeq sz (init_data_list_size il)); inv H0; auto. } + apply eqb_prop in RO. apply eqb_prop in VO. + intro EQ; inv EQ. destruct EITHER; subst init; auto. +Qed. + +Remark used_not_defined: + forall p used id, + valid_used_set p used -> + (prog_defmap p)!id = None -> + IS.mem id used = false \/ id = prog_main p. +Proof. + intros. destruct (IS.mem id used) eqn:M; auto. + exploit used_defined; eauto using IS.mem_2. intros [A|A]; auto. + apply prog_defmap_dom in A. destruct A as [g E]; congruence. +Qed. + +Remark used_not_defined_2: + forall p used id, + valid_used_set p used -> + id <> prog_main p -> + (prog_defmap p)!id = None -> + ~IS.In id used. +Proof. + intros. exploit used_not_defined; eauto. intros [A|A]. + red; intros; apply IS.mem_1 in H2; congruence. + congruence. +Qed. + +Lemma link_valid_used_set: + forall p1 p2 p used1 used2, + link p1 p2 = Some p -> + valid_used_set p1 used1 -> + valid_used_set p2 used2 -> + valid_used_set p (IS.union used1 used2). +Proof. + intros until used2; intros L V1 V2. + destruct (link_prog_inv _ _ _ L) as (X & Y & Z). + rewrite Z; clear Z; constructor. +- intros. rewrite ISF.union_iff in H. rewrite ISF.union_iff. + rewrite prog_defmap_elements, PTree.gcombine in H0. + destruct (prog_defmap p1)!id as [gd1|] eqn:GD1; + destruct (prog_defmap p2)!id as [gd2|] eqn:GD2; + simpl in H0; try discriminate. ++ (* common definition *) + exploit Y; eauto. intros (PUB1 & PUB2 & _). + exploit link_def_either; eauto. intros [EQ|EQ]; subst gd. +* left. eapply used_closed. eexact V1. eapply used_public. eexact V1. eauto. eauto. auto. +* right. eapply used_closed. eexact V2. eapply used_public. eexact V2. eauto. eauto. auto. ++ (* left definition *) + inv H0. destruct (ISP.In_dec id used1). +* left; eapply used_closed; eauto. +* assert (IS.In id used2) by tauto. + exploit used_defined. eexact V2. eauto. intros [A|A]. + exploit prog_defmap_dom; eauto. intros [g E]; congruence. + elim n. rewrite A, <- X. eapply used_main; eauto. ++ (* right definition *) + inv H0. destruct (ISP.In_dec id used2). +* right; eapply used_closed; eauto. +* assert (IS.In id used1) by tauto. + exploit used_defined. eexact V1. eauto. intros [A|A]. + exploit prog_defmap_dom; eauto. intros [g E]; congruence. + elim n. rewrite A, X. eapply used_main; eauto. ++ (* no definition *) + auto. +- simpl. rewrite ISF.union_iff; left; eapply used_main; eauto. +- simpl. intros id. rewrite in_app_iff, ISF.union_iff. + intros [A|A]; [left|right]; eapply used_public; eauto. +- intros. rewrite ISF.union_iff in H. + destruct (ident_eq id (prog_main p1)). ++ right; assumption. ++ assert (E: exists g, link_prog_merge (prog_defmap p1)!id (prog_defmap p2)!id = Some g). + { destruct (prog_defmap p1)!id as [gd1|] eqn:GD1; + destruct (prog_defmap p2)!id as [gd2|] eqn:GD2; simpl. + * apply Y with id; auto. + * exists gd1; auto. + * exists gd2; auto. + * eapply used_not_defined_2 in GD1; eauto. eapply used_not_defined_2 in GD2; eauto. + tauto. + congruence. + } + destruct E as [g LD]. + left. unfold prog_defs_names; simpl. + change id with (fst (id, g)). apply in_map. apply PTree.elements_correct. + rewrite PTree.gcombine; auto. +Qed. + +Theorem link_match_program: + forall p1 p2 tp1 tp2 p, + link p1 p2 = Some p -> + match_prog p1 tp1 -> match_prog p2 tp2 -> + exists tp, link tp1 tp2 = Some tp /\ match_prog p tp. +Proof. + intros. destruct H0 as (used1 & A1 & B1). destruct H1 as (used2 & A2 & B2). + destruct (link_prog_inv _ _ _ H) as (U & V & W). + econstructor; split. +- apply link_prog_succeeds. ++ rewrite (match_prog_main _ _ _ B1), (match_prog_main _ _ _ B2). auto. ++ intros. + rewrite (match_prog_def _ _ _ B1) in H0. + rewrite (match_prog_def _ _ _ B2) in H1. + destruct (IS.mem id used1) eqn:U1; try discriminate. + destruct (IS.mem id used2) eqn:U2; try discriminate. + edestruct V as (X & Y & gd & Z); eauto. + split. rewrite (match_prog_public _ _ _ B1); auto. + split. rewrite (match_prog_public _ _ _ B2); auto. + congruence. +- exists (IS.union used1 used2); split. ++ eapply link_valid_used_set; eauto. ++ rewrite W. constructor; simpl; intros. +* eapply match_prog_main; eauto. +* rewrite (match_prog_public _ _ _ B1), (match_prog_public _ _ _ B2). auto. +* rewrite ! prog_defmap_elements, !PTree.gcombine by auto. + rewrite (match_prog_def _ _ _ B1 id), (match_prog_def _ _ _ B2 id). + rewrite ISF.union_b. +{ + destruct (prog_defmap p1)!id as [gd1|] eqn:GD1; + destruct (prog_defmap p2)!id as [gd2|] eqn:GD2. +- (* both defined *) + exploit V; eauto. intros (PUB1 & PUB2 & _). + assert (EQ1: IS.mem id used1 = true) by (apply IS.mem_1; eapply used_public; eauto). + assert (EQ2: IS.mem id used2 = true) by (apply IS.mem_1; eapply used_public; eauto). + rewrite EQ1, EQ2; auto. +- (* left defined *) + exploit used_not_defined; eauto. intros [A|A]. + rewrite A, orb_false_r. destruct (IS.mem id used1); auto. + replace (IS.mem id used1) with true. destruct (IS.mem id used2); auto. + symmetry. apply IS.mem_1. rewrite A, <- U. eapply used_main; eauto. +- (* right defined *) + exploit used_not_defined. eexact A1. eauto. intros [A|A]. + rewrite A, orb_false_l. destruct (IS.mem id used2); auto. + replace (IS.mem id used2) with true. destruct (IS.mem id used1); auto. + symmetry. apply IS.mem_1. rewrite A, U. eapply used_main; eauto. +- (* none defined *) + destruct (IS.mem id used1), (IS.mem id used2); auto. +} +* intros. apply PTree.elements_keys_norepet. +Qed. + +Instance TransfSelectionLink : TransfLink match_prog := link_match_program. diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 979f8c0e..a4d34279 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -10,24 +10,11 @@ (* *) (* *********************************************************************) -Require Import Coqlib. -Require Import Maps. -Require Import Compopts. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Events. -Require Import Lattice. -Require Import Kildall. -Require Import Registers. -Require Import Op. -Require Import RTL. -Require Import ValueDomain. -Require Import ValueAOp. -Require Import Liveness. +Require Import Coqlib Maps Integers Floats Lattice Kildall. +Require Import Compopts AST Linking. +Require Import Values Memory Globalenvs Events. +Require Import Registers Op RTL. +Require Import ValueDomain ValueAOp Liveness. (** * The dataflow analysis *) @@ -208,7 +195,7 @@ Fixpoint store_init_data_list (ab: ablock) (p: Z) (idl: list init_data) {struct idl}: ablock := match idl with | nil => ab - | id :: idl' => store_init_data_list (store_init_data ab p id) (p + Genv.init_data_size id) idl' + | id :: idl' => store_init_data_list (store_init_data ab p id) (p + init_data_size id) idl' end. (** When CompCert is used in separate compilation mode, the [gvar_init] @@ -239,7 +226,7 @@ Definition alloc_global (rm: romem) (idg: ident * globdef fundef unit): romem := else PTree.remove id rm end. -Definition romem_for_program (p: program) : romem := +Definition romem_for (p: program) : romem := List.fold_left alloc_global p.(prog_defs) (PTree.empty _). (** * Soundness proof *) @@ -1045,10 +1032,9 @@ Qed. Section SOUNDNESS. Variable prog: program. +Variable ge: genv. -Let ge : genv := Genv.globalenv prog. - -Let rm := romem_for_program prog. +Let rm := romem_for prog. Inductive sound_stack: block_classification -> list stackframe -> mem -> block -> Prop := | sound_stack_nil: forall bc m bound, @@ -1079,7 +1065,7 @@ Inductive sound_stack: block_classification -> list stackframe -> mem -> block - (CONTENTS: bmatch bc' m sp am.(am_stack)), sound_stack bc (Stackframe res f (Vptr sp Int.zero) pc e :: stk) m bound. -Inductive sound_state: state -> Prop := +Inductive sound_state_base: state -> Prop := | sound_regular_state: forall s f sp pc e m ae am bc (STK: sound_stack bc s m sp) @@ -1089,7 +1075,7 @@ Inductive sound_state: state -> Prop := (MM: mmatch bc m am) (GE: genv_match bc ge) (SP: bc sp = BCstack), - sound_state (State s f (Vptr sp Int.zero) pc e m) + sound_state_base (State s f (Vptr sp Int.zero) pc e m) | sound_call_state: forall s fd args m bc (STK: sound_stack bc s m (Mem.nextblock m)) @@ -1098,7 +1084,7 @@ Inductive sound_state: state -> Prop := (MM: mmatch bc m mtop) (GE: genv_match bc ge) (NOSTK: bc_nostack bc), - sound_state (Callstate s fd args m) + sound_state_base (Callstate s fd args m) | sound_return_state: forall s v m bc (STK: sound_stack bc s m (Mem.nextblock m)) @@ -1107,7 +1093,7 @@ Inductive sound_state: state -> Prop := (MM: mmatch bc m mtop) (GE: genv_match bc ge) (NOSTK: bc_nostack bc), - sound_state (Returnstate s v m). + sound_state_base (Returnstate s v m). (** Properties of the [sound_stack] invariant on call stacks. *) @@ -1223,14 +1209,14 @@ Lemma sound_succ_state: genv_match bc ge -> bc sp = BCstack -> sound_stack bc s m' sp -> - sound_state (State s f (Vptr sp Int.zero) pc' e' m'). + sound_state_base (State s f (Vptr sp Int.zero) pc' e' m'). Proof. intros. exploit analyze_succ; eauto. intros (ae'' & am'' & AN & EM & MM). econstructor; eauto. Qed. -Theorem sound_step: - forall st t st', RTL.step ge st t st' -> sound_state st -> sound_state st'. +Theorem sound_step_base: + forall st t st', RTL.step ge st t st' -> sound_state_base st -> sound_state_base st'. Proof. induction 1; intros SOUND; inv SOUND. @@ -1309,7 +1295,7 @@ Proof. (* The default case *) assert (DEFAULT: transfer f rm pc ae am = transfer_builtin_default ae am rm args res -> - sound_state + sound_state_base (State s f (Vptr sp0 Int.zero) pc' (regmap_setres res vres rs) m')). { unfold transfer_builtin_default, analyze_call; intros TR'. set (aargs := map (abuiltin_arg ae am rm) args) in *. @@ -1480,6 +1466,37 @@ Qed. End SOUNDNESS. +(** ** Extension to separate compilation *) + +(** Following Kang et al, POPL 2016, we now extend the results above + to the case where only one compilation unit is analyzed, and not the + whole program. *) + +Section LINKING. + +Variable prog: program. +Let ge := Genv.globalenv prog. + +Inductive sound_state: state -> Prop := + | sound_state_intro: forall st, + (forall cunit, linkorder cunit prog -> sound_state_base cunit ge st) -> + sound_state st. + +Theorem sound_step: + forall st t st', RTL.step ge st t st' -> sound_state st -> sound_state st'. +Proof. + intros. inv H0. constructor; intros. eapply sound_step_base; eauto. +Qed. + +Remark sound_state_inv: + forall st cunit, + sound_state st -> linkorder cunit prog -> sound_state_base cunit ge st. +Proof. + intros. inv H. eauto. +Qed. + +End LINKING. + (** ** Soundness of the initial memory abstraction *) Section INITIAL. @@ -1660,8 +1677,8 @@ Proof. Qed. Definition initial_mem_match (bc: block_classification) (m: mem) (g: genv) := - forall b v, - Genv.find_var_info g b = Some v -> + forall id b v, + Genv.find_symbol g id = Some b -> Genv.find_var_info g b = Some v -> v.(gvar_volatile) = false -> v.(gvar_readonly) = true -> bmatch bc m b (store_init_data_list (ablock_init Pbot) 0 v.(gvar_init)). @@ -1672,27 +1689,32 @@ Lemma alloc_global_match: Genv.alloc_global ge m idg = Some m' -> initial_mem_match bc m' (Genv.add_global g idg). Proof. - intros; red; intros. destruct idg as [id [fd | gv]]; simpl in *. + intros; red; intros. destruct idg as [id1 [fd | gv]]; simpl in *. - destruct (Mem.alloc m 0 1) as [m1 b1] eqn:ALLOC. - unfold Genv.find_var_info, Genv.add_global in H2; simpl in H2. - assert (Plt b (Mem.nextblock m)). - { rewrite <- H. eapply Genv.genv_vars_range; eauto. } - assert (b <> b1). - { apply Plt_ne. erewrite Mem.alloc_result by eauto. auto. } + unfold Genv.find_symbol in H2; simpl in H2. + unfold Genv.find_var_info, Genv.find_def in H3; simpl in H3. + rewrite PTree.gsspec in H2. destruct (peq id id1). + inv H2. rewrite PTree.gss in H3. discriminate. + assert (Plt b (Genv.genv_next g)) by (eapply Genv.genv_symb_range; eauto). + rewrite PTree.gso in H3 by (apply Plt_ne; auto). + assert (Mem.valid_block m b) by (red; rewrite <- H; auto). + assert (b <> b1) by (apply Mem.valid_not_valid_diff with m; eauto with mem). apply bmatch_inv with m. eapply H0; eauto. - intros. transitivity (Mem.loadbytes m1 b ofs n). + intros. transitivity (Mem.loadbytes m1 b ofs n0). eapply Mem.loadbytes_drop; eauto. eapply Mem.loadbytes_alloc_unchanged; eauto. -- set (sz := Genv.init_data_list_size (gvar_init gv)) in *. +- set (sz := init_data_list_size (gvar_init gv)) in *. destruct (Mem.alloc m 0 sz) as [m1 b1] eqn:ALLOC. destruct (store_zeros m1 b1 0 sz) as [m2 | ] eqn:STZ; try discriminate. destruct (Genv.store_init_data_list ge m2 b1 0 (gvar_init gv)) as [m3 | ] eqn:SIDL; try discriminate. - unfold Genv.find_var_info, Genv.add_global in H2; simpl in H2. - rewrite PTree.gsspec in H2. destruct (peq b (Genv.genv_next g)). -+ inversion H2; clear H2; subst v. + unfold Genv.find_symbol in H2; simpl in H2. + unfold Genv.find_var_info, Genv.find_def in H3; simpl in H3. + rewrite PTree.gsspec in H2. destruct (peq id id1). ++ injection H2; clear H2; intro EQ. + rewrite EQ, PTree.gss in H3. injection H3; clear H3; intros EQ'; subst v. assert (b = b1). { erewrite Mem.alloc_result by eauto. congruence. } - clear e. subst b. + clear EQ. subst b. apply bmatch_inv with m3. eapply store_init_data_list_sound; eauto. apply ablock_init_sound. @@ -1701,11 +1723,11 @@ Proof. exploit Mem.load_alloc_same; eauto. intros EQ; subst v; constructor. exploit Mem.loadbytes_alloc_same; eauto with coqlib. congruence. intros. eapply Mem.loadbytes_drop; eauto. - right; right; right. unfold Genv.perm_globvar. rewrite H3, H4. constructor. -+ assert (Plt b (Mem.nextblock m)). - { rewrite <- H. eapply Genv.genv_vars_range; eauto. } - assert (b <> b1). - { apply Plt_ne. erewrite Mem.alloc_result by eauto. auto. } + right; right; right. unfold Genv.perm_globvar. rewrite H4, H5. constructor. ++ assert (Plt b (Genv.genv_next g)) by (eapply Genv.genv_symb_range; eauto). + rewrite PTree.gso in H3 by (apply Plt_ne; auto). + assert (Mem.valid_block m b) by (red; rewrite <- H; auto). + assert (b <> b1) by (apply Mem.valid_not_valid_diff with m; eauto with mem). apply bmatch_inv with m3. eapply store_init_data_list_other; eauto. eapply store_zeros_other; eauto. @@ -1730,44 +1752,56 @@ Proof. eapply alloc_global_match; eauto. Qed. -Definition romem_consistent (g: genv) (rm: romem) := - forall id b ab, - Genv.find_symbol g id = Some b -> rm!id = Some ab -> +Definition romem_consistent (defmap: PTree.t (globdef fundef unit)) (rm: romem) := + forall id ab, + rm!id = Some ab -> exists v, - Genv.find_var_info g b = Some v + defmap!id = Some (Gvar v) /\ v.(gvar_readonly) = true /\ v.(gvar_volatile) = false + /\ definitive_initializer v.(gvar_init) = true /\ ab = store_init_data_list (ablock_init Pbot) 0 v.(gvar_init). Lemma alloc_global_consistent: - forall g rm idg, - romem_consistent g rm -> - romem_consistent (Genv.add_global g idg) (alloc_global rm idg). + forall dm rm idg, + romem_consistent dm rm -> + romem_consistent (PTree.set (fst idg) (snd idg) dm) (alloc_global rm idg). +Proof. + intros; red; intros. destruct idg as [id1 [f1 | v1]]; simpl in *. +- rewrite PTree.grspec in H0. destruct (PTree.elt_eq id id1); try discriminate. + rewrite PTree.gso by auto. apply H; auto. +- destruct (gvar_readonly v1 && negb (gvar_volatile v1) && definitive_initializer (gvar_init v1)) eqn:RO. ++ InvBooleans. rewrite negb_true_iff in H4. + rewrite PTree.gsspec in *. destruct (peq id id1). +* inv H0. exists v1; auto. +* apply H; auto. ++ rewrite PTree.grspec in H0. destruct (PTree.elt_eq id id1); try discriminate. + rewrite PTree.gso by auto. apply H; auto. +Qed. + +Lemma romem_for_consistent: + forall cunit, romem_consistent (prog_defmap cunit) (romem_for cunit). Proof. - intros; red; intros. destruct idg as [id1 [fd1 | v1]]; - unfold Genv.add_global, Genv.find_symbol, Genv.find_var_info, alloc_global in *; simpl in *. -- rewrite PTree.gsspec in H0. rewrite PTree.grspec in H1. unfold PTree.elt_eq in *. - destruct (peq id id1). congruence. eapply H; eauto. -- rewrite PTree.gsspec in H0. destruct (peq id id1). -+ inv H0. rewrite PTree.gss. - destruct (gvar_readonly v1 && negb (gvar_volatile v1) && definitive_initializer (gvar_init v1)) eqn:RO. - InvBooleans. rewrite negb_true_iff in H4. - rewrite PTree.gss in H1. - exists v1. intuition congruence. - rewrite PTree.grs in H1. discriminate. -+ rewrite PTree.gso. eapply H; eauto. - destruct (gvar_readonly v1 && negb (gvar_volatile v1) && definitive_initializer (gvar_init v1)). - rewrite PTree.gso in H1; auto. - rewrite PTree.gro in H1; auto. - apply Plt_ne. eapply Genv.genv_symb_range; eauto. + assert (REC: forall l dm rm, + romem_consistent dm rm -> + romem_consistent (fold_left (fun m idg => PTree.set (fst idg) (snd idg) m) l dm) + (fold_left alloc_global l rm)). + { induction l; intros; simpl; auto. apply IHl. apply alloc_global_consistent; auto. } + intros. apply REC. + red; intros. rewrite PTree.gempty in H; discriminate. Qed. -Lemma alloc_globals_consistent: - forall gl g rm, - romem_consistent g rm -> - romem_consistent (Genv.add_globals g gl) (List.fold_left alloc_global gl rm). +Lemma romem_for_consistent_2: + forall cunit, linkorder cunit prog -> romem_consistent (prog_defmap prog) (romem_for cunit). Proof. - induction gl; simpl; intros. auto. apply IHgl. apply alloc_global_consistent; auto. + intros; red; intros. + exploit (romem_for_consistent cunit); eauto. intros (v & DM & RO & VO & DEFN & AB). + destruct (prog_defmap_linkorder _ _ _ _ H DM) as (gd & P & Q). + assert (gd = Gvar v). + { inv Q. inv H2. simpl in *. f_equal. f_equal. + destruct info1, info2; auto. + inv H3; auto; discriminate. } + subst gd. exists v; auto. Qed. End INIT. @@ -1779,27 +1813,28 @@ Theorem initial_mem_matches: genv_match bc ge /\ bc_below bc (Mem.nextblock m) /\ bc_nostack bc - /\ romatch bc m (romem_for_program prog) + /\ (forall cunit, linkorder cunit prog -> romatch bc m (romem_for cunit)) /\ (forall b, Mem.valid_block m b -> bc b <> BCinvalid). Proof. intros. exploit initial_block_classification; eauto. intros (bc & GE & BELOW & NOSTACK & INV & VALID). exists bc; splitall; auto. + intros. assert (A: initial_mem_match bc m ge). { apply alloc_globals_match with (m := Mem.empty); auto. - red. unfold Genv.find_var_info; simpl. intros. rewrite PTree.gempty in H0; discriminate. - } - assert (B: romem_consistent ge (romem_for_program prog)). - { - apply alloc_globals_consistent. - red; intros. rewrite PTree.gempty in H1; discriminate. + red. unfold Genv.find_symbol; simpl; intros. rewrite PTree.gempty in H1; discriminate. } + assert (B: romem_consistent (prog_defmap prog) (romem_for cunit)) by (apply romem_for_consistent_2; auto). red; intros. - exploit B; eauto. intros (v & FV & RO & NVOL & EQ). + exploit B; eauto. intros (v & DM & RO & NVOL & DEFN & EQ). + rewrite Genv.find_def_symbol in DM. destruct DM as (b1 & FS & FD). + rewrite <- Genv.find_var_info_iff in FD. + assert (b1 = b). { apply INV in H1. unfold ge in H1; congruence. } + subst b1. split. subst ab. apply store_init_data_list_summary. constructor. split. subst ab. eapply A; eauto. - unfold ge in FV; exploit Genv.init_mem_characterization; eauto. + exploit Genv.init_mem_characterization; eauto. intros (P & Q & R). intros; red; intros. exploit Q; eauto. intros [U V]. unfold Genv.perm_globvar in V; rewrite RO, NVOL in V. inv V. @@ -1814,10 +1849,10 @@ Theorem sound_initial: Proof. destruct 1. exploit initial_mem_matches; eauto. intros (bc & GE & BELOW & NOSTACK & RM & VALID). - apply sound_call_state with bc. + constructor; intros. apply sound_call_state with bc. - constructor. - simpl; tauto. -- exact RM. +- apply RM; auto. - apply mmatch_inj_top with m0. replace (inj_of_bc bc) with (Mem.flat_inj (Mem.nextblock m0)). eapply Genv.initmem_inject; eauto. @@ -1833,6 +1868,12 @@ Hint Resolve areg_sound aregs_sound: va. (** * Interface with other optimizations *) +Ltac InvSoundState := + match goal with + | H1: sound_state ?prog ?st, H2: linkorder ?cunit ?prog |- _ => + let S := fresh "S" in generalize (sound_state_inv _ _ _ H1 H2); intros S; inv S + end. + Definition avalue (a: VA.t) (r: reg) : aval := match a with | VA.Bot => Vbot @@ -1840,14 +1881,15 @@ Definition avalue (a: VA.t) (r: reg) : aval := end. Lemma avalue_sound: - forall prog s f sp pc e m r, + forall cunit prog s f sp pc e m r, sound_state prog (State s f (Vptr sp Int.zero) pc e m) -> + linkorder cunit prog -> exists bc, - vmatch bc e#r (avalue (analyze (romem_for_program prog) f)!!pc r) + vmatch bc e#r (avalue (analyze (romem_for cunit) f)!!pc r) /\ genv_match bc (Genv.globalenv prog) /\ bc sp = BCstack. Proof. - intros. inv H. exists bc; split; auto. rewrite AN. apply EM. + intros. InvSoundState. exists bc; split; auto. rewrite AN. apply EM. Qed. Definition aaddr (a: VA.t) (r: reg) : aptr := @@ -1857,16 +1899,17 @@ Definition aaddr (a: VA.t) (r: reg) : aptr := end. Lemma aaddr_sound: - forall prog s f sp pc e m r b ofs, + forall cunit prog s f sp pc e m r b ofs, sound_state prog (State s f (Vptr sp Int.zero) pc e m) -> + linkorder cunit prog -> e#r = Vptr b ofs -> exists bc, - pmatch bc b ofs (aaddr (analyze (romem_for_program prog) f)!!pc r) + pmatch bc b ofs (aaddr (analyze (romem_for cunit) f)!!pc r) /\ genv_match bc (Genv.globalenv prog) /\ bc sp = BCstack. Proof. - intros. inv H. exists bc; split; auto. - unfold aaddr; rewrite AN. apply match_aptr_of_aval. rewrite <- H0. apply EM. + intros. InvSoundState. exists bc; split; auto. + unfold aaddr; rewrite AN. apply match_aptr_of_aval. rewrite <- H1. apply EM. Qed. Definition aaddressing (a: VA.t) (addr: addressing) (args: list reg) : aptr := @@ -1876,15 +1919,16 @@ Definition aaddressing (a: VA.t) (addr: addressing) (args: list reg) : aptr := end. Lemma aaddressing_sound: - forall prog s f sp pc e m addr args b ofs, + forall cunit prog s f sp pc e m addr args b ofs, sound_state prog (State s f (Vptr sp Int.zero) pc e m) -> + linkorder cunit prog -> eval_addressing (Genv.globalenv prog) (Vptr sp Int.zero) addr e##args = Some (Vptr b ofs) -> exists bc, - pmatch bc b ofs (aaddressing (analyze (romem_for_program prog) f)!!pc addr args) + pmatch bc b ofs (aaddressing (analyze (romem_for cunit) f)!!pc addr args) /\ genv_match bc (Genv.globalenv prog) /\ bc sp = BCstack. Proof. - intros. inv H. exists bc; split; auto. + intros. InvSoundState. exists bc; split; auto. unfold aaddressing. rewrite AN. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto with va. Qed. @@ -1921,14 +1965,15 @@ Proof. Qed. Lemma aaddr_arg_sound: - forall prog s f sp pc e m a b ofs, + forall cunit prog s f sp pc e m a b ofs, sound_state prog (State s f (Vptr sp Int.zero) pc e m) -> + linkorder cunit prog -> eval_builtin_arg (Genv.globalenv prog) (fun r => e#r) (Vptr sp Int.zero) m a (Vptr b ofs) -> exists bc, - pmatch bc b ofs (aaddr_arg (analyze (romem_for_program prog) f)!!pc a) + pmatch bc b ofs (aaddr_arg (analyze (romem_for cunit) f)!!pc a) /\ genv_match bc (Genv.globalenv prog) /\ bc sp = BCstack. Proof. - intros. inv H. rewrite AN. exists bc; split; auto. + intros. InvSoundState. rewrite AN. exists bc; split; auto. eapply aaddr_arg_sound_1; eauto. Qed. diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 048ab816..f9ccd5db 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -10,21 +10,12 @@ (* *) (* *********************************************************************) -Require Import Coqlib. -Require Import Zwf. -Require Import Maps. -Require Import Compopts. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Events. -Require Import Lattice. -Require Import Kildall. -Require Import Registers. -Require Import RTL. +Require Import Zwf Coqlib Maps Integers Floats Lattice. +Require Import Compopts AST. +Require Import Values Memory Globalenvs Events. +Require Import Registers RTL. + +(** The abstract domains for value analysis *) Inductive block_class : Type := | BCinvalid @@ -3814,7 +3805,8 @@ Lemma inj_of_bc_preserves_globals: Proof. intros. destruct H as [A B]. split. intros. apply inj_of_bc_valid. rewrite A in H. congruence. - split. intros. apply inj_of_bc_valid. apply B. eapply Genv.genv_vars_range; eauto. + split. intros. apply inj_of_bc_valid. apply B. + rewrite Genv.find_var_info_iff in H. eapply Genv.genv_defs_range; eauto. intros. exploit inj_of_bc_inv; eauto. intros (P & Q & R). auto. Qed. -- cgit