From f59c540aa7cf85c89ee0cb07c20374c8ad76a46c Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 27 Oct 2020 15:21:11 +0100
Subject: new CSE3

---
 backend/CSE3analysis.v | 38 +++++++++++++++++---------------------
 1 file changed, 17 insertions(+), 21 deletions(-)

(limited to 'backend/CSE3analysis.v')

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 7316c9a9..cd7e3d84 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -282,12 +282,14 @@ 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 => PSet.add id rel'
-    | None => rel'
+    | Some id =>
+      if PSet.contains rel id
+      then rel
+      else PSet.add id (kill_reg dst rel)
+    | None => kill_reg dst rel
     end.
 
   Definition oper1 (dst : reg) (op: sym_op) (args : list reg)
@@ -307,12 +309,6 @@ 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 :=
@@ -324,18 +320,18 @@ Section OPERATIONS.
       | _ => kill_reg dst rel
       end
     else
-      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.
+      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.
   
   Definition clever_kill_store
              (chunk : memory_chunk) (addr: addressing) (args : list reg)
-- 
cgit