From d30d56425a8cf73852f7acafe21458be6c787ebc Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 26 Nov 2020 13:54:36 +0100 Subject: passage à Equ MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- backend/CSE3analysisaux.ml | 57 ++++++++++++++++++++++++++++------------------ 1 file changed, 35 insertions(+), 22 deletions(-) (limited to 'backend/CSE3analysisaux.ml') 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 -- cgit