diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-21 08:48:20 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-21 08:48:20 +0100 |
commit | 01e32a075023ce7b037d42d048b1904ba3d9a82b (patch) | |
tree | 2d01f3855234e6eb945b929e489232001c406592 /backend/Unusedglob.v | |
parent | 093e0ea167fde39429bf4bd3fc693a232af0d093 (diff) | |
parent | 1fdca8371317e656cb08eaec3adb4596d6447e9b (diff) | |
download | compcert-01e32a075023ce7b037d42d048b1904ba3d9a82b.tar.gz compcert-01e32a075023ce7b037d42d048b1904ba3d9a82b.zip |
Merge branch 'master' into cleanup
Diffstat (limited to 'backend/Unusedglob.v')
-rw-r--r-- | backend/Unusedglob.v | 56 |
1 files changed, 28 insertions, 28 deletions
diff --git a/backend/Unusedglob.v b/backend/Unusedglob.v index 8725c9af..916e111b 100644 --- a/backend/Unusedglob.v +++ b/backend/Unusedglob.v @@ -12,16 +12,9 @@ (** Elimination of unreferenced static definitions *) -Require Import FSets. -Require Import Coqlib. -Require Import Ordered. -Require Import Maps. -Require Import Iteration. -Require Import AST. -Require Import Errors. -Require Import Op. -Require Import Registers. -Require Import RTL. +Require Import FSets Coqlib Maps Ordered Iteration Errors. +Require Import AST Linking. +Require Import Op Registers RTL. Local Open Scope string_scope. @@ -90,6 +83,15 @@ Definition add_ref_definition (pm: prog_map) (id: ident) (w: workset): workset : | Some (Gvar gv) => add_ref_globvar gv w end. +(** The initial workset is composed of all public definitions of the compilation unit, + plus the "main" entry point. *) + +Definition initial_workset (p: program): workset := + add_workset p.(prog_main) + (List.fold_left (fun w id => add_workset id w) + p.(prog_public) + {| w_seen := IS.empty; w_todo := nil |}). + (** Traversal of the dependency graph. *) Definition iter_step (pm: prog_map) (w: workset) : IS.t + workset := @@ -100,20 +102,7 @@ Definition iter_step (pm: prog_map) (w: workset) : IS.t + workset := inr _ (add_ref_definition pm id {| w_seen := w.(w_seen); w_todo := rem |}) end. -Definition initial_workset (p: program): workset := - add_workset p.(prog_main) - (List.fold_left (fun w id => add_workset id w) - p.(prog_public) - {| w_seen := IS.empty; w_todo := nil |}). - -Definition add_def_prog_map (pm: prog_map) (id_df: ident * globdef fundef unit) : prog_map := - PTree.set (fst id_df) (snd id_df) pm. - -Definition program_map (p: program) : prog_map := - List.fold_left add_def_prog_map p.(prog_defs) (PTree.empty _). - -Definition used_globals (p: program) : option IS.t := - let pm := program_map p in +Definition used_globals (p: program) (pm: prog_map) : option IS.t := PrimIter.iterate _ _ (iter_step pm) (initial_workset p). (** * Elimination of unreferenced global definitions *) @@ -130,12 +119,23 @@ Fixpoint filter_globdefs (used: IS.t) (accu defs: list (ident * globdef fundef u else filter_globdefs used accu defs' end. +(** To ensure compatibility with linking, we must ensure that all the + global names referenced are defined in the compilation unit, with + the possible exception of the [prog_main] name. *) + +Definition global_defined (p: program) (pm: prog_map) (id: ident) : bool := + match pm!id with Some _ => true | None => ident_eq id (prog_main p) end. + Definition transform_program (p: program) : res program := - match used_globals p with + let pm := prog_defmap p in + match used_globals p pm with | None => Error (msg "Unusedglob: analysis failed") | Some used => - OK {| prog_defs := filter_globdefs used nil (List.rev p.(prog_defs)); - prog_public := p.(prog_public); - prog_main := p.(prog_main) |} + if IS.for_all (global_defined p pm) used then + OK {| prog_defs := filter_globdefs used nil (List.rev p.(prog_defs)); + prog_public := p.(prog_public); + prog_main := p.(prog_main) |} + else + Error (msg "Unusedglob: reference to undefined global") end. |