From 891377ce1962cdb31357d6580d6546ec22df2b4f Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 3 Mar 2010 10:22:27 +0000 Subject: Switching to the new C parser/elaborator/simplifier git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cparser/Rename.ml | 253 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 253 insertions(+) create mode 100644 cparser/Rename.ml (limited to 'cparser/Rename.ml') diff --git a/cparser/Rename.ml b/cparser/Rename.ml new file mode 100644 index 0000000..6b94631 --- /dev/null +++ b/cparser/Rename.ml @@ -0,0 +1,253 @@ +(* *********************************************************************) +(* *) +(* 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_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.builtin_idents + +(* 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 + -- cgit v1.2.3