From c3f5f3dbd088091e3fab9f357b01693932d148f8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 17:02:45 +0200 Subject: reloading and exploiting seems to work --- Makefile | 1 + backend/ProfilingExploit.v | 30 ++++++++++++++++++++++++++++++ backend/Profilingaux.ml | 8 +++++++- driver/Clflags.ml | 1 + driver/Compiler.v | 33 +++++++++++++++++++++------------ driver/Compopts.v | 3 +++ driver/Driver.ml | 4 +++- extraction/extraction.v | 7 ++++++- 8 files changed, 72 insertions(+), 15 deletions(-) create mode 100644 backend/ProfilingExploit.v 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- to turn off -f) -falign-functions Set alignment (in bytes) of function entry points -falign-branch-targets Set alignment (in bytes) of branch targets -falign-cond-branches 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 => -- cgit