From 7698300cfe2d3f944ce2e1d4a60a263620487718 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 20 Dec 2013 13:05:53 +0000 Subject: Merge of branch value-analysis. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- driver/Clflags.ml | 1 + driver/Compiler.v | 9 ++++++++- driver/Driver.ml | 3 +++ 3 files changed, 12 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 4871222..442ca68 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 5d9e1a7..d088bc9 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 5f0ae7e..874f96b 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 .inlining.rtl -dconstprop Save RTL after constant propagation in .constprop.rtl -dcse Save RTL after CSE optimization in .cse.rtl + -ddeadcode Save RTL after dead code removal in .deadcode.rtl -dalloc Save LTL after register allocation in .alloc.ltl -dmach Save generated Mach code in .mach -dasm Save generated assembly in .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; -- cgit v1.2.3