blob: c8623185f6493c8c3dc4f76efd1f11aa62883875 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(** 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. (**r a postorder numbering *)
Definition renum_pc (pc: node) : node :=
match pnum!pc with
| Some pc' => pc'
| None => 1%positive (**r 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 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.
|
