ajouté Cond, tout passe

1 files changed, 25 insertions, 9 deletions

diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml
index f50f4a46..731212eb 100644
--- a/backend/CSE3analysisaux.ml
+++ b/backend/CSE3analysisaux.ml
@@ -17,11 +17,14 @@ open Camlcoq
 open Coqlib
    
 type flattened_equation_or_condition =
-  | Flat_equ of int * sym_op * int list;;
+  | Flat_equ of int * sym_op * int list
+  | Flat_cond of Op.condition * int list;;
 
 let flatten_eq = function
   | Equ(lhs, sop, args) ->
-     Flat_equ((P.to_int lhs), sop, (List.map P.to_int args));;
+     Flat_equ((P.to_int lhs), sop, (List.map P.to_int args))
+  | Cond(cond, args) ->
+     Flat_cond(cond, (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;;
@@ -49,6 +52,9 @@ let print_eq channel (lhs, sop, args) =
      Printf.printf "%a = %s @ %a" print_reg lhs (string_of_chunk chunk)
        (PrintOp.print_addressing print_reg) (addr, args);;
 
+let print_cond channel (cond, args) =
+  Printf.printf "cond %a" (PrintOp.print_condition print_reg) (cond, args);;
+
 let pp_intset oc s =
   Printf.fprintf oc "{ ";
   List.iter (fun i -> Printf.fprintf oc "%d; " (P.to_int i)) (PSet.elements s);
@@ -66,7 +72,10 @@ 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);;
+       pp_rhs (sop, args)
+  | Cond(cond, args) ->
+     Printf.fprintf oc "cond %a"
+       (PrintOp.print_condition PrintRTL.reg) (cond, args);;
 
 let pp_P oc x = Printf.fprintf oc "%d" (P.to_int x)
               
@@ -94,8 +103,10 @@ let pp_equation hints chan x =
   | None -> output_string chan "???"
   | Some eq ->
      match eq with
-       Equ(lhs, sop, args) ->
-       print_eq chan  (P.to_int lhs, sop, List.map P.to_int args);;
+     | Equ(lhs, sop, args) ->
+        print_eq chan  (P.to_int lhs, sop, List.map P.to_int args)
+     | Cond(cond, args) ->
+        print_cond chan (cond, List.map P.to_int args);;
 
 let pp_relation hints chan rel =
   pp_set "; " (pp_equation hints) chan rel;;
@@ -222,15 +233,20 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
                (PSet.add coq_id
                   (match Hashtbl.find_opt rhs_table (flat_eq_op, flat_eq_args) with
                    | None -> PSet.empty
-                   | Some s -> s)));
+                   | Some s -> s))
+          | Flat_cond _ -> ());
          (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
-             | _, _ -> ());
+             (match sop, args with
+              | (SOp Op.Omove), [rhs] -> imp_add_i_j cur_moves lhs coq_id
+              | _, _ -> ())
+          | Cond(cond, args) ->
+             List.iter
+               (fun reg -> imp_add_i_j cur_kill_reg reg coq_id) args
+         );
          (if eq_cond_depends_on_mem eq
           then cur_kill_mem := PSet.add coq_id !cur_kill_mem);
          (if eq_cond_depends_on_store eq