a bit of progress

3 files changed, 34 insertions, 4 deletions

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index ade79c28..5fbabd93 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -298,12 +298,15 @@ Section OPERATIONS.
 
   
   Definition move (src dst : reg) (rel : RELATION.t) : RELATION.t :=
-    match eq_find {| eq_lhs := dst;
+    if peq src dst
+    then rel
+    else
+      match eq_find {| eq_lhs := dst;
                      eq_op  := SOp Omove;
                      eq_args:= src::nil |} with
-    | Some eq_id => PSet.add eq_id (kill_reg dst rel)
-    | None => kill_reg dst rel
-    end.
+      | Some eq_id => PSet.add eq_id (kill_reg dst rel)
+      | None => kill_reg dst rel
+      end.
 
   Definition oper (dst : reg) (op: sym_op) (args : list reg)
              (rel : RELATION.t) : RELATION.t :=
diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml
index 3e4a6b9e..3990b765 100644
--- a/backend/CSE3analysisaux.ml
+++ b/backend/CSE3analysisaux.ml
@@ -67,6 +67,9 @@ let pp_option pp oc = function
   | None -> output_string oc "none"
   | Some x -> pp oc x;;
 
+let is_trivial eq =
+  (eq.eq_op = SOp Op.Omove) && (eq.eq_args = [eq.eq_lhs]);;
+
 let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
   let cur_eq_id = ref 0
   and cur_catalog = ref PTree.empty
@@ -76,6 +79,7 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
   and cur_kill_mem = ref PSet.empty
   and cur_moves = ref (PMap.init PSet.empty) in
   let eq_find_oracle node eq =
+    assert (not (is_trivial eq));
     let o = Hashtbl.find_opt eq_table (flatten_eq eq) in
     (if !Clflags.option_debug_compcert > 1
      then Printf.printf "@%d: eq_find %a -> %a\n" (P.to_int node)
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index f4e3672d..0ddaa527 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -745,6 +745,25 @@ Section SOUNDNESS.
 
   Hint Resolve oper1_sound : cse3.
 
+  Lemma rel_idem_replace:
+    forall rel rs r m,
+      sem_rel rel rs m ->
+      sem_rel rel rs # r <- (rs # r) m.
+  Proof.
+    intros until m.
+    intro REL.
+    unfold sem_rel, sem_eq, sem_rhs in *.
+    intros.
+    specialize REL with (i:=i) (eq0:=eq).
+    rewrite Regmap.gsident.
+    replace ((rs # r <- (rs # r)) ## (eq_args eq)) with
+        (rs ## (eq_args eq)).
+    { apply REL; auto. }
+    apply list_map_exten.
+    intros.
+    apply Regmap.gsident.
+  Qed.
+      
   Lemma move_sound :
     forall no : node,
     forall rel : RELATION.t,
@@ -756,6 +775,10 @@ Section SOUNDNESS.
     unfold move.
     intros until m.
     intro REL.
+    destruct (peq src dst).
+    { subst dst.
+      apply rel_idem_replace; auto.
+    }
     pose proof (eq_find_sound no  {| eq_lhs := dst; eq_op := SOp Omove; eq_args := src :: nil |}) as EQ_FIND_SOUND.
     destruct eq_find.
     - intros i eq CONTAINS.