diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | backend/CSE3.v | 27 | ||||
| -rw-r--r-- | backend/CSE3analysis.v | 39 | ||||
| -rw-r--r-- | backend/CSE3analysisaux.ml | 36 | ||||
| -rw-r--r-- | backend/CSE3analysisproof.v | 12 | ||||
| -rw-r--r-- | backend/CSE3proof.v | 138 | ||||
| -rw-r--r-- | driver/Clflags.ml | 1 | ||||
| -rw-r--r-- | driver/Compiler.v | 26 | ||||
| -rw-r--r-- | driver/Compopts.v | 3 | ||||
| -rw-r--r-- | extraction/extraction.v | 9 |
10 files changed, 270 insertions, 23 deletions
@@ -89,7 +89,7 @@ BACKEND=\ CSEdomain.v CombineOp.v CSE.v CombineOpproof.v CSEproof.v \ CSE2deps.v CSE2depsproof.v \ CSE2.v CSE2proof.v \ - CSE3analysis.v \ + CSE3analysis.v CSE3analysisproof.v CSE3.v CSE3proof.v \ NeedDomain.v NeedOp.v Deadcode.v Deadcodeproof.v \ Unusedglob.v Unusedglobproof.v \ Machregs.v Locations.v Conventions1.v Conventions.v LTL.v \ diff --git a/backend/CSE3.v b/backend/CSE3.v new file mode 100644 index 00000000..f4d75c51 --- /dev/null +++ b/backend/CSE3.v @@ -0,0 +1,27 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL Maps CSE2deps. +Require Import CSE3analysis HashedSet. + +Axiom preanalysis : RTL.function -> analysis_hints. + +Definition run f := preanalysis f. + +Definition transf_instr (fmap : analysis_hints) + (pc: node) (instr: instruction) := instr. + +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 (preanalysis 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. + +Definition match_prog (p tp: RTL.program) := + match_program (fun ctx f tf => tf = transf_fundef f) eq p tp. diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 966d3fd1..ded31270 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -122,13 +122,25 @@ Definition add_i_j (i : reg) (j : eq_id) (m : Regmap.t PSet.t) := Definition add_ilist_j (ilist : list reg) (j : eq_id) (m : Regmap.t PSet.t) := List.fold_left (fun already i => add_i_j i j already) ilist m. -Definition get_kills (eqs : PTree.t equation) : +Definition get_reg_kills (eqs : PTree.t equation) : Regmap.t PSet.t := PTree.fold (fun already (eqno : eq_id) (eq : equation) => add_i_j (eq_lhs eq) eqno (add_ilist_j (eq_args eq) eqno already)) eqs (PMap.init PSet.empty). +Definition eq_depends_on_mem eq := + match eq_op eq with + | SLoad _ _ => true + | SOp op => op_depends_on_memory op + end. + +Definition get_mem_kills (eqs : PTree.t equation) : PSet.t := + PTree.fold (fun already (eqno : eq_id) (eq : equation) => + if eq_depends_on_mem eq + then PSet.add eqno already + else already) eqs PSet.empty. + Definition is_move (op : operation) : { op = Omove } + { op <> Omove }. Proof. @@ -157,7 +169,7 @@ Record eq_context := mkeqcontext eq_find_oracle : node -> equation -> option eq_id; eq_rhs_oracle : node -> sym_op -> list reg -> PSet.t; eq_kill_reg : reg -> PSet.t; - eq_kill_mem : PSet.t; + eq_kill_mem : unit -> PSet.t; eq_moves : reg -> PSet.t }. Section OPERATIONS. @@ -167,7 +179,7 @@ Section OPERATIONS. PSet.subtract rel (eq_kill_reg ctx r). Definition kill_mem (rel : RELATION.t) : RELATION.t := - PSet.subtract rel (eq_kill_mem ctx). + PSet.subtract rel (eq_kill_mem ctx tt). Definition pick_source (l : list reg) := (* todo: take min? *) match l with @@ -279,10 +291,27 @@ Definition apply_instr' code (pc : node) (ro : RB.t) : RB.t := end end. -Definition forward_map (f : RTL.function) := DS.fixpoint +Definition internal_analysis (f : RTL.function) := DS.fixpoint (RTL.fn_code f) RTL.successors_instr (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top). End OPERATIONS. -Definition totoro := RELATION.lub. +Record analysis_hints := + mkanalysis_hints + { hint_eq_catalog : PTree.t equation; + hint_eq_find_oracle : node -> equation -> option eq_id; + hint_eq_rhs_oracle : node -> sym_op -> list reg -> PSet.t }. + +Definition analysis (eqs : PTree.t equation) (hints : analysis_hints) := + let reg_kills := get_reg_kills eqs in + let mem_kills := get_mem_kills eqs in + let moves := get_moves eqs in + internal_analysis (ctx := {| + eq_catalog := fun eq_id => PTree.get eq_id (hint_eq_catalog hints); + eq_find_oracle := hint_eq_find_oracle hints ; + eq_rhs_oracle := hint_eq_rhs_oracle hints; + eq_kill_reg := fun reg => PMap.get reg reg_kills; + eq_kill_mem := fun _ => mem_kills; + eq_moves := fun reg => PMap.get reg moves + |}). diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml new file mode 100644 index 00000000..26f19fd6 --- /dev/null +++ b/backend/CSE3analysisaux.ml @@ -0,0 +1,36 @@ +open CSE3analysis +open Maps +open HashedSet +open Camlcoq + +let flatten_eq eq = + ((P.to_int eq.eq_lhs), eq.eq_op, List.map P.to_int eq.eq_args);; + +let preanalysis (f : RTL.coq_function) = + let cur_eq_id = ref 0 + and cur_catalog = ref PTree.empty + and eq_table = Hashtbl.create 100 + and rhs_table = Hashtbl.create 100 + and cur_kill_reg = ref (PMap.init PSet.empty) + and cur_kill_mem = ref PSet.empty + and cur_moves = ref (PMap.init PSet.empty) in + let eq_find_oracle node eq = + Hashtbl.find_opt eq_table (flatten_eq eq) + and rhs_find_oracle node sop args = + match Hashtbl.find_opt rhs_table (sop, List.map P.to_int args) with + | None -> PSet.empty + | Some s -> s in + let mutating_eq_find_oracle node eq = + incr cur_eq_id; None in (* FIXME *) + ignore + (internal_analysis + { eq_catalog = (fun eq_id -> PTree.get eq_id !cur_catalog); + eq_find_oracle = mutating_eq_find_oracle; + eq_rhs_oracle = rhs_find_oracle ; + eq_kill_reg = (fun reg -> PMap.get reg !cur_kill_reg); + eq_kill_mem = (fun () -> !cur_kill_mem); + eq_moves = (fun reg -> PMap.get reg !cur_moves) + } f); + { hint_eq_catalog = !cur_catalog; + hint_eq_find_oracle= eq_find_oracle; + hint_eq_rhs_oracle = rhs_find_oracle };; diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index c0a9be48..f805d2b8 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -134,9 +134,9 @@ Lemma get_kills_has_lhs : PTree.get j eqs = Some {| eq_lhs := lhs; eq_op := sop; eq_args:= args |} -> - PSet.contains (Regmap.get lhs (get_kills eqs)) j = true. + PSet.contains (Regmap.get lhs (get_reg_kills eqs)) j = true. Proof. - unfold get_kills. + unfold get_reg_kills. intros. rewrite PTree.fold_spec. change (fold_left @@ -154,9 +154,9 @@ Lemma get_kills_has_arg : eq_op := sop; eq_args:= args |} -> In arg args -> - PSet.contains (Regmap.get arg (get_kills eqs)) j = true. + PSet.contains (Regmap.get arg (get_reg_kills eqs)) j = true. Proof. - unfold get_kills. + unfold get_reg_kills. intros. rewrite PTree.fold_spec. change (fold_left @@ -232,14 +232,14 @@ Section SOUNDNESS. eq_op := SOp op; eq_args:= args |} -> op_depends_on_memory op = true -> - PSet.contains (eq_kill_mem ctx) j = true. + PSet.contains (eq_kill_mem ctx tt) j = true. Hypothesis ctx_kill_mem_has_load : forall lhs chunk addr args j, eq_catalog ctx j = Some {| eq_lhs := lhs; eq_op := SLoad chunk addr; eq_args:= args |} -> - PSet.contains (eq_kill_mem ctx) j = true. + PSet.contains (eq_kill_mem ctx tt) j = true. Theorem kill_reg_sound : forall rel rs m dst v, diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v new file mode 100644 index 00000000..408b3cee --- /dev/null +++ b/backend/CSE3proof.v @@ -0,0 +1,138 @@ +(* +Replace available expressions by the register containing their value. + +Proofs. + +David Monniaux, CNRS, VERIMAG + *) + +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL Maps. + +Require Import Globalenvs Values. +Require Import Linking Values Memory Globalenvs Events Smallstep. +Require Import Registers Op RTL. +Require Import CSE3 CSE3analysis CSE3analysisproof. + + +Section SOUNDNESS. + Variable F V : Type. + Variable genv: Genv.t F V. + Variable sp : val. +End SOUNDNESS. + + +Definition match_prog (p tp: RTL.program) := + match_program (fun cu f tf => tf = transf_fundef f) eq p tp. + +Lemma transf_program_match: + forall p, match_prog p (transf_program p). +Proof. + intros. apply match_transform_program; auto. +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; trivial. +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. + +Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop := +| match_frames_intro: forall res f sp pc rs, + (* (forall m : mem, + forall vres, (fmap_sem' sp m (forward_map f) pc rs # res <- vres)) -> *) + 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'), + (* (fmap_sem' sp m (forward_map f) pc rs) -> *) + 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, RTL.step ge S1 t S2 -> + forall S1', match_states S1 S1' -> + exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'. +Proof. +Admitted. +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_step. + apply senv_preserved. + eexact transf_initial_states. + eexact transf_final_states. + exact step_simulation. +Qed. + +End PRESERVATION. diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 6d6f1df4..f4022941 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -27,6 +27,7 @@ let option_ftailcalls = ref true let option_fconstprop = ref true let option_fcse = ref true let option_fcse2 = ref true +let option_fcse3 = ref true let option_fredundancy = ref true let option_fduplicate = ref false let option_finvertcond = ref true (* only active if option_fduplicate is also true *) diff --git a/driver/Compiler.v b/driver/Compiler.v index a641587c..22955160 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -43,7 +43,7 @@ Require Constprop. Require CSE. Require ForwardMoves. Require CSE2. -Require CSE3analysis. +Require CSE3. Require Deadcode. Require Unusedglob. Require Allnontrap. @@ -69,6 +69,7 @@ Require Constpropproof. Require CSEproof. Require ForwardMovesproof. Require CSE2proof. +Require CSE3proof. Require Deadcodeproof. Require Unusedglobproof. Require Allnontrapproof. @@ -145,14 +146,16 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 7) @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) @@ print (print_RTL 8) - @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program + @@ total_if Compopts.optim_CSE3 (time "CSE3" CSE3.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 @@ -260,6 +263,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE2 CSE2proof.match_prog) + ::: mkpass (match_if Compopts.optim_CSE3 CSE3proof.match_prog) ::: mkpass (match_if Compopts.optim_forward_moves ForwardMovesproof.match_prog) ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog) @@ -307,8 +311,9 @@ Proof. set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *. - set (p13ter := total_if optim_forward_moves ForwardMoves.transf_program p13bis) in *. - destruct (partial_if optim_redundancy Deadcode.transf_program p13ter) as [p14|e] eqn:P14; simpl in T; try discriminate. + set (p13ter := total_if optim_CSE3 CSE3.transf_program p13bis) in *. + set (p13quater := total_if optim_forward_moves ForwardMoves.transf_program p13ter) in *. + destruct (partial_if optim_redundancy Deadcode.transf_program p13quater) as [p14|e] eqn:P14; simpl in T; try discriminate. set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. @@ -332,7 +337,8 @@ Proof. exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. exists p13bis; split. apply total_if_match. apply CSE2proof.transf_program_match. - exists p13ter; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match. + exists p13ter; split. apply total_if_match. apply CSE3proof.transf_program_match. + exists p13quater; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match. exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match. exists p15; split. apply Unusedglobproof.transf_program_match; auto. @@ -393,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. @@ -423,6 +429,8 @@ Ltac DestructM := eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact CSE2proof.transf_program_correct. eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact CSE3proof.transf_program_correct. + eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact ForwardMovesproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. diff --git a/driver/Compopts.v b/driver/Compopts.v index b4b9f30d..1f952164 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -43,6 +43,9 @@ Parameter optim_CSE: unit -> bool. (** Flag -fcse2. For DMonniaux's common subexpression elimination. *) Parameter optim_CSE2: unit -> bool. +(** Flag -fcse3. For DMonniaux's common subexpression elimination. *) +Parameter optim_CSE3: unit -> bool. + (** Flag -fredundancy. For dead code elimination. *) Parameter optim_redundancy: unit -> bool. diff --git a/extraction/extraction.v b/extraction/extraction.v index ea30e7c2..61c7c746 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -36,7 +36,8 @@ Require Parser. Require Initializers. Require Asmaux. -Require CSE3analysis. (* FIXME *) +Require CSE3. +Require CSE3analysis. (* Standard lib *) Require Import ExtrOcamlBasic. @@ -115,6 +116,8 @@ Extract Constant Compopts.optim_CSE => "fun _ -> !Clflags.option_fcse". Extract Constant Compopts.optim_CSE2 => "fun _ -> !Clflags.option_fcse2". +Extract Constant Compopts.optim_CSE3 => + "fun _ -> !Clflags.option_fcse3". Extract Constant Compopts.optim_redundancy => "fun _ -> !Clflags.option_fredundancy". Extract Constant Compopts.optim_postpass => @@ -162,6 +165,8 @@ Extract Constant Cabs.loc => Extract Inlined Constant Cabs.string => "String.t". Extract Constant Cabs.char_code => "int64". +Extract Inlined Constant CSE3.preanalysis => "CSE3analysisaux.preanalysis". + Extract Inductive HashedSet.PSet_internals.pset => "HashedSetaux.pset" [ "HashedSetaux.empty" "HashedSetaux.node" ] "HashedSetaux.pset_match". Extract Inlined Constant HashedSet.PSet_internals.pset_eq => "(==)" (* "HashedSetaux.eq" *). @@ -188,7 +193,7 @@ Set Extraction AccessOpaque. Cd "extraction". Separate Extraction - CSE3analysis.totoro (* FIXME *) + CSE3analysis.internal_analysis CSE3.run Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env |