1
(**************************************************************************)
3
(* Copyright (C) 2001-2003, *)
4
(* George C. Necula <necula@cs.berkeley.edu> *)
5
(* Scott McPeak <smcpeak@cs.berkeley.edu> *)
6
(* Wes Weimer <weimer@cs.berkeley.edu> *)
7
(* Ben Liblit <liblit@cs.berkeley.edu> *)
8
(* All rights reserved. *)
10
(* Redistribution and use in source and binary forms, with or without *)
11
(* modification, are permitted provided that the following conditions *)
14
(* 1. Redistributions of source code must retain the above copyright *)
15
(* notice, this list of conditions and the following disclaimer. *)
17
(* 2. Redistributions in binary form must reproduce the above copyright *)
18
(* notice, this list of conditions and the following disclaimer in the *)
19
(* documentation and/or other materials provided with the distribution. *)
21
(* 3. The names of the contributors may not be used to endorse or *)
22
(* promote products derived from this software without specific prior *)
23
(* written permission. *)
25
(* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS *)
26
(* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT *)
27
(* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS *)
28
(* FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE *)
29
(* COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, *)
30
(* INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, *)
31
(* BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; *)
32
(* LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER *)
33
(* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT *)
34
(* LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN *)
35
(* ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE *)
36
(* POSSIBILITY OF SUCH DAMAGE. *)
38
(* File modified by CEA (Commissariat � l'�nergie Atomique). *)
39
(**************************************************************************)
42
(* implementation for rmtmps.mli *)
51
(* Set on the command-line: *)
52
let keepUnused = ref false
53
let rmUnusedInlines = ref false
54
let rmUnusedStatic = ref false
55
let rmEmptyInlines = ref true
57
let trace = Trace.trace "rmtmps"
61
(***********************************************************************
63
* Clearing of "referenced" bits
68
let clearReferencedBits file =
69
let considerGlobal global =
72
(*trace (dprintf "clearing mark: %a\n" d_shortglobal global);*)
73
info.treferenced <- false
76
| GEnumTagDecl (info, _) ->
77
(*trace (dprintf "clearing mark: %a\n" d_shortglobal global);*)
78
info.ereferenced <- false
81
| GCompTagDecl (info, _) ->
82
(*trace (dprintf "clearing mark: %a\n" d_shortglobal global);*)
83
info.creferenced <- false
85
| GVar ({vname = _name} as info, _, _)
86
| GVarDecl (_,({vname = _name} as info), _) ->
87
(*trace (dprintf "clearing mark: %a\n" d_shortglobal global);*)
88
info.vreferenced <- false
90
| GFun ({svar = info} as func, _) ->
91
(* trace (dprintf "clearing mark: %a\n" d_shortglobal global);*)
92
info.vreferenced <- false;
94
(*trace (dprintf "clearing mark: local %s\n" local.vname);*)
95
local.vreferenced <- false
97
List.iter clearMark func.slocals
102
iterGlobals file considerGlobal
105
(***********************************************************************
107
* Scanning and categorization of pragmas
112
(* collections of names of things to keep *)
113
type collection = (string, unit) H.t
115
typedefs : collection;
117
structs : collection;
119
defines : collection;
123
(* rapid transfer of control when we find a malformed pragma *)
126
let ccureddeepcopystring = "ccureddeepcopy"
127
(* Save this length so we don't recompute it each time. *)
128
let ccureddeepcopystring_length = String.length ccureddeepcopystring
130
(* CIL and CCured define several pragmas which prevent removal of
131
* various global varinfos. Here we scan for those pragmas and build
132
* up collections of the corresponding varinfos' names.
135
let categorizePragmas file =
137
(* names of things which should be retained *)
139
typedefs = H.create 0;
141
structs = H.create 0;
146
(* populate these name collections in light of each pragma *)
149
let badPragma location pragma =
150
ignore (warnLoc location "Invalid argument to pragma %s" pragma)
154
| GPragma (Attr ("cilnoremove" as directive, args), location) ->
155
(* a very flexible pragma: can retain typedefs, enums,
156
* structs, unions, or globals (functions or variables) *)
162
(* isolate and categorize one varinfo name *)
163
let collection, name =
164
(* Two words denotes a typedef, enum, struct, or
165
* union, as in "type foo" or "enum bar". A
166
* single word denotes a global function or
168
let whitespace = Str.regexp "[ \t]+" in
169
let words = Str.split whitespace specifier in
172
keepers.typedefs, name
175
| ["struct"; name] ->
176
keepers.structs, name
180
keepers.defines, name
184
H.add collection name ()
188
badPragma location directive
190
List.iter processArg args
192
| GVarDecl (_,v, _) -> begin
193
(* Look for alias attributes, e.g. Linux modules *)
194
match filterAttributes "alias" v.vattr with
195
[] -> () (* ordinary prototype. *)
196
| [Attr("alias", [AStr othername])] ->
197
H.add keepers.defines othername ()
200
(error "Bad alias attribute at %a" d_loc (CurrentLoc.get ()))
203
(*** Begin CCured-specific checks: ***)
204
(* these pragmas indirectly require that we keep the function named in
205
-- the first arguments of boxmodelof and ccuredwrapperof, and
206
-- the third argument of ccureddeepcopy*. *)
207
| GPragma (Attr("ccuredwrapper" as directive, attribute :: _), location) ->
211
H.add keepers.defines name ()
213
badPragma location directive
215
| GPragma (Attr("ccuredvararg", _funcname :: (ASizeOf t) :: _), _location) ->
218
| TComp(c,_) when c.cstruct -> (* struct *)
219
H.add keepers.structs c.cname ()
220
| TComp(c,_) -> (* union *)
221
H.add keepers.unions c.cname ()
223
H.add keepers.typedefs ti.tname ()
225
H.add keepers.enums ei.ename ()
229
| GPragma (Attr(directive, _ :: _ :: attribute :: _), location)
230
when String.length directive > ccureddeepcopystring_length
231
&& (Str.first_chars directive ccureddeepcopystring_length)
232
= ccureddeepcopystring ->
236
H.add keepers.defines name ()
238
badPragma location directive
240
(** end CCured-specific stuff **)
244
iterGlobals file considerPragma;
249
(***********************************************************************
251
* Function body elimination from pragmas
256
(* When performing global slicing, any functions not explicitly marked
257
* as pragma roots are reduced to mere declarations. This leaves one
258
* with a reduced source file that still compiles to object code, but
259
* which contains the bodies of only explicitly retained functions.
262
let amputateFunctionBodies keptGlobals file =
263
let considerGlobal = function
264
| GFun ({svar = {vname = name} as info}, location)
265
when not (H.mem keptGlobals name) ->
266
trace (dprintf "slicing: reducing to prototype: function %s\n" name);
267
GVarDecl (empty_funspec(),info, location)
271
mapGlobals file considerGlobal
275
(***********************************************************************
277
* Root collection from pragmas
282
let isPragmaRoot keepers = function
283
| GType ({tname = name}, _) ->
284
H.mem keepers.typedefs name
285
| GEnumTag ({ename = name}, _)
286
| GEnumTagDecl ({ename = name}, _) ->
287
H.mem keepers.enums name
288
| GCompTag ({cname = name; cstruct = structure}, _)
289
| GCompTagDecl ({cname = name; cstruct = structure}, _) ->
290
let collection = if structure then keepers.structs else keepers.unions in
291
H.mem collection name
292
| GVar ({vname = name; vattr = attrs}, _, _)
293
| GVarDecl (_,{vname = name; vattr = attrs}, _)
294
| GFun ({svar = {vname = name; vattr = attrs}}, _) ->
295
H.mem keepers.defines name ||
296
hasAttribute "used" attrs
302
(***********************************************************************
304
* Common root collecting utilities
309
let traceRoot _reason _global =
310
(* trace (dprintf "root (%s): %a@!" reason d_shortglobal global);*)
314
let traceNonRoot _reason _global =
315
(* trace (dprintf "non-root (%s): %a@!" reason d_shortglobal global);*)
319
let hasExportingAttribute funvar =
320
let rec isExportingAttribute = function
321
| Attr ("constructor", []) -> true
322
| Attr ("destructor", []) -> true
325
List.exists isExportingAttribute funvar.vattr
329
(***********************************************************************
331
* Root collection from external linkage
336
(* Exported roots are those global varinfos which are visible to the
337
* linker and dynamic loader. For variables, this consists of
338
* anything that is not "static". For functions, this consists of:
340
* - functions bearing a "constructor" or "destructor" attribute
341
* - functions declared extern but not inline
342
* - functions declared neither inline nor static
344
* gcc incorrectly (according to C99) makes inline functions visible to
345
* the linker. So we can only remove inline functions on MSVC.
348
let isExportedRoot global =
349
let result, _reason = match global with
350
| GVar ({vstorage = Static}, _, _) ->
351
false, "static variable"
353
true, "non-static variable"
354
| GFun ({svar = v}, _) -> begin
355
if hasExportingAttribute v then
356
true, "constructor or destructor function"
357
else if v.vstorage = Static then
358
not !rmUnusedStatic, "static function"
359
else if v.vinline && v.vstorage != Extern
360
&& (theMachine.msvcMode || !rmUnusedInlines) then
361
false, "inline function"
363
true, "other function"
365
| GVarDecl(_,v,_) when hasAttribute "alias" v.vattr ->
366
true, "has GCC alias attribute"
367
(* | GVarDecl(spec,_,_) when not (Cil.is_empty_funspec spec) ->
368
true, "has formal spec"
370
| GAnnot _ -> true, "global annotation"
372
false, "neither function nor variable nor annotation"
374
(* trace (dprintf "isExportedRoot %a -> %b, %s@!"
375
d_shortglobal global result reason);*)
380
(***********************************************************************
382
* Root collection for complete programs
387
(* Exported roots are "main()" and functions bearing a "constructor"
388
* or "destructor" attribute. These are the only things which must be
389
* retained in a complete program.
392
let isCompleteProgramRoot global =
393
let result = match global with
394
| GFun ({svar = {vname = "main"; vstorage = vstorage}}, _) ->
397
when hasExportingAttribute fundec.svar ->
402
(* trace (dprintf "complete program root -> %b for %a@!" result d_shortglobal global);*)
406
(***********************************************************************
408
* Transitive reachability closure from roots
413
(* This visitor recursively marks all reachable types and variables as used. *)
414
class markReachableVisitor
415
((globalMap: (string, Cil_types.global) H.t),
416
(currentFunc: Cil_types.fundec option ref)) = object (self)
417
inherit nopCilVisitor
419
method vglob = function
420
| GType (typeinfo, _) ->
421
typeinfo.treferenced <- true;
423
| GCompTag (compinfo, _)
424
| GCompTagDecl (compinfo, _) ->
425
compinfo.creferenced <- true;
427
| GEnumTag (enuminfo, _)
428
| GEnumTagDecl (enuminfo, _) ->
429
enuminfo.ereferenced <- true;
431
| GVar (varinfo, _, _)
432
| GVarDecl (_,varinfo, _)
433
| GFun ({svar = varinfo}, _) ->
434
varinfo.vreferenced <- true;
436
| GAnnot _ -> DoChildren
440
method vinst = function
441
Asm (_, tmpls, _, _, _, _) when theMachine.msvcMode ->
442
(* If we have inline assembly on MSVC, we cannot tell which locals
443
* are referenced. Keep thsem all *)
444
(match !currentFunc with
447
let vre = Str.regexp_string (Str.quote v.vname) in
448
if List.exists (fun tmp ->
449
try ignore (Str.search_forward vre tmp 0); true
450
with Not_found -> false)
453
v.vreferenced <- true) fd.slocals
454
| _ -> assert false);
457
Lval(Var {vname = name; vinline = true}, NoOffset), args,loc) ->
458
let glob = Hashtbl.find globalMap name in
461
GFun ({sbody = {bstmts = [] | [{skind = Return (None,_)}]}},_)
465
[Asm ([],["nop"],[],List.map (fun e -> None,"q",e) args ,[],loc)]
472
if not v.vreferenced then
474
let name = v.vname in
476
trace (dprintf "marking transitive use: global %s\n" name)
478
trace (dprintf "marking transitive use: local %s\n" name);
480
(* If this is a global, we need to keep everything used in its
481
* definition and declarations. *)
484
trace (dprintf "descending: global %s\n" name);
486
ignore (visitCilGlobal (self :> cilVisitor) global)
488
let globals = Hashtbl.find_all globalMap name in
489
List.iter descend globals
492
v.vreferenced <- true;
497
method vexpr (e: exp) =
499
Const (CEnum {eihost = ei}) -> ei.ereferenced <- true; DoChildren
504
let visitAttrs attrs =
505
ignore (visitCilAttributes (self :> cilVisitor) attrs)
508
ignore (visitCilType (self :> cilVisitor) typ)
512
let old = e.ereferenced in
515
trace (dprintf "marking transitive use: enum %s\n" e.ename);
516
e.ereferenced <- true;
523
let old = c.creferenced in
526
trace (dprintf "marking transitive use: compound %s\n" c.cname);
527
c.creferenced <- true;
529
(* to recurse, we must ask explicitly *)
530
let recurse f = visitType f.ftype in
531
List.iter recurse c.cfields;
537
| TNamed(ti, attrs) ->
538
let old = ti.treferenced in
541
trace (dprintf "marking transitive use: typedef %s\n" ti.tname);
542
ti.treferenced <- true;
544
(* recurse deeper into the type referred-to by the typedef *)
545
(* to recurse, we must ask explicitly *)
552
(* for anything else, just look inside it *)
563
let markReachable file isRoot =
564
(* build a mapping from global names back to their definitions &
566
let globalMap = Hashtbl.create 137 in
567
let considerGlobal global =
569
| GFun ({svar = info}, _)
571
| GVarDecl (_,info, _) ->
572
Hashtbl.add globalMap info.vname global
576
iterGlobals file considerGlobal;
578
let currentFunc = ref None in
580
(* mark everything reachable from the global roots *)
581
let visitor = new markReachableVisitor (globalMap, currentFunc) in
582
let visitIfRoot global =
583
if isRoot global then
585
(* trace (dprintf "traversing root global: %a\n" d_shortglobal global);*)
587
GFun(fd, _) -> currentFunc := Some fd
588
| _ -> currentFunc := None);
589
ignore (visitCilGlobal visitor global)
592
(* trace (dprintf "skipping non-root global: %a\n" d_shortglobal global)*)
595
iterGlobals file visitIfRoot
598
(**********************************************************************
600
* Marking and removing of unused labels
602
**********************************************************************)
604
(* We keep only one label, preferably one that was not introduced by CIL.
605
* Scan a list of labels and return the data for the label that should be
606
* kept, and the remaining filtered list of labels *)
607
let labelsToKeep (ll: label list) : (string * location * bool) * label list =
608
let rec loop (sofar: string * location * bool) = function
611
let newlabel, keepl =
613
| Case _ | Default _ -> sofar, true
614
| Label (ln, lloc, isorig) -> begin
615
match isorig, sofar with
616
| false, ("", _, _) ->
617
(* keep this one only if we have no label so far *)
618
(ln, lloc, isorig), false
619
| false, _ -> sofar, false
620
| true, (_, _, false) ->
621
(* this is an original label; prefer it to temporary or
623
(ln, lloc, isorig), false
624
| true, _ -> sofar, false
627
let newlabel', rest' = loop newlabel rest in
628
newlabel', (if keepl then l :: rest' else rest')
630
loop ("", Cilutil.locUnknown, false) ll
632
class markUsedLabels (labelMap: (string, unit) H.t) =
633
let keep_label dest =
634
let (ln, _, _), _ = labelsToKeep !dest.labels in
636
(Format.eprintf "@[dest: %a@\n@]@." Cil.d_stmt !dest;
637
E.s (E.bug "rmtmps: destination statement does not have labels"));
638
(* Mark it as used *)
639
H.replace labelMap ln ()
641
let keep_label_logic =
642
function LogicLabel _ -> () | StmtLabel dest -> keep_label dest
645
inherit nopCilVisitor
647
method vstmt (s: stmt) =
649
Goto (dest, _) -> keep_label dest; DoChildren
652
method vterm_node t =
655
| Tat (_,lab) -> keep_label_logic lab
657
let labs = snd (List.split labs) in List.iter keep_label_logic labs
663
method vtsets_elem t =
666
| TSat (_,lab) -> keep_label_logic lab
668
let labs = snd (List.split labs) in List.iter keep_label_logic labs
673
method vpredicate t =
676
| Pat (_,lab) -> keep_label_logic lab
678
let labs = snd (List.split labs) in List.iter keep_label_logic labs
683
(* No need to go into expressions or types *)
684
method vexpr _ = SkipChildren
685
method vtype _ = SkipChildren
688
class removeUnusedLabels (labelMap: (string, unit) H.t) = object
689
inherit nopCilVisitor
691
method vstmt (s: stmt) =
692
let (ln, lloc, lorig), lrest = labelsToKeep s.labels in
694
(if ln <> "" && H.mem labelMap ln then (* We had labels *)
695
(Label(ln, lloc, lorig) :: lrest)
700
(* No need to go into expressions or instructions *)
701
method vexpr _ = SkipChildren
702
method vinst _ = SkipChildren
703
method vtype _ = SkipChildren
706
(***********************************************************************
708
* Removal of unused varinfos
713
(* regular expression matching names of uninteresting locals *)
716
(* Cil.makeTempVar *)
719
(* sm: I don't know where it comes from but these show up all over. *)
720
(* this doesn't seem to do what I wanted.. *)
723
(* various macros in glibc's <bits/string2.h> *)
725
"__s"; "__s1"; "__s2";
726
"__s1_len"; "__s2_len";
729
(* various macros in glibc's <ctype.h> *)
732
(* We remove the __malloc variables *)
735
(* optional alpha renaming *)
736
let alpha = "\\(___[0-9]+\\)?" in
738
let pattern = "\\(" ^ (String.concat "\\|" names) ^ "\\)" ^ alpha ^ "$" in
742
let removeUnmarked isRoot file =
743
let removedLocals = ref [] in
745
let filterGlobal global =
747
(* unused global types, variables, and functions are simply removed *)
748
| GType ({treferenced = false}, _)
749
| GCompTag ({creferenced = false}, _)
750
| GCompTagDecl ({creferenced = false}, _)
751
| GEnumTag ({ereferenced = false}, _)
752
| GEnumTagDecl ({ereferenced = false}, _)
753
| GVar ({vreferenced = false}, _, _)
754
| GFun ({svar = {vreferenced = false}}, _) ->
755
(* trace (dprintf "removing global: %a\n" d_shortglobal global);*)
757
| GVarDecl (_,{vreferenced = false}, _) -> false
759
(* retained functions may wish to discard some unused locals *)
761
let rec filterLocal local =
762
if not local.vreferenced then
764
(* along the way, record the interesting locals that were removed *)
765
let name = local.vname in
766
trace (dprintf "removing local: %s\n" name);
767
if not (Str.string_match uninteresting name 0) then
768
removedLocals := (func.svar.vname ^ "::" ^ name) :: !removedLocals;
772
func.slocals <- List.filter filterLocal func.slocals;
773
(* We also want to remove unused labels. We do it all here, including
774
* marking the used labels *)
775
let usedLabels:(string, unit) H.t = H.create 13 in
776
ignore (visitCilBlock (new markUsedLabels usedLabels) func.sbody);
777
(* And now we scan again and we remove them *)
778
ignore (visitCilBlock (new removeUnusedLabels usedLabels) func.sbody);
781
(* all other globals are retained *)
783
(* trace (dprintf "keeping global: %a\n" d_shortglobal global);*)
784
true) || (isRoot global)
786
file.globals <- List.filter filterGlobal file.globals;
790
(***********************************************************************
797
type rootsFilter = global -> bool
799
let isDefaultRoot = isExportedRoot
801
let rec removeUnusedTemps ?(isRoot : rootsFilter = isDefaultRoot) file =
802
if !keepUnused || Trace.traceActive "disableTmpRemoval" then
803
Trace.trace "disableTmpRemoval" (dprintf "temp removal disabled\n")
806
if !E.verboseFlag then
807
ignore (E.log "Removing unused temporaries\n" );
809
if Trace.traceActive "printCilTree" then
810
dumpFile defaultCilPrinter stdout "stdout" file;
812
(* digest any pragmas that would create additional roots *)
813
let keepers = categorizePragmas file in
815
(* if slicing, remove the bodies of non-kept functions *)
816
if !Cilglobopt.sliceGlobal then
817
amputateFunctionBodies keepers.defines file;
819
(* build up the root set *)
821
isPragmaRoot keepers global ||
825
(* mark everything reachable from the global roots *)
826
clearReferencedBits file;
827
markReachable file isRoot;
829
(* take out the trash *)
830
let removedLocals = removeUnmarked isRoot file in
832
(* print which original source variables were removed *)
833
if false && removedLocals != [] then
834
let count = List.length removedLocals in
836
ignore (E.warn "%d unused local variables removed" count)
838
ignore (E.warn "%d unused local variables removed:@!%a"
839
count (docList ~sep:(chr ',' ++ break) text) removedLocals)
added
removed
cil/src/rmtmps.ml
