From 3ceff391e0be39cd7a3d5d861fb1f32653579bab Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 15 Oct 2020 11:50:56 +0200
Subject: some more tuning of CSE3

---
 backend/CSE3analysis.v | 27 ++++++++++++++++++---------
 1 file changed, 18 insertions(+), 9 deletions(-)

(limited to 'backend/CSE3analysis.v')

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 5fbabd93..7316c9a9 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -308,6 +308,12 @@ Section OPERATIONS.
       | 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 :=
     if is_smove op
@@ -318,15 +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)
-                          (oper1 dst op args' rel)
-        else oper1 dst op args' rel
-      | None => 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