Require CSE.
Require Extra.
Import Utf8.
Import Coqlib Errors Maps.
Import AST Registers Op.
Import Integers Values Memory.
Import RTL.
Import Extra.

Import ValueDomain ValueAnalysis.
Import Kildall.

Unset Elimination Schemes.
Coercion size_chunk : memory_chunk >-> Z.


Definition annot : Type := list Annotations.ablock.
Instance eq_ablock : EqDec Annotations.ablock := Annotations.ablock_eq.

Section OVERLAP.
  Local Coercion Int.unsigned : int >-> Z.

Definition range_disjoint (κ: Z) (r: int * int) (κ': Z) (r': int * int) : bool :=
  let '(a, b) := r in let '(c, d) := r' in
  if b + κ <=? c then true else d + κ' <=? a.

Definition range_overlap κ r κ' r' : bool :=
  negb (range_disjoint κ r κ' r').

Definition ablock_overlap κ α κ' α' : bool :=
  match α, α' with
  | Annotations.ABlocal d x r, Annotations.ABlocal d' x' r' =>
    if eq_nat_dec d d' then range_overlap κ r κ' r'
else false
  | Annotations.ABglobal x r, Annotations.ABglobal x' r' =>
    if eq_dec x x' then range_overlap κ r κ' r'
    else false
  | Annotations.ABlocal _ _ _, Annotations.ABglobal _ _
  | Annotations.ABglobal _ _, Annotations.ABlocal _ _ _ => false
  end.

Definition annot_overlap κ (α: annot) κ' (α': annot) : bool :=
  if α then true else
  if α' then true else
  list_exists (λ α,
    list_exists (λ α',
      ablock_overlap κ α κ' α'
    ) α'
  ) α.

Definition range_denote (κ: Z) (r: int * int) (o: int) : Prop :=
  fst r <= o ∧ o < snd r + κ.

Definition range_disjoint_true κ r κ' r' :
  range_disjoint κ r κ' r' = true →
  range_denote κ r ∩ range_denote κ' r' ⊆ ∅.

Corollary range_overlap_false κ r κ' r' :
  range_overlap κ r κ' r' = false →
  range_denote κ r ∩ range_denote κ' r' ⊆ ∅.

Definition range_disjoint_is_true κ r κ' r' o o' :
  o ∈ range_denote κ r → o' ∈ range_denote κ' r' →
  range_denote κ r ∩ range_denote κ' r' ⊆ ∅ →
  range_disjoint κ r κ' r' = true.

Import Globalenvs.
Variable ge : genv.
Variable stack: list block.

Hypothesis norepet_stack : list_norepet stack.
Hypothesis noglobal_alias_stack : ∀ s b,
    Genv.find_symbol ge s = Some b → ¬ In b stack.

Lemma genv_find_symbol_injective s s' b :
  Genv.find_symbol ge s = Some b →
  Genv.find_symbol ge s' = Some b →
  s' = s.

Lemma nth_split {X} (m: list X) (n: nat) (x: X) :
  nth_error m n = Some x →
  ∃ pre post,
    m = pre ++ x :: post ∧ length pre = n.

Lemma list_cut {X} m n m' n' (x: X) :
  m ++ x :: n = m' ++ x :: n' →
  ¬ In x m →
  ¬ In x m' →
  m' = m.

