diff options
-rw-r--r-- | cfrontend/C2C.ml | 43 | ||||
-rw-r--r-- | cparser/Parse.ml | 2 | ||||
-rw-r--r-- | cparser/Rename.ml | 30 |
3 files changed, 55 insertions, 20 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 1abf3326..1a2a4533 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -839,32 +839,55 @@ let rec translEnv env = function env in translEnv env' gl -(** Eliminate forward declarations of globals that are defined later. *) +(** Eliminate multiple declarations of globals. *) module IdentSet = Set.Make(struct type t = C.ident let compare = compare end) let cleanupGlobals p = + (* First pass: determine what is defined *) + let strong = ref IdentSet.empty (* def functions or variables with inits *) + and weak = ref IdentSet.empty (* variables without inits *) + and extern = ref IdentSet.empty in (* extern decls *) + let classify_def g = + updateLoc g.gloc; + match g.gdesc with + | C.Gfundef fd -> + if IdentSet.mem fd.fd_name !strong then + error ("multiple definitions of " ^ fd.fd_name.name); + strong := IdentSet.add fd.fd_name !strong + | C.Gdecl(Storage_extern, id, ty, init) -> + extern := IdentSet.add id !extern + | C.Gdecl(sto, id, ty, Some i) -> + if IdentSet.mem id !strong then + error ("multiple definitions of " ^ id.name); + strong := IdentSet.add id !strong + | C.Gdecl(sto, id, ty, None) -> + weak := IdentSet.add id !weak + | _ -> () in + List.iter classify_def p; + + (* Second pass: keep "best" definition for each identifier *) let rec clean defs accu = function | [] -> accu | g :: gl -> updateLoc g.gloc; match g.gdesc with - | C.Gdecl(sto, id, ty, None) -> - if IdentSet.mem id defs + | C.Gdecl(sto, id, ty, init) -> + let better_def_exists = + if sto = Storage_extern then + IdentSet.mem id !strong || IdentSet.mem id !weak + else if init = None then + IdentSet.mem id !strong + else + false in + if IdentSet.mem id defs || better_def_exists then clean defs accu gl else clean (IdentSet.add id defs) (g :: accu) gl - | C.Gdecl(_, id, ty, _) -> - if IdentSet.mem id defs then - error ("multiple definitions of " ^ id.name); - clean (IdentSet.add id defs) (g :: accu) gl | C.Gfundef fd -> - if IdentSet.mem fd.fd_name defs then - error ("multiple definitions of " ^ fd.fd_name.name); clean (IdentSet.add fd.fd_name defs) (g :: accu) gl | _ -> clean defs (g :: accu) gl - in clean IdentSet.empty [] (List.rev p) (** Convert a [C.program] into a [Csyntax.program] *) diff --git a/cparser/Parse.ml b/cparser/Parse.ml index 2c467a76..0fc85bf3 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -44,7 +44,7 @@ let preprocessed_file transfs name sourcefile = let ic = open_in sourcefile in let p = try - Rename.program (transform_program t (Elab.elab_preprocessed_file name ic)) + transform_program t (Elab.elab_preprocessed_file name ic) with Parsing.Parse_error -> Errors.error "Error during parsing"; [] | Errors.Abort -> diff --git a/cparser/Rename.ml b/cparser/Rename.ml index 0ce401f1..76c3c12c 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -19,26 +19,38 @@ open C open Cutil module StringSet = Set.Make(String) +module StringMap = Map.Make(String) type rename_env = { re_id: ident IdentMap.t; + re_public: ident StringMap.t; re_used: StringSet.t } -let empty_env = { re_id = IdentMap.empty; re_used = StringSet.empty } +let empty_env = + { re_id = IdentMap.empty; + re_public = StringMap.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 } +let enter_public env id = + try + let id' = StringMap.find id.name env.re_public in + { env with re_id = IdentMap.add id id' env.re_id } + with Not_found -> + { re_id = IdentMap.add id id env.re_id; + re_public = StringMap.add id.name id env.re_public; + 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 + try + (IdentMap.find id env.re_id, env) + with Not_found -> let basename = if id.name = "" then Printf.sprintf "_%d" id.stamp else id.name in let newname = @@ -53,8 +65,8 @@ let rename env id = let newid = {name = newname; stamp = id.stamp } in ( newid, { re_id = IdentMap.add id newid env.re_id; + re_public = env.re_public; re_used = StringSet.add newname env.re_used } ) - end (* Monadic map to thread an environment *) @@ -223,7 +235,7 @@ let rec globdecls env accu = function (* Reserve names of builtins *) let reserve_builtins () = - List.fold_left enter_global empty_env (Builtins.identifiers()) + List.fold_left enter_public empty_env (Builtins.identifiers()) (* Reserve global declarations with public visibility *) @@ -234,13 +246,13 @@ let rec reserve_public env = function match dcl.gdesc with | Gdecl(sto, id, _, _) -> begin match sto with - | Storage_default | Storage_extern -> enter_global env id + | Storage_default | Storage_extern -> enter_public 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_default | Storage_extern -> enter_public env f.fd_name | Storage_static -> env | _ -> assert false end |