diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-23 12:55:35 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-23 12:55:35 +0200 |
| commit | 67290187fff3f813412059c6bfed69015c95c890 (patch) | |
| tree | bd02925b22e8ad230f23380069412551b57ca72a /backend/CSE3analysis.v | |
| parent | a4e86b9131f39648e6e54f2ae5c498be0c2e5f41 (diff) | |
| parent | 2316b5dc954b4047f3f48c61e7f4e34deb729efe (diff) | |
| download | compcert-kvx-67290187fff3f813412059c6bfed69015c95c890.tar.gz compcert-kvx-67290187fff3f813412059c6bfed69015c95c890.zip | |
Merge remote-tracking branch 'origin/mppa-cse3' into mppa-licm
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 19 |
1 files changed, 14 insertions, 5 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index b495371d..91064a5d 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -274,11 +274,20 @@ Section OPERATIONS. Definition oper (dst : reg) (op: sym_op) (args : list reg) (rel : RELATION.t) : RELATION.t := - match rhs_find op (forward_move_l rel args) rel with - | Some r => RELATION.glb (move r dst rel) - (oper1 dst op args rel) - | None => oper1 dst op args rel - end. + if is_smove op + then + match args with + | src::nil => + move (forward_move rel src) dst rel + | _ => kill_reg dst rel + end + else + let args' := forward_move_l rel args in + match rhs_find op args' rel with + | Some r => (* FIXME RELATION.glb ( *) move r dst rel (* ) + (oper1 dst op args' rel) *) + | None => oper1 dst op args' rel + end. Definition clever_kill_store (chunk : memory_chunk) (addr: addressing) (args : list reg) |