diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2016-03-20 18:00:43 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2016-03-20 18:00:43 +0100 |
| commit | 1fdca8371317e656cb08eaec3adb4596d6447e9b (patch) | |
| tree | 8a5d390a4d38f4d840f516fb917eb824311a93a0 /backend | |
| parent | 1396a4051caef0957ede026f3b8fab5a9b10b6bc (diff) | |
| parent | 478ae4c3aeb1a31b0eec9ab7eb8fe20ec2671614 (diff) | |
| download | compcert-1fdca8371317e656cb08eaec3adb4596d6447e9b.tar.gz compcert-1fdca8371317e656cb08eaec3adb4596d6447e9b.zip | |
Merge pull request #93 from AbsInt/separate-compilation
This pull request implements "approach A" to separate compilation in CompCert from the paper
Lightweight verification of separate compilation
by Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis,
POPL 2016, pages 178-190
In a nutshell, semantic preservation is still stated and proved in terms of a whole C program and a whole assembly program. However, the whole C program can be the result of syntactic linking of several C compilation units, each unit being separated compiled by CompCert to produce assembly unit, and these assembly units being linked together to produce the whole assembly program.
This way, the statement of semantic preservation and its proof now take into account the fact that each compilation unit is compiled separately, knowing only a fragment of the whole program (i.e. the current compilation unit) rather than the whole program.
Diffstat (limited to 'backend')
32 files changed, 1996 insertions, 2010 deletions
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. |