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
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
|
(* *********************************************************************)
(* *)
(* 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. *)
(* *)
(* *********************************************************************)
(* Renaming of identifiers *)
open C
open Cutil
module StringSet = Set.Make(String)
type rename_env = {
re_id: ident IdentMap.t;
re_used: StringSet.t
}
let empty_env = { re_id = IdentMap.empty; re_used = StringSet.empty }
(* For public global identifiers, we must keep their names *)
let enter_global env id =
{ re_id = IdentMap.add id id env.re_id;
re_used = StringSet.add id.name env.re_used }
(* For static or local identifiers, we make up a new name if needed *)
(* If the same identifier has already been declared,
don't rename a second time *)
let rename env id =
if IdentMap.mem id env.re_id then (id, env) else begin
let basename =
if id.name = "" then Printf.sprintf "_%d" id.stamp else id.name in
let newname =
if not (StringSet.mem basename env.re_used) then basename else begin
let rec find_name n =
let s = Printf.sprintf "%s__%d" basename n in
if StringSet.mem s env.re_used
then find_name (n+1)
else s
in find_name 1
end in
let newid = {name = newname; stamp = id.stamp } in
( newid,
{ re_id = IdentMap.add id newid env.re_id;
re_used = StringSet.add newname env.re_used } )
end
(* Monadic map to thread an environment *)
let rec mmap (f: rename_env -> 'a -> 'b * rename_env) env = function
| [] -> ([], env)
| hd :: tl ->
let (hd', env1) = f env hd in
let (tl', env2) = mmap f env1 tl in
(hd' :: tl', env2)
(* Renaming *)
let ident env id =
try
IdentMap.find id env.re_id
with Not_found ->
Errors.fatal_error "Internal error: Rename: %s__%d unbound"
id.name id.stamp
let rec typ env = function
| TPtr(ty, a) -> TPtr(typ env ty, a)
| TArray(ty, sz, a) -> TArray(typ env ty, sz, a)
| TFun(res, None, va, a) -> TFun(typ env res, None, va, a)
| TFun(res, Some p, va, a) ->
let (p', _) = mmap param env p in
TFun(typ env res, Some p', va, a)
| TNamed(id, a) -> TNamed(ident env id, a)
| TStruct(id, a) -> TStruct(ident env id, a)
| TUnion(id, a) -> TUnion(ident env id, a)
| ty -> ty
and param env (id, ty) =
if id.name = "" then
((id, typ env ty), env)
else
let (id', env') = rename env id in ((id', typ env' ty), env')
let constant env = function
| CEnum(id, v) -> CEnum(ident env id, v)
| cst -> cst
let rec exp env e =
{ edesc = exp_desc env e.edesc; etyp = typ env e.etyp }
and exp_desc env = function
| EConst cst -> EConst(constant env cst)
| ESizeof ty -> ESizeof(typ env ty)
| EVar id -> EVar(ident env id)
| EUnop(op, a) -> EUnop(op, exp env a)
| EBinop(op, a, b, ty) -> EBinop(op, exp env a, exp env b, typ env ty)
| EConditional(a, b, c) -> EConditional(exp env a, exp env b, exp env c)
| ECast(ty, a) -> ECast(typ env ty, exp env a)
| ECall(a, al) -> ECall(exp env a, List.map (exp env) al)
let optexp env = function
| None -> None
| Some a -> Some (exp env a)
let field env f =
{ fld_name = f.fld_name;
fld_typ = typ env f.fld_typ;
fld_bitfield = f.fld_bitfield }
let rec init env = function
| Init_single e -> Init_single(exp env e)
| Init_array il -> Init_array (List.map (init env) il)
| Init_struct(id, il) ->
Init_struct(ident env id,
List.map (fun (f, i) -> (field env f, init env i)) il)
| Init_union(id, f, i) ->
Init_union(ident env id, field env f, init env i)
let decl env (sto, id, ty, int) =
let (id', env') = rename env id in
((sto,
id',
typ env' ty,
match int with None -> None | Some i -> Some(init env' i)),
env')
let rec stmt env s =
{ sdesc = stmt_desc env s.sdesc; sloc = s.sloc }
and stmt_desc env = function
| Sskip -> Sskip
| Sdo a -> Sdo (exp env a)
| Sseq(s1, s2) -> Sseq(stmt env s1, stmt env s2)
| Sif(a, s1, s2) -> Sif(exp env a, stmt env s1, stmt env s2)
| Swhile(a, s) -> Swhile(exp env a, stmt env s)
| Sdowhile(s, a) -> Sdowhile(stmt env s, exp env a)
| Sfor(a1, a2, a3, s) ->
Sfor(stmt env a1, exp env a2, stmt env a3, stmt env s)
| Sbreak -> Sbreak
| Scontinue -> Scontinue
| Sswitch(a, s) -> Sswitch(exp env a, stmt env s)
| Slabeled(lbl, s) -> Slabeled(slabel env lbl, stmt env s)
| Sgoto lbl -> Sgoto lbl
| Sreturn a -> Sreturn (optexp env a)
| Sblock sl -> let (sl', _) = mmap stmt_or_decl env sl in Sblock sl'
| Sdecl d -> assert false
and stmt_or_decl env s =
match s.sdesc with
| Sdecl d ->
let (d', env') = decl env d in
({ sdesc = Sdecl d'; sloc = s.sloc}, env')
| _ ->
(stmt env s, env)
and slabel env = function
| Scase e -> Scase(exp env e)
| sl -> sl
let fundef env f =
let (name', env0) = rename env f.fd_name in
let (params', env1) = mmap param env0 f.fd_params in
let (locals', env2) = mmap decl env1 f.fd_locals in
( { fd_storage = f.fd_storage;
fd_inline = f.fd_inline;
fd_name = name';
fd_ret = typ env0 f.fd_ret;
fd_params = params';
fd_vararg = f.fd_vararg;
fd_locals = locals';
fd_body = stmt env2 f.fd_body },
env0 )
let enum env (id, opte) =
let (id', env') = rename env id in
((id', optexp env' opte), env')
let rec globdecl env g =
let (desc', env') = globdecl_desc env g.gdesc in
( { gdesc = desc'; gloc = g.gloc }, env' )
and globdecl_desc env = function
| Gdecl d ->
let (d', env') = decl env d in
(Gdecl d', env')
| Gfundef fd ->
let (fd', env') = fundef env fd in
(Gfundef fd', env')
| Gcompositedecl(kind, id) ->
let (id', env') = rename env id in
(Gcompositedecl(kind, id'), env')
| Gcompositedef(kind, id, members) ->
(Gcompositedef(kind, ident env id, List.map (field env) members), env)
| Gtypedef(id, ty) ->
let (id', env') = rename env id in
(Gtypedef(id', typ env' ty), env')
| Genumdef(id, members) ->
let (id', env') = rename env id in
let (members', env'') = mmap enum env' members in
(Genumdef(id', members'), env'')
| Gpragma s ->
(Gpragma s, env)
let rec globdecls env accu = function
| [] -> List.rev accu
| dcl :: rem ->
let (dcl', env') = globdecl env dcl in
globdecls env' (dcl' :: accu) rem
(* Reserve names of builtins *)
let reserve_builtins () =
List.fold_left enter_global empty_env (Builtins.identifiers())
(* Reserve global declarations with public visibility *)
let rec reserve_public env = function
| [] -> env
| dcl :: rem ->
let env' =
match dcl.gdesc with
| Gdecl(sto, id, _, _) ->
begin match sto with
| Storage_default | Storage_extern -> enter_global env id
| Storage_static -> env
| _ -> assert false
end
| Gfundef f ->
begin match f.fd_storage with
| Storage_default | Storage_extern -> enter_global env f.fd_name
| Storage_static -> env
| _ -> assert false
end
| _ -> env in
reserve_public env' rem
(* Rename the program *)
let program p =
globdecls
(reserve_public (reserve_builtins()) p)
[] p
|