diff options
Diffstat (limited to 'backend/CSE3analysis.v')
-rw-r--r-- | backend/CSE3analysis.v | 38 |
1 files changed, 25 insertions, 13 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index ade79c28..7316c9a9 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -298,13 +298,22 @@ 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 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 @@ -315,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) |