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 --- backend/Inject.v | 4 ++-- backend/Injectproof.v | 60 ++++++++++++++++++++++++------------------------- driver/Clflags.ml | 1 + driver/Compopts.v | 3 +++ driver/Driver.ml | 2 ++ extraction/extraction.v | 3 +++ 6 files changed, 41 insertions(+), 32 deletions(-) diff --git a/backend/Inject.v b/backend/Inject.v index 4bb25615..2350c149 100644 --- a/backend/Inject.v +++ b/backend/Inject.v @@ -81,7 +81,7 @@ Definition inject prog extra_pc injections : code := *) Section INJECTOR. - Variable gen_injections : function -> PTree.t (list inj_instr). + Variable gen_injections : function -> node -> reg -> PTree.t (list inj_instr). Definition valid_injection_instr (max_reg : reg) (i : inj_instr) := match i with @@ -102,9 +102,9 @@ Section INJECTOR. valid_injections1 (max_pc_function f) (max_reg_function f). Definition transf_function (f : function) : res function := - let injections := PTree.elements (gen_injections f) in let max_pc := max_pc_function f in let max_reg := max_reg_function f in + let injections := PTree.elements (gen_injections f max_pc max_reg) in if valid_injections1 max_pc max_reg injections then OK {| fn_sig := f.(fn_sig); diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 77cae8a1..2506bcc8 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -538,7 +538,7 @@ Qed. *) Section INJECTOR. - Variable gen_injections : function -> PTree.t (list inj_instr). + Variable gen_injections : function -> node -> reg -> PTree.t (list inj_instr). Definition match_prog (p tp: RTL.program) := match_program (fun ctx f tf => transf_fundef gen_injections f = OK tf) eq p tp. @@ -808,10 +808,10 @@ Section INJECTOR. Lemma transf_function_inj_starstep_rec : forall ts f tf sp m inj_n src_pc inj_pc inj_code (FUN : transf_function gen_injections f = OK tf) - (INJ : nth_error (PTree.elements (gen_injections f)) inj_n = + (INJ : nth_error (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) inj_n = Some (src_pc, inj_code)) (POSITION : inject_l_position (Pos.succ (max_pc_function f)) - (PTree.elements (gen_injections f)) inj_n = inj_pc) + (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) inj_n = inj_pc) (k : nat) (CUR : (k <= (List.length inj_code))%nat) (trs : regset), @@ -839,7 +839,7 @@ Section INJECTOR. injection VALIDATE. intro TF. symmetry in TF. - pose proof (inject_l_injected (PTree.elements (gen_injections f)) (fn_code f) inj_n src_pc inj_code (Pos.succ (max_pc_function f)) ((List.length inj_code) - (S k))%nat) as INJECTED. + pose proof (inject_l_injected (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) (fn_code f) inj_n src_pc inj_code (Pos.succ (max_pc_function f)) ((List.length inj_code) - (S k))%nat) as INJECTED. lapply INJECTED. { clear INJECTED. intro INJECTED. @@ -848,7 +848,7 @@ Section INJECTOR. pose proof (INJECTED INJ LESS) as INJ'. replace (snd (inject_l (fn_code f) (Pos.succ (max_pc_function f)) - (PTree.elements (gen_injections f)))) with (fn_code tf) in INJ'. + (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))))) with (fn_code tf) in INJ'. 2: rewrite TF; simpl; reflexivity. apply transf_function_inj_step with (f:=f) (ts:=ts) (sp:=sp) (trs:=trs) (m := m) in INJ'. 2: assumption. { @@ -898,10 +898,10 @@ Section INJECTOR. Lemma transf_function_inj_starstep : forall ts f tf sp m inj_n src_pc inj_pc inj_code (FUN : transf_function gen_injections f = OK tf) - (INJ : nth_error (PTree.elements (gen_injections f)) inj_n = + (INJ : nth_error (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) inj_n = Some (src_pc, inj_code)) (POSITION : inject_l_position (Pos.succ (max_pc_function f)) - (PTree.elements (gen_injections f)) inj_n = inj_pc) + (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) inj_n = inj_pc) (trs : regset), exists trs', match_regs (f : function) trs trs' /\ @@ -920,11 +920,11 @@ Section INJECTOR. Lemma transf_function_inj_end : forall ts f tf sp m inj_n src_pc inj_pc inj_code i (FUN : transf_function gen_injections f = OK tf) - (INJ : nth_error (PTree.elements (gen_injections f)) inj_n = + (INJ : nth_error (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) inj_n = Some (src_pc, inj_code)) (SRC: (fn_code f) ! src_pc = Some i) (POSITION : inject_l_position (Pos.succ (max_pc_function f)) - (PTree.elements (gen_injections f)) inj_n = inj_pc) + (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) inj_n = inj_pc) (trs : regset), RTL.step tge (State ts tf sp (pos_add_nat inj_pc (List.length inj_code)) trs m) E0 @@ -938,13 +938,13 @@ Section INJECTOR. injection VALIDATE. intro TF. symmetry in TF. - pose proof (inject_l_injected_end (PTree.elements (gen_injections f)) (fn_code f) inj_n src_pc i inj_code (Pos.succ (max_pc_function f))) as INJECTED. + pose proof (inject_l_injected_end (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) (fn_code f) inj_n src_pc i inj_code (Pos.succ (max_pc_function f))) as INJECTED. lapply INJECTED. 2: assumption. clear INJECTED. intro INJECTED. lapply INJECTED. - 2: apply (PTree.elements_keys_norepet (gen_injections f)); fail. + 2: apply (PTree.elements_keys_norepet (gen_injections f (max_pc_function f) (max_reg_function f))); fail. clear INJECTED. intro INJECTED. lapply INJECTED. @@ -954,7 +954,7 @@ Section INJECTOR. clear INJECTED. replace (snd (inject_l (fn_code f) (Pos.succ (max_pc_function f)) - (PTree.elements (gen_injections f)))) with (fn_code tf) in INJ'. + (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))))) with (fn_code tf) in INJ'. 2: rewrite TF; simpl; reflexivity. rewrite POSITION in INJ'. apply exec_Inop. @@ -975,11 +975,11 @@ Section INJECTOR. Lemma transf_function_inj_plusstep : forall ts f tf sp m inj_n src_pc inj_pc inj_code i (FUN : transf_function gen_injections f = OK tf) - (INJ : nth_error (PTree.elements (gen_injections f)) inj_n = + (INJ : nth_error (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) inj_n = Some (src_pc, inj_code)) (SRC: (fn_code f) ! src_pc = Some i) (POSITION : inject_l_position (Pos.succ (max_pc_function f)) - (PTree.elements (gen_injections f)) inj_n = inj_pc) + (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) inj_n = inj_pc) (trs : regset), exists trs', match_regs (f : function) trs trs' /\ @@ -1001,7 +1001,7 @@ Section INJECTOR. forall f tf pc (FUN : transf_function gen_injections f = OK tf) (LESS : pc <= max_pc_function f) - (NOCHANGE : (gen_injections f) ! pc = None), + (NOCHANGE : (gen_injections f (max_pc_function f) (max_reg_function f)) ! pc = None), (fn_code tf) ! pc = (fn_code f) ! pc. Proof. intros. @@ -1027,7 +1027,7 @@ Section INJECTOR. forall f tf pc injl ii (FUN : transf_function gen_injections f = OK tf) (LESS : pc <= max_pc_function f) - (INJECTION : (gen_injections f) ! pc = Some injl) + (INJECTION : (gen_injections f (max_pc_function f) (max_reg_function f)) ! pc = Some injl) (INSTR: (fn_code f) ! pc = Some ii), exists pc' : node, (fn_code tf) ! pc = Some (alter_successor ii pc') /\ @@ -1043,7 +1043,7 @@ Section INJECTOR. apply In_nth_error in INJECTION. destruct INJECTION as [injn INJECTION]. exists (inject_l_position (Pos.succ (max_pc_function f)) - (PTree.elements (gen_injections f)) injn). + (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) injn). split. { unfold transf_function in FUN. destruct (valid_injections1) eqn:VALID in FUN. @@ -1067,7 +1067,7 @@ Section INJECTOR. intros. pose proof (transf_function_inj_plusstep ts f tf sp m injn pc (inject_l_position (Pos.succ (max_pc_function f)) - (PTree.elements (gen_injections f)) injn) + (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) injn) injl ii FUN INJECTION INSTR) as TRANS. lapply TRANS. 2: reflexivity. @@ -1272,7 +1272,7 @@ Section INJECTOR. Proof. induction 1; intros ts1 MS; inv MS; try (inv TRC). - (* nop *) - destruct ((gen_injections f) ! pc) eqn:INJECTION. + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } intros [pc_inj [ALTER SKIP]]. @@ -1295,7 +1295,7 @@ Section INJECTOR. * constructor; trivial. - (* op *) - destruct ((gen_injections f) ! pc) eqn:INJECTION. + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } intros [pc_inj [ALTER SKIP]]. @@ -1339,7 +1339,7 @@ Section INJECTOR. assumption. - (* load *) - destruct ((gen_injections f) ! pc) eqn:INJECTION. + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } intros [pc_inj [ALTER SKIP]]. @@ -1381,7 +1381,7 @@ Section INJECTOR. assumption. - (* load notrap1 *) - destruct ((gen_injections f) ! pc) eqn:INJECTION. + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } intros [pc_inj [ALTER SKIP]]. @@ -1421,7 +1421,7 @@ Section INJECTOR. assumption. - (* load notrap2 *) - destruct ((gen_injections f) ! pc) eqn:INJECTION. + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } intros [pc_inj [ALTER SKIP]]. @@ -1463,7 +1463,7 @@ Section INJECTOR. assumption. - (* store *) - destruct ((gen_injections f) ! pc) eqn:INJECTION. + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } intros [pc_inj [ALTER SKIP]]. @@ -1506,7 +1506,7 @@ Section INJECTOR. * constructor; trivial. - (* call *) destruct (transf_function_preserves_ros f tf pc rs trs ros args res fd pc' (funsig fd) FUN REGS H H0) as [tfd [TFD1 TFD2]]. - destruct ((gen_injections f) ! pc) eqn:INJECTION. + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } intros [pc_inj [ALTER SKIP]]. @@ -1568,7 +1568,7 @@ Section INJECTOR. - (* tailcall *) destruct (transf_function_preserves_ros_tail f tf pc rs trs ros args fd (funsig fd) FUN REGS H H0) as [tfd [TFD1 TFD2]]. - destruct ((gen_injections f) ! pc) eqn:INJECTION. + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } intros [pc_inj [ALTER SKIP]]. @@ -1606,7 +1606,7 @@ Section INJECTOR. apply match_states_call; auto. - (* builtin *) - destruct ((gen_injections f) ! pc) eqn:INJECTION. + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } intros [pc_inj [ALTER SKIP]]. @@ -1642,7 +1642,7 @@ Section INJECTOR. assumption. - (* cond *) - destruct ((gen_injections f) ! pc) eqn:INJECTION. + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + destruct b eqn:B. ++ exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } @@ -1695,7 +1695,7 @@ Section INJECTOR. *** reflexivity. ** constructor; auto. - - destruct ((gen_injections f) ! pc) eqn:INJECTION. + - destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } intros [pc_inj [ALTER SKIP]]. @@ -1718,7 +1718,7 @@ Section INJECTOR. eassumption. * constructor; trivial. - (* return *) - destruct ((gen_injections f) ! pc) eqn:INJECTION. + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } intros [pc_inj [ALTER SKIP]]. 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) ] diff --git a/extraction/extraction.v b/extraction/extraction.v index cb461361..1bb5a709 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -120,6 +120,9 @@ Extract Constant Compopts.optim_CSE3 => "fun _ -> !Clflags.option_fcse3". Extract Constant Compopts.optim_CSE3_alias_analysis => "fun _ -> !Clflags.option_fcse3_alias_analysis". +Extract Constant Compopts.optim_move_loop_invariants => + "fun _ -> !Clflags.option_fmove_loop_invariants". + Extract Constant Compopts.optim_redundancy => "fun _ -> !Clflags.option_fredundancy". Extract Constant Compopts.optim_postpass => -- cgit