diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 15:30:57 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 15:30:57 +0100 |
| commit | 8c8e6a0528a91420e399ae84ccf293c0d8be285f (patch) | |
| tree | 5052d78f49984466103ab1cb41c5354779134f1f /backend/CSE3analysis.v | |
| parent | d5bbfed2c8a0a208cf365abb1df249c9d91ff8e4 (diff) | |
| download | compcert-kvx-8c8e6a0528a91420e399ae84ccf293c0d8be285f.tar.gz compcert-kvx-8c8e6a0528a91420e399ae84ccf293c0d8be285f.zip | |
move sound
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 7357a811..cdda2cb7 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -236,6 +236,23 @@ Section OPERATIONS. then kill_reg dst rel else oper2 dst op args rel. + + Definition move (src dst : reg) (rel : RELATION.t) : RELATION.t := + 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. + + (* + Definition oper (dst : reg) (op: sym_op) (args : list reg) + (rel : RELATION.t) : RELATION.t := + match find_op rel op (forward_move_l rel args) with + | Some r => move r dst rel + | None => oper1 op dst args rel + end. +*) End PER_NODE. End OPERATIONS. |