Big merge of the newregalloc-int64 branch. Lots of changes in two directions:

1- new register allocator (+ live range splitting, spilling&reloading, etc)
   based on a posteriori validation using the Rideau-Leroy algorithm
2- support for 64-bit integer arithmetic (type "long long").


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

1 files changed, 9 insertions, 42 deletions

diff --git a/driver/Compiler.v b/driver/Compiler.v
index ea277ac..5d9e1a7 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -28,7 +28,6 @@ Require Cminor.
 Require CminorSel.
 Require RTL.
 Require LTL.
-Require LTLin.
 Require Linear.
 Require Mach.
 Require Asm.
@@ -49,16 +48,9 @@ Require Allocation.
 Require Tunneling.
 Require Linearize.
 Require CleanupLabels.
-Require Reload.
-Require RRE.
 Require Stacking.
 Require Asmgen.
-(** Type systems. *)
-Require RTLtyping.
-Require LTLtyping.
-Require LTLintyping.
-Require Lineartyping.
-(** Proofs of semantic preservation and typing preservation. *)
+(** Proofs of semantic preservation. *)
 Require SimplExprproof.
 Require SimplLocalsproof.
 Require Cshmgenproof.
@@ -71,17 +63,9 @@ Require Renumberproof.
 Require Constpropproof.
 Require CSEproof.
 Require Allocproof.
-Require Alloctyping.
 Require Tunnelingproof.
-Require Tunnelingtyping.
 Require Linearizeproof.
-Require Linearizetyping.
 Require CleanupLabelsproof.
-Require CleanupLabelstyping.
-Require Reloadproof.
-Require Reloadtyping.
-Require RREproof.
-Require RREtyping.
 Require Stackingproof.
 Require Asmgenproof.
 
@@ -93,7 +77,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_LTLin: LTLin.program -> unit.
+Parameter print_LTL: LTL.program -> unit.
 Parameter print_Mach: Mach.program -> unit.
 
 Open Local Scope string_scope.
@@ -137,12 +121,10 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program :=
   @@@ CSE.transf_program
    @@ print print_RTL_cse
   @@@ Allocation.transf_program
+   @@ print print_LTL
    @@ Tunneling.tunnel_program
   @@@ Linearize.transf_program
    @@ CleanupLabels.transf_program
-   @@ print print_LTLin
-   @@ Reload.transf_program
-   @@ RRE.transf_program
   @@@ Stacking.transf_program
    @@ print print_Mach
   @@@ Asmgen.transf_program.
@@ -150,7 +132,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program :=
 Definition transf_cminor_program (p: Cminor.program) : res Asm.program :=
    OK p
    @@ print print_Cminor
-   @@ Selection.sel_program
+  @@@ Selection.sel_program
   @@@ RTLgen.transl_program
   @@@ transf_rtl_program.
 
@@ -223,20 +205,7 @@ Proof.
   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 *.
-  set (p8 := Reload.transf_program p7) in *.
-  set (p9 := RRE.transf_program p8) in *.
-  destruct (Stacking.transf_program p9) as [p10|] eqn:?; simpl in H; try discriminate.
-
-  assert(TY1: LTLtyping.wt_program p5).
-    eapply Tunnelingtyping.program_typing_preserved. 
-    eapply Alloctyping.program_typing_preserved; eauto.
-  assert(TY2: LTLintyping.wt_program p7).
-    eapply CleanupLabelstyping.program_typing_preserved.
-    eapply Linearizetyping.program_typing_preserved; eauto.
-  assert(TY3: Lineartyping.wt_program p9).
-    eapply RREtyping.program_typing_preserved.
-    eapply Reloadtyping.program_typing_preserved; eauto.
-
+  destruct (Stacking.transf_program p7) as [p8|] eqn:?; simpl in H; try discriminate.
   eapply compose_forward_simulation. apply Tailcallproof.transf_program_correct. 
   eapply compose_forward_simulation. apply Inliningproof.transf_program_correct. eassumption.
   eapply compose_forward_simulation. apply Renumberproof.transf_program_correct. 
@@ -245,12 +214,10 @@ Proof.
   eapply compose_forward_simulation. apply CSEproof.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. eauto. 
+  eapply compose_forward_simulation. apply Linearizeproof.transf_program_correct. eassumption. 
   eapply compose_forward_simulation. apply CleanupLabelsproof.transf_program_correct. 
-  eapply compose_forward_simulation. apply Reloadproof.transf_program_correct. eauto.
-  eapply compose_forward_simulation. apply RREproof.transf_program_correct. eauto.
   eapply compose_forward_simulation. apply Stackingproof.transf_program_correct.
-    eexact Asmgenproof.return_address_exists. eassumption. eauto. 
+    eexact Asmgenproof.return_address_exists. eassumption.
   apply Asmgenproof.transf_program_correct; eauto.
   split. auto. 
   apply forward_to_backward_simulation. auto. 
@@ -269,9 +236,9 @@ Proof.
   unfold transf_cminor_program in H.
   repeat rewrite compose_print_identity in H.
   simpl in H. 
-  set (p1 := Selection.sel_program p) in *.
+  destruct (Selection.sel_program p) as [p1|] eqn:?; simpl in H; try discriminate.
   destruct (RTLgen.transl_program p1) as [p2|] eqn:?; simpl in H; try discriminate.
-  eapply compose_forward_simulation. apply Selectionproof.transf_program_correct.
+  eapply compose_forward_simulation. apply Selectionproof.transf_program_correct. eauto.
   eapply compose_forward_simulation. apply RTLgenproof.transf_program_correct. eassumption.
   exact (fst (transf_rtl_program_correct _ _ H)).