Module Renumber

Postorder renumbering of RTL control-flow graphs.

Require Import Coqlib.
Require Import Maps.
Require Import Postorder.
Require Import RTL.

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) : node :=
  match pnum!pc with
  | Some pc' => pc'
  | None => 1%positive (* impossible case, never exercised *)
  end.

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

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

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

End RENUMBER.

Definition transf_function (f: function) : function :=
  let pnum := postorder (successors_map f) f.(fn_entrypoint) in
  mkfunction
    f.(fn_sig)
    f.(fn_params)
    f.(fn_stacksize)
    (renum_cfg pnum f.(fn_code))
    (renum_pc pnum f.(fn_entrypoint)).

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

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