diff options
Diffstat (limited to 'backend/CSE3analysis.v')
-rw-r--r-- | backend/CSE3analysis.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 5de4ba80..41fa67f6 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -153,6 +153,7 @@ Definition get_moves (eqs : PTree.t equation) : Record eq_context := mkeqcontext { eq_catalog : eq_id -> option equation; eq_find_oracle : node -> equation -> option eq_id; + eq_rhs_oracle : node -> sym_op -> list reg -> PSet.t; eq_kill_reg : reg -> PSet.t; eq_kill_mem : PSet.t; eq_moves : reg -> PSet.t }. @@ -201,6 +202,20 @@ Section OPERATIONS. end | None => None end. + + + Definition rhs_find (no : node) (sop : sym_op) (args : list reg) (rel : RELATION.t) : option reg := + match pick_source (PSet.elements (PSet.inter (eq_rhs_oracle ctx no sop args) rel)) with + | None => None + | Some src => + match eq_catalog ctx src with + | None => None + | Some eq => + if eq_dec_sym_op sop (eq_op eq) && eq_dec_args args (eq_args eq) + then Some (eq_lhs eq) + else None + end + end. End OPERATIONS. Definition totoro := RELATION.lub. |