Require Recdef.
Require Import FSets.
Require Import Coqlib.
Require Import Ordered.
Require Import Errors.
Require Import Maps.
Require Import AST.
Require Import Registers.
Require Import RTL.
Require Import RTLutils.
Require Import Kildall.
Require Import Utils.
Require Import Relation_Operators.

Local Open Scope error_monad_scope.

Utility functions

Definition not_seen_sons (code:code) (pc : node) (seen: PTree.t unit) : (list positive) * PTree.t unit :=
  match code ! pc with
    | None => (nil, seen)
    | Some i =>
      List.fold_left (fun (ns:(list node) * PTree.t unit) j =>
        let (new,seen) := ns in
          match PTree.get j seen with
            | None => (j::new, PTree.set j tt seen)
            | Some _ => ns
          end)
        (successors_instr i)
        (nil, seen)
  end.

Definition remove_dead (i:option instruction) (b:option unit) : option instruction :=
  match b with
    | Some _ => i
    | None => None
  end.

Fixpoint acc_succ (code:code) (workl: list node) (acc: res (PTree.t unit * (list positive) * (list positive))) : res ((list positive) * RTL.code) :=
  do acc <- acc;
    let '(seen_set,seen_list,stack) := acc in
      match stack with
        | nil => OK (seen_list, combine remove_dead code seen_set)
        | x::q =>
          match workl with
            | nil => Error (msg "workl too small")
            | pc::m =>
              let seen_set' := PTree.set x tt seen_set in
                let (new,seen_set) := not_seen_sons code x seen_set' in
                  acc_succ code m (OK (seen_set,x::seen_list,new++q))
          end
      end.

Definition dfs (tf: RTL.function) : res (list node * RTL.code) :=
  do (res, code') <-
    (acc_succ
      (RTL.fn_code tf)
      (map (@fst node instruction) (PTree.elements (RTL.fn_code tf)))
      (OK (PTree.empty _,nil,(RTL.fn_entrypoint tf)::nil))) ;
    OK (rev_append res nil, code').

Actual code of the transformations

Definition transf_function (f: RTL.function) : res (list node * RTL.function) :=
  do (seen,code) <- dfs f ;
    OK (seen, (RTL.mkfunction
                 (RTL.fn_sig f)
                 (RTL.fn_params f)
                 (RTL.fn_stacksize f)
                 code
                 (RTL.fn_entrypoint f))).