refixcse3

1 files changed, 29 insertions, 16 deletions

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 5eb92a82..5ed04bc4 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -326,18 +326,21 @@ 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)
@@ -380,11 +383,21 @@ Section OPERATIONS.
       end
     else rel'.
     
-  Definition store
+  Definition store (tenv : typing_env)
              (chunk : memory_chunk) (addr: addressing) (args : list reg)
-             (src : reg) (ty: typ)
+             (src : reg)
              (rel : RELATION.t) : RELATION.t :=
-    store1 chunk addr (forward_move_l rel args) (forward_move rel src) ty rel.
+    let args' := forward_move_l rel args in
+    let src' := forward_move rel src in
+    let tsrc := tenv src in
+    let tsrc' := tenv src' in
+    RELATION.glb
+      (RELATION.glb
+         (store1 chunk addr args src tsrc rel)
+         (store1 chunk addr args' src tsrc rel))
+      (RELATION.glb
+         (store1 chunk addr args src' tsrc' rel)
+         (store1 chunk addr args' src' tsrc' rel)).
 
   Definition kill_builtin_res res rel :=
     match res with
@@ -427,7 +440,7 @@ Section OPERATIONS.
   | Icond _ _ _ _ _
   | Ijumptable _ _ => Some rel
   | Istore chunk addr args src _ =>
-    Some (store chunk addr args src (tenv (forward_move rel src)) rel)
+    Some (store tenv chunk addr args src rel)
   | Iop op args dst _ => Some (oper dst (SOp op) args rel)
   | Iload trap chunk addr args dst _ => Some (oper dst (SLoad chunk addr) args rel)
   | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel))