diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-31 09:23:53 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-31 09:23:53 +0100 |
| commit | 60e28f582b37d4080686992ea114857f75cfe6c2 (patch) | |
| tree | 655ceff73b68c79ea382207b4a872f330ec83941 /backend/CSE3analysis.v | |
| parent | 9cf81f29d1d1b1be3575414fceec2a03378918ed (diff) | |
| download | compcert-kvx-60e28f582b37d4080686992ea114857f75cfe6c2.tar.gz compcert-kvx-60e28f582b37d4080686992ea114857f75cfe6c2.zip | |
seems to work better
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 7316c9a9..5eb92a82 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -282,12 +282,14 @@ Section OPERATIONS. Definition oper2 (dst : reg) (op: sym_op)(args : list reg) (rel : RELATION.t) : RELATION.t := - let rel' := kill_reg dst rel in match eq_find {| eq_lhs := dst; eq_op := op; eq_args:= args |} with - | Some id => PSet.add id rel' - | None => rel' + | Some id => + if PSet.contains rel id + then rel + else PSet.add id (kill_reg dst rel) + | None => kill_reg dst rel end. Definition oper1 (dst : reg) (op: sym_op) (args : list reg) |