diff options
| -rw-r--r-- | driver/Compiler.vexpand | 19 | ||||
| -rw-r--r-- | tools/compiler_expand.ml | 14 |
2 files changed, 14 insertions, 19 deletions
diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index d0ba33d3..c044d9ef 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -208,24 +208,7 @@ Definition CompCert's_passes := ::: mkpass Cminorgenproof.match_prog ::: mkpass Selectionproof.match_prog ::: mkpass RTLgenproof.match_prog - ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) - ::: mkpass Inliningproof.match_prog - ::: mkpass (match_if Compopts.profile_arcs Profilingproof.match_prog) - ::: mkpass (match_if Compopts.branch_probabilities ProfilingExploitproof.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 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) - ::: mkpass (match_if Compopts.optim_CSE2 CSE2proof.match_prog) - ::: mkpass (match_if Compopts.optim_CSE3 CSE3proof.match_prog) - ::: mkpass (match_if Compopts.optim_forward_moves ForwardMovesproof.match_prog) - ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) - ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog) - ::: mkpass Unusedglobproof.match_prog +EXPAND_RTL_MKPASS ::: mkpass Allocproof.match_prog ::: mkpass Tunnelingproof.match_prog ::: mkpass Linearizeproof.match_prog diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml index 7ca3c755..1ef233e7 100644 --- a/tools/compiler_expand.ml +++ b/tools/compiler_expand.ml @@ -53,7 +53,17 @@ let print_rtl_transf oc = Printf.fprintf oc "%s.transf_program)\n" pass_name; Printf.fprintf oc " @@ print (print_RTL %d)\n" (succ i) ) rtl_passes;; - + +let print_rtl_mkpass oc = + Array.iter (fun (partial, trigger, time_label, pass_name) -> + output_string oc " ::: mkpass ("; + (match trigger with + | Always -> () + | Option s -> + Printf.fprintf oc "match_if Compopts.%s " s); + Printf.fprintf oc "%sproof.match_prog)\n" pass_name) + rtl_passes;; + if (Array.length Sys.argv)<>3 then exit 1;; @@ -69,6 +79,8 @@ let filename_in = Sys.argv.(1) and filename_out = Sys.argv.(2) in print_rtl_require oc | "EXPAND_RTL_REQUIRE_PROOF" -> print_rtl_require_proof oc + | "EXPAND_RTL_MKPASS" -> + print_rtl_mkpass oc | line -> (output_string oc line; output_char oc '\n') done |