From 7158ee7375fc78ea73248354febdbedfd4abf1fc Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 30 Oct 2020 20:59:54 +0100
Subject: reinstated old version

---
 backend/CSE3analysis.v | 80 ++++++++++++++------------------------------------
 1 file changed, 22 insertions(+), 58 deletions(-)

(limited to 'backend/CSE3analysis.v')

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index dbf1afe2..7316c9a9 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -227,22 +227,13 @@ Section OPERATIONS.
   Definition kill_mem (rel : RELATION.t) : RELATION.t :=
     PSet.subtract rel (eq_kill_mem ctx tt).
 
-  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) := (* todo: take min? *)
     match l with
     | h::t => Some h
     | nil => None
     end.
   
-  Definition forward_move1 (rel : RELATION.t)  (x : reg) : reg :=
+  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 =>
@@ -259,37 +250,6 @@ Section OPERATIONS.
       end
     end.
 
-  Definition pick_min_source (l : list reg) :=
-    match l with
-    | h::t => Some (reg_min_rec t h)
-    | nil => None
-    end.
-
-  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 :: (get_sources x others)
-          | _ => get_sources x others
-          end
-        else get_sources x others
-      | _ => get_sources x others
-      end
-    end.
-      
-  Definition forward_move2 (rel : RELATION.t)  (x : reg) : reg :=
-    match pick_min_source (get_sources x (PSet.elements (PSet.inter rel (eq_moves ctx x)))) with
-    | None => x
-    | Some src => src
-    end.
-
-  Definition forward_move := forward_move1.
-  
   Definition forward_move_l (rel : RELATION.t) : list reg -> list reg :=
     List.map (forward_move rel).
 
@@ -322,14 +282,12 @@ Section OPERATIONS.
 
   Definition oper2 (dst : reg) (op: sym_op)(args : list reg)
            (rel : RELATION.t) : RELATION.t :=
+    let rel' := kill_reg dst rel in
     match eq_find {| eq_lhs := dst;
                      eq_op  := op;
                      eq_args:= args |} with
-    | Some id =>
-      if PSet.contains rel id
-      then rel
-      else PSet.add id (kill_reg dst rel)
-    | None => kill_reg dst rel
+    | Some id => PSet.add id rel'
+    | None => rel'
     end.
 
   Definition oper1 (dst : reg) (op: sym_op) (args : list reg)
@@ -349,6 +307,12 @@ Section OPERATIONS.
       | Some eq_id => PSet.add eq_id (kill_reg dst rel)
       | None => kill_reg dst rel
       end.
+
+  Definition is_trivial_sym_op sop :=
+    match sop with
+    | SOp op => is_trivial_op op
+    | SLoad _ _ => false
+    end.
   
   Definition oper (dst : reg) (op: sym_op) (args : list reg)
              (rel : RELATION.t) : RELATION.t :=
@@ -360,18 +324,18 @@ Section OPERATIONS.
       | _ => kill_reg dst rel
       end
     else
-      let args' := forward_move_l rel args in
-      match rhs_find op args' rel with
-      | Some r =>
-        if Compopts.optim_CSE3_glb tt
-        then RELATION.glb (move r dst rel)
-                          (RELATION.glb (oper1 dst op args' rel)
-                                        (oper1 dst op args rel))
-        else RELATION.glb (oper1 dst op args' rel)
-                          (oper1 dst op args rel)
-      | None => RELATION.glb (oper1 dst op args' rel)
-                             (oper1 dst op args rel)
-      end.
+      if is_trivial_sym_op op
+      then kill_reg dst rel
+      else
+        let args' := forward_move_l rel args in
+        match rhs_find op args' rel with
+        | Some r =>
+          if Compopts.optim_CSE3_glb tt
+          then RELATION.glb (move r dst rel)
+                            (oper1 dst op args' rel)
+          else oper1 dst op args' rel
+        | None => oper1 dst op args' rel
+        end.
   
   Definition clever_kill_store
              (chunk : memory_chunk) (addr: addressing) (args : list reg)
-- 
cgit