in CSE3 choose lowest variable as representative for moves

1 files changed, 27 insertions, 12 deletions

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index cd7e3d84..34df644e 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -227,29 +227,44 @@ Section OPERATIONS.
   Definition kill_mem (rel : RELATION.t) : RELATION.t :=
     PSet.subtract rel (eq_kill_mem ctx tt).
 
-  Definition pick_source (l : list reg) := (* todo: take min? *)
+  Definition reg_min (x y : reg) :=
+    if plt x y then x else y.
+  
+  Fixpoint reg_min_rec (l : list reg) (before : reg)  :=
+    match l with
+    | h::t => reg_min_rec t (reg_min before h)
+    | nil => before
+    end.
+
+  Definition pick_source (l : list reg) :=
     match l with
-    | h::t => Some h
+    | h::t => Some (reg_min_rec t 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 =>
+
+  Fixpoint get_sources (x : reg) eqs :=
+    match eqs with
+    | nil => nil
+    | eqno::others =>
       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
+          | src::nil => src :: (get_sources x others)
+          | _ => get_sources x others
           end
-        else x
-      | _ => x
+        else get_sources x others
+      | _ => get_sources x others
       end
     end.
-
+      
+  Definition forward_move (rel : RELATION.t)  (x : reg) : reg :=
+    match pick_source (get_sources x (PSet.elements (PSet.inter rel (eq_moves ctx x)))) with
+    | None => x
+    | Some src => src
+    end.
+  
   Definition forward_move_l (rel : RELATION.t) : list reg -> list reg :=
     List.map (forward_move rel).