Lemma nth_norepet_injective {X} (m: list X) (n n': nat) (x: X) :
  list_norepet m →
  nth_error m n = Some x →
  nth_error m n' = Some x →
  n' = n.

Definition block_of_ablock a : option block :=
  match a with
  | Annotations.ABlocal d _ r => nth_error stack d
  | Annotations.ABglobal s r => Genv.find_symbol ge s
  end.

Definition range_of_ablock a : int * int :=
  match a with
  | Annotations.ABlocal _ _ r
  | Annotations.ABglobal _ r => r
  end.

Definition ablock_denote κ a bi : Prop :=
  block_of_ablock a = Some (fst bi) ∧ range_denote κ (range_of_ablock a) (snd bi).

Lemma ablock_overlap_false κ a κ' a' :
  ablock_overlap κ a κ' a' = false →
  ablock_denote κ a ∩ ablock_denote κ' a' ⊆ ∅.

Definition annot_denote κ (α: annot) bi : Prop :=
  if α then True else
  ∃ a, In a α ∧ ablock_denote κ a bi.

Lemma annot_overlap_false κ α κ' α' :
  annot_overlap κ α κ' α' = false →
  annot_denote κ α ∩ annot_denote κ' α' ⊆ ∅.

End OVERLAP.


Definition valnum := positive.

Inductive rhs : Type :=
  | Op: operation -> list valnum -> rhs
  | Load `(memory_chunk) `(annot) `(addressing) `(list valnum).

Record equation : Type :=
  Eq { v : valnum ; strict : bool ; r : rhs }.

Instance eq_rhs : EqDec rhs.

Record numbering : Type := mknumbering {
  num_next: valnum; (* first unused value number *)
  num_eqs: list equation; (* valid equations *)
  num_reg: PTree.t valnum; (* mapping register to valnum *)
  num_val: PMap.t (list reg) (* reverse mapping valnum to regs containing it *)
}.

Definition empty_numbering :=
  {| num_next := 1%positive;
     num_eqs := nil;
     num_reg := PTree.empty _;
     num_val := PMap.init nil |}.

Definition valnums_rhs (r: rhs): list valnum :=
  match r with
  | Op _ vl
  | Load _ _ _ vl => vl
  end.

Definition wf_rhs (next: valnum) (r: rhs) : Prop :=
forall v, In v (valnums_rhs r) -> Plt v next.

Definition wf_equation (next: valnum) (e: equation) : Prop :=
  match e with Eq l str r => Plt l next /\ wf_rhs next r end.

Record wf_numbering (n: numbering) : Prop := {
  wf_num_eqs: forall e,
      In e n.(num_eqs) -> wf_equation n.(num_next) e;
  wf_num_reg: forall r v,
      PTree.get r n.(num_reg) = Some v -> Plt v n.(num_next);
  wf_num_val: forall r v,
      In r (PMap.get v n.(num_val)) -> PTree.get r n.(num_reg) = Some v
}.

Hint Resolve wf_num_eqs wf_num_reg wf_num_val: cse.

Definition valuation := valnum -> val.

Definition rhs_eval_to (valu: valuation) (ge: genv) (sp: val) (m: mem) (r: rhs) : val → Prop :=
  match r with
  | Op op vl => λ v, eval_operation ge sp op (map valu vl) m = Some v
  | Load κ α addr vl =>
    λ v, ∃ a,
      eval_addressing ge sp addr (map valu vl) = Some a ∧
      Mem.loadv κ m a = Some v
  end.

Definition equation_holds (valu: valuation) (ge: genv) (sp: val) (m: mem) (eqn: equation) : Prop :=
  match eqn with
  | Eq l true r => rhs_eval_to valu ge sp m r (valu l)
  | Eq l false r =>
    ∃ v, rhs_eval_to valu ge sp m r v ∧ Val.lessdef v (valu l)
end.

Record numbering_holds (valu: valuation) (ge: genv) (sp: val)
                       (rs: regset) (m: mem) (n: numbering) : Prop := {
  num_holds_wf:
     wf_numbering n;
  num_holds_eq: forall eq,
     In eq n.(num_eqs) -> equation_holds valu ge sp m eq;
  num_holds_reg: forall r v,
     n.(num_reg)!r = Some v -> rs#r = valu v
}.

Hint Resolve num_holds_wf num_holds_eq num_holds_reg: cse.

Lemma empty_numbering_holds:
  forall valu ge sp rs m,
  numbering_holds valu ge sp rs m empty_numbering.

Operations on value numberings

Definition valnum_reg (n: numbering) (r: reg) : numbering * valnum :=
  match PTree.get r n.(num_reg) with
  | Some v => (n, v)
  | None =>
      let v := n.(num_next) in
      ( {| num_next := Psucc v;
           num_eqs := n.(num_eqs);
           num_reg := PTree.set r v n.(num_reg);
           num_val := PMap.set v (r :: nil) n.(num_val) |},
       v)
  end.

Fixpoint valnum_regs (n: numbering) (rl: list reg)
                     {struct rl} : numbering * list valnum :=
  match rl with
  | nil =>
      (n, nil)
  | r1 :: rs =>
      let (n1, v1) := valnum_reg n r1 in
      let (ns, vs) := valnum_regs n1 rs in
      (ns, v1 :: vs)
  end.

Fixpoint find_valnum_rhs (r: rhs) (eqs: list equation)
                         {struct eqs} : option valnum :=
  match eqs with
  | nil => None
  | Eq v str r' :: eqs1 =>
      if (if str then eq_rhs r r' : bool else false) then Some v else find_valnum_rhs r eqs1
  end.

Fixpoint find_valnum_rhs' (r: rhs) (eqs: list equation)
                          {struct eqs} : option valnum :=
  match eqs with
  | nil => None
  | Eq v str r' :: eqs1 =>
      if eq_rhs r r' then Some v else find_valnum_rhs' r eqs1
  end.

Fixpoint find_valnum_num (v: valnum) (eqs: list equation)
                         {struct eqs} : option rhs :=
  match eqs with
  | nil => None
  | Eq v' str r' :: eqs1 =>
      if if str then peq v v' : bool else false then Some r' else find_valnum_num v eqs1
  end.

Definition reg_valnum (n: numbering) (vn: valnum) : option reg :=
  match PMap.get vn n.(num_val) with
  | nil => None
  | r :: rs => Some r
  end.

Fixpoint regs_valnums (n: numbering) (vl: list valnum) : option (list reg) :=
  match vl with
  | nil => Some nil
  | v1 :: vs =>
      match reg_valnum n v1 with
      | Some r1 => match regs_valnums n vs with
                   | Some rs => Some (r1 :: rs)
                   | _ => None
                   end
      | _ => None
      end
  end.

Definition find_rhs (n: numbering) (rh: rhs) : option reg :=
  match find_valnum_rhs' rh n.(num_eqs) with
  | None => None
  | Some vres => reg_valnum n vres
  end.

Definition forget_reg (n: numbering) (rd: reg) : PMap.t (list reg) :=
  match PTree.get rd n.(num_reg) with
  | None => n.(num_val)
  | Some v => PMap.set v (List.remove peq rd (PMap.get v n.(num_val))) n.(num_val)
  end.

Definition update_reg (n: numbering) (rd: reg) (vn: valnum) : PMap.t (list reg) :=
  let nv := forget_reg n rd in PMap.set vn (rd :: PMap.get vn nv) nv.

Definition add_rhs (n: numbering) (rd: reg) (rh: rhs) : numbering :=
  match find_valnum_rhs rh n.(num_eqs) with
  | Some vres =>
      {| num_next := n.(num_next);
         num_eqs := n.(num_eqs);
         num_reg := PTree.set rd vres n.(num_reg);
         num_val := update_reg n rd vres |}
  | None =>
      {| num_next := Psucc n.(num_next);
         num_eqs := Eq n.(num_next) true rh :: n.(num_eqs);
         num_reg := PTree.set rd n.(num_next) n.(num_reg);
         num_val := update_reg n rd n.(num_next) |}
  end.

Definition add_op (n: numbering) (rd: reg) (op: operation) (rs: list reg) :=
  match is_move_operation op rs with
  | Some r =>
      let (n1, v) := valnum_reg n r in
      {| num_next := n1.(num_next);
         num_eqs := n1.(num_eqs);
         num_reg := PTree.set rd v n1.(num_reg);
         num_val := update_reg n1 rd v |}
  | None =>
      let (n1, vs) := valnum_regs n rs in
      add_rhs n1 rd (Op op vs)
  end.

Definition add_load (n: numbering) (rd: reg)
                    (chunk: memory_chunk) (α: annot) (addr: addressing)
                    (rs: list reg) :=
  let (n1, vs) := valnum_regs n rs in
  add_rhs n1 rd (Load chunk α addr vs).

Definition set_unknown (n: numbering) (rd: reg) :=
  {| num_next := n.(num_next);
     num_eqs := n.(num_eqs);
     num_reg := PTree.remove rd n.(num_reg);
     num_val := forget_reg n rd |}.

Definition set_res_unknown (n: numbering) (res: builtin_res reg) :=
  match res with
  | BR r => set_unknown n r
  | _ => n
  end.

Fixpoint kill_eqs (pred: rhs -> bool) (eqs: list equation) : list equation :=
  match eqs with
  | nil => nil
  | (Eq l strict r) as eq :: rem =>
      if pred r then kill_eqs pred rem else eq :: kill_eqs pred rem
  end.

Definition kill_equations (pred: rhs -> bool) (n: numbering) : numbering :=
  {| num_next := n.(num_next);
     num_eqs := kill_eqs pred n.(num_eqs);
     num_reg := n.(num_reg);
     num_val := n.(num_val) |}.

Definition filter_loads (r: rhs) : bool :=
  match r with
  | Op op _ => op_depends_on_memory op
  | Load _ _ _ _ => true
  end.

Definition kill_all_loads (n: numbering) : numbering :=
  kill_equations filter_loads n.


Definition filter_after_store κ α (r: rhs) : bool :=
  match r with
  | Op op _ => op_depends_on_memory op
  | Load κ' α' _ _ => annot_overlap κ α κ' α'
  end.

Definition kill_loads_after_store (n: numbering) κ α : numbering :=
  kill_equations (filter_after_store κ α) n.

Definition store_normalized_range (chunk: memory_chunk) : aval :=
  match chunk with
  | Mint8signed => Sgn Ptop 8
  | Mint8unsigned => Uns Ptop 8
  | Mint16signed => Sgn Ptop 16
  | Mint16unsigned => Uns Ptop 16
  | _ => Vtop
  end.

Definition add_store_result (app: VA.t) (n: numbering) (chunk: memory_chunk) α (addr: addressing)
                            (rargs: list reg) (rsrc: reg) :=
  if vincl (avalue app rsrc) (store_normalized_range chunk) then
    let (n1, vsrc) := valnum_reg n rsrc in
    let (n2, vargs) := valnum_regs n1 rargs in
    {| num_next := n2.(num_next);
       num_eqs := Eq vsrc false (Load chunk α addr vargs) :: n2.(num_eqs);
       num_reg := n2.(num_reg);
       num_val := n2.(num_val) |}
  else n.


Section REDUCE.

Variable A: Type.
Variable f: (valnum -> option rhs) -> A -> list valnum -> option (A * list valnum).
Variable n: numbering.

Fixpoint reduce_rec (niter: nat) (op: A) (args: list valnum) : option(A * list reg) :=
  match niter with
  | O => None
  | Datatypes.S niter' =>
      match f (fun v => find_valnum_num v n.(num_eqs)) op args with
      | None => None
      | Some(op', args') =>
          match reduce_rec niter' op' args' with
          | None =>
              match regs_valnums n args' with Some rl => Some(op', rl) | None => None end
          | Some _ as res =>
              res
          end
      end
  end.

Definition reduce (op: A) (rl: list reg) (vl: list valnum) : A * list reg :=
  match reduce_rec 4%nat op vl with
  | None => (op, rl)
  | Some res => res
  end.

End REDUCE.

The static analysis

Module Numbering.
  Definition t := numbering.
  Definition ge (n1 n2: numbering) : Prop :=
    forall valu ge sp rs m,
    numbering_holds valu ge sp rs m n2 ->
    numbering_holds valu ge sp rs m n1.
  Definition top := empty_numbering.
  Lemma top_ge: forall x, ge top x.
  Lemma refl_ge: forall x, ge x x.
End Numbering.


Module Solver := BBlock_solver(Numbering).


Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numbering) :=
  match f.(fn_code)!pc with
  | None => before
  | Some i =>
      match i with
      | Inop s =>
          before
      | Iop op args res s =>
          add_op before res op args
      | Iload alpha chunk addr args dst s =>
          add_load before dst chunk (snd alpha) addr args
      | Istore alpha chunk addr args src s =>
          let app := approx!!pc in
          let n := kill_loads_after_store before chunk (snd alpha) in
          add_store_result app n chunk (snd alpha) addr args src
      | Icall sig ros args res s =>
          empty_numbering
      | Itailcall sig ros args =>
          empty_numbering
      | Ibuiltin ef args res s =>
          match ef with
          | EF_external _ _ | EF_malloc | EF_free | EF_inline_asm _ _ _ =>
              empty_numbering
          | EF_memcpy _ _
          | EF_builtin _ _ | EF_vstore _ =>
              set_res_unknown (kill_all_loads before) res
          | EF_vload _ | EF_annot _ _ | EF_annot_val _ _ | EF_debug _ _ _ =>
              set_res_unknown before res
          end
      | Icond cond args ifso ifnot =>
          before
      | Ijumptable arg tbl =>
          before
      | Ireturn optarg =>
          before
      end
  end.


