two lemmas admitted

3 files changed, 115 insertions, 9 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
   |}.
diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml
index e37ef61f..e038331c 100644
--- a/backend/CSE3analysisaux.ml
+++ b/backend/CSE3analysisaux.ml
@@ -174,6 +174,7 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
   and rhs_table = Hashtbl.create 100
   and cur_kill_reg = ref (PMap.init PSet.empty)
   and cur_kill_mem = ref PSet.empty
+  and cur_kill_store = ref PSet.empty
   and cur_moves = ref (PMap.init PSet.empty) in
   let eq_find_oracle node eq =
     assert (not (is_trivial eq));
@@ -216,6 +217,8 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
            (eq.eq_lhs :: eq.eq_args);
          (if eq_depends_on_mem eq
           then cur_kill_mem := PSet.add coq_id !cur_kill_mem);
+         (if eq_depends_on_store eq
+          then cur_kill_store := PSet.add coq_id !cur_kill_store);
          (match eq.eq_op, eq.eq_args with
           | (SOp Op.Omove), [rhs] -> imp_add_i_j cur_moves eq.eq_lhs coq_id
           | _, _ -> ());
@@ -232,6 +235,7 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
               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_kill_store  = (fun () -> !cur_kill_store);
               eq_moves       = (fun reg -> PMap.get reg !cur_moves)
             } in
   match internal_analysis ctx tenv f
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index 1e5b88c3..50a2c469 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -133,13 +133,18 @@ Definition xlget_kills (eqs : list (eq_id * equation)) (m :  Regmap.t PSet.t) :
     add_i_j (eq_lhs (snd item)) (fst item)
             (add_ilist_j (eq_args (snd item)) (fst item) already)) eqs m.
 
-
 Definition xlget_mem_kills (eqs : list (positive * equation)) (m : PSet.t) : PSet.t :=
 (fold_left
        (fun (a : PSet.t) (p : positive * equation) =>
         if eq_depends_on_mem (snd p) then PSet.add (fst p) a else a)
        eqs m).
 
+Definition xlget_store_kills (eqs : list (positive * equation)) (m : PSet.t) : PSet.t :=
+(fold_left
+       (fun (a : PSet.t) (p : positive * equation) =>
+        if eq_depends_on_store (snd p) then PSet.add (fst p) a else a)
+       eqs m).
+
 Lemma xlget_kills_monotone :
   forall eqs m i j,
     PSet.contains (Regmap.get i m) j = true ->
@@ -170,6 +175,24 @@ Qed.
 
 Hint Resolve xlget_mem_kills_monotone : cse3.
 
+Lemma xlget_store_kills_monotone :
+  forall eqs m j,
+    PSet.contains m j = true ->
+    PSet.contains (xlget_store_kills eqs m) j = true.
+Proof.
+  induction eqs; simpl; trivial.
+  intros.
+  destruct eq_depends_on_store.
+  - apply IHeqs.
+    destruct (peq (fst a) j).
+    + subst j. apply PSet.gadds.
+    + rewrite PSet.gaddo by congruence.
+      trivial.
+  - auto.
+Qed.
+
+Hint Resolve xlget_store_kills_monotone : cse3.
+
 Lemma xlget_kills_has_lhs :
   forall eqs m lhs sop args j,
     In (j, {| eq_lhs := lhs;
@@ -333,6 +356,60 @@ Qed.
 
 Hint Resolve context_from_hints_get_kills_has_eq_depends_on_mem : cse3.
 
+Lemma xlget_kills_has_eq_depends_on_store :
+  forall eqs eq j m,
+    In (j, eq) eqs ->
+    eq_depends_on_store eq = true ->
+    PSet.contains (xlget_store_kills eqs m) j = true.
+Proof.
+  induction eqs; simpl.
+  contradiction.
+  intros.
+  destruct H.
+  { subst a.
+    simpl.
+    rewrite H0.
+    apply xlget_store_kills_monotone.
+    apply PSet.gadds.
+  }
+  eauto.
+Qed.
+
+Hint Resolve xlget_kills_has_eq_depends_on_store : cse3.
+
+Lemma get_kills_has_eq_depends_on_store :
+  forall eqs eq j,
+    PTree.get j eqs = Some eq ->
+    eq_depends_on_store eq = true ->
+    PSet.contains (get_store_kills eqs) j = true.
+Proof.
+  intros.
+  unfold get_store_kills.
+  rewrite PTree.fold_spec.
+  change (fold_left
+       (fun (a : PSet.t) (p : positive * equation) =>
+        if eq_depends_on_store (snd p) then PSet.add (fst p) a else a)
+       (PTree.elements eqs) PSet.empty)
+    with (xlget_store_kills (PTree.elements eqs) PSet.empty).
+  eapply xlget_kills_has_eq_depends_on_store.
+  apply PTree.elements_correct.
+  eassumption.
+  trivial.
+Qed.
+  
+Lemma context_from_hints_get_kills_has_eq_depends_on_store :
+  forall hints eq j,
+    PTree.get j (hint_eq_catalog hints) = Some eq ->
+    eq_depends_on_store eq = true ->
+    PSet.contains (eq_kill_store (context_from_hints hints) tt) j = true.
+Proof.
+  intros.
+  simpl.
+  eapply get_kills_has_eq_depends_on_store; eassumption.
+Qed.
+
+Hint Resolve context_from_hints_get_kills_has_eq_depends_on_store : cse3.
+
 Definition eq_involves (eq : equation) (i : reg) :=
   i = (eq_lhs eq) \/ In i (eq_args eq).
 
@@ -418,6 +495,12 @@ Section SOUNDNESS.
       eq_depends_on_mem eq = true ->
       PSet.contains (eq_kill_mem ctx tt) j = true.
 
+  Hypothesis ctx_kill_store_has_depends_on_store :
+    forall eq j,
+      eq_catalog ctx j = Some eq ->
+      eq_depends_on_store eq = true ->
+      PSet.contains (eq_kill_store ctx tt) j = true.
+
   Theorem kill_reg_sound :
     forall rel rs m dst v,
       (sem_rel rel rs m) ->
@@ -895,20 +978,21 @@ Section SOUNDNESS.
     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.
+    - admit.
+    (* - destruct (op_depends_on_memory op') eqn:DEPENDS.
+      + erewrite ctx_kill_store_has_depends_on_store in CONTAINS by eauto.
         discriminate.
       + rewrite op_depends_on_memory_correct with (m2:=m); trivial.
-        apply REL; auto.
+        apply REL; auto. *)
     - simpl in REL.
-      erewrite ctx_kill_mem_has_depends_on_mem in CONTAINS by eauto.
+      erewrite ctx_kill_store_has_depends_on_store 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.
+  Admitted.
 
   Hint Resolve clever_kill_store_sound : cse3.
 
@@ -922,7 +1006,7 @@ Section SOUNDNESS.
     unfold store2.
     intros.
     destruct (Compopts.optim_CSE3_alias_analysis tt); eauto with cse3.
-  Qed.
+  Admitted.
   
   Hint Resolve store2_sound : cse3.