reinstated old version

1 files changed, 12 insertions, 154 deletions

diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index 29254a4f..66b199cc 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -478,102 +478,6 @@ Section SOUNDNESS.
     rewrite negb_true_iff in H.
     intuition.
   Qed.
-
-  Lemma reg_min_sound:
-    forall x y, (reg_min x y) = x \/ (reg_min x y) = y.
-  Proof.
-    intros; unfold reg_min.
-    destruct plt; auto.
-  Qed.
-  
-  Lemma reg_min_rec_sound :
-    forall (l : list reg) (before : reg),
-      In (reg_min_rec l before) l \/
-      reg_min_rec l before = before.
-  Proof.
-    induction l; cbn.
-    { auto. }
-    intro bef.
-    destruct (IHl (reg_min bef a)).
-    { auto. }
-    rewrite H.
-    destruct (reg_min_sound bef a); auto.
-  Qed.
-    
-  Lemma pick_min_source_sound :
-    forall (l : list reg),
-      match pick_min_source l with
-      | Some x => In x l
-      | None => True
-      end.
-  Proof.
-    destruct l; cbn; trivial.
-    destruct (reg_min_rec_sound l r); auto.
-  Qed.
-
-  Hint Resolve pick_min_source_sound : cse3.
-
-  Theorem get_sources_sound :
-    forall l src rs m x,
-    (forall i eq,
-      In i l ->
-      eq_catalog ctx i = Some eq ->
-      sem_eq eq rs m) ->
-      (In src (get_sources (ctx := ctx) x l)) ->
-      rs # src = rs # x.
-  Proof.
-    induction l; cbn; intros until x; intros SEM IN.
-    contradiction.
-    destruct (eq_catalog ctx a) eqn:CATALOG.
-    2: eauto using IHl; fail.
-    pose proof (SEM a e) as SEMeq.
-    destruct e; cbn in *.
-    destruct (is_smove eq_op && peq x eq_lhs) eqn:CORRECT.
-    2: eauto using IHl; fail.
-    destruct eq_args.
-    eauto using IHl; fail.
-    destruct eq_args.
-    2: eauto using IHl; fail.
-    cbn in IN.
-    destruct IN.
-    2: eauto using IHl; fail.
-    rewrite andb_true_iff in CORRECT.
-    intuition.
-    destruct (peq x eq_lhs).
-    2: discriminate.
-    subst eq_lhs.
-    destruct (is_smove eq_op).
-    2: discriminate.
-    subst eq_op.
-    subst src.
-    cbn in H2.
-    symmetry.
-    assumption.
-  Qed.
-    
-  Theorem forward_move2_sound :
-    forall rel rs m x,
-      (sem_rel rel rs m) ->
-      rs # (forward_move2 (ctx := ctx) rel x) = rs # x.
-  Proof.
-    unfold forward_move2.
-    intros until x; intros REL.
-    pose proof (pick_min_source_sound (get_sources (ctx := ctx) x (PSet.elements (PSet.inter rel (eq_moves ctx x))))) as PICK.
-    destruct pick_min_source.
-    2: reflexivity.
-    apply get_sources_sound with (l := (PSet.elements (PSet.inter rel (eq_moves ctx x)))) (m:=m).
-    2: assumption.
-    intros i eq IN CATALOG.
-    rewrite PSet.elements_spec in IN.
-    rewrite PSet.ginter in IN.
-    rewrite andb_true_iff in IN.
-    destruct IN.
-    unfold sem_rel in REL.
-    apply REL with (i:=i); assumption.
-  Qed.
-  
-  Hint Resolve forward_move2_sound : cse3.
-
     
   Lemma pick_source_sound :
     forall (l : list reg),
@@ -589,12 +493,12 @@ Section SOUNDNESS.
     
   Hint Resolve pick_source_sound : cse3.
 
-  Theorem forward_move1_sound :
+  Theorem forward_move_sound :
     forall rel rs m x,
       (sem_rel rel rs m) ->
-      rs # (forward_move1 (ctx := ctx) rel x) = rs # x.
+      rs # (forward_move (ctx := ctx) rel x) = rs # x.
   Proof.
