diff options
| -rw-r--r-- | backend/CSE2proof.v | 10 | ||||
| -rw-r--r-- | driver/Clflags.ml | 1 | ||||
| -rw-r--r-- | driver/Compiler.v | 36 | ||||
| -rw-r--r-- | driver/Compopts.v | 3 | ||||
| -rw-r--r-- | driver/Driver.ml | 7 | ||||
| -rw-r--r-- | extraction/extraction.v | 2 |
6 files changed, 51 insertions, 8 deletions
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 558490ba..1d0a617a 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -405,7 +405,6 @@ Lemma kill_reg_weaken: sem_rel mpc rs -> sem_rel (kill_reg res mpc) rs. Proof. - Check kill_reg_sound. intros until rs. intros REL x. pose proof (REL x) as RELx. @@ -471,6 +470,14 @@ Qed. End SOUNDNESS. +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. @@ -849,7 +856,6 @@ Proof. eapply exec_Itailcall with (fd := transf_fundef fd); eauto. eapply find_function_translated; eauto. apply sig_preserved. - Check subst_args_ok. rewrite (subst_args_ok' (Vptr stk Ptrofs.zero) m) by assumption. constructor. auto. diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 2db9399f..b4ab51e7 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -26,6 +26,7 @@ let option_ffloatconstprop = ref 2 let option_ftailcalls = ref true let option_fconstprop = ref true let option_fcse = ref true +let option_fcse2 = ref true let option_fredundancy = ref true let option_fifconversion = ref true let option_Obranchless = ref false diff --git a/driver/Compiler.v b/driver/Compiler.v index 75247f71..33e31057 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -40,6 +40,7 @@ Require Inlining. Require Renumber. Require Constprop. Require CSE. +Require CSE2. Require Deadcode. Require Unusedglob. Require Allocation. @@ -61,6 +62,7 @@ Require Inliningproof. Require Renumberproof. Require Constpropproof. Require CSEproof. +Require CSE2proof. Require Deadcodeproof. Require Unusedglobproof. Require Allocproof. @@ -132,10 +134,12 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 5) @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 6) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) @@ print (print_RTL 7) - @@@ time "Unused globals" Unusedglob.transform_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 8) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 9) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -241,6 +245,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_CSE2 CSE2proof.match_prog) ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) ::: mkpass Unusedglobproof.match_prog ::: mkpass Allocproof.match_prog @@ -284,7 +289,27 @@ Proof. 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. + set (p12bis := @total_if RTL.program optim_CSE2 CSE2.transf_program p12). + change (@eq (res Asm.program) + (apply_partial Mach.program Asm.program + (apply_partial Linear.program Mach.program + (apply_partial Linear.program Linear.program + (apply_total Linear.program Linear.program + (apply_partial LTL.program Linear.program + (apply_total LTL.program LTL.program + (apply_partial RTL.program LTL.program + (apply_partial RTL.program RTL.program + (@partial_if RTL.program optim_redundancy + Deadcode.transf_program + p12bis) + Unusedglob.transform_program) + Allocation.transf_program) + Tunneling.tunnel_program) Linearize.transf_program) + CleanupLabels.transf_program) + (@partial_if Linear.program debug Debugvar.transf_program)) + Stacking.transf_program) Asmgen.transf_program) + (@OK Asm.program tp)) in T. + destruct (partial_if optim_redundancy Deadcode.transf_program p12bis) 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 *. @@ -305,6 +330,7 @@ Proof. 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 p12bis; split. apply total_if_match. apply CSE2proof.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. @@ -364,7 +390,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 p22)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -390,6 +416,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 CSE2proof.transf_program_correct. + eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Unusedglobproof.transf_program_correct; eassumption. diff --git a/driver/Compopts.v b/driver/Compopts.v index 2a213350..594b74f1 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -36,6 +36,9 @@ Parameter optim_constprop: unit -> bool. (** Flag -fcse. For common subexpression elimination. *) Parameter optim_CSE: unit -> bool. +(** Flag -fcse2. For DMonniaux's common subexpression elimination. *) +Parameter optim_CSE2: unit -> bool. + (** Flag -fredundancy. For dead code elimination. *) Parameter optim_redundancy: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index be1252f9..bdf72250 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -194,6 +194,7 @@ Processing options: -ffloat-const-prop <n> Control constant propagation of floats (<n>=0: none, <n>=1: limited, <n>=2: full; default is full) -fcse Perform common subexpression elimination [on] + -fcse2 Perform inter-loop common subexpression elimination [on] -fredundancy Perform redundancy elimination [on] -finline Perform inlining of functions [on] -finline-functions-called-once Integrate functions only required by their @@ -253,8 +254,9 @@ let dump_mnemonics destfile = exit 0 let optimization_options = [ - option_ftailcalls; option_fifconversion; option_fconstprop; option_fcse; - option_fredundancy; option_finline; option_finline_functions_called_once; + option_ftailcalls; option_fifconversion; option_fconstprop; + option_fcse; option_fcse2; + option_fredundancy; option_finline; option_finline_functions_called_once; ] let set_all opts () = List.iter (fun r -> r := true) opts @@ -372,6 +374,7 @@ let cmdline_actions = @ f_opt "if-conversion" option_fifconversion @ f_opt "const-prop" option_fconstprop @ f_opt "cse" option_fcse + @ f_opt "cse2" option_fcse2 @ f_opt "redundancy" option_fredundancy @ f_opt "inline" option_finline @ f_opt "inline-functions-called-once" option_finline_functions_called_once diff --git a/extraction/extraction.v b/extraction/extraction.v index 521c0cdd..4635f5a2 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -108,6 +108,8 @@ Extract Constant Compopts.optim_constprop => "fun _ -> !Clflags.option_fconstprop". Extract Constant Compopts.optim_CSE => "fun _ -> !Clflags.option_fcse". +Extract Constant Compopts.optim_CSE2 => + "fun _ -> !Clflags.option_fcse2". Extract Constant Compopts.optim_redundancy => "fun _ -> !Clflags.option_fredundancy". Extract Constant Compopts.thumb => |