diff options
| -rw-r--r-- | Makefile | 1 | ||||
| -rw-r--r-- | driver/Clflags.ml | 3 | ||||
| -rw-r--r-- | driver/Compiler.v | 19 | ||||
| -rw-r--r-- | driver/Compopts.v | 3 | ||||
| -rw-r--r-- | driver/Driver.ml | 1 | ||||
| -rw-r--r-- | extraction/extraction.v | 2 |
6 files changed, 23 insertions, 6 deletions
@@ -89,6 +89,7 @@ BACKEND=\ NeedDomain.v NeedOp.v Deadcode.v Deadcodeproof.v \ Unusedglob.v Unusedglobproof.v \ Machregs.v Locations.v Conventions1.v Conventions.v LTL.v \ + ForwardMoves.v ForwardMovesproof.v \ Allnontrap.v Allnontrapproof.v \ Allocation.v Allocproof.v \ Tunneling.v Tunnelingproof.v \ diff --git a/driver/Clflags.ml b/driver/Clflags.ml index fd8227c9..9aa4a2bf 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -74,5 +74,6 @@ let option_fglobaladdrtmp = ref false let option_fglobaladdroffset = ref false let option_fxsaddr = ref true let option_faddx = ref false -let option_fcoalesce_mem = ref true +let option_fcoalesce_mem = ref true +let option_fforward_moves = ref true let option_all_loads_nontrap = ref false diff --git a/driver/Compiler.v b/driver/Compiler.v index 72db86e9..24964237 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -41,6 +41,7 @@ Require Renumber. Require Duplicate. Require Constprop. Require CSE. +Require ForwardMoves. Require Deadcode. Require Unusedglob. Require Allnontrap. @@ -64,6 +65,7 @@ Require Renumberproof. Require Duplicateproof. Require Constpropproof. Require CSEproof. +Require ForwardMovesproof. Require Deadcodeproof. Require Unusedglobproof. Require Allnontrapproof. @@ -138,12 +140,14 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 6) @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 7) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program @@ print (print_RTL 8) - @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 9) - @@@ time "Unused globals" Unusedglob.transform_program + @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program @@ print (print_RTL 10) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 11) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -250,6 +254,7 @@ Definition CompCert's_passes := ::: 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_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 @@ -295,7 +300,8 @@ Proof. 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. - destruct (partial_if optim_redundancy Deadcode.transf_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. + set (p13bis := total_if optim_forward_moves ForwardMoves.transf_program p13) in *. + destruct (partial_if optim_redundancy Deadcode.transf_program p13bis) 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. @@ -318,6 +324,7 @@ Proof. 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. 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. @@ -378,7 +385,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 p23)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p24)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -405,6 +412,8 @@ Ltac DestructM := eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact CSEproof.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. diff --git a/driver/Compopts.v b/driver/Compopts.v index 6e3b0d62..fdd2b1d6 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -66,6 +66,9 @@ Parameter debug: unit -> bool. (** Flag -fall-loads-nontrap. Turn user loads into non trapping. *) Parameter all_loads_nontrap: unit -> bool. +(** Flag -fforward-moves. Forward moves after CSE. *) +Parameter optim_forward_moves: unit -> bool. + (* TODO is there a more appropriate place? *) Require Import Coqlib. Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f. diff --git a/driver/Driver.ml b/driver/Driver.ml index 59b7b222..eab66a2b 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -392,6 +392,7 @@ let cmdline_actions = @ f_opt "addx" option_faddx @ f_opt "coalesce-mem" option_fcoalesce_mem @ f_opt "all-loads-nontrap" option_all_loads_nontrap + @ f_opt "forward-moves" option_fforward_moves (* Code generation options *) @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) diff --git a/extraction/extraction.v b/extraction/extraction.v index 828d0dac..0c19ea70 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -127,6 +127,8 @@ Extract Constant Compopts.optim_addx => "fun _ -> !Clflags.option_faddx". Extract Constant Compopts.optim_coalesce_mem => "fun _ -> !Clflags.option_fcoalesce_mem". +Extract Constant Compopts.optim_forward_moves => + "fun _ -> !Clflags.option_fforward_moves". Extract Constant Compopts.va_strict => "fun _ -> false". Extract Constant Compopts.all_loads_nontrap => |