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
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
|
(* *********************************************************************)
(* *)
(* 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 GNU General Public License as published by *)
(* the Free Software Foundation, either version 2 of the License, or *)
(* (at your option) any later version. This file is also distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(* Removing unused declarations *)
open C
open Cutil
(* The set of all identifiers referenced so far *)
let referenced = ref IdentSet.empty
(* Record that a new identifier was added to this set *)
let ref_changed = ref false
(* Record a reference to an identifier. If seen for the first time,
add it to worklist. *)
let addref id =
if not (IdentSet.mem id !referenced) then begin
(* Printf.printf "Referenced: %s$%d\n" id.name id.stamp; *)
referenced := IdentSet.add id !referenced;
ref_changed := true
end
let needed id =
IdentSet.mem id !referenced
(* Iterate [addref] on all syntactic categories. *)
let rec add_typ = function
| TPtr(ty, _) -> add_typ ty
| TArray(ty, _, _) -> add_typ ty
| TFun(res, None, _, _) -> add_typ res
| TFun(res, Some params, _, _) -> add_typ res; add_vars params
| TNamed(id, _) -> addref id
| TStruct(id, _) -> addref id
| TUnion(id, _) -> addref id
| TEnum(id, _) -> addref id
| _ -> ()
and add_vars vl =
List.iter (fun (id, ty) -> add_typ ty) vl
let rec add_exp e =
add_typ e.etyp; (* perhaps not necessary but play it safe *)
match e.edesc with
| EConst (CEnum(id, v)) -> addref id
| EConst _ -> ()
| ESizeof ty -> add_typ ty
| EAlignof ty -> add_typ ty
| EVar id -> addref id
| EUnop(op, e1) -> add_exp e1
| EBinop(op, e1, e2, ty) -> add_exp e1; add_exp e2
| EConditional(e1, e2, e3) -> add_exp e1; add_exp e2; add_exp e3
| ECast(ty, e1) -> add_typ ty; add_exp e1
| ECompound(ty, ie) -> add_typ ty; add_init ie
| ECall(e1, el) -> add_exp e1; List.iter add_exp el
and add_init = function
| Init_single e -> add_exp e
| Init_array il -> List.iter add_init il
| Init_struct(id, il) -> addref id; List.iter (fun (_, i) -> add_init i) il
| Init_union(id, _, i) -> addref id; add_init i
let add_decl (sto, id, ty, init) =
add_typ ty;
match init with None -> () | Some i -> add_init i
let rec add_stmt s =
match s.sdesc with
| Sskip -> ()
| Sdo e -> add_exp e
| Sseq(s1, s2) -> add_stmt s1; add_stmt s2
| Sif(e, s1, s2) -> add_exp e; add_stmt s1; add_stmt s2
| Swhile(e, s1) -> add_exp e; add_stmt s1
| Sdowhile(s1, e) -> add_stmt s1; add_exp e
| Sfor(e1, e2, e3, s1) -> add_stmt e1; add_exp e2; add_stmt e3; add_stmt s1
| Sbreak -> ()
| Scontinue -> ()
| Sswitch(e, s1) -> add_exp e; add_stmt s1
| Slabeled(lbl, s) ->
begin match lbl with Scase e -> add_exp e | _ -> () end;
add_stmt s
| Sgoto lbl -> ()
| Sreturn None -> ()
| Sreturn(Some e) -> add_exp e
| Sblock sl -> List.iter add_stmt sl
| Sdecl d -> add_decl d
| Sasm _ -> ()
let add_fundef f =
add_typ f.fd_ret;
add_vars f.fd_params;
List.iter add_decl f.fd_locals;
add_stmt f.fd_body
let add_field f = add_typ f.fld_typ
let add_enum e =
List.iter
(fun (id, v, opt_e) -> match opt_e with Some e -> add_exp e | None -> ())
e
(* Saturate the set of referenced identifiers, starting with externally
visible global declarations *)
let visible_decl (sto, id, ty, init) =
sto = Storage_default &&
match ty with TFun _ -> false | _ -> true
let visible_fundef f =
match f.fd_storage with
| Storage_default -> not f.fd_inline
| Storage_extern -> true
| Storage_static -> false
| Storage_register -> assert false
let rec add_init_globdecls accu = function
| [] -> accu
| g :: rem ->
match g.gdesc with
| Gdecl decl when visible_decl decl ->
add_decl decl; add_init_globdecls accu rem
| Gfundef f when visible_fundef f ->
add_fundef f; add_init_globdecls accu rem
| Gdecl _ | Gfundef _ | Gcompositedef _ | Gtypedef _ | Genumdef _ ->
(* Keep for later iterations *)
add_init_globdecls (g :: accu) rem
| Gcompositedecl _ | Gpragma _ ->
(* Discard, since these cannot introduce more references later *)
add_init_globdecls accu rem
let rec add_needed_globdecls accu = function
| [] -> accu
| g :: rem ->
match g.gdesc with
| Gdecl((sto, id, ty, init) as decl) ->
if needed id
then (add_decl decl; add_needed_globdecls accu rem)
else add_needed_globdecls (g :: accu) rem
| Gfundef f ->
if needed f.fd_name
then (add_fundef f; add_needed_globdecls accu rem)
else add_needed_globdecls (g :: accu) rem
| Gcompositedef(_, id, _, flds) ->
if needed id
then (List.iter add_field flds; add_needed_globdecls accu rem)
else add_needed_globdecls (g :: accu) rem
| Gtypedef(id, ty) ->
if needed id
then (add_typ ty; add_needed_globdecls accu rem)
else add_needed_globdecls (g :: accu) rem
| Genumdef(id, _, enu) ->
if needed id || List.exists (fun (id, _, _) -> needed id) enu
then (add_enum enu; add_needed_globdecls accu rem)
else add_needed_globdecls (g :: accu) rem
| _ ->
assert false
let saturate p =
let rec loop p =
if !ref_changed then begin
ref_changed := false;
loop (add_needed_globdecls [] p)
end in
ref_changed := false;
loop (add_init_globdecls [] p)
(* Remove unreferenced definitions *)
let rec simpl_globdecls accu = function
| [] -> accu
| g :: rem ->
let need =
match g.gdesc with
| Gdecl((sto, id, ty, init) as decl) -> visible_decl decl || needed id
| Gfundef f -> visible_fundef f || needed f.fd_name
| Gcompositedecl(_, id, _) -> needed id
| Gcompositedef(_, id, _, flds) -> needed id
| Gtypedef(id, ty) -> needed id
| Genumdef(id, _, enu) ->
needed id || List.exists (fun (id, _, _) -> needed id) enu
| Gpragma s -> true in
if need
then simpl_globdecls (g :: accu) rem
else simpl_globdecls accu rem
let program p =
referenced := IdentSet.empty;
saturate p;
let p' = simpl_globdecls [] p in
referenced := IdentSet.empty;
p'
|
