cparser/Rename.ml

   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
  18 open C
  19 open Cutil
  20
  21 module StringSet = Set.Make(String)
  22
  23 type rename_env = {
  24   re_id: ident IdentMap.t;
  25   re_used: StringSet.t
  26 }
  27
  28 let empty_env = { re_id = IdentMap.empty; re_used = StringSet.empty }
  29
  30 (* For public global identifiers, we must keep their names *)
  31
  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 }
  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
  40 let 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
  61 let 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
  70 let 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
  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)
  87   | ty -> ty
  88
  89 and 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
  95 let constant env = function
  96   | CEnum(id, v) -> CEnum(ident env id, v)
  97   | cst -> cst
  98
  99 let rec exp env e =
 100   { edesc = exp_desc env e.edesc; etyp = typ env e.etyp }
 101
 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)
 111
 112 let optexp env = function
 113   | None -> None
 114   | Some a -> Some (exp env a)
 115
 116 let field env f =
 117   { fld_name = f.fld_name;
 118     fld_typ = typ env f.fld_typ;
 119     fld_bitfield = f.fld_bitfield }
 120
 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)
 129
 130 let 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
 138 let rec stmt env s =
 139   { sdesc = stmt_desc env s.sdesc; sloc = s.sloc }
 140
 141 and 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
 159 and 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
 167 and slabel env = function
 168   | Scase e -> Scase(exp env e)
 169   | sl -> sl
 170
 171 let 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
 185 let enum env (id, opte) =
 186   let (id', env') = rename env id in
 187   ((id', optexp env' opte), env')
 188
 189 let rec globdecl env g =
 190   let (desc', env') = globdecl_desc env g.gdesc in
 191   ( { gdesc = desc'; gloc = g.gloc }, env' )
 192
 193 and globdecl_desc env = function
 194   | Gdecl d ->
 195       let (d', env') = decl env d in
 196       (Gdecl 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
 215 let 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
 223 let reserve_builtins () =
 224   List.fold_left enter_global empty_env (Builtins.identifiers())
 225
 226 (* Reserve global declarations with public visibility *)
 227
 228 let 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
 250 let program p =
 251   globdecls
 252     (reserve_public (reserve_builtins()) p)
 253     [] p
 254