From 07f2bfbd62568e2e0d983ccb33d020bf6985e874 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 29 Mar 2020 18:30:01 +0200 Subject: nop insertion at entrypoint --- driver/Compiler.v | 38 +++++++++++++++++++++++--------------- 1 file changed, 23 insertions(+), 15 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 47fb8236..cc1e7917 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -37,6 +37,7 @@ Require Selection. Require RTLgen. Require Tailcall. Require Inlining. +Require FirstNop. Require Renumber. Require Duplicate. Require Constprop. @@ -63,6 +64,7 @@ Require Selectionproof. Require RTLgenproof. Require Tailcallproof. Require Inliningproof. +Require FirstNopproof. Require Renumberproof. Require Duplicateproof. Require Constpropproof. @@ -134,28 +136,30 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 1) @@@ time "Inlining" Inlining.transf_program @@ print (print_RTL 2) - @@ time "Renumbering" Renumber.transf_program + @@ time "Inserting initial nop" FirstNop.transf_program @@ print (print_RTL 3) - @@@ time "Tail-duplicating" Duplicate.transf_program + @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 4) - @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) + @@@ time "Tail-duplicating" Duplicate.transf_program @@ print (print_RTL 5) - @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) + @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 6) - @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) + @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) @@ print (print_RTL 7) - @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) + @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 8) - @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program) + @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) @@ print (print_RTL 9) - @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program + @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program) @@ print (print_RTL 10) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program @@ print (print_RTL 11) - @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 12) - @@@ time "Unused globals" Unusedglob.transform_program + @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program @@ print (print_RTL 13) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 14) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -257,6 +261,7 @@ Definition CompCert's_passes := ::: mkpass RTLgenproof.match_prog ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) ::: mkpass Inliningproof.match_prog + ::: mkpass FirstNopproof.match_prog ::: mkpass Renumberproof.match_prog ::: mkpass Duplicateproof.match_prog ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) @@ -305,8 +310,9 @@ Proof. unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T. 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 *. - destruct (Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. + set (p9 := FirstNop.transf_program p8) in *. + set (p9bis := Renumber.transf_program p9) in *. + destruct (Duplicate.transf_program p9bis) 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. @@ -331,7 +337,8 @@ Proof. exists p6; split. apply RTLgenproof.transf_program_match; auto. 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 p9; split. apply FirstNopproof.transf_program_match; auto. + exists p9bis; split. apply Renumberproof.transf_program_match; auto. exists p10; split. 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. @@ -399,7 +406,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 p26)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p27)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -417,6 +424,7 @@ Ltac DestructM := eapply match_if_simulation. eassumption. exact Tailcallproof.transf_program_correct. eapply compose_forward_simulations. eapply Inliningproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. eapply FirstNopproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Duplicateproof.transf_program_correct; eassumption. -- cgit From d0590cab5ee32df395c129ee3edfa2dc3aaa202d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 13:30:30 +0200 Subject: begin adapting for LICM phase --- driver/Clflags.ml | 1 + driver/Compopts.v | 3 +++ driver/Driver.ml | 2 ++ 3 files changed, 6 insertions(+) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index ff2647a7..ae96e820 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -82,5 +82,6 @@ let option_fxsaddr = ref true let option_faddx = ref false let option_fcoalesce_mem = ref true let option_fforward_moves = ref true +let option_fmove_loop_invariants = ref false let option_all_loads_nontrap = ref false let option_inline_auto_threshold = ref 0 diff --git a/driver/Compopts.v b/driver/Compopts.v index a3181da8..e4dae87d 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -48,6 +48,9 @@ Parameter optim_CSE3: unit -> bool. (** Flag -fcse3-alias-analysis. For DMonniaux's common subexpression elimination. *) Parameter optim_CSE3_alias_analysis: unit -> bool. +(** Flag -fmove-loop-invariants. *) +Parameter optim_move_loop_invariants: unit -> bool. + (** Flag -fredundancy. For dead code elimination. *) Parameter optim_redundancy: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index b167dbd1..0f9e637c 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -199,6 +199,7 @@ Processing options: -fcse2 Perform inter-loop common subexpression elimination [off] -fcse3 Perform inter-loop common subexpression elimination [on] -fcse3-alias-analysis Perform inter-loop common subexpression elimination with alias analysis [on] + -fmove-loop-invariants Perform loop-invariant code motion [off] -fredundancy Perform redundancy elimination [on] -fpostpass Perform postpass scheduling (only for K1 architecture) [on] -fpostpass= Perform postpass scheduling with the specified optimization [list] @@ -401,6 +402,7 @@ let cmdline_actions = @ f_opt "cse2" option_fcse2 @ f_opt "cse3" option_fcse3 @ f_opt "cse3-alias-analysis" option_fcse3_alias_analysis + @ f_opt "move-loop-invariants" option_fmove_loop_invariants @ f_opt "redundancy" option_fredundancy @ f_opt "postpass" option_fpostpass @ [ Exact "-fduplicate", Integer (fun n -> option_fduplicate := n) ] -- cgit From 6379f6291eea909426f074db67837b04a1dec9ae Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 14:24:05 +0200 Subject: attempt at compiling --- driver/Compiler.v | 36 ++++++++++++++++++++++++------------ 1 file changed, 24 insertions(+), 12 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 5175abdb..dbf62368 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -41,6 +41,7 @@ Require FirstNop. Require Renumber. Require Duplicate. Require Constprop. +Require LICM. Require CSE. Require ForwardMoves. Require CSE2. @@ -68,6 +69,7 @@ Require FirstNopproof. Require Renumberproof. Require Duplicateproof. Require Constpropproof. +Require LICMproof. Require CSEproof. Require ForwardMovesproof. Require CSE2proof. @@ -136,7 +138,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 1) @@@ time "Inlining" Inlining.transf_program @@ print (print_RTL 2) - @@ time "Inserting initial nop" FirstNop.transf_program + @@ total_if Compopts.optim_move_loop_invariants (time "Inserting initial nop" FirstNop.transf_program) @@ print (print_RTL 3) @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 4) @@ -144,22 +146,26 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 5) @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 6) - @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) + @@ time "Renumbering pre LICM" Renumber.transf_program @@ print (print_RTL 7) - @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) + @@@ partial_if Compopts.optim_move_loop_invariants (time "LICM" LICM.transf_program) @@ print (print_RTL 8) - @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) + @@ total_if Compopts.optim_move_loop_invariants (time "Renumbering pre CSE" Renumber.transf_program) @@ print (print_RTL 9) - @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program) + @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 10) - @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program + @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) @@ print (print_RTL 11) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program) @@ print (print_RTL 12) - @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program @@ print (print_RTL 13) - @@@ time "Unused globals" Unusedglob.transform_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 14) + @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@ print (print_RTL 15) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 16) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -261,10 +267,11 @@ Definition CompCert's_passes := ::: mkpass RTLgenproof.match_prog ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) ::: mkpass Inliningproof.match_prog - ::: mkpass FirstNopproof.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 (match_if Compopts.optim_constprop Constpropproof.match_prog) + ::: mkpass (match_if Compopts.optim_move_loop_invariants LICMproof.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) @@ -308,14 +315,19 @@ Proof. destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T. + ::: mkpass (match_if Compopts.optim_move_loop_invariants LICM.match_prog) + ::: mkpass (match_if Compopts.optim_move_loop_invariants Renumberproof.match_prog) + ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) 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 := FirstNop.transf_program p8) in *. + set (p9 := total_if Compopts.optim_move_loop_invariants FirstNop.transf_program p8) 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 := 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_move_loop_invariants LICM.transf_program p12) as [p12bis|e] eqn:P12bis; simpl in T; try discriminate. + set (p12ter :=(total_if optim_move_loop_invariant 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 *. -- cgit From 01f42ef55d91bbb57b47ecc2be7e691165778980 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 15:38:06 +0200 Subject: fix Compiler.v --- driver/Compiler.v | 28 ++++++++++++++++------------ 1 file changed, 16 insertions(+), 12 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index dbf62368..89a15d93 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -271,8 +271,9 @@ Definition CompCert's_passes := ::: mkpass Renumberproof.match_prog ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) + ::: mkpass Renumberproof.match_prog ::: mkpass (match_if Compopts.optim_move_loop_invariants LICMproof.match_prog) - ::: mkpass (match_if Compopts.optim_constprop Renumberproof.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) @@ -315,18 +316,15 @@ Proof. destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T. - ::: mkpass (match_if Compopts.optim_move_loop_invariants LICM.match_prog) - ::: mkpass (match_if Compopts.optim_move_loop_invariants Renumberproof.match_prog) - ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) 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 := total_if Compopts.optim_move_loop_invariants FirstNop.transf_program p8) 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 := total_if optim_constprop Constprop.transf_program p10) in *. - set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. + set (p12 := Renumber.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_invariant Renumber.transf_program p12bis)) in *. + 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. @@ -349,11 +347,13 @@ Proof. exists p6; split. apply RTLgenproof.transf_program_match; auto. 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 FirstNopproof.transf_program_match; auto. - exists p9bis; 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 p12; split. apply Renumberproof.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. @@ -418,7 +418,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 p27)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p29)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -436,12 +436,16 @@ Ltac DestructM := eapply match_if_simulation. eassumption. exact Tailcallproof.transf_program_correct. eapply compose_forward_simulations. eapply Inliningproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. eapply FirstNopproof.transf_program_correct; eassumption. + 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 match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. + eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. + 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. -- cgit From 87d2c34910a017c13a908cfe2cf2c627e56e6cfe Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 15:46:03 +0200 Subject: reordering passes --- driver/Compiler.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 89a15d93..e6d39152 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -144,9 +144,9 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 4) @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) @@ print (print_RTL 5) - @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) + @@ time "Renumbering pre constprop" Renumber.transf_program @@ print (print_RTL 6) - @@ time "Renumbering pre LICM" Renumber.transf_program + @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 7) @@@ partial_if Compopts.optim_move_loop_invariants (time "LICM" LICM.transf_program) @@ print (print_RTL 8) @@ -270,8 +270,8 @@ Definition CompCert's_passes := ::: 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 (match_if Compopts.optim_constprop Constpropproof.match_prog) ::: mkpass Renumberproof.match_prog + ::: mkpass (match_if Compopts.optim_constprop Constpropproof.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) @@ -321,8 +321,8 @@ Proof. set (p9 := total_if Compopts.optim_move_loop_invariants FirstNop.transf_program p8) 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 := total_if optim_constprop Constprop.transf_program p10) in *. - set (p12 := Renumber.transf_program p11) in *. + 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. @@ -350,8 +350,8 @@ Proof. 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 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. @@ -442,8 +442,8 @@ Ltac DestructM := 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. -- cgit From a95735290d61f50a388895ef86627becd67c4553 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 19 Apr 2020 20:04:15 +0200 Subject: activate LICM --- driver/Clflags.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index ae96e820..8deb5224 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -82,6 +82,6 @@ let option_fxsaddr = ref true let option_faddx = ref false let option_fcoalesce_mem = ref true let option_fforward_moves = ref true -let option_fmove_loop_invariants = ref false +let option_fmove_loop_invariants = ref true let option_all_loads_nontrap = ref false let option_inline_auto_threshold = ref 0 -- cgit From eead578fde08a1555086ed75714bca3ca1f9b1dc Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 19 Apr 2020 21:14:21 +0200 Subject: add options for controlling madd and notrap selection --- driver/Clflags.ml | 4 +++- driver/Compopts.v | 3 +++ driver/Driver.ml | 2 ++ 3 files changed, 8 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 8deb5224..8e3305ef 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -79,9 +79,11 @@ let use_standard_headers = ref Configuration.has_standard_headers let option_fglobaladdrtmp = ref false let option_fglobaladdroffset = ref false let option_fxsaddr = ref true -let option_faddx = ref false +let option_faddx = ref false +let option_fmadd = ref true let option_fcoalesce_mem = ref true let option_fforward_moves = ref true let option_fmove_loop_invariants = ref true +let option_fnontrap_loads = ref true let option_all_loads_nontrap = ref false let option_inline_auto_threshold = ref 0 diff --git a/driver/Compopts.v b/driver/Compopts.v index e4dae87d..5acd2640 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -69,6 +69,9 @@ Parameter optim_xsaddr: unit -> bool. (** FIXME TEMPORARY Flag -fcoaelesce-mem. Fuse (default true) *) Parameter optim_coalesce_mem: unit -> bool. +(* FIXME TEMPORARY Flag -faddx. Fuse (default true) *) +Parameter optim_madd: unit -> bool. + (** FIXME TEMPORARY Flag -faddx. Fuse (default false) *) Parameter optim_addx: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index 0f9e637c..6a9e9b92 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -415,6 +415,8 @@ let cmdline_actions = @ f_opt "globaladdroffset" option_fglobaladdroffset @ f_opt "xsaddr" option_fxsaddr @ f_opt "addx" option_faddx + @ f_opt "madd" option_fmadd + @ f_opt "nontrap-loads" option_fnontrap_loads @ f_opt "coalesce-mem" option_fcoalesce_mem @ f_opt "all-loads-nontrap" option_all_loads_nontrap @ f_opt "forward-moves" option_fforward_moves -- cgit