diff options
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 201 |
1 files changed, 120 insertions, 81 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 8b7f1190..75e00f67 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -145,18 +145,17 @@ Proof. exact peq. Defined. -Record equation := - mkequation - { eq_lhs : reg; - eq_op : sym_op; - eq_args : list reg }. +Inductive equation_or_condition := +| Equ : reg -> sym_op -> list reg -> equation_or_condition +| Cond : condition -> list reg -> equation_or_condition. Definition eq_dec_equation : - forall eq eq' : equation, {eq = eq'} + {eq <> eq'}. + forall eq eq' : equation_or_condition, {eq = eq'} + {eq <> eq'}. Proof. generalize peq. generalize eq_dec_sym_op. generalize eq_dec_args. + generalize eq_condition. decide equality. Defined. @@ -168,34 +167,42 @@ Definition add_i_j (i : reg) (j : eq_id) (m : Regmap.t PSet.t) := Definition add_ilist_j (ilist : list reg) (j : eq_id) (m : Regmap.t PSet.t) := List.fold_left (fun already i => add_i_j i j already) ilist m. -Definition get_reg_kills (eqs : PTree.t equation) : +Definition get_reg_kills (eqs : PTree.t equation_or_condition) : Regmap.t PSet.t := - PTree.fold (fun already (eqno : eq_id) (eq : equation) => - add_i_j (eq_lhs eq) eqno - (add_ilist_j (eq_args eq) eqno already)) eqs + PTree.fold (fun already (eqno : eq_id) (eq_cond : equation_or_condition) => + match eq_cond with + | Equ lhs sop args => + add_i_j lhs eqno + (add_ilist_j args eqno already) + | Cond cond args => add_ilist_j args eqno already + end) eqs (PMap.init PSet.empty). -Definition eq_depends_on_mem eq := - match eq_op eq with - | SLoad _ _ => true - | SOp op => op_depends_on_memory op +Definition eq_cond_depends_on_mem eq_cond := + match eq_cond with + | Equ lhs sop args => + match sop with + | SLoad _ _ => true + | SOp op => op_depends_on_memory op + end + | Cond cond args => cond_depends_on_memory cond end. -Definition eq_depends_on_store eq := - match eq_op eq with - | SLoad _ _ => true - | SOp op => false +Definition eq_cond_depends_on_store eq_cond := + match eq_cond with + | Equ _ (SLoad _ _) _ => true + | _ => false end. -Definition get_mem_kills (eqs : PTree.t equation) : PSet.t := - PTree.fold (fun already (eqno : eq_id) (eq : equation) => - if eq_depends_on_mem eq +Definition get_mem_kills (eqs : PTree.t equation_or_condition) : PSet.t := + PTree.fold (fun already (eqno : eq_id) (eq : equation_or_condition) => + if eq_cond_depends_on_mem eq then PSet.add eqno already else already) eqs PSet.empty. -Definition get_store_kills (eqs : PTree.t equation) : PSet.t := - PTree.fold (fun already (eqno : eq_id) (eq : equation) => - if eq_depends_on_store eq +Definition get_store_kills (eqs : PTree.t equation_or_condition) : PSet.t := + PTree.fold (fun already (eqno : eq_id) (eq : equation_or_condition) => + if eq_cond_depends_on_store eq then PSet.add eqno already else already) eqs PSet.empty. @@ -215,21 +222,25 @@ Proof. - right; congruence. Qed. -Definition get_moves (eqs : PTree.t equation) : +Definition get_moves (eqs : PTree.t equation_or_condition) : Regmap.t PSet.t := - PTree.fold (fun already (eqno : eq_id) (eq : equation) => - if is_smove (eq_op eq) - then add_i_j (eq_lhs eq) eqno already - else already) eqs (PMap.init PSet.empty). + PTree.fold (fun already (eqno : eq_id) (eq : equation_or_condition) => + match eq with + | Equ lhs sop args => + if is_smove sop + then add_i_j lhs eqno already + else already + | _ => already + end) eqs (PMap.init PSet.empty). Record eq_context := mkeqcontext - { eq_catalog : eq_id -> option equation; - eq_find_oracle : node -> equation -> option eq_id; - eq_rhs_oracle : node -> sym_op -> list reg -> PSet.t; - eq_kill_reg : reg -> PSet.t; - eq_kill_mem : unit -> PSet.t; - eq_kill_store : unit -> PSet.t; - eq_moves : reg -> PSet.t }. + { eq_catalog : eq_id -> option equation_or_condition; + eq_find_oracle : node -> equation_or_condition -> option eq_id; + eq_rhs_oracle : node -> sym_op -> list reg -> PSet.t; + eq_kill_reg : reg -> PSet.t; + eq_kill_mem : unit -> PSet.t; + eq_kill_store : unit -> PSet.t; + eq_moves : reg -> PSet.t }. Section OPERATIONS. Context {ctx : eq_context}. @@ -251,10 +262,10 @@ Section OPERATIONS. | None => x | Some eqno => match eq_catalog ctx eqno with - | Some eq => - if is_smove (eq_op eq) && peq x (eq_lhs eq) + | Some (Equ lhs sop args) => + if is_smove sop && peq x lhs then - match eq_args eq with + match args with | src::nil => src | _ => x end @@ -269,7 +280,7 @@ Section OPERATIONS. Section PER_NODE. Variable no : node. - Definition eq_find (eq : equation) := + Definition eq_find (eq : equation_or_condition) := match eq_find_oracle ctx no eq with | Some id => match eq_catalog ctx id with @@ -279,25 +290,29 @@ Section OPERATIONS. | None => None end. + Definition is_condition_present + (rel : RELATION.t) (cond : condition) (args : list reg) := + match eq_find (Cond cond args) with + | Some id => PSet.contains rel id + | None => false + end. Definition rhs_find (sop : sym_op) (args : list reg) (rel : RELATION.t) : option reg := match pick_source (PSet.elements (PSet.inter (eq_rhs_oracle ctx no sop args) rel)) with | None => None | Some src => match eq_catalog ctx src with - | None => None - | Some eq => - if eq_dec_sym_op sop (eq_op eq) && eq_dec_args args (eq_args eq) - then Some (eq_lhs eq) + | Some (Equ eq_lhs eq_sop eq_args) => + if eq_dec_sym_op sop eq_sop && eq_dec_args args eq_args + then Some eq_lhs else None + | _ => None end end. Definition oper2 (dst : reg) (op: sym_op)(args : list reg) (rel : RELATION.t) : RELATION.t := - match eq_find {| eq_lhs := dst; - eq_op := op; - eq_args:= args |} with + match eq_find (Equ dst op args) with | Some id => if PSet.contains rel id then rel @@ -316,9 +331,7 @@ Section OPERATIONS. if peq src dst then rel else - match eq_find {| eq_lhs := dst; - eq_op := SOp Omove; - eq_args:= src::nil |} with + match eq_find (Equ dst (SOp Omove) (src::nil)) with | Some eq_id => PSet.add eq_id (kill_reg dst rel) | None => kill_reg dst rel end. @@ -366,13 +379,13 @@ Section OPERATIONS. (PSet.filter (fun eqno => match eq_catalog ctx eqno with - | None => false - | Some eq => - match eq_op eq with + | Some (Equ eq_lhs eq_sop eq_args) => + match eq_sop with | SOp op => true | SLoad chunk' addr' => - may_overlap chunk addr args chunk' addr' (eq_args eq) + may_overlap chunk addr args chunk' addr' eq_args end + | _ => false end) (PSet.inter rel (eq_kill_store ctx tt))). @@ -391,9 +404,7 @@ Section OPERATIONS. let rel' := store2 chunk addr args src rel in if loadv_storev_compatible_type chunk ty then - match eq_find {| eq_lhs := src; - eq_op := SLoad chunk addr; - eq_args:= args |} with + match eq_find (Equ src (SLoad chunk addr) args) with | Some id => PSet.add id rel' | None => rel' end @@ -450,28 +461,55 @@ Section OPERATIONS. | _ => rel end. - Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : RB.t := + Definition apply_cond1 cond args (rel : RELATION.t) : RB.t := + match eq_find (Cond (negate_condition cond) args) with + | Some eq_id => + if PSet.contains rel eq_id + then RB.bot + else Some rel + | None => Some rel + end. + + Definition apply_cond0 cond args (rel : RELATION.t) : RELATION.t := + match eq_find (Cond cond args) with + | Some eq_id => PSet.add eq_id rel + | None => rel + end. + + Definition apply_cond cond args (rel : RELATION.t) : RB.t := + if Compopts.optim_CSE3_conditions tt + then + match apply_cond1 cond args rel with + | Some rel => Some (apply_cond0 cond args rel) + | None => RB.bot + end + else Some rel. + + Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : list (node * RB.t) := match instr with - | Inop _ - | Icond _ _ _ _ _ - | Ijumptable _ _ => Some rel - | Istore chunk addr args src _ => - Some (store tenv chunk addr args src rel) - | Iop op args dst _ => Some (oper dst (SOp op) args rel) - | Iload trap chunk addr args dst _ => Some (oper dst (SLoad chunk addr) args rel) - | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel)) - | Ibuiltin ef _ res _ => Some (kill_builtin_res res (apply_external_call ef rel)) - | Itailcall _ _ _ | Ireturn _ => RB.bot + | Inop pc' => (pc', (Some rel))::nil + | Icond cond args ifso ifnot _ => + (ifso, (apply_cond cond args rel)):: + (ifnot, (apply_cond (negate_condition cond) args rel))::nil + | Ijumptable _ targets => List.map (fun pc' => (pc', (Some rel))) targets + | Istore chunk addr args src pc' => + (pc', (Some (store tenv chunk addr args src rel)))::nil + | Iop op args dst pc' => (pc', (Some (oper dst (SOp op) args rel)))::nil + | Iload trap chunk addr args dst pc' => (pc', (Some (oper dst (SLoad chunk addr) args rel)))::nil + | Icall _ _ _ dst pc' => (pc', (Some (kill_reg dst (kill_mem rel))))::nil + | Ibuiltin ef _ res pc' => (pc', (Some (kill_builtin_res res (apply_external_call ef rel))))::nil + | Itailcall _ _ _ | Ireturn _ => nil end. End PER_NODE. -Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) : RB.t := - match ro with - | None => None - | Some x => - match code ! pc with - | None => RB.bot - | Some instr => apply_instr pc tenv instr x +Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) : + list (node * RB.t) := + match code ! pc with + | None => nil + | Some instr => + match ro with + | None => List.map (fun pc' => (pc', RB.bot)) (successors_instr instr) + | Some x => apply_instr pc tenv instr x end end. @@ -493,24 +531,25 @@ Definition check_inductiveness (fn : RTL.function) (tenv: typing_env) (inv: inva match PMap.get pc inv with | None => true | Some rel => - let rel' := apply_instr pc tenv instr rel in List.forallb - (fun pc' => relb_leb rel' (PMap.get pc' inv)) - (RTL.successors_instr instr) + (fun szz => + relb_leb (snd szz) (PMap.get (fst szz) inv)) + (apply_instr pc tenv instr rel) end). +(* No longer used. Incompatible with transfer functions that yield a different result depending on the successor. Definition internal_analysis (tenv : typing_env) (f : RTL.function) : option invariants := DS.fixpoint (RTL.fn_code f) RTL.successors_instr (apply_instr' tenv (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top). - +*) End OPERATIONS. Record analysis_hints := mkanalysis_hints - { hint_eq_catalog : PTree.t equation; - hint_eq_find_oracle : node -> equation -> option eq_id; + { hint_eq_catalog : PTree.t equation_or_condition; + hint_eq_find_oracle : node -> equation_or_condition -> option eq_id; hint_eq_rhs_oracle : node -> sym_op -> list reg -> PSet.t }. Definition context_from_hints (hints : analysis_hints) := |