diff options
-rw-r--r-- | Makefile | 2 | ||||
-rw-r--r-- | backend/Allocationproof.v (renamed from backend/Allocproof.v) | 0 | ||||
-rw-r--r-- | backend/Tunneling.v | 2 | ||||
-rw-r--r-- | backend/Tunnelingproof.v | 2 | ||||
-rw-r--r-- | driver/Compiler.vexpand | 119 | ||||
-rw-r--r-- | tools/compiler_expand.ml | 87 |
6 files changed, 90 insertions, 122 deletions
@@ -100,7 +100,7 @@ BACKEND=\ ForwardMoves.v ForwardMovesproof.v \ FirstNop.v FirstNopproof.v \ Allnontrap.v Allnontrapproof.v \ - Allocation.v Allocproof.v \ + Allocation.v Allocationproof.v \ Tunneling.v Tunnelingproof.v \ Linear.v Lineartyping.v \ Linearize.v Linearizeproof.v \ diff --git a/backend/Allocproof.v b/backend/Allocationproof.v index 3c7df58a..3c7df58a 100644 --- a/backend/Allocproof.v +++ b/backend/Allocationproof.v diff --git a/backend/Tunneling.v b/backend/Tunneling.v index a4c4a195..78458582 100644 --- a/backend/Tunneling.v +++ b/backend/Tunneling.v @@ -101,5 +101,5 @@ Definition tunnel_function (f: LTL.function) : LTL.function := Definition tunnel_fundef (f: LTL.fundef) : LTL.fundef := transf_fundef tunnel_function f. -Definition tunnel_program (p: LTL.program) : LTL.program := +Definition transf_program (p: LTL.program) : LTL.program := transform_program tunnel_fundef p. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index d3b8a9f0..cdf6c800 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -22,7 +22,7 @@ Definition match_prog (p tp: program) := match_program (fun ctx f tf => tf = tunnel_fundef f) eq p tp. Lemma transf_program_match: - forall p, match_prog p (tunnel_program p). + forall p, match_prog p (transf_program p). Proof. intros. eapply match_transform_program; eauto. Qed. diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index c044d9ef..17b504b7 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -36,12 +36,6 @@ Require Cminorgen. Require Selection. Require RTLgen. EXPAND_RTL_REQUIRE -Require Allocation. -Require Tunneling. -Require Linearize. -Require CleanupLabels. -Require Debugvar. -Require Stacking. Require Asmgen. (** Proofs of semantic preservation. *) Require SimplExprproof. @@ -51,12 +45,6 @@ Require Cminorgenproof. Require Selectionproof. Require RTLgenproof. EXPAND_RTL_REQUIRE_PROOF -Require Allocproof. -Require Tunnelingproof. -Require Linearizeproof. -Require CleanupLabelsproof. -Require Debugvarproof. -Require Stackingproof. Require Import Asmgenproof. (** Command-line flags. *) Require Import Compopts. @@ -109,16 +97,8 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := OK f @@ print (print_RTL 0) EXPAND_RTL_TRANSF_PROGRAM - @@@ time "Register allocation" Allocation.transf_program - @@ print print_LTL - @@ time "Branch tunneling" Tunneling.tunnel_program - @@@ time "CFG linearization" Linearize.transf_program - @@ time "Label cleanup" CleanupLabels.transf_program - @@@ partial_if Compopts.debug (time "Debugging info for local variables" Debugvar.transf_program) - @@@ time "Mach generation" Stacking.transf_program - @@ print print_Mach @@@ time "Total Mach->Asm generation" Asmgen.transf_program. - + Definition transf_cminor_program (p: Cminor.program) : res Asm.program := OK p @@ print print_Cminor @@ -209,12 +189,6 @@ Definition CompCert's_passes := ::: mkpass Selectionproof.match_prog ::: mkpass RTLgenproof.match_prog EXPAND_RTL_MKPASS - ::: mkpass Allocproof.match_prog - ::: mkpass Tunnelingproof.match_prog - ::: mkpass Linearizeproof.match_prog - ::: mkpass CleanupLabelsproof.match_prog - ::: mkpass (match_if Compopts.debug Debugvarproof.match_prog) - ::: mkpass Stackingproof.match_prog ::: mkpass Asmgenproof.match_prog ::: pass_nil _. @@ -244,30 +218,7 @@ Proof. destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T. - set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. - destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. - set (p8bis := total_if profile_arcs Profiling.transf_program p8) in *. - set (p8ter := total_if branch_probabilities ProfilingExploit.transf_program p8bis) in *. - set (p9 := total_if Compopts.optim_move_loop_invariants FirstNop.transf_program p8ter) in *. - set (p9bis := Renumber.transf_program p9) in *. - destruct (partial_if optim_duplicate Duplicate.transf_program p9bis) as [p10|e] eqn:P10; simpl in T; try discriminate. - set (p11 := Renumber.transf_program p10) in *. - set (p12 := total_if optim_constprop Constprop.transf_program p11) in *. - destruct (partial_if optim_move_loop_invariants LICM.transf_program p12) as [p12bis|e] eqn:P12bis; simpl in T; try discriminate. - set (p12ter :=(total_if optim_move_loop_invariants Renumber.transf_program p12bis)) in *. - destruct (partial_if optim_CSE CSE.transf_program p12ter) as [p13|e] eqn:P13; simpl in T; try discriminate. - set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *. - destruct (partial_if optim_CSE3 CSE3.transf_program p13bis) as [p13ter|e] eqn:P13ter; simpl in T; try discriminate. - set (p13quater := total_if optim_forward_moves ForwardMoves.transf_program p13ter) in *. - destruct (partial_if optim_redundancy Deadcode.transf_program p13quater) as [p14|e] eqn:P14; simpl in T; try discriminate. - set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. - destruct (Unusedglob.transf_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. - destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. - set (p17 := Tunneling.tunnel_program p16) in *. - destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate. - set (p19 := CleanupLabels.transf_program p18) in *. - destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. - destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; simpl in T; try discriminate. +EXPAND_RTL_PROOF unfold match_prog; simpl. exists p1; split. apply SimplExprproof.transf_program_match; auto. exists p2; split. apply SimplLocalsproof.match_transf_program; auto. @@ -275,30 +226,7 @@ Proof. exists p4; split. apply Cminorgenproof.transf_program_match; auto. exists p5; split. apply Selectionproof.transf_program_match; auto. exists p6; split. apply RTLgenproof.transf_program_match; auto. - exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. - exists p8; split. apply Inliningproof.transf_program_match; auto. - exists p8bis; split. apply total_if_match. apply Profilingproof.transf_program_match; auto. - exists p8ter; split. apply total_if_match. apply ProfilingExploitproof.transf_program_match; auto. - exists p9; split. apply total_if_match. apply FirstNopproof.transf_program_match. - exists p9bis; split. apply Renumberproof.transf_program_match. - exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto. - exists p11; split. apply Renumberproof.transf_program_match. - exists p12; split. apply total_if_match. apply Constpropproof.transf_program_match. - exists p12bis; split. eapply partial_if_match; eauto. apply LICMproof.transf_program_match. - exists p12ter; split. apply total_if_match; eauto. apply Renumberproof.transf_program_match. - exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. - exists p13bis; split. apply total_if_match. apply CSE2proof.transf_program_match. - exists p13ter; split. eapply partial_if_match; eauto. apply CSE3proof.transf_program_match. - exists p13quater; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match. - exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. - exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match. - exists p15; split. apply Unusedglobproof.transf_program_match; auto. - exists p16; split. apply Allocproof.transf_program_match; auto. - exists p17; split. apply Tunnelingproof.transf_program_match. - exists p18; split. apply Linearizeproof.transf_program_match; auto. - exists p19; split. apply CleanupLabelsproof.transf_program_match; auto. - exists p20; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. - exists p21; split. apply Stackingproof.transf_program_match; auto. +EXPAND_RTL_PROOF2 exists tp; split. apply Asmgenproof.transf_program_match; auto. reflexivity. Qed. @@ -350,7 +278,9 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p31)). + assert (F: forward_simulation (Cstrategy.semantics p) +EXPAND_ASM_SEMANTICS + ). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -364,42 +294,9 @@ Ltac DestructM := eapply Selectionproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply RTLgenproof.transf_program_correct; eassumption. +EXPAND_RTL_FORWARD_SIMULATIONS eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Tailcallproof.transf_program_correct. - eapply compose_forward_simulations. - eapply Inliningproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Profilingproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact ProfilingExploitproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact FirstNopproof.transf_program_correct. - eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Duplicateproof.transf_program_correct. - eapply compose_forward_simulations. - eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. - eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact LICMproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Renumberproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact CSEproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact CSE2proof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact CSE3proof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact ForwardMovesproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Allnontrapproof.transf_program_correct. - eapply compose_forward_simulations. - eapply Unusedglobproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply Allocproof.transf_program_correct; eassumption. + eapply Allocationproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Tunnelingproof.transf_program_correct; eassumption. eapply compose_forward_simulations. 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 |