CSE3 alias analysis

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 <n>  Control constant propagation of floats
                    (<n>=0: none, <n>=1: limited, <n>=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= <optim> 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 =>