diff options
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 566 |
1 files changed, 566 insertions, 0 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v new file mode 100644 index 00000000..9a6c9c0d --- /dev/null +++ b/backend/CSE3analysis.v @@ -0,0 +1,566 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL Maps CSE2deps. +Require Import HashedSet. +Require List Compopts. + +Definition typing_env := reg -> typ. + +Definition loadv_storev_compatible_type + (chunk : memory_chunk) (ty : typ) : bool := + match chunk, ty with + | Mint32, Tint + | Mint64, Tlong + | Mfloat32, Tsingle + | Mfloat64, Tfloat => true + | _, _ => false + end. + +Module RELATION <: SEMILATTICE_WITHOUT_BOTTOM. + Definition t := PSet.t. + Definition eq (x : t) (y : t) := x = y. + + Lemma eq_refl: forall x, eq x x. + Proof. + unfold eq. trivial. + Qed. + + Lemma eq_sym: forall x y, eq x y -> eq y x. + Proof. + unfold eq. congruence. + Qed. + + Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z. + Proof. + unfold eq. congruence. + Qed. + + Definition beq (x y : t) := if PSet.eq x y then true else false. + + Lemma beq_correct: forall x y, beq x y = true -> eq x y. + Proof. + unfold beq. + intros. + destruct PSet.eq; congruence. + Qed. + + Definition ge (x y : t) := (PSet.is_subset x y) = true. + + Lemma ge_refl: forall x y, eq x y -> ge x y. + Proof. + unfold eq, ge. + intros. + subst y. + apply PSet.is_subset_spec. + trivial. + Qed. + + Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. + Proof. + unfold ge. + intros. + rewrite PSet.is_subset_spec in *. + intuition. + Qed. + + Definition lub x y := + if Compopts.optim_CSE3_across_merges tt + then PSet.inter x y + else + if PSet.eq x y + then x + else PSet.empty. + + Definition glb := PSet.union. + + Lemma ge_lub_left: forall x y, ge (lub x y) x. + Proof. + unfold ge, lub. + intros. + destruct (Compopts.optim_CSE3_across_merges tt). + - apply PSet.is_subset_spec. + intro. + rewrite PSet.ginter. + rewrite andb_true_iff. + intuition. + - apply PSet.is_subset_spec. + intro. + destruct (PSet.eq x y). + + auto. + + rewrite PSet.gempty. + discriminate. + Qed. + + Lemma ge_lub_right: forall x y, ge (lub x y) y. + Proof. + unfold ge, lub. + intros. + destruct (Compopts.optim_CSE3_across_merges tt). + - apply PSet.is_subset_spec. + intro. + rewrite PSet.ginter. + rewrite andb_true_iff. + intuition. + - apply PSet.is_subset_spec. + intro. + destruct (PSet.eq x y). + + subst. auto. + + rewrite PSet.gempty. + discriminate. + Qed. + + Definition top := PSet.empty. +End RELATION. + +Module RB := ADD_BOTTOM(RELATION). +Module DS := Dataflow_Solver(RB)(NodeSetForward). + +Inductive sym_op : Type := +| SOp : operation -> sym_op +| SLoad : memory_chunk -> addressing -> sym_op. + +Definition eq_dec_sym_op : forall s s' : sym_op, {s = s'} + {s <> s'}. +Proof. + generalize eq_operation. + generalize eq_addressing. + generalize chunk_eq. + decide equality. +Defined. + +Definition eq_dec_args : forall l l' : list reg, { l = l' } + { l <> l' }. +Proof. + apply List.list_eq_dec. + exact peq. +Defined. + +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_or_condition, {eq = eq'} + {eq <> eq'}. +Proof. + generalize peq. + generalize eq_dec_sym_op. + generalize eq_dec_args. + generalize eq_condition. + decide equality. +Defined. + +Definition eq_id := node. + +Definition add_i_j (i : reg) (j : eq_id) (m : Regmap.t PSet.t) := + Regmap.set i (PSet.add j (Regmap.get i m)) m. + +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_or_condition) : + Regmap.t PSet.t := + 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_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_cond_depends_on_store eq_cond := + match eq_cond with + | Equ _ (SLoad _ _) _ => true + | _ => false + end. + +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_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. + +Definition is_move (op : operation) : + { op = Omove } + { op <> Omove }. +Proof. + destruct op; try (right ; congruence). + left; trivial. +Qed. + +Definition is_smove (sop : sym_op) : + { sop = SOp Omove } + { sop <> SOp Omove }. +Proof. + destruct sop; try (right ; congruence). + destruct (is_move o). + - left; congruence. + - right; congruence. +Qed. + +Definition get_moves (eqs : PTree.t equation_or_condition) : + Regmap.t PSet.t := + 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_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}. + + Definition kill_reg (r : reg) (rel : RELATION.t) : RELATION.t := + PSet.subtract rel (eq_kill_reg ctx r). + + Definition kill_mem (rel : RELATION.t) : RELATION.t := + PSet.subtract rel (eq_kill_mem ctx tt). + + Definition pick_source (l : list reg) := (* todo: take min? *) + match l with + | h::t => Some h + | nil => None + end. + + Definition forward_move (rel : RELATION.t) (x : reg) : reg := + match pick_source (PSet.elements (PSet.inter rel (eq_moves ctx x))) with + | None => x + | Some eqno => + match eq_catalog ctx eqno with + | Some (Equ lhs sop args) => + if is_smove sop && peq x lhs + then + match args with + | src::nil => src + | _ => x + end + else x + | _ => x + end + end. + + Definition forward_move_l (rel : RELATION.t) : list reg -> list reg := + List.map (forward_move rel). + + Section PER_NODE. + Variable no : node. + + Definition eq_find (eq : equation_or_condition) := + match eq_find_oracle ctx no eq with + | Some id => + match eq_catalog ctx id with + | Some eq' => if eq_dec_equation eq eq' then Some id else None + | None => None + end + | 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 + | 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 (Equ dst op args) with + | Some id => + if PSet.contains rel id + then rel + else PSet.add id (kill_reg dst rel) + | None => kill_reg dst rel + end. + + Definition oper1 (dst : reg) (op: sym_op) (args : list reg) + (rel : RELATION.t) : RELATION.t := + if List.in_dec peq dst args + then kill_reg dst rel + else oper2 dst op args rel. + + + Definition move (src dst : reg) (rel : RELATION.t) : RELATION.t := + if peq src dst + then rel + else + 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. + + Definition is_trivial_sym_op sop := + match sop with + | SOp op => is_trivial_op op + | SLoad _ _ => false + end. + + Definition oper (dst : reg) (op: sym_op) (args : list reg) + (rel : RELATION.t) : RELATION.t := + if is_smove op + then + match args with + | src::nil => + move (forward_move rel src) dst rel + | _ => kill_reg dst rel + end + else + let args' := forward_move_l rel args in + match rhs_find op args rel with + | Some r => + if Compopts.optim_CSE3_glb tt + then RELATION.glb (move r dst rel) + (RELATION.glb + (oper1 dst op args rel) + (oper1 dst op args' rel)) + else RELATION.glb + (oper1 dst op args rel) + (oper1 dst op args' rel) + | None => RELATION.glb + (oper1 dst op args rel) + (oper1 dst op args' rel) + end. + + Definition kill_store (rel : RELATION.t) : RELATION.t := + PSet.subtract rel (eq_kill_store ctx tt). + + Definition clever_kill_store + (chunk : memory_chunk) (addr: addressing) (args : list reg) + (src : reg) + (rel : RELATION.t) : RELATION.t := + PSet.subtract rel + (PSet.filter + (fun eqno => + match eq_catalog ctx eqno 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 + end + | _ => false + end) + (PSet.inter rel (eq_kill_store ctx tt))). + + Definition store2 + (chunk : memory_chunk) (addr: addressing) (args : list reg) + (src : reg) + (rel : RELATION.t) : RELATION.t := + if Compopts.optim_CSE3_alias_analysis tt + then clever_kill_store chunk addr args src rel + else kill_store rel. + + Definition store1 + (chunk : memory_chunk) (addr: addressing) (args : list reg) + (src : reg) (ty: typ) + (rel : RELATION.t) : RELATION.t := + let rel' := store2 chunk addr args src rel in + if loadv_storev_compatible_type chunk ty + then + match eq_find (Equ src (SLoad chunk addr) args) with + | Some id => PSet.add id rel' + | None => rel' + end + else rel'. + + Definition store (tenv : typing_env) + (chunk : memory_chunk) (addr: addressing) (args : list reg) + (src : reg) + (rel : RELATION.t) : RELATION.t := + let args' := forward_move_l rel args in + let src' := forward_move rel src in + let tsrc := tenv src in + let tsrc' := tenv src' in + RELATION.glb + (RELATION.glb + (store1 chunk addr args src tsrc rel) + (store1 chunk addr args' src tsrc rel)) + (RELATION.glb + (store1 chunk addr args src' tsrc' rel) + (store1 chunk addr args' src' tsrc' rel)). + + Definition kill_builtin_res res rel := + match res with + | BR r => kill_reg r rel + | _ => rel + end. + + Definition apply_external_call ef (rel : RELATION.t) : RELATION.t := + match ef with + | EF_builtin name sg => + match Builtins.lookup_builtin_function name sg with + | Some bf => rel + | None => if Compopts.optim_CSE3_across_calls tt + then kill_mem rel + else RELATION.top + end + | EF_runtime name sg => + if Compopts.optim_CSE3_across_calls tt + then + match Builtins.lookup_builtin_function name sg with + | Some bf => rel + | None => kill_mem rel + end + else RELATION.top + | EF_malloc + | EF_external _ _ + | EF_free => + if Compopts.optim_CSE3_across_calls tt + then kill_mem rel + else RELATION.top + | EF_vstore _ + | EF_memcpy _ _ (* FIXME *) + | EF_inline_asm _ _ _ => kill_mem rel + | _ => rel + end. + + 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 := + match apply_cond1 cond args rel with + | Some rel => Some (apply_cond0 cond args rel) + | None => RB.bot + end. + + Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : list (node * RB.t) := + match instr with + | 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) : + 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. + +Definition invariants := PMap.t RB.t. + +Definition rel_leb (x y : RELATION.t) : bool := (PSet.is_subset y x). + +Definition relb_leb (x y : RB.t) : bool := + match x, y with + | None, _ => true + | (Some _), None => false + | (Some x), (Some y) => rel_leb x y + end. + +Definition check_inductiveness (fn : RTL.function) (tenv: typing_env) (inv: invariants) := + (RB.beq (Some RELATION.top) (PMap.get (fn_entrypoint fn) inv)) && + PTree_Properties.for_all (fn_code fn) + (fun pc instr => + match PMap.get pc inv with + | None => true + | Some rel => + List.forallb + (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_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) := + let eqs := hint_eq_catalog hints in + let reg_kills := get_reg_kills eqs in + let mem_kills := get_mem_kills eqs in + let store_kills := get_store_kills eqs in + let moves := get_moves eqs in + {| + eq_catalog := fun eq_id => PTree.get eq_id eqs; + eq_find_oracle := hint_eq_find_oracle hints ; + eq_rhs_oracle := hint_eq_rhs_oracle hints; + eq_kill_reg := fun reg => PMap.get reg reg_kills; + eq_kill_mem := fun _ => mem_kills; + eq_kill_store := fun _ => store_kills; + eq_moves := fun reg => PMap.get reg moves + |}. |