two lemmas admitted

1 files changed, 20 insertions, 2 deletions

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 5ed04bc4..8b7f1190 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -181,12 +181,24 @@ Definition eq_depends_on_mem eq :=
   | SOp op => op_depends_on_memory op
   end.
 
+Definition eq_depends_on_store eq :=
+  match eq_op eq with
+  | SLoad _ _ => true
+  | SOp op => false
+  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 get_store_kills (eqs : PTree.t equation) : PSet.t :=
+  PTree.fold (fun already (eqno : eq_id) (eq : equation) =>
+                if eq_depends_on_store eq
+                then PSet.add eqno already
+                else already) eqs PSet.empty.
+
 Definition is_move (op : operation) :
   { op = Omove } + { op <> Omove }.
 Proof.
@@ -216,6 +228,7 @@ Record eq_context := mkeqcontext
                          eq_rhs_oracle : node -> sym_op -> list reg -> PSet.t;
                          eq_kill_reg : reg -> PSet.t;
                          eq_kill_mem : unit -> PSet.t;
+                         eq_kill_store : unit -> PSet.t;
                          eq_moves : reg -> PSet.t }.
 
 Section OPERATIONS.
@@ -342,6 +355,9 @@ Section OPERATIONS.
                   (oper1 dst op args' rel)
       end.
   
+  Definition kill_store (rel : RELATION.t) : RELATION.t :=
+    PSet.subtract rel (eq_kill_store ctx tt).
+
   Definition clever_kill_store
              (chunk : memory_chunk) (addr: addressing) (args : list reg)
              (src : reg)
@@ -358,7 +374,7 @@ Section OPERATIONS.
                 may_overlap chunk addr args chunk' addr' (eq_args eq)
               end
             end)
-         (PSet.inter rel (eq_kill_mem ctx tt))).
+         (PSet.inter rel (eq_kill_store ctx tt))).
 
   Definition store2
              (chunk : memory_chunk) (addr: addressing) (args : list reg)
@@ -366,7 +382,7 @@ Section OPERATIONS.
              (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.
+    else kill_store rel.
 
   Definition store1
              (chunk : memory_chunk) (addr: addressing) (args : list reg)
@@ -501,6 +517,7 @@ Definition context_from_hints (hints : analysis_hints) :=
   let eqs := hint_eq_catalog hints in
   let reg_kills := get_reg_kills eqs in 
   let mem_kills := get_mem_kills eqs in
+  let store_kills := get_store_kills eqs in
   let moves := get_moves eqs in
   {|
     eq_catalog := fun eq_id => PTree.get eq_id eqs;
@@ -508,5 +525,6 @@ Definition context_from_hints (hints : analysis_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_kill_store := fun _ => store_kills;
     eq_moves    := fun reg => PMap.get reg moves
   |}.