Module Renumber2

Postorder renumbering of RTL control-flow graphs.

Require Import Coqlib.
Require Import Maps.
Require Import Postorder.
Require Import RTL.
Require Import Annotations.
Require Import Errors.

Open Scope error_monad_scope.

CompCert's dataflow analyses (module Kildall) are more precise and run faster when the sequence 1, 2, 3, ... is a postorder enumeration of the nodes of the control-flow graph. This property can be guaranteed when generating the CFG (module RTLgen), but is, however, invalidated by further RTL optimization passes such as Inlining. In this module, we renumber the nodes of RTL control-flow graphs to restore the postorder property given above. In passing, we also eliminate CFG nodes that are not reachable from the entry point: these nodes are dead code.

Section RENUMBER.

Variable pnum: PTree.t positive. (* a postorder numbering *)

Definition renum_pc (pc: node) : res node :=
  match pnum!pc with
  | Some pc' => OK pc'
  | None => Error (msg "impossible case, never exercised")
  end.

Definition renum_instr (i: instruction) : res instruction :=
  match i with
  | Inop s =>
    do s' <- renum_pc s;
    OK (Inop s')
  | Iop op args res s =>
    do s' <- renum_pc s;
    OK (Iop op args res s')
  | Iload alpha chunk addr args res s =>
    do s' <- renum_pc s;
    OK (Iload alpha chunk addr args res s')
  | Istore alpha chunk addr args src s =>
    do s' <- renum_pc s;
    OK (Istore alpha chunk addr args src s')
  | Icall sg ros args res s =>
    do s' <- renum_pc s;
    OK (Icall sg ros args res s')
  | Itailcall sg ros args => OK i
  | Ibuiltin ef args res s =>
    do s' <- renum_pc s;
    OK (Ibuiltin ef args res s')
  | Icond cond args s1 s2 =>
    do s1' <- renum_pc s1;
    do s2' <- renum_pc s2;
    OK (Icond cond args s1' s2')
  | Ijumptable arg tbl =>
    do tbl' <- mmap renum_pc tbl;
    OK (Ijumptable arg tbl')
  | Ireturn or => OK i
  end.

Definition renum_node (c': res code) (pc: node) (i: instruction) : res code :=
  match pnum!pc with
  | None => c'
  | Some pc' =>
    do c' <- c';
    do i' <- renum_instr i;
    OK (PTree.set pc' i' c')
  end.

Definition renum_cfg (c: code) : res code :=
  PTree.fold renum_node c (OK (PTree.empty instruction)).

End RENUMBER.

Definition transf_function (f: function) : res function :=
  let pnum := postorder (successors_map f) f.(fn_entrypoint) in
  do c <- renum_cfg pnum f.(fn_code);
  do entrypoint <- renum_pc pnum f.(fn_entrypoint);
  OK (mkfunction
        f.(fn_sig)
        f.(fn_params)
        f.(fn_stacksize)
        c
        entrypoint).

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

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