diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-27 15:21:11 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-27 15:21:11 +0100 |
| commit | f59c540aa7cf85c89ee0cb07c20374c8ad76a46c (patch) | |
| tree | de0849bc8c130598ce39ac472bc90f282ba4ab7b /backend/CSE3analysis.v | |
| parent | 9646053ba537d24f973e104aebd80500381ce11d (diff) | |
| download | compcert-kvx-f59c540aa7cf85c89ee0cb07c20374c8ad76a46c.tar.gz compcert-kvx-f59c540aa7cf85c89ee0cb07c20374c8ad76a46c.zip | |
new CSE3
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 38 |
1 files changed, 17 insertions, 21 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 7316c9a9..cd7e3d84 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) @@ -307,12 +309,6 @@ Section OPERATIONS. | 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 := @@ -324,18 +320,18 @@ Section OPERATIONS. | _ => kill_reg dst rel end else - 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. + 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) + (RELATION.glb (oper1 dst op args' rel) + (oper1 dst op args rel)) + else RELATION.glb (oper1 dst op args' rel) + (oper1 dst op args rel) + | None => RELATION.glb (oper1 dst op args' rel) + (oper1 dst op args rel) + end. Definition clever_kill_store (chunk : memory_chunk) (addr: addressing) (args : list reg) |