Postorder renumbering of RTL control-flow graphs.
Require Import Coqlib.
Require Import Maps.
Require Import Postorder.
Require Import AST.
Require Import CFG.
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
|
Iskip s =>
Iskip (
renum_pc s)
|
Iassign id args s =>
Iassign id args (
renum_pc s)
|
Istore chunk addr src s =>
Istore chunk addr src (
renum_pc s)
|
Icall optres sg fn args s =>
Icall optres sg fn args (
renum_pc s)
|
Itailcall sg fn args =>
i
|
Ibuiltin optres ef args s =>
Ibuiltin optres ef args (
renum_pc s)
|
Iifthenelse a ifso ifnot =>
Iifthenelse a (
renum_pc ifso) (
renum_pc ifnot)
|
Iswitch a cases default =>
Iswitch a (
List.map (
fun i_pc => (
fst i_pc, (
renum_pc (
snd i_pc))))
cases) (
renum_pc default)
|
Ireturn oe =>
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.
Computation of the possible successors of an instruction.
This is used in particular for dataflow analyses.
Definition successors_instr (
i:
instruction) :
list node :=
match i with
|
Iskip s =>
s ::
nil
|
Iassign _ _ s =>
s ::
nil
|
Istore _ _ _ s =>
s ::
nil
|
Icall _ _ _ _ s =>
s ::
nil
|
Itailcall _ _ _ =>
nil
|
Ibuiltin _ _ _ s =>
s ::
nil
|
Iifthenelse _ ifso ifnot =>
ifso ::
ifnot ::
nil
|
Iswitch _ cases default =>
default :: (
List.map snd cases)
|
Ireturn _ =>
nil
end.
Definition successors (
f:
function) :
PTree.t (
list node) :=
PTree.map1 successors_instr f.(
fn_code).
Definition transf_function (
f:
function) :
function :=
let pnum :=
postorder (
successors f)
f.(
fn_entrypoint)
in
mkfunction
f.(
fn_sig)
f.(
fn_params)
f.(
fn_vars)
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.