Merge remote-tracking branch 'origin/mppa-profiling' into mppa-features

4 files changed, 48 insertions, 15 deletions

diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index ff2647a7..558e1d09 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -84,3 +84,6 @@ let option_fcoalesce_mem = ref true
 let option_fforward_moves = ref true
 let option_all_loads_nontrap = ref false
 let option_inline_auto_threshold = ref 0
+
+let option_profile_arcs = ref false
+let option_fbranch_probabilities = ref true
diff --git a/driver/Compiler.v b/driver/Compiler.v
index 3dbd35ce..ee091c37 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -37,6 +37,8 @@ Require Selection.
 Require RTLgen.
 Require Tailcall.
 Require Inlining.
+Require Profiling.
+Require ProfilingExploit.
 Require Renumber.
 Require Duplicate.
 Require Constprop.
@@ -63,6 +65,8 @@ Require Selectionproof.
 Require RTLgenproof.
 Require Tailcallproof.
 Require Inliningproof.
+Require Profilingproof.
+Require ProfilingExploitproof.
 Require Renumberproof.
 Require Duplicateproof.
 Require Constpropproof.
@@ -134,28 +138,32 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program :=
    @@ print (print_RTL 1)
   @@@ time "Inlining" Inlining.transf_program
    @@ print (print_RTL 2)
-   @@ time "Renumbering" Renumber.transf_program
+   @@ total_if Compopts.profile_arcs (time "Profiling insertion" Profiling.transf_program)
    @@ print (print_RTL 3)
-  @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program)
+   @@ total_if Compopts.branch_probabilities (time "Profiling use" ProfilingExploit.transf_program)
    @@ print (print_RTL 4)
-   @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program)
+   @@ time "Renumbering" Renumber.transf_program
    @@ print (print_RTL 5)
-   @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program)
+  @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program)
    @@ print (print_RTL 6)
-  @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program)
+   @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program)
    @@ print (print_RTL 7)
-   @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program)
+   @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program)
    @@ print (print_RTL 8)
-  @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program)
+  @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program)
    @@ print (print_RTL 9)
-   @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program
+   @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program)
    @@ print (print_RTL 10)
-  @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
+  @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program)
    @@ print (print_RTL 11)
-   @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program
+   @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program
    @@ print (print_RTL 12)
-  @@@ time "Unused globals" Unusedglob.transform_program
+  @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
    @@ print (print_RTL 13)
+   @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program
+   @@ print (print_RTL 14)
+  @@@ time "Unused globals" Unusedglob.transform_program
+   @@ print (print_RTL 15)
   @@@ time "Register allocation" Allocation.transf_program
    @@ print print_LTL
    @@ time "Branch tunneling" Tunneling.tunnel_program
@@ -257,6 +265,8 @@ Definition CompCert's_passes :=
   ::: mkpass RTLgenproof.match_prog
   ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog)
   ::: mkpass Inliningproof.match_prog
+  ::: mkpass (match_if Compopts.profile_arcs Profilingproof.match_prog)
+  ::: mkpass (match_if Compopts.branch_probabilities ProfilingExploitproof.match_prog)
   ::: mkpass Renumberproof.match_prog
   ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog)
   ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog)
@@ -305,7 +315,9 @@ Proof.
   unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T.
   set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *.
   destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate.
