From 9cc12b684ee6833971c9549aa76cc683ba931090 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 21 Apr 2020 22:08:07 +0200 Subject: begin scripting the Compiler.v file --- tools/compiler_expand.ml | 62 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) create mode 100644 tools/compiler_expand.ml (limited to 'tools') 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);; -- cgit From 1bd4d678fb719a6a52ade232eb2b36a6e621677a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 21 Apr 2020 22:24:31 +0200 Subject: Require autogen --- tools/compiler_expand.ml | 30 ++++++++++++++++++++++-------- 1 file changed, 22 insertions(+), 8 deletions(-) (limited to 'tools') diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml index 63808c1f..7ca3c755 100644 --- a/tools/compiler_expand.ml +++ b/tools/compiler_expand.ml @@ -1,7 +1,7 @@ type is_partial = TOTAL | PARTIAL;; type when_triggered = Always | Option of string;; -let passes = +let rtl_passes = [| TOTAL, (Option "optim_tailcalls"), (Some "Tail calls"), "Tailcall"; PARTIAL, Always, (Some "Inlining"), "Inlining"; @@ -25,7 +25,17 @@ PARTIAL, Always, (Some "Unused globals"), "Unusedglob" let totality = function TOTAL -> "total" | PARTIAL -> "partial";; -let print_transf oc = +let print_rtl_require oc = + Array.iter (fun (partial, trigger, time_label, pass_name) -> + Printf.fprintf oc "Require %s.\n" pass_name) + rtl_passes;; + +let print_rtl_require_proof oc = + Array.iter (fun (partial, trigger, time_label, pass_name) -> + Printf.fprintf oc "Require %sproof.\n" pass_name) + rtl_passes;; + +let print_rtl_transf oc = Array.iteri (fun i (partial, trigger, time_label, pass_name) -> output_string oc (match partial with @@ -42,7 +52,7 @@ let print_transf oc = 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;; + ) rtl_passes;; if (Array.length Sys.argv)<>3 then exit 1;; @@ -52,11 +62,15 @@ let filename_in = Sys.argv.(1) and filename_out = Sys.argv.(2) 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') + match input_line ic with + | "EXPAND_RTL_TRANSF_PROGRAM" -> + print_rtl_transf oc + | "EXPAND_RTL_REQUIRE" -> + print_rtl_require oc + | "EXPAND_RTL_REQUIRE_PROOF" -> + print_rtl_require_proof oc + | line -> (output_string oc line; + output_char oc '\n') done with End_of_file -> (close_in ic; close_out oc);; -- cgit From 25547c7d1f6a0fb75ff1d8e7287d9305e0dbf293 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 21 Apr 2020 22:42:32 +0200 Subject: generate mkpass --- tools/compiler_expand.ml | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) (limited to 'tools') 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 -- cgit From f5da5188171962d13b9f3eac04845dd19d0aa931 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 22 Apr 2020 08:08:21 +0200 Subject: automated writing Compiler.v --- tools/compiler_expand.ml | 87 +++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 79 insertions(+), 8 deletions(-) (limited to 'tools') diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml index 1ef233e7..1555d75b 100644 --- a/tools/compiler_expand.ml +++ b/tools/compiler_expand.ml @@ -1,4 +1,5 @@ type is_partial = TOTAL | PARTIAL;; +type print_result = Noprint | Print of string;; type when_triggered = Always | Option of string;; let rtl_passes = @@ -23,21 +24,38 @@ TOTAL, (Option "all_loads_nontrap"), None, "Allnontrap"; PARTIAL, Always, (Some "Unused globals"), "Unusedglob" |];; +let post_rtl_passes = +[| + PARTIAL, Always, (Some "Register allocation"), "Allocation", (Print "LTL"); + TOTAL, Always, (Some "Branch tunneling"), "Tunneling", Noprint; + PARTIAL, Always, (Some "CFG linearization"), "Linearize", Noprint; + TOTAL, Always, (Some "Label cleanup"), "CleanupLabels", Noprint; + PARTIAL, (Option "debug"), (Some "Debugging info for local variables"), "Debugvar", Noprint; + PARTIAL, Always, (Some "Mach generation"), "Stacking", (Print "Mach") +|];; + +let all_passes = + Array.concat + [Array.mapi + (fun i (a,b,c,d) -> (a,b,c,d, Print (Printf.sprintf "RTL %d" (i+1)))) + rtl_passes; + post_rtl_passes];; + let totality = function TOTAL -> "total" | PARTIAL -> "partial";; let print_rtl_require oc = - Array.iter (fun (partial, trigger, time_label, pass_name) -> + Array.iter (fun (partial, trigger, time_label, pass_name, printing) -> Printf.fprintf oc "Require %s.\n" pass_name) - rtl_passes;; + all_passes;; let print_rtl_require_proof oc = - Array.iter (fun (partial, trigger, time_label, pass_name) -> + Array.iter (fun (partial, trigger, time_label, pass_name, printing) -> Printf.fprintf oc "Require %sproof.\n" pass_name) - rtl_passes;; + all_passes;; let print_rtl_transf oc = Array.iteri - (fun i (partial, trigger, time_label, pass_name) -> + (fun i (partial, trigger, time_label, pass_name, printing) -> output_string oc (match partial with | TOTAL -> " @@ " | PARTIAL -> " @@@ "); @@ -51,17 +69,61 @@ let print_rtl_transf oc = | 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) - ) rtl_passes;; + (match printing with + | Noprint -> () + | Print s -> + Printf.fprintf oc " @@ print (print_%s)\n" s) + ) all_passes;; let print_rtl_mkpass oc = - Array.iter (fun (partial, trigger, time_label, pass_name) -> + Array.iter (fun (partial, trigger, time_label, pass_name, printing) -> 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) + all_passes;; + +let print_if kind oc = function + | Always -> () + | Option s -> Printf.fprintf oc "%s_if %s " kind s;; + +let numbering_base = 7 + +let print_rtl_proof oc = + Array.iteri (fun i (partial, trigger, time_label, pass_name, printing) -> + let j = i+numbering_base in + match partial with + | TOTAL -> + Printf.fprintf oc "set (p%d := %a%s.transf_program p%d) in *.\n" + j (print_if "total") trigger pass_name (pred j) + | PARTIAL -> + Printf.fprintf oc "destruct (%a%s.transf_program p%d) as [p%d|e] eqn:P%d; simpl in T; try discriminate.\n" + (print_if "partial") trigger pass_name (pred j) j j) + all_passes;; + +let print_rtl_proof2 oc = + Array.iteri (fun i (partial, trigger, time_label, pass_name, printing) -> + let j = i+numbering_base in + Printf.fprintf oc " exists p%d; split. " j; + (match trigger with + | Always -> () + | Option _ -> + (match partial with + | TOTAL -> output_string oc "apply total_if_match. " + | PARTIAL -> output_string oc "eapply partial_if_match; eauto. ")); + Printf.fprintf oc "apply %sproof.transf_program_match; auto.\n" pass_name) + all_passes;; + +let print_rtl_forward_simulations oc = + Array.iter (fun (partial, trigger, time_label, pass_name) -> + output_string oc " eapply compose_forward_simulations.\n "; + (match trigger with + | Always -> () + | Option s -> output_string oc "eapply match_if_simulation. eassumption. "); + Printf.fprintf oc "eapply %sproof.transf_program_correct; eassumption." pass_name + ) rtl_passes;; if (Array.length Sys.argv)<>3 @@ -81,6 +143,15 @@ let filename_in = Sys.argv.(1) and filename_out = Sys.argv.(2) in print_rtl_require_proof oc | "EXPAND_RTL_MKPASS" -> print_rtl_mkpass oc + | "EXPAND_RTL_PROOF" -> + print_rtl_proof oc + | "EXPAND_RTL_PROOF2" -> + print_rtl_proof2 oc + | "EXPAND_ASM_SEMANTICS" -> + Printf.fprintf oc " (Asm.semantics p%d)\n" + ((Array.length all_passes) + 7) + | "EXPAND_RTL_FORWARD_SIMULATIONS" -> + print_rtl_forward_simulations oc | line -> (output_string oc line; output_char oc '\n') done -- cgit From 05a5825ee55227327ba1b09a548e3b9ba876d0cf Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 22 Apr 2020 08:53:06 +0200 Subject: use cbn in T instead of simpl in T --- tools/compiler_expand.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tools') diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml index 1555d75b..4fc746f0 100644 --- a/tools/compiler_expand.ml +++ b/tools/compiler_expand.ml @@ -99,7 +99,7 @@ let print_rtl_proof oc = Printf.fprintf oc "set (p%d := %a%s.transf_program p%d) in *.\n" j (print_if "total") trigger pass_name (pred j) | PARTIAL -> - Printf.fprintf oc "destruct (%a%s.transf_program p%d) as [p%d|e] eqn:P%d; simpl in T; try discriminate.\n" + Printf.fprintf oc "destruct (%a%s.transf_program p%d) as [p%d|e] eqn:P%d; cbn in T; try discriminate.\n" (print_if "partial") trigger pass_name (pred j) j j) all_passes;; -- cgit From c991b6f67778634cf1c8df5fb429a74d068c8fb8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 22 Apr 2020 11:27:15 +0200 Subject: cbn and copyright --- tools/compiler_expand.ml | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'tools') diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml index 4fc746f0..960d1ce1 100644 --- a/tools/compiler_expand.ml +++ b/tools/compiler_expand.ml @@ -1,3 +1,13 @@ +(* +The Compcert verified compiler + +Compiler.vexpand -> Compiler.v + +Expand the list of RTL compiler passes into Compiler.v + +David Monniaux, CNRS, VERIMAG + *) + type is_partial = TOTAL | PARTIAL;; type print_result = Noprint | Print of string;; type when_triggered = Always | Option of string;; -- cgit From ce36b497e2af67f09bb98247e03d0d7a1fe6216f Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 23 Apr 2020 16:57:18 +0200 Subject: sync with licm --- tools/compiler_expand.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tools') diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml index 960d1ce1..025dbacc 100644 --- a/tools/compiler_expand.ml +++ b/tools/compiler_expand.ml @@ -24,7 +24,7 @@ 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"; +TOTAL, Always, (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"; -- cgit From fd81859f8a8299b4f3d399d605175ff1b8ee2a81 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 24 Apr 2020 09:07:57 +0200 Subject: run a separate CSE3 for LICM --- tools/compiler_expand.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'tools') diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml index 025dbacc..8738c3af 100644 --- a/tools/compiler_expand.ml +++ b/tools/compiler_expand.ml @@ -23,13 +23,15 @@ 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, Always, (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"; +PARTIAL, (Option "optim_move_loop_invariants"), (Some "LICM"), "LICM"; +PARTIAL, (Option "optim_move_loop_invariants"), (Some "CSE3 for LICM"), "CSE3"; +PARTIAL, (Option "optim_move_loop_invariants"), (Some "Redundancy elimination for LICM"), "Deadcode"; TOTAL, (Option "all_loads_nontrap"), None, "Allnontrap"; PARTIAL, Always, (Some "Unused globals"), "Unusedglob" |];; -- cgit From cb7f9dae1d354bbf94d8da87e3d4c72057992965 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 30 Apr 2020 22:41:22 +0200 Subject: add a renumber phase --- tools/compiler_expand.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'tools') diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml index 8738c3af..1fa5ad28 100644 --- a/tools/compiler_expand.ml +++ b/tools/compiler_expand.ml @@ -30,6 +30,7 @@ PARTIAL, (Option "optim_CSE3"), (Some "CSE3"), "CSE3"; TOTAL, (Option "optim_forward_moves"), (Some "Forwarding moves"), "ForwardMoves"; PARTIAL, (Option "optim_redundancy"), (Some "Redundancy elimination"), "Deadcode"; PARTIAL, (Option "optim_move_loop_invariants"), (Some "LICM"), "LICM"; +TOTAL, (Option "optim_move_loop_invariants"), (Some "Renumbering for LICM"), "Renumber"; PARTIAL, (Option "optim_move_loop_invariants"), (Some "CSE3 for LICM"), "CSE3"; PARTIAL, (Option "optim_move_loop_invariants"), (Some "Redundancy elimination for LICM"), "Deadcode"; TOTAL, (Option "all_loads_nontrap"), None, "Allnontrap"; -- cgit From e7fad4516e0e7705480312caa427e838f3321948 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 28 May 2020 07:27:46 +0200 Subject: automatic date in the html index --- tools/fix_html_date.sh | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100755 tools/fix_html_date.sh (limited to 'tools') diff --git a/tools/fix_html_date.sh b/tools/fix_html_date.sh new file mode 100755 index 00000000..c7fbdabe --- /dev/null +++ b/tools/fix_html_date.sh @@ -0,0 +1,8 @@ +#!/bin/bash +# +# Replace an HTML comment "" by the current date +# in the file given by $1 (with $2 as prefix and $3 as suffix) +# +# Result on standard output + +sed -e "s//$2$(date +'%F')$3/g" $1 -- cgit