source: Deliverables/D2.3/8051-memoryspaces-branch/cparser/Rename.ml @ 460

Last change on this file since 460 was 460, checked in by campbell, 9 years ago

Port memory spaces changes to latest prototype compiler.

File size: 8.0 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
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.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* Renaming of identifiers *)
17
18open C
19open Cutil
20
21module StringSet = Set.Make(String)
22
23type rename_env = {
24  re_id: ident IdentMap.t;
25  re_used: StringSet.t
26}
27
28let empty_env = { re_id = IdentMap.empty; re_used = StringSet.empty }
29
30(* For public global identifiers, we must keep their names *)
31
32let enter_global env id =
33  { re_id = IdentMap.add id id env.re_id;
34    re_used = StringSet.add id.name env.re_used }
35
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 *)
39
40let rename env id =
41  if IdentMap.mem id env.re_id then (id, env) else begin
42    let basename =
43      if id.name = "" then Printf.sprintf "_%d" id.stamp else id.name in
44    let newname =
45      if not (StringSet.mem basename env.re_used) then basename else begin
46        let rec find_name n =
47          let s = Printf.sprintf "%s__%d" basename n in
48          if StringSet.mem s env.re_used
49          then find_name (n+1)
50          else s
51        in find_name 1
52      end in
53    let newid = {name = newname; stamp = id.stamp } in
54    ( newid,
55      { re_id = IdentMap.add id newid env.re_id;
56        re_used = StringSet.add newname env.re_used } )
57  end
58
59(* Monadic map to thread an environment *)
60
61let rec mmap (f: rename_env -> 'a -> 'b * rename_env) env = function
62  | [] -> ([], env)
63  | hd :: tl ->
64      let (hd', env1) = f env hd in
65      let (tl', env2) = mmap f env1 tl in
66      (hd' :: tl', env2)
67
68(* Renaming *)
69
70let ident env id =
71  try
72    IdentMap.find id env.re_id
73  with Not_found ->
74    Errors.fatal_error "Internal error: Rename: %s__%d unbound" 
75                       id.name id.stamp
76
77let rec typ env = function
78  | TPtr(sp, ty, a) -> TPtr(sp, typ env ty, a)
79  | TArray(sp, ty, sz, a) -> TArray(sp, 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)
87  | ty -> ty
88
89and param env (id, ty) =
90  if id.name = "" then 
91    ((id, typ env ty), env)
92  else
93    let (id', env') = rename env id in ((id', typ env' ty), env')
94
95let constant env = function
96  | CEnum(id, v) -> CEnum(ident env id, v)
97  | cst -> cst
98
99let rec exp env e =
100  { edesc = exp_desc env e.edesc; etyp = typ env e.etyp; espace = e.espace }
101
102and 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)
111
112let optexp env = function
113  | None -> None
114  | Some a -> Some (exp env a)
115
116let field env f =
117  { fld_name = f.fld_name;
118    fld_typ = typ env f.fld_typ;
119    fld_bitfield = f.fld_bitfield }
120
121let 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)
129
130let decl env (sto, id, ty, int) =
131  let (id', env') = rename env id in
132  ((sto,
133    id',
134    typ env' ty,
135    match int with None -> None | Some i -> Some(init env' i)),
136   env')
137
138let rec stmt env s =
139  { sdesc = stmt_desc env s.sdesc; sloc = s.sloc }
140
141and stmt_desc env = function
142  | Sskip -> Sskip
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)
150  | Sbreak -> Sbreak
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
158
159and stmt_or_decl env s =
160  match s.sdesc with
161  | Sdecl d ->
162      let (d', env') = decl env d in
163      ({ sdesc = Sdecl d'; sloc = s.sloc}, env')
164  | _ ->
165      (stmt env s, env)
166
167and slabel env = function
168  | Scase e -> Scase(exp env e)
169  | sl -> sl
170
171let fundef env f =
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;
177      fd_name = name';
178      fd_ret = typ env0 f.fd_ret;
179      fd_params = params';
180      fd_vararg = f.fd_vararg;
181      fd_locals = locals';
182      fd_body = stmt env2 f.fd_body },
183    env0 )
184
185let enum env (id, opte) = 
186  let (id', env') = rename env id in
187  ((id', optexp env' opte), env')
188
189let rec globdecl env g =
190  let (desc', env') = globdecl_desc env g.gdesc in
191  ( { gdesc = desc'; gloc = g.gloc }, env' )
192
193and globdecl_desc env = function
194  | Gdecl (sp,d) ->
195      let (d', env') = decl env d in
196      (Gdecl (sp,d'), env')
197  | Gfundef fd ->
198      let (fd', env') = fundef env fd in
199      (Gfundef fd', env')
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'')
212  | Gpragma s ->
213      (Gpragma s, env)
214
215let rec globdecls env accu = function
216  | [] -> List.rev accu
217  | dcl :: rem ->
218      let (dcl', env') = globdecl env dcl in
219      globdecls env' (dcl' :: accu) rem
220
221(* Reserve names of builtins *)
222
223let reserve_builtins () =
224  List.fold_left enter_global empty_env (Builtins.identifiers())
225
226(* Reserve global declarations with public visibility *)
227
228let rec reserve_public env = function
229  | [] -> env
230  | dcl :: rem ->
231      let env' =
232        match dcl.gdesc with
233        | Gdecl (_, (sto, id, _, _)) ->
234            begin match sto with
235            | Storage_default | Storage_extern -> enter_global env id
236            | Storage_static -> env
237            | _ -> assert false
238            end
239        | Gfundef f ->
240            begin match f.fd_storage with
241            | Storage_default | Storage_extern -> enter_global env f.fd_name
242            | Storage_static -> env
243            | _ -> assert false
244            end
245        | _ -> env in
246      reserve_public env' rem
247
248(* Rename the program *)
249
250let program p =
251  globdecls
252    (reserve_public (reserve_builtins()) p)
253    [] p
254 
Note: See TracBrowser for help on using the repository browser.