diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-12-20 13:05:53 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-12-20 13:05:53 +0000 |
commit | 7698300cfe2d3f944ce2e1d4a60a263620487718 (patch) | |
tree | 74292bb5f65bc797906b5c768df2e2e937e869b6 /driver | |
parent | c511207bd0f25c4199770233175924a725526bd3 (diff) | |
download | compcert-7698300cfe2d3f944ce2e1d4a60a263620487718.tar.gz compcert-7698300cfe2d3f944ce2e1d4a60a263620487718.zip |
Merge of branch value-analysis.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'driver')
-rw-r--r-- | driver/Clflags.ml | 1 | ||||
-rw-r--r-- | driver/Compiler.v | 9 | ||||
-rw-r--r-- | driver/Driver.ml | 3 |
3 files changed, 12 insertions, 1 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 4871222e..442ca68a 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -36,6 +36,7 @@ let option_dtailcall = ref false let option_dinlining = ref false let option_dconstprop = ref false let option_dcse = ref false +let option_ddeadcode = ref false let option_dalloc = ref false let option_dalloctrace = ref false let option_dmach = ref false diff --git a/driver/Compiler.v b/driver/Compiler.v index 5d9e1a71..d088bc94 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -44,6 +44,7 @@ Require Inlining. Require Renumber. Require Constprop. Require CSE. +Require Deadcode. Require Allocation. Require Tunneling. Require Linearize. @@ -62,6 +63,7 @@ Require Inliningproof. Require Renumberproof. Require Constpropproof. Require CSEproof. +Require Deadcodeproof. Require Allocproof. Require Tunnelingproof. Require Linearizeproof. @@ -77,6 +79,7 @@ Parameter print_RTL_tailcall: RTL.program -> unit. Parameter print_RTL_inline: RTL.program -> unit. Parameter print_RTL_constprop: RTL.program -> unit. Parameter print_RTL_cse: RTL.program -> unit. +Parameter print_RTL_deadcode: RTL.program -> unit. Parameter print_LTL: LTL.program -> unit. Parameter print_Mach: Mach.program -> unit. @@ -120,6 +123,8 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print print_RTL_constprop @@@ CSE.transf_program @@ print print_RTL_cse + @@@ Deadcode.transf_program + @@ print print_RTL_deadcode @@@ Allocation.transf_program @@ print print_LTL @@ Tunneling.tunnel_program @@ -201,7 +206,8 @@ Proof. set (p2 := Constprop.transf_program p12) in *. set (p21 := Renumber.transf_program p2) in *. destruct (CSE.transf_program p21) as [p3|] eqn:?; simpl in H; try discriminate. - destruct (Allocation.transf_program p3) as [p4|] eqn:?; simpl in H; try discriminate. + destruct (Deadcode.transf_program p3) as [p31|] eqn:?; simpl in H; try discriminate. + destruct (Allocation.transf_program p31) as [p4|] eqn:?; simpl in H; try discriminate. set (p5 := Tunneling.tunnel_program p4) in *. destruct (Linearize.transf_program p5) as [p6|] eqn:?; simpl in H; try discriminate. set (p7 := CleanupLabels.transf_program p6) in *. @@ -212,6 +218,7 @@ Proof. eapply compose_forward_simulation. apply Constpropproof.transf_program_correct. eapply compose_forward_simulation. apply Renumberproof.transf_program_correct. eapply compose_forward_simulation. apply CSEproof.transf_program_correct. eassumption. + eapply compose_forward_simulation. apply Deadcodeproof.transf_program_correct. eassumption. eapply compose_forward_simulation. apply Allocproof.transf_program_correct. eassumption. eapply compose_forward_simulation. apply Tunnelingproof.transf_program_correct. eapply compose_forward_simulation. apply Linearizeproof.transf_program_correct. eassumption. diff --git a/driver/Driver.ml b/driver/Driver.ml index 5f0ae7e8..874f96b8 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -149,6 +149,7 @@ let compile_c_ast sourcename csyntax ofile = set_dest PrintRTL.destination_inlining option_dinlining ".inlining.rtl"; set_dest PrintRTL.destination_constprop option_dconstprop ".constprop.rtl"; set_dest PrintRTL.destination_cse option_dcse ".cse.rtl"; + set_dest PrintRTL.destination_deadcode option_ddeadcode ".deadcode.rtl"; set_dest Regalloc.destination_alloctrace option_dalloctrace ".alloctrace"; set_dest PrintLTL.destination option_dalloc ".alloc.ltl"; set_dest PrintMach.destination option_dmach ".mach"; @@ -413,6 +414,7 @@ Tracing options: -dinlining Save RTL after inlining optimization in <file>.inlining.rtl -dconstprop Save RTL after constant propagation in <file>.constprop.rtl -dcse Save RTL after CSE optimization in <file>.cse.rtl + -ddeadcode Save RTL after dead code removal in <file>.deadcode.rtl -dalloc Save LTL after register allocation in <file>.alloc.ltl -dmach Save generated Mach code in <file>.mach -dasm Save generated assembly in <file>.s @@ -460,6 +462,7 @@ let cmdline_actions = "-dinlining$", Set option_dinlining; "-dconstprop$", Set option_dconstprop; "-dcse$", Set option_dcse; + "-ddeadcode$", Set option_ddeadcode; "-dalloc$", Set option_dalloc; "-dalloctrace$", Set option_dalloctrace; "-dmach$", Set option_dmach; |