diff options
| -rw-r--r-- | backend/Profiling.v | 23 | ||||
| -rw-r--r-- | backend/Profilingaux.ml | 8 | ||||
| -rw-r--r-- | backend/Profilingproof.v | 227 | ||||
| -rw-r--r-- | driver/Compiler.v | 33 | ||||
| -rw-r--r-- | extraction/extraction.v | 7 |
5 files changed, 273 insertions, 25 deletions
diff --git a/backend/Profiling.v b/backend/Profiling.v index 4995c507..1840af6e 100644 --- a/backend/Profiling.v +++ b/backend/Profiling.v @@ -4,7 +4,7 @@ Require Import Memory Registers Op RTL. Local Open Scope positive. -Parameter fundef_id : fundef -> Z. +Parameter function_id : function -> Z. Parameter branch_id : Z -> node -> Z. Section PER_FUNCTION_ID. @@ -47,20 +47,19 @@ Section PER_FUNCTION_ID. | Icond cond args ifso ifnot expected => true | _ => false end) prog)). - - Definition transf_function (f : function) : function := - let max_pc := max_pc_function f in - let conditions := gen_conditions (fn_code f) in - {| fn_sig := f.(fn_sig); - fn_params := f.(fn_params); - fn_stacksize := f.(fn_stacksize); - fn_code := snd (inject_l (fn_code f) (Pos.succ max_pc) conditions); - fn_entrypoint := f.(fn_entrypoint) |}. - End PER_FUNCTION_ID. +Definition transf_function (f : function) : function := + let max_pc := max_pc_function f in + let conditions := gen_conditions (fn_code f) in + {| fn_sig := f.(fn_sig); + fn_params := f.(fn_params); + fn_stacksize := f.(fn_stacksize); + fn_code := snd (inject_l (function_id f) (fn_code f) (Pos.succ max_pc) conditions); + fn_entrypoint := f.(fn_entrypoint) |}. + Definition transf_fundef (fd: fundef) : fundef := - AST.transf_fundef (transf_function (fundef_id fd)) fd. + 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 new file mode 100644 index 00000000..ad963a48 --- /dev/null +++ b/backend/Profilingaux.ml @@ -0,0 +1,8 @@ +open Camlcoq +open RTL + +let function_id (f : coq_function) : Z.t = + Z.of_uint 0;; + +let branch_id (f_id : Z.t) (node : P.t) = + Z.of_uint 0;; diff --git a/backend/Profilingproof.v b/backend/Profilingproof.v new file mode 100644 index 00000000..0e6171d6 --- /dev/null +++ b/backend/Profilingproof.v @@ -0,0 +1,227 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Values Memory Globalenvs Events Smallstep. +Require Import Registers Op RTL. +Require Import Profiling. +Require Import Lia. + +Definition match_prog (p tp: RTL.program) := + match_program (fun ctx f tf => tf = transf_fundef f) eq p tp. + +Lemma transf_program_match: + forall p, match_prog p (transf_program p). +Proof. + intros. eapply match_transform_program; eauto. +Qed. + +Section PRESERVATION. + +Variables prog tprog: program. +Hypothesis TRANSL: match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Lemma functions_translated: + forall v f, + Genv.find_funct ge v = Some f -> + Genv.find_funct tge v = Some (transf_fundef f). +Proof (Genv.find_funct_transf TRANSL). + +Lemma function_ptr_translated: + forall v f, + Genv.find_funct_ptr ge v = Some f -> + Genv.find_funct_ptr tge v = Some (transf_fundef f). +Proof (Genv.find_funct_ptr_transf TRANSL). + +Lemma symbols_preserved: + forall id, + Genv.find_symbol tge id = Genv.find_symbol ge id. +Proof (Genv.find_symbol_transf TRANSL). + +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_transf TRANSL). + +Lemma sig_preserved: + forall f, funsig (transf_fundef f) = funsig f. +Proof. + destruct f; reflexivity. +Qed. + +Lemma find_function_translated: + forall ros rs fd, + find_function ge ros rs = Some fd -> + find_function tge ros rs = Some (transf_fundef fd). +Proof. + unfold find_function; intros. destruct ros as [r|id]. + eapply functions_translated; eauto. + rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try congruence. + eapply function_ptr_translated; eauto. +Qed. + +(* +Lemma transf_function_at: + forall hash f pc i, + f.(fn_code)!pc = Some i -> + (match i with + | Icond _ _ _ _ _ => False + | _ => True) -> + (transf_function hash f).(fn_code)!pc = Some i. +Proof. + intros until i. intro Hcode. + unfold transf_function; simpl. + destruct (peq pc (Pos.succ (max_pc_function f))) as [EQ | NEQ]. + { assert (pc <= (max_pc_function f))%positive as LE by (eapply max_pc_function_sound; eassumption). + subst pc. + lia. + } + rewrite PTree.gso by congruence. + assumption. +Qed. + *) + + +Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop := +| match_frames_intro: forall res f sp pc rs, + match_frames (Stackframe res f sp pc rs) + (Stackframe res (transf_function f) sp pc rs). + +Inductive match_states: RTL.state -> RTL.state -> Prop := + | match_regular_states: forall stk f sp pc rs m stk' + (STACKS: list_forall2 match_frames stk stk'), + match_states (State stk f sp pc rs m) + (State stk' (transf_function f) sp pc rs m) + | match_callstates: forall stk f args m stk' + (STACKS: list_forall2 match_frames stk stk'), + match_states (Callstate stk f args m) + (Callstate stk' (transf_fundef f) args m) + | match_returnstates: forall stk v m stk' + (STACKS: list_forall2 match_frames stk stk'), + match_states (Returnstate stk v m) + (Returnstate stk' v m). + + +Lemma step_simulation: + forall s1 t s2 (STEP : step ge s1 t s2) + s1' (MS: match_states s1 s1'), + exists s2', plus step tge s1' t s2' /\ match_states s2 s2'. +Proof. + induction 1; intros; inv MS. +Admitted. + +(* + - left. econstructor. split. + + eapply plus_one. eapply exec_Inop; eauto with firstnop. + + constructor; auto with firstnop. + - left. econstructor. split. + + eapply plus_one. eapply exec_Iop with (v:=v); eauto with firstnop. + rewrite <- H0. + apply eval_operation_preserved. + apply symbols_preserved. + + constructor; auto with firstnop. + - left. econstructor. split. + + eapply plus_one. eapply exec_Iload with (v:=v); eauto with firstnop. + all: rewrite <- H0. + all: auto using eval_addressing_preserved, symbols_preserved. + + constructor; auto with firstnop. + - left. econstructor. split. + + eapply plus_one. eapply exec_Iload_notrap1; eauto with firstnop. + all: rewrite <- H0; + apply eval_addressing_preserved; + apply symbols_preserved. + + constructor; auto with firstnop. + - left. econstructor. split. + + eapply plus_one. eapply exec_Iload_notrap2; eauto with firstnop. + all: rewrite <- H0; + apply eval_addressing_preserved; + apply symbols_preserved. + + constructor; auto with firstnop. + - left. econstructor. split. + + eapply plus_one. eapply exec_Istore; eauto with firstnop. + all: rewrite <- H0; + apply eval_addressing_preserved; + apply symbols_preserved. + + constructor; auto with firstnop. + - left. econstructor. split. + + eapply plus_one. eapply exec_Icall. + apply match_pc_same. exact H. + apply find_function_translated. + exact H0. + apply sig_preserved. + + constructor. + constructor; auto. + constructor. + - left. econstructor. split. + + eapply plus_one. eapply exec_Itailcall. + apply match_pc_same. exact H. + apply find_function_translated. + exact H0. + apply sig_preserved. + unfold transf_function; simpl. + eassumption. + + constructor; auto. + - left. econstructor. split. + + eapply plus_one. eapply exec_Ibuiltin; eauto with firstnop. + eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + + constructor; auto. + - left. econstructor. split. + + eapply plus_one. eapply exec_Icond; eauto with firstnop. + + constructor; auto. + - left. econstructor. split. + + eapply plus_one. eapply exec_Ijumptable; eauto with firstnop. + + constructor; auto. + - left. econstructor. split. + + eapply plus_one. eapply exec_Ireturn; eauto with firstnop. + + constructor; auto. + - left. econstructor. split. + + eapply plus_two. + * eapply exec_function_internal; eauto with firstnop. + * eapply exec_Inop. + unfold transf_function; simpl. + rewrite PTree.gss. + reflexivity. + * auto. + + constructor; auto. + - left. econstructor. split. + + eapply plus_one. eapply exec_function_external; eauto with firstnop. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + + constructor; auto. + - left. + inv STACKS. inv H1. + econstructor; split. + + eapply plus_one. eapply exec_return; eauto. + + constructor; auto. +Qed. + *) + +Lemma transf_initial_states: + forall S1, RTL.initial_state prog S1 -> + exists S2, RTL.initial_state tprog S2 /\ match_states S1 S2. +Proof. + intros. inv H. econstructor; split. + econstructor. + eapply (Genv.init_mem_transf TRANSL); eauto. + rewrite symbols_preserved. rewrite (match_program_main TRANSL). eauto. + eapply function_ptr_translated; eauto. + rewrite <- H3; apply sig_preserved. + constructor. constructor. +Qed. + +Lemma transf_final_states: + forall S1 S2 r, match_states S1 S2 -> RTL.final_state S1 r -> RTL.final_state S2 r. +Proof. + intros. inv H0. inv H. inv STACKS. constructor. +Qed. + +Theorem transf_program_correct: + forward_simulation (RTL.semantics prog) (RTL.semantics tprog). +Proof. + eapply forward_simulation_plus. + apply senv_preserved. + eexact transf_initial_states. + eexact transf_final_states. + exact step_simulation. +Qed. + +End PRESERVATION. diff --git a/driver/Compiler.v b/driver/Compiler.v index 499feff2..dc32cd3f 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -37,6 +37,7 @@ Require Selection. Require RTLgen. Require Tailcall. Require Inlining. +Require Profiling. Require Renumber. Require Duplicate. Require Constprop. @@ -62,6 +63,7 @@ Require Selectionproof. Require RTLgenproof. Require Tailcallproof. Require Inliningproof. +Require Profilingproof. Require Renumberproof. Require Duplicateproof. Require Constpropproof. @@ -132,26 +134,28 @@ 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) + @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 4) - @@ 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 5) - @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) + @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 6) - @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) + @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) @@ print (print_RTL 7) - @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) + @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 8) - @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program + @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) @@ print (print_RTL 9) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program @@ print (print_RTL 10) - @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 11) - @@@ time "Unused globals" Unusedglob.transform_program + @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program @@ print (print_RTL 12) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 13) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -253,6 +257,7 @@ 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 Renumberproof.match_prog ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) @@ -300,7 +305,8 @@ 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 (p9 := Renumber.transf_program p8bis) 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 *. @@ -325,6 +331,7 @@ 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 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. @@ -392,7 +399,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 p25)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p26)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -410,6 +417,8 @@ 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 Renumberproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Duplicateproof.transf_program_correct. diff --git a/extraction/extraction.v b/extraction/extraction.v index 9b568951..c2b5d83e 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -137,6 +137,8 @@ Extract Constant Compopts.va_strict => "fun _ -> false". Extract Constant Compopts.all_loads_nontrap => "fun _ -> !Clflags.option_all_loads_nontrap". +Extract Constant Compopts.profile_arcs => + "fun _ -> !Clflags.option_profile_arcs". (* Compiler *) Extract Constant Compiler.print_Clight => "PrintClight.print_if". @@ -147,9 +149,12 @@ Extract Constant Compiler.print_Mach => "PrintMach.print_if". Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x". Extract Constant Compiler.time => "Timing.time_coq". Extract Constant Compopts.time => "Timing.time_coq". - (*Extraction Inline Compiler.apply_total Compiler.apply_partial.*) +(* Profiling *) +Extract Constant Profiling.function_id => "Profilingaux.function_id". +Extract Constant Profiling.branch_id => "Profilingaux.branch_id". + (* Cabs *) Extract Constant Cabs.loc => "{ lineno : int; |