blob: caaf09daa09d9b4e2cefba90b1160d1567c02c81 (
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
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
|
(* *********************************************************************)
(* *)
(* 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. *)
(* *)
(* *********************************************************************)
(** Register allocation. *)
Require Import Coqlib.
Require Import Errors.
Require Import Maps.
Require Import Lattice.
Require Import AST.
Require Import Op.
Require Import Registers.
Require Import RTL.
Require Import RTLtyping.
Require Import Liveness.
Require Import Locations.
Require Import LTL.
Require Import Coloring.
(** * Translation from RTL to LTL *)
(** Each [RTL] instruction translates to an [LTL] instruction.
The register assignment [assign] returned by register allocation
is applied to the arguments and results of the RTL
instruction. Moreover, dead instructions and redundant moves
are eliminated (turned into a [Lnop] instruction).
Dead instructions are instructions without side-effects ([Iop] and
[Iload]) whose result register is dead, i.e. whose result value
is never used. Redundant moves are moves whose source and destination
are assigned the same location. *)
Definition is_redundant_move
(op: operation) (args: list reg) (res: reg) (assign: reg -> loc) : bool :=
match is_move_operation op args with
| None => false
| Some src => if Loc.eq (assign src) (assign res) then true else false
end.
Definition transf_instr
(f: RTL.function) (live: PMap.t Regset.t) (assign: reg -> loc)
(pc: node) (instr: RTL.instruction) : LTL.instruction :=
match instr with
| Inop s =>
Lnop s
| Iop op args res s =>
if Regset.mem res live!!pc then
if is_redundant_move op args res assign then
Lnop s
else
Lop op (List.map assign args) (assign res) s
else
Lnop s
| Iload chunk addr args dst s =>
if Regset.mem dst live!!pc then
Lload chunk addr (List.map assign args) (assign dst) s
else
Lnop s
| Istore chunk addr args src s =>
Lstore chunk addr (List.map assign args) (assign src) s
| Icall sig ros args res s =>
Lcall sig (sum_left_map assign ros) (List.map assign args)
(assign res) s
| Itailcall sig ros args =>
Ltailcall sig (sum_left_map assign ros) (List.map assign args)
| Ibuiltin ef args res s =>
Lbuiltin ef (List.map assign args) (assign res) s
| Icond cond args ifso ifnot =>
Lcond cond (List.map assign args) ifso ifnot
| Ijumptable arg tbl =>
Ljumptable (assign arg) tbl
| Ireturn optarg =>
Lreturn (option_map assign optarg)
end.
Definition transf_fun (f: RTL.function) (live: PMap.t Regset.t)
(assign: reg -> loc) : LTL.function :=
LTL.mkfunction
(RTL.fn_sig f)
(List.map assign (RTL.fn_params f))
(RTL.fn_stacksize f)
(PTree.map (transf_instr f live assign) (RTL.fn_code f))
(RTL.fn_entrypoint f).
(** The translation of a function performs liveness analysis,
construction and coloring of the inference graph, and per-instruction
transformation as described above. *)
Definition live0 (f: RTL.function) (live: PMap.t Regset.t) :=
transfer f f.(RTL.fn_entrypoint) live!!(f.(RTL.fn_entrypoint)).
Open Scope string_scope.
Definition transf_function (f: RTL.function) : res LTL.function :=
match type_function f with
| Error msg => Error msg
| OK env =>
match analyze f with
| None => Error (msg "Liveness analysis failure")
| Some live =>
match regalloc f live (live0 f live) env with
| None => Error (msg "Incorrect graph coloring")
| Some assign => OK (transf_fun f live assign)
end
end
end.
Definition transf_fundef (fd: RTL.fundef) : res LTL.fundef :=
AST.transf_partial_fundef transf_function fd.
Definition transf_program (p: RTL.program) : res LTL.program :=
transform_partial_program transf_fundef p.
|
