begin implementing cond table

1 files changed, 13 insertions, 6 deletions

diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml
index 731212eb..e8964090 100644
--- a/backend/CSE3analysisaux.ml
+++ b/backend/CSE3analysisaux.ml
@@ -186,12 +186,20 @@ let refine_analysis ctx tenv
   refine_invariants
     (List.map fst (PTree.elements f.RTL.fn_code))
     f.RTL.fn_entrypoint succ_f pred_f tfr invariants0;;
+
+let add_to_set_in_table table key item =
+  Hashtbl.add table key
+    (PSet.add item
+       (match Hashtbl.find_opt table key with
+        | None -> PSet.empty
+        | Some s -> s));;
   
 let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
   let cur_eq_id = ref 0
   and cur_catalog = ref PTree.empty
   and eq_table = Hashtbl.create 100
   and rhs_table = Hashtbl.create 100
+  and cond_table = Hashtbl.create 100
   and cur_kill_reg = ref (PMap.init PSet.empty)
   and cur_kill_mem = ref PSet.empty
   and cur_kill_store = ref PSet.empty
@@ -229,12 +237,11 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
          (cur_catalog := PTree.set coq_id eq !cur_catalog);
          (match flat_eq with
           | Flat_equ(flat_eq_lhs, flat_eq_op, flat_eq_args) ->
-             Hashtbl.add rhs_table (flat_eq_op, flat_eq_args)
-               (PSet.add coq_id
-                  (match Hashtbl.find_opt rhs_table (flat_eq_op, flat_eq_args) with
-                   | None -> PSet.empty
-                   | Some s -> s))
-          | Flat_cond _ -> ());
+             add_to_set_in_table rhs_table
+               (flat_eq_op, flat_eq_args) coq_id
+          | Flat_cond(flat_eq_cond, flat_eq_args) ->
+             add_to_set_in_table cond_table
+               (flat_eq_cond, flat_eq_args) coq_id);
          (match eq with
           | Equ(lhs, sop, args) ->
              List.iter