diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-14 21:56:30 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-14 21:56:30 +0200 |
| commit | 7c6ce18466ed1de58a0f99c785c777d63a9a6149 (patch) | |
| tree | c1afac8e4b12fc833b4da838abbd38eca3f98be0 /backend/CSE3analysis.v | |
| parent | 1050bb788994cd6944770bf754230f4c90d9442b (diff) | |
| download | compcert-kvx-7c6ce18466ed1de58a0f99c785c777d63a9a6149.tar.gz compcert-kvx-7c6ce18466ed1de58a0f99c785c777d63a9a6149.zip | |
a bit of progress
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 11 |
1 files changed, 7 insertions, 4 deletions
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 := |