diff options
Diffstat (limited to 'backend/CSE3analysis.v')
-rw-r--r-- | backend/CSE3analysis.v | 485 |
1 files changed, 485 insertions, 0 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v new file mode 100644 index 00000000..ade79c28 --- /dev/null +++ b/backend/CSE3analysis.v @@ -0,0 +1,485 @@ +(* *************************************************************) +(* *) +(* 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. + +Record equation := + mkequation + { eq_lhs : reg; + eq_op : sym_op; + eq_args : list reg }. + +Definition eq_dec_equation : + forall eq eq' : equation, {eq = eq'} + {eq <> eq'}. +Proof. + generalize peq. + generalize eq_dec_sym_op. + generalize eq_dec_args. + 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) : + 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 + (PMap.init PSet.empty). + +Definition eq_depends_on_mem eq := + match eq_op eq with + | SLoad _ _ => true + | SOp op => op_depends_on_memory op + 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 + 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) : + 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). + +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_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 eq => + if is_smove (eq_op eq) && peq x (eq_lhs eq) + then + match eq_args eq 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) := + 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 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) + else None + end + end. + + Definition oper2 (dst : reg) (op: sym_op)(args : list reg) + (rel : RELATION.t) : RELATION.t := + let rel' := kill_reg dst rel in + match eq_find {| eq_lhs := dst; + eq_op := op; + eq_args:= args |} with + | Some id => PSet.add id rel' + | None => 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 := + match eq_find {| eq_lhs := dst; + eq_op := SOp Omove; + eq_args:= src::nil |} with + | Some eq_id => PSet.add eq_id (kill_reg dst rel) + | None => kill_reg dst rel + 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) + (oper1 dst op args' rel) + else oper1 dst op args' rel + | None => oper1 dst op args' rel + end. + + 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 + | None => false + | Some eq => + match eq_op eq with + | SOp op => true + | SLoad chunk' addr' => + may_overlap chunk addr args chunk' addr' (eq_args eq) + end + end) + (PSet.inter rel (eq_kill_mem 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_mem 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 {| eq_lhs := src; + eq_op := SLoad chunk addr; + eq_args:= args |} with + | Some id => PSet.add id rel' + | None => rel' + end + else rel'. + + Definition store + (chunk : memory_chunk) (addr: addressing) (args : list reg) + (src : reg) (ty: typ) + (rel : RELATION.t) : RELATION.t := + store1 chunk addr (forward_move_l rel args) (forward_move rel src) ty 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_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : RB.t := + match instr with + | Inop _ + | Icond _ _ _ _ _ + | Ijumptable _ _ => Some rel + | Istore chunk addr args src _ => + Some (store chunk addr args src (tenv (forward_move rel 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 + 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 + 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 => + let rel' := apply_instr pc tenv instr rel in + List.forallb + (fun pc' => relb_leb rel' (PMap.get pc' inv)) + (RTL.successors_instr instr) + end). + +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_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 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_moves := fun reg => PMap.get reg moves + |}. |