diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 09:45:34 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 09:45:34 +0100 |
| commit | 0892b99d00aac6ad9f7467f1383fe5dc1b45e94f (patch) | |
| tree | f3415a55149b8ab2af86c08b2c9bfee699b835ab /backend/CSE3analysis.v | |
| parent | 9cf4ca7760982b40e5721b2d6510eae0ced248a8 (diff) | |
| download | compcert-kvx-0892b99d00aac6ad9f7467f1383fe5dc1b45e94f.tar.gz compcert-kvx-0892b99d00aac6ad9f7467f1383fe5dc1b45e94f.zip | |
eq_find_sound
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 37 |
1 files changed, 36 insertions, 1 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index c88f06fa..5de4ba80 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -2,6 +2,7 @@ Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Memory Registers Op RTL Maps CSE2deps. Require Import HashedSet. +Require List. Module RELATION <: SEMILATTICE_WITHOUT_BOTTOM. Definition t := PSet.t. @@ -82,12 +83,35 @@ Inductive sym_op : Type := | SOp : operation -> sym_op | SLoad : memory_chunk -> addressing -> sym_op. +Definition eq_dec_sym_op : forall s s' : sym_op, {s = s'} + {s <> s'}. +Proof. + generalize eq_operation. + generalize eq_addressing. + generalize chunk_eq. + decide equality. +Defined. + +Definition eq_dec_args : forall l l' : list reg, { l = l' } + { l <> l' }. +Proof. + apply List.list_eq_dec. + exact peq. +Defined. + Record equation := mkequation { eq_lhs : reg; eq_op : sym_op; eq_args : list reg }. +Definition eq_dec_equation : + forall eq eq' : equation, {eq = eq'} + {eq <> eq'}. +Proof. + generalize peq. + generalize eq_dec_sym_op. + generalize eq_dec_args. + decide equality. +Defined. + Definition eq_id := node. Definition add_i_j (i : reg) (j : eq_id) (m : Regmap.t PSet.t) := @@ -127,7 +151,8 @@ Definition get_moves (eqs : PTree.t equation) : else already) eqs (PMap.init PSet.empty). Record eq_context := mkeqcontext - { eq_catalog : node -> option equation; + { eq_catalog : eq_id -> option equation; + eq_find_oracle : node -> equation -> option eq_id; eq_kill_reg : reg -> PSet.t; eq_kill_mem : PSet.t; eq_moves : reg -> PSet.t }. @@ -166,6 +191,16 @@ Section OPERATIONS. Definition forward_move_l (rel : RELATION.t) : list reg -> list reg := List.map (forward_move rel). + + Definition eq_find (no : node) (eq : equation) := + match eq_find_oracle ctx no eq with + | Some id => + match eq_catalog ctx id with + | Some eq' => if eq_dec_equation eq eq' then Some id else None + | None => None + end + | None => None + end. End OPERATIONS. Definition totoro := RELATION.lub. |