(* *************************************************************)
(*                                                             *)
(*             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
  |}.