Module SSAfastlive

Require Import List. Import ListNotations.

Require Import Coqlib.
Require Import AST.
Require Import Maps.
Require Import Utils.
Require Import TrMaps2.
Require Import SSA.
Require Import SCCPopt.
Require Import Time.

Require Import SSAfastliveutils.
Require Import SSAfastliveprecompute.

Local Open Scope string_scope.

Definition fold_t r c itvm uses l min max :=
  let fix aux l min :=
    match l with
    | [] => false
    | v :: l =>
      match itvm ! v with
      | None => false
      | Some num =>
        if max <? num.(pre) then false
        else if num.(pre) <=? min then aux l min
        else existsb (can_reach r c v) uses || aux l num.(post)
      end
    end
  in
  aux l min.

Definition is_live_in (dom : PTree.t itv) (def : reg -> node)
  (du_chain : P2Map.t (list node)) (r : PTree.t (positive * positive))
  (c : PTree.t (PTree.t unit)) (t : PTree.t (list node)) (x : reg) (u : node)
:=
  let d := def x in
  match dom ! d with
  | None => false
  | Some num =>
    match dom ! u with
    | None => false
    | Some num' =>
      (num.(pre) <? num'.(pre)) && (num'.(post) <=? num.(post)) &&
      let uses := du_chain !!2 x in
      match t ! u with
      | None => false
      | Some l => fold_t r c dom uses l num.(pre) num.(post)
      end
    end
  end.

Definition analyze (f : function) : (reg -> node -> bool) * (reg -> node -> bool) :=
  let dom_pre u :=
    match f.(fn_dom) ! u with
    | None => 0
    | Some num => num.(pre)
    end
  in
  let '(r, c, t, back) := time (Some "analyze ") "precompute_r_t " (fun _ => precompute_r_t (successors f) f.(fn_entrypoint) dom_pre) tt in
  let du_chain := time (Some "analyze ") "du_chain_dom " (fun _ => make_du_chain f) tt in
  let all_defs := time (Some "analyze ") "all_defs_dom " (fun _ => get_all_def f) tt in
  let def := time (Some "analyze ") "compute_def_dom " (fun _ => compute_def f all_defs) tt in
  (fun x u =>
    let d := def x in
    sdom_test f d u &&
    let uses := du_chain !!2 x in
    match t ! u with
    | None => false
    | Some l => List.fold_left (fun acc v => acc || (sdom_test f d v && existsb (can_reach r c v) uses)) l false
    end,
  is_live_in f.(fn_dom) def du_chain r c t).