aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backend/Inject.v4
-rw-r--r--backend/Injectproof.v60
-rw-r--r--driver/Clflags.ml1
-rw-r--r--driver/Compopts.v3
-rw-r--r--driver/Driver.ml2
-rw-r--r--extraction/extraction.v3
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= <optim> 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 =>
generated by cgit (git 2.34.1) at 2024-05-20 09:24:30 +0000