From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 20 Apr 2013 07:54:52 +0000 Subject: 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 --- driver/Clflags.ml | 1 + driver/Compiler.v | 51 +++++++++------------------------------------------ driver/Driver.ml | 5 ++++- driver/Interp.ml | 1 + 4 files changed, 15 insertions(+), 43 deletions(-) (limited to 'driver') 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 -- cgit v1.2.3