Module SSAlivewrap

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

Require Import SSAfastliveutils.
Require Import SSAlive.

Local Open Scope string_scope.
Local Open Scope positive_scope.

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

Definition transf_function (f: function) : function :=
  time (Some "SSA liveness (Kildall)") "SSA liveness " (fun _ =>
    let live :=
      match precompute f with
      | None => assert_false
      | Some live => live
      end
    in
    let preds := make_predecessors (fn_code f) successors_instr in
    let live := PTree.map (fun pc _ => transfer f preds pc (live !! pc)) f.(fn_code) in

    let vars := time (Some "SSA liveness ") "collect variables " (fun _ => collect_variables f) tt in
    let b := time (Some "SSA liveness ") "joinpoints traversal " (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 ") "joinpoints live " (fun _ =>
            SSARegSet.fold (fun x _b =>
              match live ! pc with
              | None => assert_false
              | Some live => SSARegSet.mem x live
              end) vars b) tt
        else b
      end) f.(fn_code) true) tt
    in

    ignore2 f b) 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.