123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808809810811812813814815816817818819820(*
Copyright (c) 2001-2002,
George C. Necula <necula@cs.berkeley.edu>
Scott McPeak <smcpeak@cs.berkeley.edu>
Wes Weimer <weimer@cs.berkeley.edu>
Ben Liblit <liblit@cs.berkeley.edu>
All rights reserved.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
met:
1. Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
3. The names of the contributors may not be used to endorse or promote
products derived from this software without specific prior written
permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)(* rmtmps.ml *)(* implementation for rmtmps.mli *)openPrettyopenCilmoduleH=HashtblmoduleE=ErrormsgmoduleU=Util(* Set on the command-line: *)letkeepUnused=reffalseletrmUnusedInlines=reffalselettrace=Trace.trace"rmtmps"(***********************************************************************
Clearing of "referenced" bits
*)letclearReferencedBitsfile=letconsiderGlobalglobal=matchglobalwith|GType(info,_)->trace(dprintf"clearing mark: %a\n"d_shortglobalglobal);info.treferenced<-false|GEnumTag(info,_)|GEnumTagDecl(info,_)->trace(dprintf"clearing mark: %a\n"d_shortglobalglobal);info.ereferenced<-false|GCompTag(info,_)|GCompTagDecl(info,_)->trace(dprintf"clearing mark: %a\n"d_shortglobalglobal);info.creferenced<-false|GVar({vname=name;_}asinfo,_,_)|GVarDecl({vname=name;_}asinfo,_)->trace(dprintf"clearing mark: %a\n"d_shortglobalglobal);info.vreferenced<-false|GFun({svar=info;_}asfunc,_)->trace(dprintf"clearing mark: %a\n"d_shortglobalglobal);info.vreferenced<-false;letclearMarklocal=trace(dprintf"clearing mark: local %s\n"local.vname);local.vreferenced<-falseinList.iterclearMarkfunc.slocals|_->()initerGlobalsfileconsiderGlobal(***********************************************************************
Scanning and categorization of pragmas
*)(* collections of names of things to keep *)typecollection=(string,unit)H.ttypekeepers={typedefs:collection;enums:collection;structs:collection;unions:collection;defines:collection;}(* rapid transfer of control when we find a malformed pragma *)exceptionBad_pragmaletccureddeepcopystring="ccureddeepcopy"(* Save this length so we don't recompute it each time. *)letccureddeepcopystring_length=String.lengthccureddeepcopystring(* CIL and CCured define several pragmas which prevent removal of
various global symbols. Here we scan for those pragmas and build
up collections of the corresponding symbols' names.
*)letcategorizePragmasfile=(* names of things which should be retained *)letkeepers={typedefs=H.create0;enums=H.create0;structs=H.create0;unions=H.create0;defines=H.create1}in(* populate these name collections in light of each pragma *)letconsiderPragma=letbadPragmalocationpragma=ignore(warnLoclocation"Invalid argument to pragma %s"pragma)infunction|GPragma(Attr("cilnoremove"asdirective,args),location)->(* a very flexible pragma: can retain typedefs, enums,
structs, unions, or globals (functions or variables) *)beginletprocessArgarg=trymatchargwith|AStrspecifier->(* isolate and categorize one symbol name *)letcollection,name=(* Two words denotes a typedef, enum, struct, or
union, as in "type foo" or "enum bar". A
single word denotes a global function or
variable. *)letwhitespace=Str.regexp"[ \t]+"inletwords=Str.splitwhitespacespecifierinmatchwordswith|["type";name]->keepers.typedefs,name|["enum";name]->keepers.enums,name|["struct";name]->keepers.structs,name|["union";name]->keepers.unions,name|[name]->keepers.defines,name|_->raiseBad_pragmainH.addcollectionname()|_->raiseBad_pragmawithBad_pragma->badPragmalocationdirectiveinList.iterprocessArgargsend|GVarDecl(v,_)->begin(* Look for alias attributes, e.g. Linux modules *)matchfilterAttributes"alias"v.vattrwith[]->()(* ordinary prototype. *)|[Attr("alias",[AStrothername])]->H.addkeepers.definesothername()|_->E.s(error"Bad alias attribute at %a"d_loc!currentLoc)end(*** Begin CCured-specific checks: ***)(* these pragmas indirectly require that we keep the function named in
-- the first arguments of boxmodelof and ccuredwrapperof, and
-- the third argument of ccureddeepcopy*. *)|GPragma(Attr("ccuredwrapper"asdirective,attribute::_),location)->beginmatchattributewith|AStrname->H.addkeepers.definesname()|_->badPragmalocationdirectiveend|GPragma(Attr("ccuredvararg",funcname::(ASizeOft)::_),location)->beginmatchtwith|TComp(c,_)whenc.cstruct->(* struct *)H.addkeepers.structsc.cname()|TComp(c,_)->(* union *)H.addkeepers.unionsc.cname()|TNamed(ti,_)->H.addkeepers.typedefsti.tname()|TEnum(ei,_)->H.addkeepers.enumsei.ename()|_->()end|GPragma(Attr(directive,_::_::attribute::_),location)whenString.lengthdirective>ccureddeepcopystring_length&&(Str.first_charsdirectiveccureddeepcopystring_length)=ccureddeepcopystring->beginmatchattributewith|AStrname->H.addkeepers.definesname()|_->badPragmalocationdirectiveend(*** end CCured-specific stuff ***)|_->()initerGlobalsfileconsiderPragma;keepers(***********************************************************************
Function body elimination from pragmas
*)(* When performing global slicing, any functions not explicitly marked
as pragma roots are reduced to mere declarations. This leaves one
with a reduced source file that still compiles to object code, but
which contains the bodies of only explicitly retained functions.
*)letamputateFunctionBodieskeptGlobalsfile=letconsiderGlobal=function|GFun({svar={vname=name;_}asinfo;_},location)whennot(H.memkeptGlobalsname)->trace(dprintf"slicing: reducing to prototype: function %s\n"name);GVarDecl(info,location)|other->otherinmapGlobalsfileconsiderGlobal(***********************************************************************
Root collection from pragmas
*)letisPragmaRootkeepers=function|GType({tname=name;_},_)->H.memkeepers.typedefsname|GEnumTag({ename=name;_},_)|GEnumTagDecl({ename=name;_},_)->H.memkeepers.enumsname|GCompTag({cname=name;cstruct=structure;_},_)|GCompTagDecl({cname=name;cstruct=structure;_},_)->letcollection=ifstructurethenkeepers.structselsekeepers.unionsinH.memcollectionname|GVar({vname=name;vattr=attrs;_},_,_)|GVarDecl({vname=name;vattr=attrs;_},_)|GFun({svar={vname=name;vattr=attrs;_};_},_)->H.memkeepers.definesname||hasAttribute"used"attrs|_->false(***********************************************************************
Common root collecting utilities
*)lethasExportingAttributefunvar=letisExportingAttribute=function|Attr("constructor",[])->true|Attr("destructor",[])->true|_->falseinList.existsisExportingAttributefunvar.vattr(***********************************************************************
Root collection from external linkage
*)(* Exported roots are those global symbols which are visible to the
linker and dynamic loader. For variables, this consists of
anything that is not "static". For functions, this consists of:
- functions bearing a "constructor" or "destructor" attribute
- functions declared extern but not inline
- functions declared neither inline nor static
gcc incorrectly (according to C99) makes inline functions visible to
the linker.
*)letisExportedRootglobal=letresult,reason=matchglobalwith|GVar({vstorage=Static;_},_,_)->false,"static variable"|GVar_->true,"non-static variable"|GFun({svar=v;_},_)->beginifhasExportingAttributevthentrue,"constructor or destructor function"elseifv.vstorage=Staticthenfalse,"static function"elseifv.vinline&&v.vstorage!=Extern&&(!rmUnusedInlines)thenfalse,"inline function"elsetrue,"other function"end|GVarDecl(v,_)whenhasAttribute"alias"v.vattr->true,"has GCC alias attribute"|_->false,"neither function nor variable"intrace(dprintf"isExportedRoot %a -> %b, %s@!"d_shortglobalglobalresultreason);result(***********************************************************************
Root collection for complete programs
*)(* Exported roots are "main()" and functions bearing a "constructor"
or "destructor" attribute. These are the only things which must be
retained in a complete program.
*)letisCompleteProgramRootglobal=letresult=matchglobalwith|GFun({svar={vname="main";vstorage=vstorage;_};_},_)->vstorage<>Static|GFun(fundec,_)whenhasExportingAttributefundec.svar->true|_->falseintrace(dprintf"complete program root -> %b for %a@!"resultd_shortglobalglobal);result(***********************************************************************
Transitive reachability closure from roots
*)(* This visitor recursively marks all reachable types and variables as used. *)classmarkReachableVisitor((globalMap:(string,Cil.global)H.t),(currentFunc:fundecoptionref))=object(self)inheritnopCilVisitormethod!vglob=function|GType(typeinfo,_)->typeinfo.treferenced<-true;DoChildren|GCompTag(compinfo,_)|GCompTagDecl(compinfo,_)->compinfo.creferenced<-true;DoChildren|GEnumTag(enuminfo,_)|GEnumTagDecl(enuminfo,_)->enuminfo.ereferenced<-true;DoChildren|GVar(varinfo,_,_)|GVarDecl(varinfo,_)|GFun({svar=varinfo;_},_)->varinfo.vreferenced<-true;DoChildren|_->SkipChildrenmethod!vinst=function|_->DoChildrenmethod!vvrblv=ifnotv.vreferencedthenbeginletname=v.vnameinifv.vglobthentrace(dprintf"marking transitive use: global %s\n"name)elsetrace(dprintf"marking transitive use: local %s\n"name);(* If this is a global, we need to keep everything used in its
definition and declarations. *)ifv.vglobthenbegintrace(dprintf"descending: global %s\n"name);letdescendglobal=ignore(visitCilGlobal(self:>cilVisitor)global)inletglobals=Hashtbl.find_allglobalMapnameinList.iterdescendglobalsendelsev.vreferenced<-true;end;SkipChildrenmethod!vexpr(e:exp)=matchewithConst(CEnum(_,_,ei))->ei.ereferenced<-true;DoChildren|_->DoChildrenmethod!vtypetyp=letold:bool=letvisitAttrsattrs=ignore(visitCilAttributes(self:>cilVisitor)attrs)inletvisitTypetyp=ignore(visitCilType(self:>cilVisitor)typ)inmatchtypwith|TEnum(e,attrs)->letold=e.ereferencedinifnotoldthenbegintrace(dprintf"marking transitive use: enum %s\n"e.ename);e.ereferenced<-true;visitAttrsattrs;visitAttrse.eattrend;old|TComp(c,attrs)->letold=c.creferencedinifnotoldthenbegintrace(dprintf"marking transitive use: compound %s\n"c.cname);c.creferenced<-true;(* to recurse, we must ask explicitly *)letrecursef=visitTypef.ftypeinList.iterrecursec.cfields;visitAttrsattrs;visitAttrsc.cattrend;old|TNamed(ti,attrs)->letold=ti.treferencedinifnotoldthenbegintrace(dprintf"marking transitive use: typedef %s\n"ti.tname);ti.treferenced<-true;(* recurse deeper into the type referred-to by the typedef *)(* to recurse, we must ask explicitly *)visitTypeti.ttype;visitAttrsattrsend;old|_->(* for anything else, just look inside it *)falseinifoldthenSkipChildrenelseDoChildrenendletmarkReachablefileisRoot=(* build a mapping from global names back to their definitions &
declarations *)letglobalMap=Hashtbl.create137inletconsiderGlobalglobal=matchglobalwith|GFun({svar=info;_},_)|GVar(info,_,_)|GVarDecl(info,_)->Hashtbl.addglobalMapinfo.vnameglobal|_->()initerGlobalsfileconsiderGlobal;letcurrentFunc=refNonein(* mark everything reachable from the global roots *)letvisitor=newmarkReachableVisitor(globalMap,currentFunc)inletvisitIfRootglobal=ifisRootglobalthenbegintrace(dprintf"traversing root global: %a\n"d_shortglobalglobal);(matchglobalwithGFun(fd,_)->currentFunc:=Somefd|_->currentFunc:=None);ignore(visitCilGlobalvisitorglobal)endelsetrace(dprintf"skipping non-root global: %a\n"d_shortglobalglobal)initerGlobalsfilevisitIfRoot(**********************************************************************
Marking and removing of unused labels
**********************************************************************)(* We keep only one label, preferably one that was not introduced by CIL.
Scan a list of labels and return the data for the label that should be
kept, and the remaining filtered list of labels. After this cleanup,
every statement's labels will be either a single 'Default' or any
number of 'Case's, in either case possibly preceded by a single 'Label'. *)letlabelsToKeep(ll:labellist):(string*location*bool)*labellist=letrecloop(sofar:string*location*bool)=function[]->sofar,[]|l::rest->letnewlabel,keepl=matchlwith|CaseRange_|Case_|Default_->sofar,true|Label(ln,lloc,isorig)->beginmatchisorig,sofarwith|false,("",_,_)->(* keep this one only if we have no label so far *)(ln,lloc,isorig),false|false,_->sofar,false|true,(_,_,false)->(* this is an original label; prefer it to temporary or
missing labels *)(ln,lloc,isorig),false|true,_->sofar,falseendinletnewlabel',rest'=loopnewlabelrestinnewlabel',(ifkeeplthenl::rest'elserest')inletsofar,labels=loop("",locUnknown,false)llintry(* If there is a 'default' label, remove all 'case' labels, as they are unnecessary *)letdefault=List.find(functionDefault_->true|_->false)labelsinsofar,[default]withNot_found->sofar,labels(* Remove some trivial gotos, typically inserted at the end of for loops,
because they are not printed by CIL which might yield an unused label
warning. See test/small1/warnings-unused-label.c for a regression test. *)classremoveUnusedGoto=object(self)inheritnopCilVisitormethodprivatepStmtNext(next:stmt)(s:stmt)=matchs.skindwith(* Else-if: don't call visitCilStmt, recurse manually instead *)|If(_,t,{bstmts=[{skind=If_;_}aselsif];battrs=[]},_,_)->ignore(visitCilBlock(self:>cilVisitor)t);self#pStmtNextnextelsif|If(_,_,({bstmts=[{skind=Goto(gref,_);labels=[];_}];battrs=[]}asb),_,_)when!gref==next->b.bstmts<-[];ignore(visitCilStmt(self:>cilVisitor)s)|If(_,({bstmts=[{skind=Goto(gref,_);labels=[];_}];battrs=[]}asb),_,_,_)when!gref==next->b.bstmts<-[];ignore(visitCilStmt(self:>cilVisitor)s)|_->ignore(visitCilStmt(self:>cilVisitor)s)method!vblockblk=letrecdofirst=function[]->()|[x]->self#pStmtNextinvalidStmtx|x::rest->dorestxrestanddorestprev=function[]->self#pStmtNextinvalidStmtprev|x::rest->self#pStmtNextxprev;dorestxrestindofirstblk.bstmts;SkipChildren(* No need to go into expressions or instructions *)method!vexpr_=SkipChildrenmethod!vinst_=SkipChildrenmethod!vtype_=SkipChildrenendclassmarkUsedLabels(labelMap:(string,unit)H.t)=objectinheritnopCilVisitormethod!vstmt(s:stmt)=matchs.skindwithGoto(dest,_)->let(ln,_,_),_=labelsToKeep!dest.labelsinifln=""thenE.s(E.bug"rmtmps: destination of statement does not have labels");(* Mark it as used *)H.replacelabelMapln();DoChildren|_->DoChildrenmethod!vexpre=matchewith|AddrOfLabeldest->let(ln,_,_),_=labelsToKeep!dest.labelsinifln=""thenE.s(E.bug"rmtmps: destination of address of label does not have labels");(* Mark it as used *)H.replacelabelMapln();SkipChildren|_->DoChildrenendclassremoveUnusedLabels(labelMap:(string,unit)H.t)=objectinheritnopCilVisitormethod!vstmt(s:stmt)=let(ln,lloc,lorig),lrest=labelsToKeeps.labelsin(* Check our desired invariants for labels: 'lrest' must be either a
single 'Default' or only 'Case's. It is okay for 'lrest' to be
empty, because a 'Label' can exist on its own, independent of
switch statement labels, and the 'for_all' accepts this case. *)assert(matchlrestwith[Default_]->true|_->List.for_all(functionCase_|CaseRange_->true|_->false)lrest);s.labels<-(ifln<>""&&H.memlabelMaplnthen(* We had labels *)(Label(ln,lloc,lorig)::lrest)elselrest);DoChildren(* No need to go into expressions or instructions *)method!vexpr_=SkipChildrenmethod!vinst_=SkipChildrenmethod!vtype_=SkipChildrenend(***********************************************************************
Removal of unused symbols
*)(* regular expression matching names of uninteresting locals *)letuninteresting=letnames=[(* Cil.makeTempVar *)"__cil_tmp";(* sm: I don't know where it comes from but these show up all over. *)(* this doesn't seem to do what I wanted.. *)"iter";(* various macros in glibc's <bits/string2.h> *)"__result";"__s";"__s1";"__s2";"__s1_len";"__s2_len";"__retval";"__len";(* various macros in glibc's <ctype.h> *)"__c";"__res";(* We remove the __malloc variables *)]in(* optional alpha renaming *)letalpha="\\(___[0-9]+\\)?"inletpattern="\\("^(String.concat"\\|"names)^"\\)"^alpha^"$"inStr.regexppatternletremoveUnmarkedfile=letremovedLocals=ref[]inletfilterGlobalglobal=matchglobalwith(* unused global types, variables, and functions are simply removed *)|GType({treferenced=false;_},_)|GCompTag({creferenced=false;_},_)|GCompTagDecl({creferenced=false;_},_)|GEnumTag({ereferenced=false;_},_)|GEnumTagDecl({ereferenced=false;_},_)|GVar({vreferenced=false;_},_,_)|GVarDecl({vreferenced=false;_},_)|GFun({svar={vreferenced=false;_};_},_)->trace(dprintf"removing global: %a\n"d_shortglobalglobal);false(* retained functions may wish to discard some unused locals *)|GFun(func,_)->letfilterLocallocal=ifnotlocal.vreferencedthenbegin(* along the way, record the interesting locals that were removed *)letname=local.vnameintrace(dprintf"removing local: %s\n"name);ifnot(Str.string_matchuninterestingname0)thenremovedLocals:=(func.svar.vname^"::"^name)::!removedLocals;end;local.vreferencedinfunc.slocals<-List.filterfilterLocalfunc.slocals;(* We also want to remove unused labels. We do it all here, including
marking the used labels *)letusedLabels:(string,unit)H.t=H.create13inignore(visitCilFunction(newremoveUnusedGoto)func);(* scan the function, not only the body, since there might be
AddrOfLabel in initializers *)ignore(visitCilFunction(newmarkUsedLabelsusedLabels)func);(* And now we scan again and we remove them *)ignore(visitCilBlock(newremoveUnusedLabelsusedLabels)func.sbody);true(* all other globals are retained *)|_->trace(dprintf"keeping global: %a\n"d_shortglobalglobal);trueinfile.globals<-List.filterfilterGlobalfile.globals;!removedLocals(***********************************************************************
Exported interface
*)typerootsFilter=global->boolletisDefaultRoot=isExportedRootletremoveUnusedTemps?(isRoot:rootsFilter=isDefaultRoot)file=if!keepUnused||Trace.traceActive"disableTmpRemoval"thenTrace.trace"disableTmpRemoval"(dprintf"temp removal disabled\n")elsebeginif!E.verboseFlagthenignore(E.log"Removing unused temporaries\n");ifTrace.traceActive"printCilTree"thendumpFiledefaultCilPrinterstdout"stdout"file;(* digest any pragmas that would create additional roots *)letkeepers=categorizePragmasfilein(* if slicing, remove the bodies of non-kept functions *)if!Cilutil.sliceGlobalthenamputateFunctionBodieskeepers.definesfile;(* build up the root set *)letisRootglobal=isPragmaRootkeepersglobal||isRootglobalin(* mark everything reachable from the global roots *)clearReferencedBitsfile;markReachablefileisRoot;(* take out the trash *)letremovedLocals=removeUnmarkedfilein(* print which original source variables were removed *)iffalse&&removedLocals!=[]thenletcount=List.lengthremovedLocalsinifcount>2000thenignore(E.warn"%d unused local variables removed"count)elseignore(E.warn"%d unused local variables removed:@!%a"count(docList~sep:(chr','++break)text)removedLocals)end