diff options
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. |