Definition analyze (f: RTL.function) (approx: PMap.t VA.t): option (PMap.t numbering) :=
  Solver.fixpoint (fn_code f) successors_instr (transfer f approx) f.(fn_entrypoint).

Code transformation

Section COMBINE.

Variable get: valnum -> option rhs.

Definition combine_compimm_ne_0 (x: valnum) : option(condition * list valnum) :=
  match get x with
  | Some(Op (Ocmp c) ys) => Some (c, ys)
  | Some(Op (Oandimm n) ys) => Some (Cmasknotzero n, ys)
  | _ => None
  end.

Definition combine_compimm_eq_0 (x: valnum) : option(condition * list valnum) :=
  match get x with
  | Some(Op (Ocmp c) ys) => Some (negate_condition c, ys)
  | Some(Op (Oandimm n) ys) => Some (Cmaskzero n, ys)
  | _ => None
  end.

Definition combine_compimm_eq_1 (x: valnum) : option(condition * list valnum) :=
  match get x with
  | Some(Op (Ocmp c) ys) => Some (c, ys)
  | _ => None
  end.

Definition combine_compimm_ne_1 (x: valnum) : option(condition * list valnum) :=
  match get x with
  | Some(Op (Ocmp c) ys) => Some (negate_condition c, ys)
  | _ => None
  end.

