diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2020-03-09 15:16:08 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2020-03-09 15:16:08 +0100 |
commit | b016de5a1a8230b5a6c51d8e7cd8829d39a4c781 (patch) | |
tree | da167bb86a5eba736db551df7df613eb5201a30c /driver/Compiler.v | |
parent | ec0d767ba602c35e320ee77f2ccd6f513adeb7b6 (diff) | |
download | compcert-kvx-b016de5a1a8230b5a6c51d8e7cd8829d39a4c781.tar.gz compcert-kvx-b016de5a1a8230b5a6c51d8e7cd8829d39a4c781.zip |
[BROKEN] Replacing the boolean -fduplicate option by an integer
To control the threshold for duplication
Diffstat (limited to 'driver/Compiler.v')
-rw-r--r-- | driver/Compiler.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/driver/Compiler.v b/driver/Compiler.v index 499feff2..da19a0b9 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -134,7 +134,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 2) @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 3) - @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) + @@@ time "Tail-duplicating" Duplicate.transf_program @@ print (print_RTL 4) @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 5) @@ -254,7 +254,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) ::: mkpass Inliningproof.match_prog ::: mkpass Renumberproof.match_prog - ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) + ::: mkpass Duplicateproof.match_prog ::: 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) @@ -301,7 +301,7 @@ Proof. 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 (partial_if optim_duplicate Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. + destruct (Duplicate.transf_program p9) 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. @@ -326,7 +326,7 @@ Proof. 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 p10; split. eapply partial_if_match; eauto. apply Duplicateproof.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. exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. @@ -412,7 +412,7 @@ Ltac DestructM := eapply Inliningproof.transf_program_correct; eassumption. 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 Duplicateproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. eapply compose_forward_simulations. |