cse3: forward_move_sound

2 files changed, 72 insertions, 3 deletions

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index da527995..bbe76f75 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -125,16 +125,41 @@ Definition get_moves (eqs : PTree.t equation) :
                 if is_smove (eq_op eq)
                 then add_i_j (eq_lhs eq) eqno already
                 else already) eqs (PMap.init PSet.empty).
-
+  
 Record eq_context := mkeqcontext
                        { eq_catalog : node -> option equation;
-                         eq_kills : reg -> PSet.t }.
+                         eq_kills : reg -> PSet.t;
+                         eq_moves : reg -> PSet.t }.
 
 Section OPERATIONS.
   Context {ctx : eq_context}.
   
   Definition kill_reg (r : reg) (rel : RELATION.t) : RELATION.t :=
     PSet.subtract rel (eq_kills ctx r).
+
+  Definition pick_source (l : list reg) := (* todo: take min? *)
+    match l with
+    | h::t => Some h
+    | nil => None
+    end.
+  
+  Definition forward_move (rel : RELATION.t)  (x : reg) : reg :=
+    match pick_source (PSet.elements (PSet.inter rel (eq_moves ctx x))) with
+    | None => x
+    | Some eqno =>
+      match eq_catalog ctx eqno with
+      | Some eq =>
+        if is_smove (eq_op eq) && peq x (eq_lhs eq)
+        then
+          match eq_args eq with
+          | src::nil => src
+          | _ => x
+          end
+        else x
+      | _ => x
+      end
+    end.
+  
 End OPERATIONS.
 
 Definition totoro := RELATION.lub.
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index 29c6618c..deb8b6e4 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -262,5 +262,49 @@ Section SOUNDNESS.
       assumption.
   Qed.
 
-
+  Lemma pick_source_sound :
+    forall (l : list reg),
+      match pick_source l with
+      | Some x => In x l
+      | None => True
+      end.
+  Proof.
+    unfold pick_source.
+    destruct l; simpl; trivial.
+    left; trivial.
+  Qed.
+    
+  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 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.
+    destruct (pick_source (PSet.elements (PSet.inter rel (eq_moves ctx x)))).
+    2: reflexivity.
+    destruct (eq_catalog ctx r) as [eq | ] eqn:CATALOG.
+    2: reflexivity.
+    specialize REL with (i := r) (eq0 := eq).
+    destruct (is_smove (eq_op eq)) as [MOVE | ].
+    2: reflexivity.
+    destruct (peq x (eq_lhs eq)).
+    2: reflexivity.
+    simpl.
+    subst x.
+    rewrite PSet.elements_spec in ELEMENT.
+    rewrite PSet.ginter in ELEMENT.
+    rewrite andb_true_iff in ELEMENT.
+    unfold sem_eq in REL.
+    rewrite MOVE in REL.
+    simpl in REL.
+    destruct (eq_args eq) as [ | h t].
+    reflexivity.
+    destruct t.
+    2: reflexivity.
+    simpl in REL.
+    intuition congruence.
+  Qed.
 End SOUNDNESS.