rhs_find_op_sound

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.