diff options
Diffstat (limited to 'backend/Unusedglob.ml')
-rw-r--r-- | backend/Unusedglob.ml | 90 |
1 files changed, 0 insertions, 90 deletions
diff --git a/backend/Unusedglob.ml b/backend/Unusedglob.ml deleted file mode 100644 index 1a88ee96..00000000 --- a/backend/Unusedglob.ml +++ /dev/null @@ -1,90 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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 INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Removing unused definitions of static functions and global variables *) - -open Camlcoq -open Maps -open AST -open Asm -open Unusedglob1 - -module IdentSet = Set.Make(struct type t = ident let compare = compare end) - -(* The set of globals referenced from a function definition *) - -let add_referenced_instr rf i = - List.fold_right IdentSet.add (referenced_instr i) rf - -let referenced_function f = - List.fold_left add_referenced_instr IdentSet.empty (code_of_function f) - -(* The set of globals referenced from a variable definition (initialization) *) - -let add_referenced_init_data rf = function - | Init_addrof(id, ofs) -> IdentSet.add id rf - | _ -> rf - -let referenced_globvar gv = - List.fold_left add_referenced_init_data IdentSet.empty gv.gvar_init - -(* The map global |-> set of globals it references *) - -let referenced_globdef gd = - match gd with - | Gfun(Internal f) -> referenced_function f - | Gfun(External ef) -> IdentSet.empty - | Gvar gv -> referenced_globvar gv - -let use_map p = - List.fold_left (fun m (id, gd) -> PTree.set id (referenced_globdef gd) m) - PTree.empty p.prog_defs - -(* Worklist algorithm computing the set of used globals *) - -let rec used_idents usemap used wrk = - match wrk with - | [] -> used - | id :: wrk -> - if IdentSet.mem id used then used_idents usemap used wrk else - match PTree.get id usemap with - | None -> used_idents usemap used wrk - | Some s -> used_idents usemap (IdentSet.add id used) - (IdentSet.fold (fun id l -> id::l) s wrk) - -(* The worklist is initially populated with all nonstatic globals *) - -let add_nonstatic wrk id = - if C2C.atom_is_static id then wrk else id :: wrk - -let initial_worklist p = - List.fold_left (fun wrk (id, gd) -> add_nonstatic wrk id) - [] p.prog_defs - -(* Eliminate unused definitions *) - -let rec filter used = function - | [] -> [] - | (id, def) :: rem -> - if IdentSet.mem id used - then (id, def) :: filter used rem - else filter used rem - -let filter_prog used p = - { prog_defs = filter used p.prog_defs; - prog_main = p.prog_main } - -(* Entry point *) - -let transf_program p = - filter_prog (used_idents (use_map p) IdentSet.empty (initial_worklist p)) p - |