use in transformation

1 files changed, 21 insertions, 3 deletions

diff --git a/backend/CSE2.v b/backend/CSE2.v
index a042b0a9..79c52973 100644
--- a/backend/CSE2.v
+++ b/backend/CSE2.v
@@ -709,7 +709,7 @@ Definition apply_instr instr (rel : RELATION.t) : RB.t :=
   | Icond _ _ _ _
   | Ijumptable _ _ => Some rel
   | Istore _ _ _ _ _ => Some (kill_mem rel)
-  | Iop op args dst _ => Some (gen_oper op dst args rel) 
+  | Iop op args dst _ => Some (gen_oper op dst args rel)
   | Iload _ _ _ dst _
   | Icall _ _ _ dst _ => Some (kill_reg dst rel)
   | Ibuiltin _ _ res _ => Some (RELATION.top) (* TODO (kill_builtin_res res x) *)
@@ -743,13 +743,31 @@ Definition subst_arg (fmap : option (PMap.t RB.t)) (pc : node) (x : reg) : reg :
   end.
 
 Definition subst_args fmap pc := List.map (subst_arg fmap pc).
-    
+
+Definition gen_move src dst s :=
+  if peq src dst
+  then Inop s
+  else Iop Omove (src::nil) dst s.
+
 (* Transform *)
+Definition find_op_in_fmap fmap pc op args :=
+  match fmap with
+  | None => None
+  | Some map =>
+    match PMap.get pc map with
+    | Some rel => find_op rel op args
+    | None => None
+    end
+  end.
+
 Definition transf_instr (fmap : option (PMap.t RB.t))
            (pc: node) (instr: instruction) :=
   match instr with
   | Iop op args dst s =>
-    Iop op (subst_args fmap pc args) dst s
+    match find_op_in_fmap fmap pc op args with
+    | None => Iop op (subst_args fmap pc args) dst s
+    | Some src => gen_move src dst s
+    end
   | Iload chunk addr args dst s =>
     Iload chunk addr (subst_args fmap pc args) dst s
   | Istore chunk addr args src s =>