-    unfold sem_rel, forward_move1.
+    unfold sem_rel, forward_move.
     intros until x.
     intro REL.
     pose proof (pick_source_sound (PSet.elements (PSet.inter rel (eq_moves ctx x)))) as ELEMENT.
@@ -623,17 +527,6 @@ Section SOUNDNESS.
     intuition congruence.
   Qed.
 
-  Hint Resolve forward_move1_sound : cse3.
-
-  Theorem forward_move_sound :
-    forall rel rs m x,
-      (sem_rel rel rs m) ->
-      rs # (forward_move (ctx := ctx) rel x) = rs # x.
-  Proof.
-    unfold forward_move.
-    apply forward_move1_sound.
-  Qed.
-  
   Hint Resolve forward_move_sound : cse3.
 
   Theorem forward_move_l_sound :
@@ -806,28 +699,6 @@ Section SOUNDNESS.
       + congruence.
   Qed.
 
-
-  Lemma arglist_idem_write:
-    forall { A : Type} args (rs : Regmap.t A) dst,
-      (rs # dst <- (rs # dst)) ## args = rs ## args.
-  Proof.
-    induction args; trivial.
-    intros. cbn.
-    f_equal; trivial.
-    apply Regmap.gsident.
-  Qed.
-  
-  Lemma sem_rhs_idem_write:
-    forall sop args rs dst m v,
-      sem_rhs sop args rs m v ->
-      sem_rhs sop args (rs # dst <- (rs # dst)) m v.
-  Proof.
-    intros.
-    unfold sem_rhs in *.
-    rewrite arglist_idem_write.
-    assumption.
-  Qed.
-  
   Theorem oper2_sound:
     forall no dst sop args rel rs m v,
       sem_rel rel rs m ->
@@ -855,17 +726,6 @@ Section SOUNDNESS.
       rewrite Regmap.gss.
       apply sem_rhs_depends_on_args_only; auto.
     }
-    intros INi.
-    destruct (PSet.contains rel e) eqn:CONTAINSe.
-    { pose proof (REL e {| eq_lhs := dst; eq_op := sop; eq_args := args |} CONTAINSe H) as RELe.
-      pose proof (REL i eq CONTAINS INi) as RELi.
-      unfold sem_eq in *.
-      cbn in RELe.
-      replace v with (rs # dst) by (eapply sem_rhs_det; eassumption).
-      rewrite Regmap.gsident.
-      apply sem_rhs_idem_write.
-      assumption.
-    }
     rewrite PSet.gaddo in CONTAINS by congruence.
     apply (kill_reg_sound rel rs m dst v REL i eq); auto.
   Qed.
@@ -961,7 +821,11 @@ Section SOUNDNESS.
       subst.
       rewrite <- (forward_move_sound rel rs m r) by auto.
       apply move_sound; auto.
-    - destruct rhs_find as [src |] eqn:RHS_FIND.
+    - destruct (is_trivial_sym_op sop).
+      {
+        apply kill_reg_sound; auto.
+      }
+      destruct rhs_find as [src |] eqn:RHS_FIND.
       + destruct (Compopts.optim_CSE3_glb tt).
         * apply sem_rel_glb; split.
           ** pose proof (rhs_find_sound no sop (forward_move_l (ctx:=ctx) rel args) rel src rs m REL RHS_FIND) as SOUND.
@@ -969,18 +833,12 @@ Section SOUNDNESS.
              2: eassumption.
              rewrite <- (sem_rhs_det SOUND RHS).
              apply move_sound; auto.
-          ** apply sem_rel_glb; split.
-             *** apply oper1_sound; auto.
-                 apply forward_move_rhs_sound; auto.
-             *** apply oper1_sound; auto.
-        * apply sem_rel_glb; split.
           ** apply oper1_sound; auto.
              apply forward_move_rhs_sound; auto.
-          ** apply oper1_sound; auto.
-      + apply sem_rel_glb; split.
-        * apply oper1_sound; auto.
-          apply forward_move_rhs_sound; auto.
-        * apply oper1_sound; auto.
+        * ** apply oper1_sound; auto.
+             apply forward_move_rhs_sound; auto.
+      + apply oper1_sound; auto.
+        apply forward_move_rhs_sound; auto.
   Qed.
 
   Hint Resolve oper_sound : cse3.