passage à Equ

1 files changed, 35 insertions, 22 deletions

diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml
index e038331c..f50f4a46 100644
--- a/backend/CSE3analysisaux.ml
+++ b/backend/CSE3analysisaux.ml
@@ -16,8 +16,12 @@ open HashedSet
 open Camlcoq
 open Coqlib
    
-let flatten_eq eq =
-  ((P.to_int eq.eq_lhs), eq.eq_op, List.map P.to_int eq.eq_args);;
+type flattened_equation_or_condition =
+  | Flat_equ of int * sym_op * int list;;
+
+let flatten_eq = function
+  | Equ(lhs, sop, args) ->
+     Flat_equ((P.to_int lhs), sop, (List.map P.to_int args));;
 
 let imp_add_i_j s i j =
   s := PMap.set i (PSet.add j (PMap.get i !s)) !s;;
@@ -58,9 +62,11 @@ let pp_rhs oc (sop, args) =
        (PrintAST.name_of_chunk chunk)
          (PrintOp.print_addressing PrintRTL.reg) (addr, args);;
 
-let pp_eq oc eq =
-  Printf.fprintf oc "x%d = %a" (P.to_int eq.eq_lhs)
-    pp_rhs (eq.eq_op, eq.eq_args);;
+let pp_eq oc eq_cond =
+  match eq_cond with
+  | Equ(lhs, sop, args) ->
+     Printf.fprintf oc "x%d = %a" (P.to_int lhs)
+       pp_rhs (sop, args);;
 
 let pp_P oc x = Printf.fprintf oc "%d" (P.to_int x)
               
@@ -68,8 +74,9 @@ let pp_option pp oc = function
   | None -> output_string oc "none"
   | Some x -> pp oc x;;
 
-let is_trivial eq =
-  (eq.eq_op = SOp Op.Omove) && (eq.eq_args = [eq.eq_lhs]);;
+let is_trivial = function
+  | Equ(lhs, (SOp Op.Omove), [lhs']) -> lhs=lhs'
+  | _ -> false;;
 
 let rec pp_list separator pp_item chan = function
   | [] -> ()
@@ -86,7 +93,9 @@ let pp_equation hints chan x =
   match PTree.get x hints.hint_eq_catalog with
   | None -> output_string chan "???"
   | Some eq ->
-     print_eq chan  (P.to_int eq.eq_lhs, eq.eq_op, List.map P.to_int eq.eq_args);;
+     match eq with
+       Equ(lhs, sop, args) ->
+       print_eq chan  (P.to_int lhs, sop, List.map P.to_int args);;
 
 let pp_relation hints chan rel =
   pp_set "; " (pp_equation hints) chan rel;;
@@ -194,7 +203,7 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
             (P.to_int node) pp_rhs (sop, args) pp_intset o);
     o in
   let mutating_eq_find_oracle node eq : P.t option =
-    let (flat_eq_lhs, flat_eq_op, flat_eq_args) as flat_eq = flatten_eq eq in
+    let flat_eq = flatten_eq eq in
     let o =
     match Hashtbl.find_opt eq_table flat_eq with
     | Some x ->
@@ -207,21 +216,25 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
        begin
          Hashtbl.add eq_table flat_eq coq_id;
          (cur_catalog := PTree.set coq_id eq !cur_catalog);
-         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));
-         List.iter
-           (fun reg -> imp_add_i_j cur_kill_reg reg coq_id)
-           (eq.eq_lhs :: eq.eq_args);
-         (if eq_depends_on_mem eq
+         (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)));
+         (match eq with
+          | Equ(lhs, sop, args) ->
+             List.iter
+               (fun reg -> imp_add_i_j cur_kill_reg reg coq_id)
+               (lhs :: args);
+             match sop, args with
+             | (SOp Op.Omove), [rhs] -> imp_add_i_j cur_moves lhs coq_id
+             | _, _ -> ());
+         (if eq_cond_depends_on_mem eq
           then cur_kill_mem := PSet.add coq_id !cur_kill_mem);
-         (if eq_depends_on_store eq
+         (if eq_cond_depends_on_store eq
           then cur_kill_store := PSet.add coq_id !cur_kill_store);
-         (match eq.eq_op, eq.eq_args with
-          | (SOp Op.Omove), [rhs] -> imp_add_i_j cur_moves eq.eq_lhs coq_id
-          | _, _ -> ());
          Some coq_id
        end
     in