diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-21 18:04:43 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-21 18:04:43 +0200 |
| commit | 14388a6be6cf7aac50f2af4ff29fe9726ad83435 (patch) | |
| tree | 4d6c2816957e1bdbe262a59ed60cfb72dd1aa3c6 /backend/CSE3analysis.v | |
| parent | d10bc429a5c08a25471e3f65e328f5cee12e4542 (diff) | |
| download | compcert-kvx-14388a6be6cf7aac50f2af4ff29fe9726ad83435.tar.gz compcert-kvx-14388a6be6cf7aac50f2af4ff29fe9726ad83435.zip | |
improvement in precision
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index d3d1c043..b495371d 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -64,6 +64,7 @@ Module RELATION <: SEMILATTICE_WITHOUT_BOTTOM. Qed. Definition lub := PSet.inter. + Definition glb := PSet.union. Lemma ge_lub_left: forall x y, ge (lub x y) x. Proof. @@ -274,7 +275,8 @@ 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 => move r dst rel + | Some r => RELATION.glb (move r dst rel) + (oper1 dst op args rel) | None => oper1 dst op args rel end. |