From d09c509f8d1bd8335ebedbe260320bb43c5a2723 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 26 Nov 2020 15:11:15 +0100 Subject: ajouté Cond, tout passe MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- backend/CSE3analysisaux.ml | 34 +++++++++++++++++++++++++--------- 1 file changed, 25 insertions(+), 9 deletions(-) (limited to 'backend/CSE3analysisaux.ml') 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 -- cgit