diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | backend/Duplicate.v | 26 | ||||
| -rw-r--r-- | backend/Duplicateaux.ml | 34 | ||||
| -rw-r--r-- | backend/Duplicatepasses.v | 64 | ||||
| -rw-r--r-- | backend/Duplicateproof.v | 5 | ||||
| -rw-r--r-- | driver/Compiler.vexpand | 1 | ||||
| -rw-r--r-- | tools/compiler_expand.ml | 97 |
7 files changed, 166 insertions, 63 deletions
@@ -85,7 +85,7 @@ BACKEND=\ Profiling.v Profilingproof.v \ ProfilingExploit.v ProfilingExploitproof.v \ Renumber.v Renumberproof.v \ - Duplicate.v Duplicateproof.v \ + Duplicate.v Duplicateproof.v Duplicatepasses.v \ RTLtyping.v \ Kildall.v Liveness.v \ ValueDomain.v ValueAOp.v ValueAnalysis.v \ diff --git a/backend/Duplicate.v b/backend/Duplicate.v index 0e04b07d..6ae5475d 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -18,14 +18,28 @@ Require Import AST RTL Maps Globalenvs. Require Import Coqlib Errors Op. -Local Open Scope error_monad_scope. -Local Open Scope positive_scope. -(** External oracle returning the new RTL code (entry point unchanged), + +Module Type DuplicateParam. + + (** External oracle returning the new RTL code (entry point unchanged), along with the new entrypoint, and a mapping of new nodes to old nodes *) -Axiom duplicate_aux: function -> code * node * (PTree.t node). + Parameter duplicate_aux: function -> code * node * (PTree.t node). + +End DuplicateParam. + + -Extract Constant duplicate_aux => "Duplicateaux.duplicate_aux". +Module Duplicate (D: DuplicateParam). + +Export D. + +Definition duplicate_aux := duplicate_aux. + +(* Extract Constant duplicate_aux => "Duplicateaux.duplicate_aux". *) + +Local Open Scope error_monad_scope. +Local Open Scope positive_scope. (** * Verification of node duplications *) @@ -215,3 +229,5 @@ Definition transf_fundef (f: fundef) : res fundef := Definition transf_program (p: program) : res program := transform_partial_program transf_fundef p. + +End Duplicate. diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml index eb9f42e0..2b13ab5d 100644 --- a/backend/Duplicateaux.ml +++ b/backend/Duplicateaux.ml @@ -836,42 +836,48 @@ let unroll_inner_loops_body f code revmap = (!code', !revmap') end -let duplicate_aux f = - (* initializing *) +let static_predict f = let entrypoint = f.fn_entrypoint in let code = f.fn_code in let revmap = make_identity_ptree code in - - (* static prediction *) let code = if !Clflags.option_fpredict then update_directions code entrypoint else code in + let code = + if !Clflags.option_fpredict then + invert_iconds code + else code in + ((code, entrypoint), revmap) - (* unroll single *) +let unroll_single f = + let entrypoint = f.fn_entrypoint in + let code = f.fn_code in + let revmap = make_identity_ptree code in let (code, revmap) = if !Clflags.option_funrollsingle > 0 then unroll_inner_loops_single f code revmap else (code, revmap) in + ((code, entrypoint), revmap) - (* unroll body *) +let unroll_body f = + let entrypoint = f.fn_entrypoint in + let code = f.fn_code in + let revmap = make_identity_ptree code in let (code, revmap) = if !Clflags.option_funrollbody > 0 then unroll_inner_loops_body f code revmap else (code, revmap) in + ((code, entrypoint), revmap) - (* static prediction bis *) - let code = - if !Clflags.option_fpredict then - invert_iconds code - else code in - - (* tail duplication *) +let tail_duplicate f = + let entrypoint = f.fn_entrypoint in + let code = f.fn_code in + let revmap = make_identity_ptree code in let (code, revmap) = if !Clflags.option_ftailduplicate > 0 then let traces = select_traces code entrypoint in let preds = get_predecessors_rtl code in superblockify_traces code preds traces revmap else (code, revmap) in - ((code, entrypoint), revmap) diff --git a/backend/Duplicatepasses.v b/backend/Duplicatepasses.v new file mode 100644 index 00000000..f1770494 --- /dev/null +++ b/backend/Duplicatepasses.v @@ -0,0 +1,64 @@ +Require Import RTL. +Require Import Maps. +Require Import Duplicate. +Require Import Duplicateproof. + +(** Static Prediction *) + +Axiom static_predict_aux : function -> code * node * (PTree.t node). +Extract Constant static_predict_aux => "Duplicateaux.static_predict". + +Module StaticPredictParam <: DuplicateParam. + Definition duplicate_aux := static_predict_aux. +End StaticPredictParam. + +Module StaticPredictDef := Duplicate StaticPredictParam. + +Module Staticpredictproof := DuplicateProof StaticPredictDef. + +Module Staticpredict := Staticpredictproof. + +(** Unrolling one iteration out of the body *) + +Axiom unroll_single_aux : function -> code * node * (PTree.t node). +Extract Constant unroll_single_aux => "Duplicateaux.unroll_single". + +Module UnrollSingleParam <: DuplicateParam. + Definition duplicate_aux := unroll_single_aux. +End UnrollSingleParam. + +Module UnrollSingleDef := Duplicate UnrollSingleParam. + +Module Unrollsingleproof := DuplicateProof UnrollSingleDef. + +Module Unrollsingle := Unrollsingleproof. + +(** Unrolling the body of innermost loops *) + +Axiom unroll_body_aux : function -> code * node * (PTree.t node). +Extract Constant unroll_body_aux => "Duplicateaux.unroll_body". + +Module UnrollBodyParam <: DuplicateParam. + Definition duplicate_aux := unroll_body_aux. +End UnrollBodyParam. + +Module UnrollBodyDef := Duplicate UnrollBodyParam. + +Module Unrollbodyproof := DuplicateProof UnrollBodyDef. + +Module Unrollbody := Unrollbodyproof. + +(** Tail Duplication *) + +Axiom tail_duplicate_aux : function -> code * node * (PTree.t node). +Extract Constant tail_duplicate_aux => "Duplicateaux.tail_duplicate". + +Module TailDuplicateParam <: DuplicateParam. + Definition duplicate_aux := tail_duplicate_aux. +End TailDuplicateParam. + +Module TailDuplicateDef := Duplicate TailDuplicateParam. + +Module Tailduplicateproof := DuplicateProof TailDuplicateDef. + +Module Tailduplicate := Tailduplicateproof.
\ No newline at end of file diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index 62455076..719ff8e9 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -17,6 +17,9 @@ Require Import AST Linking Errors Globalenvs Smallstep. Require Import Coqlib Maps Events Values. Require Import Op RTL Duplicate. +Module DuplicateProof (D: DuplicateParam). +Include Duplicate D. + Local Open Scope positive_scope. (** * Definition of [match_states] (independently of the translation) *) @@ -535,3 +538,5 @@ Proof. Qed. End PRESERVATION. + +End DuplicateProof. diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index 8aaa40c6..80db9097 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -35,6 +35,7 @@ Require Cshmgen. Require Cminorgen. Require Selection. Require RTLgen. +Require Import Duplicatepasses. EXPAND_RTL_REQUIRE Require Asmgen. (** Proofs of semantic preservation. *) diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml index 7e1e0181..35ddfe5e 100644 --- a/tools/compiler_expand.ml +++ b/tools/compiler_expand.ml @@ -11,68 +11,79 @@ David Monniaux, CNRS, VERIMAG type is_partial = TOTAL | PARTIAL;; type print_result = Noprint | Print of string;; type when_triggered = Always | Option of string;; +type needs_require = Require | NoRequire;; +(* FIXME - The gestion of NoRequire is a bit ugly right now. *) let rtl_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_CSE"), (Some "CSE"), "CSE"; -PARTIAL, Always, (Some "Duplicating blocks"), "Duplicate"; -TOTAL, Always, (Some "Renumbering pre constprop"), "Renumber"; -TOTAL, (Option "optim_constprop"), (Some "Constant propagation"), "Constprop"; -TOTAL, Always, (Some "Renumbering pre CSE"), "Renumber"; -TOTAL, (Option "optim_CSE2"), (Some "CSE2"), "CSE2"; -PARTIAL, (Option "optim_CSE3"), (Some "CSE3"), "CSE3"; -TOTAL, (Option "optim_CSE3"), (Some "Kill useless moves after CSE3"), "KillUselessMoves"; -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"; -PARTIAL, Always, (Some "Unused globals"), "Unusedglob"; +TOTAL, (Option "optim_tailcalls"), Require, (Some "Tail calls"), "Tailcall"; +PARTIAL, Always, Require, (Some "Inlining"), "Inlining"; +TOTAL, (Option "profile_arcs"), Require, (Some "Profiling insertion"), "Profiling"; +TOTAL, (Option "branch_probabilities"), Require, (Some "Profiling use"), "ProfilingExploit"; +TOTAL, (Option "optim_move_loop_invariants"), Require, (Some "Inserting initial nop"), "FirstNop"; +TOTAL, Always, Require, (Some "Renumbering"), "Renumber"; +PARTIAL, (Option "optim_CSE"), Require, (Some "CSE"), "CSE"; +PARTIAL, Always, NoRequire, (Some "Static Prediction + inverting conditions"), "Staticpredict"; +PARTIAL, Always, NoRequire, (Some "Unrolling one iteration out of innermost loops"), "Unrollsingle"; +TOTAL, Always, Require, (Some "Renumbering pre unrolling"), "Renumber"; +PARTIAL, Always, NoRequire, (Some "Unrolling the body of innermost loops"), "Unrollbody"; +TOTAL, Always, NoRequire, (Some "Renumbering pre tail duplication"), "Renumber"; +PARTIAL, Always, NoRequire, (Some "Performing tail duplication"), "Tailduplicate"; +TOTAL, Always, NoRequire, (Some "Renumbering pre constprop"), "Renumber"; +TOTAL, (Option "optim_constprop"), Require, (Some "Constant propagation"), "Constprop"; +TOTAL, Always, NoRequire, (Some "Renumbering pre CSE"), "Renumber"; +TOTAL, (Option "optim_CSE2"), Require, (Some "CSE2"), "CSE2"; +PARTIAL, (Option "optim_CSE3"), Require, (Some "CSE3"), "CSE3"; +TOTAL, (Option "optim_CSE3"), Require, (Some "Kill useless moves after CSE3"), "KillUselessMoves"; +TOTAL, (Option "optim_forward_moves"), Require, (Some "Forwarding moves"), "ForwardMoves"; +PARTIAL, (Option "optim_redundancy"), Require, (Some "Redundancy elimination"), "Deadcode"; +PARTIAL, (Option "optim_move_loop_invariants"), Require, (Some "LICM"), "LICM"; +TOTAL, (Option "optim_move_loop_invariants"), NoRequire, (Some "Renumbering for LICM"), "Renumber"; +PARTIAL, (Option "optim_move_loop_invariants"), NoRequire, (Some "CSE3 for LICM"), "CSE3"; +PARTIAL, (Option "optim_move_loop_invariants"), NoRequire, (Some "Redundancy elimination for LICM"), "Deadcode"; +TOTAL, (Option "all_loads_nontrap"), Require, None, "Allnontrap"; +PARTIAL, Always, Require, (Some "Unused globals"), "Unusedglob" |];; let post_rtl_passes = [| - PARTIAL, Always, (Some "RTLpath generation"), "RTLpathLivegen", Noprint; - PARTIAL, Always, (Some "Prepass scheduling"), "RTLpathScheduler", Noprint; - TOTAL, Always, (Some "Projection to RTL"), "RTLpath", (Print (Printf.sprintf "RTL %d" ((Array.length rtl_passes) + 1))); - 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") + PARTIAL, Always, Require, (Some "RTLpath generation"), "RTLpathLivegen", Noprint; + PARTIAL, Always, Require, (Some "Prepass scheduling"), "RTLpathScheduler", Noprint; + TOTAL, Always, Require, (Some "Projection to RTL"), "RTLpath", (Print (Printf.sprintf "RTL %d" ((Array.length rtl_passes) + 1))); + PARTIAL, Always, Require, (Some "Register allocation"), "Allocation", (Print "LTL"); + TOTAL, Always, Require, (Some "Branch tunneling"), "Tunneling", Noprint; + PARTIAL, Always, Require, (Some "CFG linearization"), "Linearize", Noprint; + TOTAL, Always, Require, (Some "Label cleanup"), "CleanupLabels", Noprint; + PARTIAL, (Option "debug"), Require, (Some "Debugging info for local variables"), "Debugvar", Noprint; + PARTIAL, Always, Require, (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)))) + (fun i (a,b,r,c,d) -> (a,b,r,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, printing) -> - Printf.fprintf oc "Require %s.\n" pass_name) - all_passes;; + Array.iter (fun (partial, trigger, require, time_label, pass_name, printing) -> + match require with Require -> + Printf.fprintf oc "Require %s.\n" pass_name + | _ -> () + ) all_passes;; let print_rtl_require_proof oc = - Array.iter (fun (partial, trigger, time_label, pass_name, printing) -> - Printf.fprintf oc "Require %sproof.\n" pass_name) - all_passes;; + Array.iter (fun (partial, trigger, require, time_label, pass_name, printing) -> + match require with Require -> + Printf.fprintf oc "Require %sproof.\n" pass_name + | _ -> () + ) all_passes;; let print_rtl_transf oc = Array.iteri - (fun i (partial, trigger, time_label, pass_name, printing) -> + (fun i (partial, trigger, require, time_label, pass_name, printing) -> output_string oc (match partial with | TOTAL -> " @@ " | PARTIAL -> " @@@ "); @@ -93,7 +104,7 @@ let print_rtl_transf oc = ) all_passes;; let print_rtl_mkpass oc = - Array.iter (fun (partial, trigger, time_label, pass_name, printing) -> + Array.iter (fun (partial, trigger, require, time_label, pass_name, printing) -> output_string oc " ::: mkpass ("; (match trigger with | Always -> () @@ -109,7 +120,7 @@ let print_if kind oc = function let numbering_base = 7 let print_rtl_proof oc = - Array.iteri (fun i (partial, trigger, time_label, pass_name, printing) -> + Array.iteri (fun i (partial, trigger, require, time_label, pass_name, printing) -> let j = i+numbering_base in match partial with | TOTAL -> @@ -121,7 +132,7 @@ let print_rtl_proof oc = all_passes;; let print_rtl_proof2 oc = - Array.iteri (fun i (partial, trigger, time_label, pass_name, printing) -> + Array.iteri (fun i (partial, trigger, require, time_label, pass_name, printing) -> let j = i+numbering_base in Printf.fprintf oc " exists p%d; split. " j; (match trigger with @@ -134,7 +145,7 @@ let print_rtl_proof2 oc = all_passes;; let print_rtl_forward_simulations oc = - Array.iter (fun (partial, trigger, time_label, pass_name) -> + Array.iter (fun (partial, trigger, require, time_label, pass_name) -> output_string oc " eapply compose_forward_simulations.\n "; (match trigger with | Always -> () |