Definition combine_cond (cond: condition) (args: list valnum) : option(condition * list valnum) :=
  match cond, args with
  | Ccompimm Cne n, x::nil =>
      if Int.eq_dec n Int.zero then combine_compimm_ne_0 x
      else if Int.eq_dec n Int.one then combine_compimm_ne_1 x
      else None
  | Ccompimm Ceq n, x::nil =>
      if Int.eq_dec n Int.zero then combine_compimm_eq_0 x
      else if Int.eq_dec n Int.one then combine_compimm_eq_1 x
      else None
  | Ccompuimm Cne n, x::nil =>
      if Int.eq_dec n Int.zero then combine_compimm_ne_0 x
      else if Int.eq_dec n Int.one then combine_compimm_ne_1 x
      else None
  | Ccompuimm Ceq n, x::nil =>
      if Int.eq_dec n Int.zero then combine_compimm_eq_0 x
      else if Int.eq_dec n Int.one then combine_compimm_eq_1 x
      else None
  | _, _ => None
  end.

Definition combine_addr (addr: addressing) (args: list valnum) : option(addressing * list valnum) :=
  match addr, args with
  | Aindexed n, x::nil =>
      match get x with
      | Some(Op (Olea a) ys) => Some(offset_addressing_total a n, ys)
      | _ => None
      end
  | _, _ => None
  end.

