From 0b76b98fcec5b13565f5403f7f7f63f46c09829c Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 25 Nov 2020 12:59:29 +0100
Subject: two lemmas admitted

---
 backend/CSE3analysisproof.v | 98 +++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 91 insertions(+), 7 deletions(-)

(limited to 'backend/CSE3analysisproof.v')

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.
 
-- 
cgit