Module SSAfastlivewrap

Require Import List. Import ListNotations.

Require Import Coqlib.
Require Import Time.
Require Import AST.
Require Import Maps.
Require Import SSA.
Require Import SSAutils.

Require Import SSAfastliveutils.
Require Import SSAlive.
Require Import SSAfastlive.

Local Open Scope string_scope.
Local Open Scope positive_scope.

Definition precompute f :=
  let live := time (Some "SSA fast liveness ") "analyze " (fun _ => analyze f) tt in
  live.

Definition transf_function (f: function) : function :=
  time (Some "SSA fast liveness") "SSA fast liveness " (fun _ =>
  let preds := Kildall.make_predecessors (fn_code f) successors_instr in
  let (live1, live2) := precompute f in
  let vars := time (Some "SSA fast liveness ") "collect variables " (fun _ => collect_variables f) tt in

  let b1 := time (Some "SSA fast liveness ") "joinpoints traversal 1 " (fun _ => PTree.fold (fun b pc _ =>
    match preds ! pc with
    | None => b
    | Some l =>
      if List.existsb (dom_test f pc) l then
        time (Some "joinpoints traversal 1 ") "joinpoints fastlive 1 " (fun _ =>
          SSARegSet.fold (fun x _b => live1 x pc) vars b) tt
      else b
    end) f.(fn_code) true) tt
  in
  let b2 := time (Some "SSA fast liveness ") "joinpoints traversal 2 " (fun _ => PTree.fold (fun b pc _ =>
    match preds ! pc with
    | None => b
    | Some l =>
      if List.existsb (dom_test f pc) l then
        time (Some "joinpoints traversal 2 ") "joinpoints fastlive 2 " (fun _ =>
          SSARegSet.fold (fun x _b => live2 x pc) vars b) tt
      else b
    end) f.(fn_code) true) tt
  in
  ignore2 f (b1, b2)) tt.

Definition transf_fundef (f: fundef) : fundef :=
  AST.transf_fundef transf_function f.

Definition transf_program (p: program) : program :=
  AST.transform_program transf_fundef p.