diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-09 17:10:01 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-09 17:10:01 +0100 |
| commit | 3f33a6e366b0c018690c2b3246eb303c5eb57f46 (patch) | |
| tree | c2f4509e526bdd83da42ca8d8c8af4076fdf3312 /backend/CSE3analysis.v | |
| parent | 3c34c386912e904b432c53e1dbb2b3dda3f8501f (diff) | |
| download | compcert-kvx-3f33a6e366b0c018690c2b3246eb303c5eb57f46.tar.gz compcert-kvx-3f33a6e366b0c018690c2b3246eb303c5eb57f46.zip | |
kill_reg_sound
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 257149b5..485b6067 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -88,7 +88,7 @@ Record equation := eq_op : sym_op; eq_args : list reg }. -Definition eq_id := positive. +Definition eq_id := node. Definition add_i_j (i : reg) (j : eq_id) (m : Regmap.t PSet.t) := Regmap.set i (PSet.add j (Regmap.get i m)) m. @@ -103,4 +103,15 @@ Definition get_kills (eqs : PTree.t equation) : (add_ilist_j (eq_args eq) eqno already)) eqs (PMap.init PSet.empty). +Record eq_context := mkeqcontext + { eq_catalog : node -> option equation; + eq_kills : 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). +End OPERATIONS. + Definition totoro := RELATION.lub. |