Definition combine_op (op: operation) (args: list valnum) : option(operation * list valnum) :=
  match op, args with
  | Olea addr, _ =>
      match combine_addr addr args with
      | Some(addr', args') => Some(Olea addr', args')
      | None => None
      end
  | Oandimm n, x :: nil =>
      match get x with
      | Some(Op (Oandimm m) ys) => Some(Oandimm (Int.and m n), ys)
      | _ => None
      end
  | Oorimm n, x :: nil =>
      match get x with
      | Some(Op (Oorimm m) ys) => Some(Oorimm (Int.or m n), ys)
      | _ => None
      end
  | Oxorimm n, x :: nil =>
      match get x with
      | Some(Op (Oxorimm m) ys) => Some(Oxorimm (Int.xor m n), ys)
      | _ => None
      end
  | Ocmp cond, _ =>
      match combine_cond cond args with
      | Some(cond', args') => Some(Ocmp cond', args')
      | None => None
      end
  | _, _ => None
  end.

End COMBINE.

Definition transf_instr (n: numbering) (instr: instruction) :=
  match instr with
  | Iop op args res s =>
      if is_trivial_op op then instr else
        let (n1, vl) := valnum_regs n args in
        match find_rhs n1 (Op op vl) with
        | Some r =>
            Iop Omove (r :: nil) res s
        | None =>
            let (op', args') := reduce _ combine_op n1 op args vl in
            Iop op' args' res s
        end
  | Iload alpha chunk addr args dst s =>
      let (n1, vl) := valnum_regs n args in
      match find_rhs n1 (Load chunk (snd alpha) addr vl) with
      | Some r =>
          Iop Omove (r :: nil) dst s
      | None =>
          let (addr', args') := reduce _ combine_addr n1 addr args vl in
          Iload alpha chunk addr' args' dst s
      end
  | Istore alpha chunk addr args src s =>
      let (n1, vl) := valnum_regs n args in
      let (addr', args') := reduce _ combine_addr n1 addr args vl in
      Istore alpha chunk addr' args' src s
  | Icond cond args s1 s2 =>
      let (n1, vl) := valnum_regs n args in
      let (cond', args') := reduce _ combine_cond n1 cond args vl in
      Icond cond' args' s1 s2
  | _ =>
      instr
  end.

Definition transf_code (approxs: PMap.t numbering) (instrs: code) : code :=
  PTree.map (fun pc instr => transf_instr approxs!!pc instr) instrs.

Definition vanalyze := ValueAnalysis.analyze.

Definition transf_function (rm: romem) (f: function) : res function :=
  let approx := vanalyze rm f in
  match analyze f approx with
  | None => Error (msg "CSE failure")
  | Some approxs =>
      OK(mkfunction
           f.(fn_sig)
           f.(fn_params)
           f.(fn_stacksize)
           (transf_code approxs f.(fn_code))
           f.(fn_entrypoint))
  end.

Definition transf_fundef (rm: romem) (name: ident) (f: fundef) : res fundef :=
  AST.transf_partial_fundef (transf_function rm) f.

Definition transf_program (p: program) : res program :=
  transform_partial_ident_program (transf_fundef (romem_for_program p)) p.