diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-12 14:31:36 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-12 14:31:36 +0100 |
| commit | 1f862e1e61ac9b52509e6843bb3948e0a0b2c770 (patch) | |
| tree | bfe716c6601733e32c4f0ecc4d2db2cdfa8fa823 | |
| parent | 65464e2b1623f9fa725f4503d0f78ac2a502a4fb (diff) | |
| download | compcert-kvx-1f862e1e61ac9b52509e6843bb3948e0a0b2c770.tar.gz compcert-kvx-1f862e1e61ac9b52509e6843bb3948e0a0b2c770.zip | |
our phase needs to go before renumbering
| -rw-r--r-- | backend/RTLblockrevgen.v | 5 | ||||
| -rw-r--r-- | driver/Compiler.v | 18 |
2 files changed, 13 insertions, 10 deletions
diff --git a/backend/RTLblockrevgen.v b/backend/RTLblockrevgen.v index 9e208b8d..ca61e8ee 100644 --- a/backend/RTLblockrevgen.v +++ b/backend/RTLblockrevgen.v @@ -4,6 +4,7 @@ Require Import Op Registers. Require Import RTL. Require Import RTLblock. Require Import Errors. +Require Coq.PArith.Pnat. Local Open Scope error_monad_scope. @@ -138,9 +139,11 @@ Fixpoint transl_code end end. +Definition transl_function_fuel := 10000%positive . + Definition transl_function (fn : RTLblock.function): Errors.res (RTL.function) := do ns <- transl_code initial_nodestate (RTLblock.fn_code fn) - (RTLblock.fn_entrypoint fn :: nil) 300%nat ; + (RTLblock.fn_entrypoint fn :: nil) (Pos.to_nat transl_function_fuel) ; match PTree.get (RTLblock.fn_entrypoint fn) (ns_label2node ns) with | None => Error (Errors.msg "RTLblockrevgen.transl_function: cannot find entrypoint") | Some entrypoint => diff --git a/driver/Compiler.v b/driver/Compiler.v index dc809490..06685237 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -127,21 +127,21 @@ 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 "To RTLblock" RTLblockgen.transl_program + @@ print (print_RTLblock 0) + @@@ time "Back from RTLblock" RTLblockrevgen.transl_program @@ print (print_RTL 3) - @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) + @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 4) - @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) + @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 5) - @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) + @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) @@ print (print_RTL 6) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.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 "To RTLblock" RTLblockgen.transl_program - @@ print (print_RTLblock 0) - @@@ time "Back from RTLblock" RTLblockrevgen.transl_program + @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 9) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL |