reloading and exploiting seems to work

8 files changed, 72 insertions, 15 deletions

diff --git a/Makefile b/Makefile
index cad61d9d..5acaee19 100644
--- a/Makefile
+++ b/Makefile
@@ -80,6 +80,7 @@ BACKEND=\
   Tailcall.v Tailcallproof.v \
   Inlining.v Inliningspec.v Inliningproof.v \
   Profiling.v Profilingproof.v \
+  ProfilingExploit.v ProfilingExploitproof.v \
   Renumber.v Renumberproof.v \
   Duplicate.v Duplicateproof.v \
   RTLtyping.v \
diff --git a/backend/ProfilingExploit.v b/backend/ProfilingExploit.v
new file mode 100644
index 00000000..cfca1a12
--- /dev/null
+++ b/backend/ProfilingExploit.v
@@ -0,0 +1,30 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL.
+
+Local Open Scope positive.
+
+Parameter function_id : function -> AST.profiling_id.
+Parameter branch_id : AST.profiling_id -> node -> AST.profiling_id.
+Parameter condition_oracle : AST.profiling_id -> option bool.
+
+Definition transf_instr (f_id : AST.profiling_id)
+           (pc : node) (i : instruction) : instruction :=
+  match i with
+  | Icond cond args ifso ifnot None =>
+    Icond cond args ifso ifnot (condition_oracle (branch_id f_id pc))
+  | _ => i
+  end.
+
+Definition transf_function (f : function) : function :=
+  {| fn_sig := f.(fn_sig);
+     fn_params := f.(fn_params);
+     fn_stacksize := f.(fn_stacksize);
+     fn_code := PTree.map (transf_instr (function_id f)) f.(fn_code);
+     fn_entrypoint := f.(fn_entrypoint) |}.
+
+Definition transf_fundef (fd: fundef) : fundef :=
+  AST.transf_fundef transf_function fd.
+
+Definition transf_program (p: program) : program :=
+  transform_program transf_fundef p.
diff --git a/backend/Profilingaux.ml b/backend/Profilingaux.ml
index 0644e843..51718303 100644
--- a/backend/Profilingaux.ml
+++ b/backend/Profilingaux.ml
@@ -48,7 +48,13 @@ let load_profiling_info (filename : string) : unit =
       let id : identifier = really_input_string ic 16 in
       let counter0 = input_counter ic in
       let counter1 = input_counter ic in
-      Printf.fprintf stderr "%a : %Ld %Ld\n" pp_id id counter0 counter1; 
+      (* Printf.fprintf stderr "%a : %Ld %Ld\n" pp_id id counter0 counter1; *)
       add_profiling_counts id counter0 counter1
     done
   with End_of_file -> close_in ic;;
+
+let condition_oracle (id : identifier) : bool option =
+  let (count0, count1) = get_counts id in
+  Printf.fprintf stderr "%a : %Ld %Ld\n" pp_id id count0 count1;
+  if count0 = count1 then None
+  else Some(count1 > count0);;
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 600c3371..e8f7cef2 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -84,3 +84,4 @@ 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 dc32cd3f..3f0ac3e5 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -38,6 +38,7 @@ Require RTLgen.
 Require Tailcall.
 Require Inlining.
 Require Profiling.
+Require ProfilingExploit.
 Require Renumber.
 Require Duplicate.
 Require Constprop.
@@ -64,6 +65,7 @@ Require RTLgenproof.
 Require Tailcallproof.
 Require Inliningproof.
 Require Profilingproof.
+Require ProfilingExploitproof.
 Require Renumberproof.
 Require Duplicateproof.
 Require Constpropproof.
@@ -136,26 +138,28 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program :=
    @@ print (print_RTL 2)
    @@ total_if Compopts.profile_arcs (time "Profiling insertion" Profiling.transf_program)
    @@ print (print_RTL 3)
-   @@ time "Renumbering" Renumber.transf_program
+   @@ total_if Compopts.branch_probabilities (time "Profiling use" ProfilingExploit.transf_program)
    @@ print (print_RTL 4)
-  @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program)
+   @@ time "Renumbering" Renumber.transf_program
    @@ print (print_RTL 5)
-   @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program)
+  @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program)
    @@ print (print_RTL 6)
-   @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program)
+   @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program)
    @@ print (print_RTL 7)
-  @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program)
+   @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program)
    @@ print (print_RTL 8)
-   @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.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)
+   @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program
    @@ print (print_RTL 11)
-   @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program
+  @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
    @@ print (print_RTL 12)
-  @@@ time "Unused globals" Unusedglob.transform_program
+   @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program
    @@ print (print_RTL 13)
+  @@@ time "Unused globals" Unusedglob.transform_program
+   @@ print (print_RTL 14)
   @@@ time "Register allocation" Allocation.transf_program
    @@ print print_LTL
    @@ time "Branch tunneling" Tunneling.tunnel_program
@@ -258,6 +262,7 @@ Definition CompCert's_passes :=
   ::: 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)
@@ -306,7 +311,8 @@ Proof.
   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 (p8bis := total_if profile_arcs Profiling.transf_program p8) in *.
-  set (p9 := Renumber.transf_program p8bis) 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 *.
@@ -332,6 +338,7 @@ Proof.
   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 +406,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 p27)).
   {
   eapply compose_forward_simulations.
     eapply SimplExprproof.transl_program_correct; eassumption.
@@ -419,6 +426,8 @@ Ltac DestructM :=
     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 245322ef..98cbcc37 100644
--- a/driver/Compopts.v
+++ b/driver/Compopts.v
@@ -78,6 +78,9 @@ 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 7fbcb025..29fbaa7c 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -222,8 +222,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 ^
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 72c19385..eb811f6c 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -138,7 +138,9 @@ Extract Constant Compopts.va_strict =>
 Extract Constant Compopts.all_loads_nontrap =>
   "fun _ -> !Clflags.option_all_loads_nontrap".
 Extract Constant Compopts.profile_arcs =>
-  "fun _ -> !Clflags.option_profile_arcs".
+"fun _ -> !Clflags.option_profile_arcs".
+Extract Constant Compopts.branch_probabilities =>
+  "fun _ -> !Clflags.option_fbranch_probabilities".
 
 (* Compiler *)
 Extract Constant Compiler.print_Clight => "PrintClight.print_if".
@@ -156,6 +158,9 @@ Extract Constant AST.profiling_id => "Digest.t".
 Extract Constant AST.profiling_id_eq => "Digest.equal".
 Extract Constant Profiling.function_id => "Profilingaux.function_id".
 Extract Constant Profiling.branch_id => "Profilingaux.branch_id".
+Extract Constant ProfilingExploit.function_id => "Profilingaux.function_id".
+Extract Constant ProfilingExploit.branch_id => "Profilingaux.branch_id".
+Extract Constant ProfilingExploit.condition_oracle => "Profilingaux.condition_oracle".
 
 (* Cabs *)
 Extract Constant Cabs.loc =>