diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 09:11:12 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 09:11:12 +0100 |
| commit | 9cf4ca7760982b40e5721b2d6510eae0ced248a8 (patch) | |
| tree | 78bb00e9705d690f4b567268330c8f47f0a2751d /backend/CSE3analysis.v | |
| parent | 33c7fc589ebbbd0ebda9739c479bbd9ee7e526db (diff) | |
| download | compcert-kvx-9cf4ca7760982b40e5721b2d6510eae0ced248a8.tar.gz compcert-kvx-9cf4ca7760982b40e5721b2d6510eae0ced248a8.zip | |
forward_move_l
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index bbe76f75..c88f06fa 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -128,14 +128,18 @@ Definition get_moves (eqs : PTree.t equation) : Record eq_context := mkeqcontext { eq_catalog : node -> option equation; - eq_kills : reg -> PSet.t; + eq_kill_reg : reg -> PSet.t; + eq_kill_mem : PSet.t; eq_moves : reg -> PSet.t }. Section OPERATIONS. Context {ctx : eq_context}. Definition kill_reg (r : reg) (rel : RELATION.t) : RELATION.t := - PSet.subtract rel (eq_kills ctx r). + PSet.subtract rel (eq_kill_reg ctx r). + + Definition kill_mem (rel : RELATION.t) : RELATION.t := + PSet.subtract rel (eq_kill_mem ctx). Definition pick_source (l : list reg) := (* todo: take min? *) match l with @@ -159,7 +163,9 @@ Section OPERATIONS. | _ => x end end. - + + Definition forward_move_l (rel : RELATION.t) : list reg -> list reg := + List.map (forward_move rel). End OPERATIONS. Definition totoro := RELATION.lub. |