aboutsummaryrefslogtreecommitdiffstats
path: root/tools
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-04-21 22:08:07 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-04-21 22:08:07 +0200
commit9cc12b684ee6833971c9549aa76cc683ba931090 (patch)
treec3c602e334aea87be90e9d6b4988df225554e454 /tools
parentb17a25bae0f9580caadfa5f795a3c12a050075f5 (diff)
downloadcompcert-kvx-9cc12b684ee6833971c9549aa76cc683ba931090.tar.gz
compcert-kvx-9cc12b684ee6833971c9549aa76cc683ba931090.zip
begin scripting the Compiler.v file
Diffstat (limited to 'tools')
-rw-r--r--tools/compiler_expand.ml62
1 files changed, 62 insertions, 0 deletions
diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml
new file mode 100644
index 00000000..63808c1f
--- /dev/null
+++ b/tools/compiler_expand.ml
@@ -0,0 +1,62 @@
+type is_partial = TOTAL | PARTIAL;;
+type when_triggered = Always | Option of string;;
+
+let passes =
+[|
+TOTAL, (Option "optim_tailcalls"), (Some "Tail calls"), "Tailcall";
+PARTIAL, Always, (Some "Inlining"), "Inlining";
+TOTAL, (Option "profile_arcs"), (Some "Profiling insertion"), "Profiling";
+TOTAL, (Option "branch_probabilities"), (Some "Profiling use"), "ProfilingExploit";
+TOTAL, (Option "optim_move_loop_invariants"), (Some "Inserting initial nop"), "FirstNop";
+TOTAL, Always, (Some "Renumbering"), "Renumber";
+PARTIAL, (Option "optim_duplicate"), (Some "Tail-duplicating"), "Duplicate";
+TOTAL, Always, (Some "Renumbering pre constprop"), "Renumber";
+TOTAL, (Option "optim_constprop"), (Some "Constant propagation"), "Constprop";
+PARTIAL, (Option "optim_move_loop_invariants"), (Some "LICM"), "LICM";
+TOTAL, (Option "optim_move_loop_invariants"), (Some "Renumbering pre CSE"), "Renumber";
+PARTIAL, (Option "optim_CSE"), (Some "CSE"), "CSE";
+TOTAL, (Option "optim_CSE2"), (Some "CSE2"), "CSE2";
+PARTIAL, (Option "optim_CSE3"), (Some "CSE3"), "CSE3";
+TOTAL, (Option "optim_forward_moves"), (Some "Forwarding moves"), "ForwardMoves";
+PARTIAL, (Option "optim_redundancy"), (Some "Redundancy elimination"), "Deadcode";
+TOTAL, (Option "all_loads_nontrap"), None, "Allnontrap";
+PARTIAL, Always, (Some "Unused globals"), "Unusedglob"
+|];;
+
+let totality = function TOTAL -> "total" | PARTIAL -> "partial";;
+
+let print_transf oc =
+ Array.iteri
+ (fun i (partial, trigger, time_label, pass_name) ->
+ output_string oc (match partial with
+ | TOTAL -> " @@ "
+ | PARTIAL -> " @@@ ");
+ (match trigger with
+ | Always -> ()
+ | Option s ->
+ Printf.fprintf oc "%s_if Compopts.%s " (totality partial) s);
+ output_char oc '(';
+ (match time_label with
+ | None -> ()
+ | Some s ->
+ Printf.fprintf oc "time \"%s\" " s);
+ Printf.fprintf oc "%s.transf_program)\n" pass_name;
+ Printf.fprintf oc " @@ print (print_RTL %d)\n" (succ i)
+ ) passes;;
+
+if (Array.length Sys.argv)<>3
+then exit 1;;
+
+let filename_in = Sys.argv.(1) and filename_out = Sys.argv.(2) in
+ let ic = open_in filename_in and oc = open_out filename_out in
+ try
+ while true
+ do
+ let line = input_line ic in
+ if line = "EXPAND_TRANSF_PROGRAM"
+ then print_transf oc
+ else (output_string oc line;
+ output_char oc '\n')
+ done
+ with End_of_file ->
+ (close_in ic; close_out oc);;