From 7c6ce18466ed1de58a0f99c785c777d63a9a6149 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 14 Oct 2020 21:56:30 +0200
Subject: a bit of progress

---
 backend/CSE3analysis.v | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'backend/CSE3analysis.v')

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index ade79c28..5fbabd93 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -298,12 +298,15 @@ Section OPERATIONS.
 
   
   Definition move (src dst : reg) (rel : RELATION.t) : RELATION.t :=
-    match eq_find {| eq_lhs := dst;
+    if peq src dst
+    then rel
+    else
+      match eq_find {| eq_lhs := dst;
                      eq_op  := SOp Omove;
                      eq_args:= src::nil |} with
-    | Some eq_id => PSet.add eq_id (kill_reg dst rel)
-    | None => kill_reg dst rel
-    end.
+      | Some eq_id => PSet.add eq_id (kill_reg dst rel)
+      | None => kill_reg dst rel
+      end.
 
   Definition oper (dst : reg) (op: sym_op) (args : list reg)
              (rel : RELATION.t) : RELATION.t :=
-- 
cgit