Merge of branch value-analysis.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

3 files changed, 12 insertions, 1 deletions

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 <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;