diff options
Diffstat (limited to 'driver/Compiler.v')
-rw-r--r-- | driver/Compiler.v | 92 |
1 files changed, 64 insertions, 28 deletions
diff --git a/driver/Compiler.v b/driver/Compiler.v index c683c136..499feff2 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -38,10 +38,14 @@ Require RTLgen. Require Tailcall. Require Inlining. Require Renumber. +Require Duplicate. Require Constprop. Require CSE. +Require ForwardMoves. +Require CSE2. Require Deadcode. Require Unusedglob. +Require Allnontrap. Require Allocation. Require Tunneling. Require Linearize. @@ -59,10 +63,14 @@ Require RTLgenproof. Require Tailcallproof. Require Inliningproof. Require Renumberproof. +Require Duplicateproof. Require Constpropproof. Require CSEproof. +Require ForwardMovesproof. +Require CSE2proof. Require Deadcodeproof. Require Unusedglobproof. +Require Allnontrapproof. Require Allocproof. Require Tunnelingproof. Require Linearizeproof. @@ -126,16 +134,24 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 2) @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 3) - @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) + @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) @@ print (print_RTL 4) - @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) + @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 5) - @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) + @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) @@ print (print_RTL 6) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 7) - @@@ time "Unused globals" Unusedglob.transform_program + @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) @@ print (print_RTL 8) + @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program + @@ print (print_RTL 9) + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@ print (print_RTL 10) + @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@ print (print_RTL 11) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 12) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -238,10 +254,14 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) ::: mkpass Inliningproof.match_prog ::: mkpass Renumberproof.match_prog + ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) + ::: mkpass (match_if Compopts.optim_CSE2 CSE2proof.match_prog) + ::: mkpass (match_if Compopts.optim_forward_moves ForwardMovesproof.match_prog) ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) + ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog) ::: mkpass Unusedglobproof.match_prog ::: mkpass Allocproof.match_prog ::: mkpass Tunnelingproof.match_prog @@ -281,17 +301,21 @@ Proof. set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. set (p9 := Renumber.transf_program p8) in *. - set (p10 := total_if optim_constprop Constprop.transf_program p9) in *. - set (p11 := total_if optim_constprop Renumber.transf_program p10) in *. - destruct (partial_if optim_CSE CSE.transf_program p11) as [p12|e] eqn:P12; simpl in T; try discriminate. - destruct (partial_if optim_redundancy Deadcode.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. - destruct (Unusedglob.transform_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. - destruct (Allocation.transf_program p14) as [p15|e] eqn:P15; simpl in T; try discriminate. - set (p16 := Tunneling.tunnel_program p15) in *. - destruct (Linearize.transf_program p16) as [p17|e] eqn:P17; simpl in T; try discriminate. - set (p18 := CleanupLabels.transf_program p17) in *. - destruct (partial_if debug Debugvar.transf_program p18) as [p19|e] eqn:P19; simpl in T; try discriminate. - destruct (Stacking.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. + destruct (partial_if optim_duplicate Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. + set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. + set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. + destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. + set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *. + set (p13ter := total_if optim_forward_moves ForwardMoves.transf_program p13bis) in *. + destruct (partial_if optim_redundancy Deadcode.transf_program p13ter) as [p14|e] eqn:P14; simpl in T; try discriminate. + set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. + destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. + destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. + set (p17 := Tunneling.tunnel_program p16) in *. + destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate. + set (p19 := CleanupLabels.transf_program p18) in *. + destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. + destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; simpl in T; try discriminate. unfold match_prog; simpl. exists p1; split. apply SimplExprproof.transf_program_match; auto. exists p2; split. apply SimplLocalsproof.match_transf_program; auto. @@ -302,17 +326,21 @@ Proof. exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. exists p8; split. apply Inliningproof.transf_program_match; auto. exists p9; split. apply Renumberproof.transf_program_match; auto. - exists p10; split. apply total_if_match. apply Constpropproof.transf_program_match. - exists p11; split. apply total_if_match. apply Renumberproof.transf_program_match. - exists p12; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. - exists p13; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. - exists p14; split. apply Unusedglobproof.transf_program_match; auto. - exists p15; split. apply Allocproof.transf_program_match; auto. - exists p16; split. apply Tunnelingproof.transf_program_match. - exists p17; split. apply Linearizeproof.transf_program_match; auto. - exists p18; split. apply CleanupLabelsproof.transf_program_match; auto. - exists p19; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. - exists p20; split. apply Stackingproof.transf_program_match; auto. + exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto. + exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match. + exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match. + exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. + exists p13bis; split. apply total_if_match. apply CSE2proof.transf_program_match. + exists p13ter; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match. + exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. + exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match. + exists p15; split. apply Unusedglobproof.transf_program_match; auto. + exists p16; split. apply Allocproof.transf_program_match; auto. + exists p17; split. apply Tunnelingproof.transf_program_match. + exists p18; split. apply Linearizeproof.transf_program_match; auto. + exists p19; split. apply CleanupLabelsproof.transf_program_match; auto. + exists p20; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. + exists p21; split. apply Stackingproof.transf_program_match; auto. exists tp; split. apply Asmgenproof.transf_program_match; auto. reflexivity. Qed. @@ -364,7 +392,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p21)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p25)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -384,14 +412,22 @@ Ltac DestructM := eapply Inliningproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Duplicateproof.transf_program_correct. + eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Renumberproof.transf_program_correct. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact CSEproof.transf_program_correct. eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact CSE2proof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact ForwardMovesproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Allnontrapproof.transf_program_correct. + eapply compose_forward_simulations. eapply Unusedglobproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Allocproof.transf_program_correct; eassumption. |