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 RTLt.
Require Import RTL.
Require Import RTLutils.
Require Import Kildall.
Require Import Utils.
Require Import Relation_Operators.
Require Import Time.

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, PTree.combine_inter 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 * RTLt.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 RTLt.function :=
  time (Some "RTL unreachable code elimination"%string)
       "RTL unreachable code elimination " (fun _ =>
  do (seen,code) <- dfs f ;
    OK (RTLt.mkfunction
      (RTL.fn_sig f)
      (RTL.fn_params f)
      (RTL.fn_stacksize f)
      code
      (RTL.fn_entrypoint f)
      seen)) tt.

Definition transf_fundef (fd: RTL.fundef) : res RTLt.fundef :=
  AST.transf_partial_fundef transf_function fd.

Definition transf_program (p: RTL.program) : res RTLt.program :=
  transform_partial_program transf_fundef p.

Well-formed dfs functions and programs

Record wf_dfs_function (f: RTLt.function) : Prop := {
  fn_dfs_comp : forall j ins, (RTLt.fn_code f) ! j = Some ins -> In j (fn_dfs f);
  fn_dfs_reached: forall j, In j (fn_dfs f) -> (cfg (RTLt.fn_code f))** (RTLt.fn_entrypoint f) j;
  fn_dfs_norep : list_norepet (fn_dfs f)
}.

Inductive wf_dfs_fundef: RTLt.fundef -> Prop :=
  | wf_dfs_fundef_external: forall ef,
      wf_dfs_fundef (External ef)
  | wf_dfs_function_internal: forall f,
      wf_dfs_function f ->
      wf_dfs_fundef (Internal f).

Definition wf_dfs_program (p: RTLt.program) : Prop :=
  forall f id, In (id,Gfun f) (prog_defs p) -> wf_dfs_fundef f.