diff options
Diffstat (limited to 'driver/Compiler.v')
| -rw-r--r-- | driver/Compiler.v | 68 |
1 files changed, 46 insertions, 22 deletions
diff --git a/driver/Compiler.v b/driver/Compiler.v index ee091c37..69041ab0 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -39,9 +39,11 @@ Require Tailcall. Require Inlining. Require Profiling. Require ProfilingExploit. +Require FirstNop. Require Renumber. Require Duplicate. Require Constprop. +Require LICM. Require CSE. Require ForwardMoves. Require CSE2. @@ -67,9 +69,11 @@ Require Tailcallproof. Require Inliningproof. Require Profilingproof. Require ProfilingExploitproof. +Require FirstNopproof. Require Renumberproof. Require Duplicateproof. Require Constpropproof. +Require LICMproof. Require CSEproof. Require ForwardMovesproof. Require CSE2proof. @@ -142,28 +146,34 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 3) @@ total_if Compopts.branch_probabilities (time "Profiling use" ProfilingExploit.transf_program) @@ print (print_RTL 4) - @@ time "Renumbering" Renumber.transf_program + @@ total_if Compopts.optim_move_loop_invariants (time "Inserting initial nop" FirstNop.transf_program) @@ print (print_RTL 5) - @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) + @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 6) - @@ 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 7) - @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) + @@ time "Renumbering pre constprop" Renumber.transf_program @@ print (print_RTL 8) - @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) + @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 9) - @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) + @@@ partial_if Compopts.optim_move_loop_invariants (time "LICM" LICM.transf_program) @@ print (print_RTL 10) - @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program) + @@ total_if Compopts.optim_move_loop_invariants (time "Renumbering pre CSE" Renumber.transf_program) @@ print (print_RTL 11) - @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program + @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 12) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) @@ print (print_RTL 13) - @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program) @@ print (print_RTL 14) - @@@ time "Unused globals" Unusedglob.transform_program + @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program @@ print (print_RTL 15) + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@ print (print_RTL 16) + @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@ print (print_RTL 17) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 18) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -267,10 +277,13 @@ Definition CompCert's_passes := ::: mkpass Inliningproof.match_prog ::: mkpass (match_if Compopts.profile_arcs Profilingproof.match_prog) ::: mkpass (match_if Compopts.branch_probabilities ProfilingExploitproof.match_prog) + ::: mkpass (match_if Compopts.optim_move_loop_invariants FirstNopproof.match_prog) ::: mkpass Renumberproof.match_prog ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) + ::: mkpass Renumberproof.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_move_loop_invariants LICMproof.match_prog) + ::: mkpass (match_if Compopts.optim_move_loop_invariants 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_CSE3 CSE3proof.match_prog) @@ -317,11 +330,14 @@ Proof. destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. set (p8bis := total_if profile_arcs Profiling.transf_program p8) in *. set (p8ter := total_if branch_probabilities ProfilingExploit.transf_program p8bis) in *. - set (p9 := Renumber.transf_program p8ter) in *. - 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 (p9 := total_if Compopts.optim_move_loop_invariants FirstNop.transf_program p8ter) in *. + set (p9bis := Renumber.transf_program p9) in *. + destruct (partial_if optim_duplicate Duplicate.transf_program p9bis) as [p10|e] eqn:P10; simpl in T; try discriminate. + set (p11 := Renumber.transf_program p10) in *. + set (p12 := total_if optim_constprop Constprop.transf_program p11) in *. + destruct (partial_if optim_move_loop_invariants LICM.transf_program p12) as [p12bis|e] eqn:P12bis; simpl in T; try discriminate. + set (p12ter :=(total_if optim_move_loop_invariants Renumber.transf_program p12bis)) in *. + destruct (partial_if optim_CSE CSE.transf_program p12ter) as [p13|e] eqn:P13; simpl in T; try discriminate. set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *. destruct (partial_if optim_CSE3 CSE3.transf_program p13bis) as [p13ter|e] eqn:P13ter; simpl in T; try discriminate. set (p13quater := total_if optim_forward_moves ForwardMoves.transf_program p13ter) in *. @@ -345,10 +361,13 @@ Proof. exists p8; split. apply Inliningproof.transf_program_match; auto. exists p8bis; split. apply total_if_match. apply Profilingproof.transf_program_match; auto. exists p8ter; split. apply total_if_match. apply ProfilingExploitproof.transf_program_match; auto. - exists p9; split. apply Renumberproof.transf_program_match; auto. + exists p9; split. apply total_if_match. apply FirstNopproof.transf_program_match. + exists p9bis; split. apply Renumberproof.transf_program_match. 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 p11; split. apply Renumberproof.transf_program_match. + exists p12; split. apply total_if_match. apply Constpropproof.transf_program_match. + exists p12bis; split. eapply partial_if_match; eauto. apply LICMproof.transf_program_match. + exists p12ter; split. apply total_if_match; eauto. 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 partial_if_match; eauto. apply CSE3proof.transf_program_match. @@ -413,7 +432,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 p28)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p31)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -435,11 +454,16 @@ Ltac DestructM := eapply match_if_simulation. eassumption. exact Profilingproof.transf_program_correct. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact ProfilingExploitproof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact FirstNopproof.transf_program_correct. 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 Renumberproof.transf_program_correct; eassumption. + eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact LICMproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Renumberproof.transf_program_correct. eapply compose_forward_simulations. |