-  set (p9 := Renumber.transf_program p8) in *.
+  set (p8bis := total_if profile_arcs Profiling.transf_program p8) in *.
+  set (p8ter := total_if branch_probabilities ProfilingExploit.transf_program p8bis) in *.
+  set (p9 := Renumber.transf_program p8ter) in *.
   destruct (partial_if optim_duplicate Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate.
   set (p11 := total_if optim_constprop Constprop.transf_program p10) in *.
   set (p12 := total_if optim_constprop Renumber.transf_program p11) in *.
@@ -331,6 +343,8 @@ Proof.
   exists p6; split. apply RTLgenproof.transf_program_match; auto.
   exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match.
   exists p8; split. apply Inliningproof.transf_program_match; auto.
+  exists p8bis; split. apply total_if_match. apply Profilingproof.transf_program_match; auto.
+  exists p8ter; split. apply total_if_match. apply ProfilingExploitproof.transf_program_match; auto.
   exists p9; split. apply Renumberproof.transf_program_match; auto.
   exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto.
   exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match.
@@ -399,7 +413,7 @@ Ltac DestructM :=
       destruct H as (p & M & MM); clear H
   end.
   repeat DestructM. subst tp.
-  assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p26)).
+  assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p28)).
   {
   eapply compose_forward_simulations.
     eapply SimplExprproof.transl_program_correct; eassumption.
@@ -417,6 +431,10 @@ Ltac DestructM :=
     eapply match_if_simulation. eassumption. exact Tailcallproof.transf_program_correct.
   eapply compose_forward_simulations.
     eapply Inliningproof.transf_program_correct; eassumption.
+  eapply compose_forward_simulations.
+    eapply match_if_simulation. eassumption. exact Profilingproof.transf_program_correct.
+  eapply compose_forward_simulations.
+    eapply match_if_simulation. eassumption. exact ProfilingExploitproof.transf_program_correct.
   eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
     eapply match_if_simulation. eassumption. exact Duplicateproof.transf_program_correct.
diff --git a/driver/Compopts.v b/driver/Compopts.v
index a3181da8..1e10009d 100644
--- a/driver/Compopts.v
+++ b/driver/Compopts.v
@@ -81,6 +81,12 @@ Parameter all_loads_nontrap: unit -> bool.
 (** Flag -fforward-moves. Forward moves after CSE. *)
 Parameter optim_forward_moves: unit -> bool.
 
+(** Flag -fprofile-arcs. Add profiling logger. *)
+Parameter profile_arcs : unit -> bool.
+
+(** Flag -fbranch_probabilities. Use profiling information if available *)
+Parameter branch_probabilities : unit -> bool.
+
 (* TODO is there a more appropriate place? *)
 Require Import Coqlib.
 Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f.
diff --git a/driver/Driver.ml b/driver/Driver.ml
index b167dbd1..72715e65 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -224,7 +224,10 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>)
   -falign-functions <n>  Set alignment (in bytes) of function entry points
   -falign-branch-targets <n>  Set alignment (in bytes) of branch targets
   -falign-cond-branches <n>  Set alignment (in bytes) of conditional branches
-  -fcommon       Put uninitialized globals in the common section [on].
+  -fcommon       Put uninitialized globals in the common section [on]
+  -fprofile-arcs  Profile branches [off].
+  -fprofile-use= filename  Use profiling information in filename
+  -fbranch-probabilities Use profiling information (if available) for branches [on]
 |} ^
  target_help ^
  toolchain_help ^
@@ -329,6 +332,7 @@ let cmdline_actions =
   _Regexp "-O[123]$", Unit (set_all optimization_options);
   Exact "-Os", Set option_Osize;
   Exact "-Obranchless", Set option_Obranchless;
+  Exact "-fprofile-use=", String (fun s -> Profilingaux.load_profiling_info s);
   Exact "-finline-auto-threshold", Integer (fun n -> option_inline_auto_threshold := n);
   Exact "-fsmall-data", Integer(fun n -> option_small_data := n);
   Exact "-fsmall-const", Integer(fun n -> option_small_const := n);
@@ -416,7 +420,9 @@ let cmdline_actions =
   @ f_opt "coalesce-mem" option_fcoalesce_mem
   @ f_opt "all-loads-nontrap" option_all_loads_nontrap
   @ f_opt "forward-moves" option_fforward_moves
-(* Code generation options *)
+ (* Code generation options *)
+  @ f_opt "profile-arcs" option_profile_arcs
+  @ f_opt "branch-probabilities" option_fbranch_probabilities
   @ f_opt "fpu" option_ffpu
   @ f_opt "sse" option_ffpu (* backward compatibility *)
   @ [