From bbe0809b3cd483ce5fc82e4f2d0a106823c54f26 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 14 Mar 2020 09:19:26 +0100 Subject: CSE3 alias analysis --- backend/CSE3.v | 2 +- backend/CSE3analysis.v | 25 +++++++++++++++++++++++-- backend/CSE3analysisproof.v | 39 ++++++++++++++++++++++++++++++++++++++- driver/Clflags.ml | 5 +++-- driver/Compopts.v | 3 +++ driver/Driver.ml | 6 ++++-- extraction/extraction.v | 2 ++ 7 files changed, 74 insertions(+), 8 deletions(-) diff --git a/backend/CSE3.v b/backend/CSE3.v index 161a394a..d0dc3aef 100644 --- a/backend/CSE3.v +++ b/backend/CSE3.v @@ -46,7 +46,7 @@ Definition transf_instr (fmap : PMap.t RB.t) match instr with | Iop op args dst s => let args' := subst_args fmap pc args in - match find_op_in_fmap fmap pc op args' with + match (if is_trivial_op op then None else find_op_in_fmap fmap pc op args') with | None => Iop op args' dst s | Some src => Iop Omove (src::nil) dst s end diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 76723f40..12fb2d1f 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -2,7 +2,7 @@ Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Memory Registers Op RTL Maps CSE2deps. Require Import HashedSet. -Require List. +Require List Compopts. Definition typing_env := reg -> typ. @@ -278,10 +278,31 @@ Section OPERATIONS. | None => oper1 dst op args rel end. + Definition clever_kill_store + (chunk : memory_chunk) (addr: addressing) (args : list reg) + (src : reg) + (rel : RELATION.t) : RELATION.t := + PSet.subtract rel + (PSet.filter + (fun eqno => + match eq_catalog ctx eqno with + | None => false + | Some eq => + match eq_op eq with + | SOp op => true + | SLoad chunk' addr' => + may_overlap chunk addr args chunk' addr' (eq_args eq) + end + end) + (PSet.inter rel (eq_kill_mem ctx tt))). + Definition store2 (chunk : memory_chunk) (addr: addressing) (args : list reg) (src : reg) - (rel : RELATION.t) : RELATION.t := kill_mem rel. + (rel : RELATION.t) : RELATION.t := + if Compopts.optim_CSE3_alias_analysis tt + then clever_kill_store chunk addr args src rel + else kill_mem rel. Definition store1 (chunk : memory_chunk) (addr: addressing) (args : list reg) diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 7ddbaed8..b87ec92c 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -765,6 +765,43 @@ Section SOUNDNESS. Hint Resolve oper_sound : cse3. + + Theorem clever_kill_store_sound: + forall chunk addr args a src rel rs m m', + sem_rel rel rs m -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.storev chunk m a (rs # src) = Some m' -> + sem_rel (clever_kill_store (ctx:=ctx) chunk addr args src rel) rs m'. + Proof. + unfold clever_kill_store. + intros until m'. intros REL ADDR STORE i eq CONTAINS CATALOG. + autorewrite with pset in CONTAINS. + destruct (PSet.contains rel i) eqn:RELi; simpl in CONTAINS. + 2: discriminate. + rewrite CATALOG in CONTAINS. + unfold sem_rel in REL. + specialize REL with (i := i) (eq0 := eq). + destruct eq; simpl in *. + unfold sem_eq in *. + simpl in *. + destruct eq_op as [op' | chunk' addr']; simpl. + - destruct (op_depends_on_memory op') eqn:DEPENDS. + + erewrite ctx_kill_mem_has_depends_on_mem in CONTAINS by eauto. + discriminate. + + rewrite op_depends_on_memory_correct with (m2:=m); trivial. + apply REL; auto. + - simpl in REL. + erewrite ctx_kill_mem_has_depends_on_mem in CONTAINS by eauto. + simpl in CONTAINS. + rewrite negb_true_iff in CONTAINS. + destruct (eval_addressing genv sp addr' rs ## eq_args) as [a'|] eqn:ADDR'. + + erewrite may_overlap_sound with (chunk:=chunk) (addr:=addr) (args:=args) (chunk':=chunk') (addr':=addr') (args':=eq_args); try eassumption. + apply REL; auto. + + apply REL; auto. + Qed. + + Hint Resolve clever_kill_store_sound : cse3. + Theorem store2_sound: forall chunk addr args a src rel rs m m', sem_rel rel rs m -> @@ -774,7 +811,7 @@ Section SOUNDNESS. Proof. unfold store2. intros. - apply kill_mem_sound with (m:=m); auto. + destruct (Compopts.optim_CSE3_alias_analysis tt); eauto with cse3. Qed. Hint Resolve store2_sound : cse3. diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 7e3b23d8..a8594be4 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -25,9 +25,10 @@ let option_ffpu = ref true let option_ffloatconstprop = ref 2 let option_ftailcalls = ref true let option_fconstprop = ref true -let option_fcse = ref true -let option_fcse2 = ref true +let option_fcse = ref false +let option_fcse2 = ref false let option_fcse3 = ref true +let option_fcse3_alias_analysis = ref true let option_fredundancy = ref true let option_fduplicate = ref 0 let option_finvertcond = ref true diff --git a/driver/Compopts.v b/driver/Compopts.v index 1f952164..f1ab4f7b 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -46,6 +46,9 @@ Parameter optim_CSE2: unit -> bool. (** Flag -fcse3. For DMonniaux's common subexpression elimination. *) Parameter optim_CSE3: unit -> bool. +(** Flag -fcse3-alias-analysis. For DMonniaux's common subexpression elimination. *) +Parameter optim_CSE3_alias_analysis: unit -> bool. + (** Flag -fredundancy. For dead code elimination. *) Parameter optim_redundancy: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index 12b61d86..133bac0a 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -194,9 +194,10 @@ Processing options: -fconst-prop Perform global constant propagation [on] -ffloat-const-prop Control constant propagation of floats (=0: none, =1: limited, =2: full; default is full) - -fcse Perform common subexpression elimination [on] - -fcse2 Perform inter-loop common subexpression elimination [on] + -fcse Perform common subexpression elimination [off] + -fcse2 Perform inter-loop common subexpression elimination [off] -fcse3 Perform inter-loop common subexpression elimination [on] + -fcse3-alias-analysis Perform inter-loop common subexpression elimination with alias analysis [on] -fredundancy Perform redundancy elimination [on] -fpostpass Perform postpass scheduling (only for K1 architecture) [on] -fpostpass= Perform postpass scheduling with the specified optimization [list] @@ -393,6 +394,7 @@ let cmdline_actions = @ f_opt "cse" option_fcse @ f_opt "cse2" option_fcse2 @ f_opt "cse3" option_fcse3 + @ f_opt "cse3-alias-analysis" option_fcse3_alias_analysis @ f_opt "redundancy" option_fredundancy @ f_opt "postpass" option_fpostpass @ [ Exact "-fduplicate", Integer (fun n -> option_fduplicate := n) ] diff --git a/extraction/extraction.v b/extraction/extraction.v index 9b47b203..f868264c 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -116,6 +116,8 @@ Extract Constant Compopts.optim_CSE2 => "fun _ -> !Clflags.option_fcse2". Extract Constant Compopts.optim_CSE3 => "fun _ -> !Clflags.option_fcse3". +Extract Constant Compopts.optim_CSE3_alias_analysis => + "fun _ -> !Clflags.option_fcse3_alias_analysis". Extract Constant Compopts.optim_redundancy => "fun _ -> !Clflags.option_fredundancy". Extract Constant Compopts.optim_postpass => -- cgit