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

4 files changed, 15 insertions, 43 deletions

diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index a433c59..619be1e 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -37,6 +37,7 @@ let option_dinlining = ref false
 let option_dconstprop = ref false
 let option_dcse = ref false
 let option_dalloc = ref false
+let option_dalloctrace = ref false
 let option_dmach = ref false
 let option_dasm = ref false
 let option_sdump = ref false
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)).
 
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 3a5981e..eb0e004 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -89,6 +89,7 @@ let parse_c_file sourcename ifile =
   (* Simplification options *)
   let simplifs =
     "b" (* blocks: mandatory *)
+(*  ^ (if !option_flonglong then "l" else "") *)
   ^ (if !option_fstruct_return then "s" else "")
   ^ (if !option_fbitfields then "f" else "")
   ^ (if !option_fpacked_structs then "p" else "")
@@ -148,7 +149,8 @@ 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 PrintLTLin.destination option_dalloc ".alloc.ltl";
+  set_dest Regalloc.destination_alloctrace option_dalloctrace ".alloctrace";
+  set_dest PrintLTL.destination option_dalloc ".alloc.ltl";
   set_dest PrintMach.destination option_dmach ".mach";
   (* Convert to Asm *)
   let asm =
@@ -451,6 +453,7 @@ let cmdline_actions =
   "-dconstprop$", Set option_dconstprop;
   "-dcse$", Set option_dcse;
   "-dalloc$", Set option_dalloc;
+  "-dalloctrace$", Set option_dalloctrace;
   "-dmach$", Set option_dmach;
   "-dasm$", Set option_dasm;
   "-sdump$", Set option_sdump;
diff --git a/driver/Interp.ml b/driver/Interp.ml
index b7971ed..4f50514 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -49,6 +49,7 @@ let print_id_ofs p (id, ofs) =
 let print_eventval p = function
   | EVint n -> fprintf p "%ld" (camlint_of_coqint n)
   | EVfloat f -> fprintf p "%F" (camlfloat_of_coqfloat f)
+  | EVlong n -> fprintf p "%Ld" (camlint64_of_coqint n)
   | EVptr_global(id, ofs) -> fprintf p "&%a" print_id_ofs (id, ofs)
 
 let print_eventval_list p = function