1 (* *********************************************************************)
3 (* The Compcert verified compiler *)
5 (* Xavier Leroy, INRIA Paris-Rocquencourt *)
7 (* Copyright Institut National de Recherche en Informatique et en *)
8 (* Automatique. All rights reserved. This file is distributed *)
9 (* under the terms of the GNU General Public License as published by *)
10 (* the Free Software Foundation, either version 2 of the License, or *)
11 (* (at your option) any later version. This file is also distributed *)
12 (* under the terms of the INRIA Non-Commercial License Agreement. *)
14 (* *********************************************************************)
16 (* Renaming of identifiers *)
21 module StringSet = Set.Make(String)
24 re_id: ident IdentMap.t;
28 let empty_env = { re_id = IdentMap.empty; re_used = StringSet.empty }
30 (* For public global identifiers, we must keep their names *)
32 let enter_global env id =
33 { re_id = IdentMap.add id id env.re_id;
34 re_used = StringSet.add id.name env.re_used }
36 (* For static or local identifiers, we make up a new name if needed *)
37 (* If the same identifier has already been declared,
38 don't rename a second time *)
41 if IdentMap.mem id env.re_id then (id, env) else begin
43 if id.name = "" then Printf.sprintf "_%d" id.stamp else id.name in
45 if not (StringSet.mem basename env.re_used) then basename else begin
47 let s = Printf.sprintf "%s__%d" basename n in
48 if StringSet.mem s env.re_used
53 let newid = {name = newname; stamp = id.stamp } in
55 { re_id = IdentMap.add id newid env.re_id;
56 re_used = StringSet.add newname env.re_used } )
59 (* Monadic map to thread an environment *)
61 let rec mmap (f: rename_env -> 'a -> 'b * rename_env) env = function
64 let (hd', env1) = f env hd in
65 let (tl', env2) = mmap f env1 tl in
72 IdentMap.find id env.re_id
74 Errors.fatal_error "Internal error: Rename: %s__%d unbound"
77 let rec typ env = function
78 | TPtr(ty, a) -> TPtr(typ env ty, a)
79 | TArray(ty, sz, a) -> TArray(typ env ty, sz, a)
80 | TFun(res, None, va, a) -> TFun(typ env res, None, va, a)
81 | TFun(res, Some p, va, a) ->
82 let (p', _) = mmap param env p in
83 TFun(typ env res, Some p', va, a)
84 | TNamed(id, a) -> TNamed(ident env id, a)
85 | TStruct(id, a) -> TStruct(ident env id, a)
86 | TUnion(id, a) -> TUnion(ident env id, a)
89 and param env (id, ty) =
91 ((id, typ env ty), env)
93 let (id', env') = rename env id in ((id', typ env' ty), env')
95 let constant env = function
96 | CEnum(id, v) -> CEnum(ident env id, v)
100 { edesc = exp_desc env e.edesc; etyp = typ env e.etyp }
102 and exp_desc env = function
103 | EConst cst -> EConst(constant env cst)
104 | ESizeof ty -> ESizeof(typ env ty)
105 | EVar id -> EVar(ident env id)
106 | EUnop(op, a) -> EUnop(op, exp env a)
107 | EBinop(op, a, b, ty) -> EBinop(op, exp env a, exp env b, typ env ty)
108 | EConditional(a, b, c) -> EConditional(exp env a, exp env b, exp env c)
109 | ECast(ty, a) -> ECast(typ env ty, exp env a)
110 | ECall(a, al) -> ECall(exp env a, List.map (exp env) al)
112 let optexp env = function
114 | Some a -> Some (exp env a)
117 { fld_name = f.fld_name;
118 fld_typ = typ env f.fld_typ;
119 fld_bitfield = f.fld_bitfield }
121 let rec init env = function
122 | Init_single e -> Init_single(exp env e)
123 | Init_array il -> Init_array (List.map (init env) il)
124 | Init_struct(id, il) ->
125 Init_struct(ident env id,
126 List.map (fun (f, i) -> (field env f, init env i)) il)
127 | Init_union(id, f, i) ->
128 Init_union(ident env id, field env f, init env i)
130 let decl env (sto, id, ty, int) =
131 let (id', env') = rename env id in
135 match int with None -> None | Some i -> Some(init env' i)),
139 { sdesc = stmt_desc env s.sdesc; sloc = s.sloc }
141 and stmt_desc env = function
143 | Sdo a -> Sdo (exp env a)
144 | Sseq(s1, s2) -> Sseq(stmt env s1, stmt env s2)
145 | Sif(a, s1, s2) -> Sif(exp env a, stmt env s1, stmt env s2)
146 | Swhile(a, s) -> Swhile(exp env a, stmt env s)
147 | Sdowhile(s, a) -> Sdowhile(stmt env s, exp env a)
148 | Sfor(a1, a2, a3, s) ->
149 Sfor(stmt env a1, exp env a2, stmt env a3, stmt env s)
151 | Scontinue -> Scontinue
152 | Sswitch(a, s) -> Sswitch(exp env a, stmt env s)
153 | Slabeled(lbl, s) -> Slabeled(slabel env lbl, stmt env s)
154 | Sgoto lbl -> Sgoto lbl
155 | Sreturn a -> Sreturn (optexp env a)
156 | Sblock sl -> let (sl', _) = mmap stmt_or_decl env sl in Sblock sl'
157 | Sdecl d -> assert false
159 and stmt_or_decl env s =
162 let (d', env') = decl env d in
163 ({ sdesc = Sdecl d'; sloc = s.sloc}, env')
167 and slabel env = function
168 | Scase e -> Scase(exp env e)
172 let (name', env0) = rename env f.fd_name in
173 let (params', env1) = mmap param env0 f.fd_params in
174 let (locals', env2) = mmap decl env1 f.fd_locals in
175 ( { fd_storage = f.fd_storage;
176 fd_inline = f.fd_inline;
178 fd_ret = typ env0 f.fd_ret;
180 fd_vararg = f.fd_vararg;
182 fd_body = stmt env2 f.fd_body },
185 let enum env (id, opte) =
186 let (id', env') = rename env id in
187 ((id', optexp env' opte), env')
189 let rec globdecl env g =
190 let (desc', env') = globdecl_desc env g.gdesc in
191 ( { gdesc = desc'; gloc = g.gloc }, env' )
193 and globdecl_desc env = function
195 let (d', env') = decl env d in
198 let (fd', env') = fundef env fd in
200 | Gcompositedecl(kind, id) ->
201 let (id', env') = rename env id in
202 (Gcompositedecl(kind, id'), env')
203 | Gcompositedef(kind, id, members) ->
204 (Gcompositedef(kind, ident env id, List.map (field env) members), env)
205 | Gtypedef(id, ty) ->
206 let (id', env') = rename env id in
207 (Gtypedef(id', typ env' ty), env')
208 | Genumdef(id, members) ->
209 let (id', env') = rename env id in
210 let (members', env'') = mmap enum env' members in
211 (Genumdef(id', members'), env'')
215 let rec globdecls env accu = function
216 | [] -> List.rev accu
218 let (dcl', env') = globdecl env dcl in
219 globdecls env' (dcl' :: accu) rem
221 (* Reserve names of builtins *)
223 let reserve_builtins () =
224 List.fold_left enter_global empty_env (Builtins.identifiers())
226 (* Reserve global declarations with public visibility *)
228 let rec reserve_public env = function
233 | Gdecl(sto, id, _, _) ->
235 | Storage_default | Storage_extern -> enter_global env id
236 | Storage_static -> env
240 begin match f.fd_storage with
241 | Storage_default | Storage_extern -> enter_global env f.fd_name
242 | Storage_static -> env
246 reserve_public env' rem
248 (* Rename the program *)
252 (reserve_public (reserve_builtins()) p)