Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Source file availexpslv.ml
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437(* compute available expressions, although in a somewhat
non-traditional way. the abstract state is a mapping from
lvalues to expressions as opposed to a set of
expressions *)openGoblintCilopenPrettyopenExpcompareopenLivenessmoduleE=ErrormsgmoduleDF=DataflowmoduleUD=UsedefmoduleIH=InthashmoduleH=HashtblmoduleU=UtilmoduleS=StatsexceptionUnimplementedofstringletdebug=reffalseletdoTime=reffalselettimesfa=if!doTimethenS.timesfaelsefa(*
When ignore_inst returns true, then
the instruction in question has no
effects on the abstract state.
When ignore_call returns true, then
the instruction only has side-effects
from the assignment if there is one.
*)letignore_inst=ref(funi->false)letignore_call=ref(funi->false)letregisterIgnoreInst(f:instr->bool):unit=letf'=!ignore_instinignore_inst:=(funi->(fi)||(f'i))letregisterIgnoreCall(f:instr->bool):unit=letf'=!ignore_callinignore_call:=(funi->(fi)||(f'i))moduleLvExpHash=H.Make(structtypet=lvalletequallv1lv2=compareLvallv1lv2lethash=H.hashend)(* exp LvExpHash.t -> exp LvExpHash.t -> bool *)letlvh_equalslvh1lvh2=ifnot(LvExpHash.lengthlvh1=LvExpHash.lengthlvh2)thenfalseelseLvExpHash.fold(funlveb->ifnotbthenbelsetrylete2=LvExpHash.findlvh2lvinifnot(compareExpStripCastsee2)thenfalseelsetruewithNot_found->false)lvh1trueletlvh_pretty()lvh=LvExpHash.fold(funlved->d++line++(d_lval()lv)++text" -> "++(d_exp()e))lvhnil(* the result must be the intersection of eh1 and eh2 *)(* exp IH.t -> exp IH.t -> exp IH.t *)letlvh_combinelvh1lvh2=if!debugthenignore(E.log"lvh_combine: combining %a\n and\n %a\n"lvh_prettylvh1lvh_prettylvh2);letlvh'=LvExpHash.copylvh1in(* eh' gets all of eh1 *)LvExpHash.iter(funlve1->trylete2l=LvExpHash.find_alllvh2lvinifnot(List.exists(fune2->compareExpStripCastse1e2)e2l)(* remove things from eh' that eh2 doesn't have *)thenlete1l=LvExpHash.find_alllvh'lvinlete1l'=List.filter(fune->not(compareExpStripCastsee1))e1linLvExpHash.removelvh'lv;List.iter(fune->LvExpHash.addlvh'lve)e1l'withNot_found->LvExpHash.removelvh'lv)lvh1;if!debugthenignore(E.log"with result %a\n"lvh_prettylvh');lvh'(* On a memory write, kill expressions containing memory reads
variables whose address has been taken, and globals. *)classmemReadOrAddrOfFinderClassbr=object(self)inheritnopCilVisitormethod!vexpre=matchewith|AddrOf(Mem_,_)|StartOf(Mem_,_)|Lval(Mem_,_)->beginbr:=true;SkipChildrenend|AddrOf(Varvi,NoOffset)->(* Writing to memory won't change the address of something *)SkipChildren|_->DoChildrenmethod!vvrblvi=ifvi.vaddrof||vi.vglobthen(br:=true;SkipChildren)elseDoChildrenend(* exp -> bool *)letexp_has_mem_reade=letbr=reffalseinletvis=newmemReadOrAddrOfFinderClassbrinignore(visitCilExprvise);!brletlval_has_mem_readlv=letbr=reffalseinletvis=newmemReadOrAddrOfFinderClassbrinignore(visitCilLvalvislv);!brletoffset_has_mem_readoff=letbr=reffalseinletvis=newmemReadOrAddrOfFinderClassbrinignore(visitCilOffsetvisoff);!brletlvh_kill_memlvh=LvExpHash.iter(funlve->matchlvwith|(Mem_,_)->LvExpHash.removelvhlv|_->ifexp_has_mem_reade||lval_has_mem_readlvthenLvExpHash.removelvhlv)lvh(* need to kill exps containing a particular vi sometimes *)classviFinderClassvibr=object(self)inheritnopCilVisitormethod!vvrblvi'=ifvi.vid=vi'.vidthen(br:=true;SkipChildren)elseDoChildrenendletinstr_has_vivii=letbr=reffalseinletvis=newviFinderClassvibrinignore(visitCilInstrvisi);!brletexp_has_vivie=letbr=reffalseinletvis=newviFinderClassvibrinignore(visitCilExprvise);!brletlval_has_vivilv=letbr=reffalseinletvis=newviFinderClassvibrinignore(visitCilLvalvislv);!brletlvh_kill_vilvhvi=LvExpHash.iter(funlve->ifexp_has_vivie||lval_has_vivilvthenLvExpHash.removelvhlv)lvh(* need to kill exps containing a particular lval sometimes *)classlvalFinderClasslvbr=object(self)inheritnopCilVisitormethod!vlvall=ifcompareLvalllvthen(br:=true;SkipChildren)elseDoChildrenendletexp_has_lvallve=letbr=reffalseinletvis=newlvalFinderClasslvbrinignore(visitCilExprvise);!brletlval_has_lvallv(host,hostoff)=letbr=reffalseinletvis=newlvalFinderClasslvbrin(matchhostwith|Meme->ignore(visitCilExprvise)|_->());ignore(visitCilOffsetvishostoff);!brletlvh_kill_lvallvhlv=LvExpHash.iter(funlv'e->ifexp_has_lvallve||lval_has_lvallvlv'thenLvExpHash.removelvhlv')lvhclassvolatileFinderClassbr=object(self)inheritnopCilVisitormethod!vexpre=if(hasAttribute"volatile"(typeAttrs(typeOfe)))then(br:=true;SkipChildren)elseDoChildrenendletexp_is_volatilee:bool=letbr=reffalseinletvis=newvolatileFinderClassbrinignore(visitCilExprvise);!br(* let varHash = IH.create 32 *)classaddrOfOrGlobalFinderClassbr=object(self)inheritnopCilVisitormethod!vvrblvi=ifvi.vaddrof||vi.vglobthen(br:=true;SkipChildren)elseDoChildrenendletexp_has_addrof_or_globale=letbr=reffalseinletvis=newaddrOfOrGlobalFinderClassbrinignore(visitCilExprvise);!brletlval_has_addrof_or_globallv=letbr=reffalseinletvis=newaddrOfOrGlobalFinderClassbrinignore(visitCilLvalvislv);!brletlvh_kill_addrof_or_globallvh=LvExpHash.iter(funlve->iflval_has_addrof_or_globallvthenLvExpHash.removelvhlv)lvhletlvh_handle_instilvh=if(!ignore_inst)ithenlvhelsematchiwithSet(lv,e,_,_)->beginmatchlvwith|(Mem_,_)->beginLvExpHash.replacelvhlve;lvh_kill_memlvh;lvh_kill_addrof_or_globallvh;lvhend|_whennot(exp_is_volatilee)->begin(* ignore x = x *)ifcompareExpStripCasts(Lvallv)ethenlvhelsebeginLvExpHash.replacelvhlve;lvh_kill_lvallvhlv;lvhendend|_->begin(* e is volatile *)(* must remove mapping for lv *)if!debugthenignore(E.log"lvh_handle_inst: %a is volatile. killing %a\n"d_exped_lvallv);LvExpHash.removelvhlv;lvh_kill_lvallvhlv;lvhendend|Call(Somelv,_,_,_,_)->beginLvExpHash.removelvhlv;lvh_kill_lvallvhlv;ifnot((!ignore_call)i)thenbeginlvh_kill_memlvh;lvh_kill_addrof_or_globallvhend;lvhend|Call(_,_,_,_,_)->beginifnot((!ignore_call)i)thenbeginlvh_kill_memlvh;lvh_kill_addrof_or_globallvh;end;lvhend|Asm(_,_,_,_,_,_)->beginlet_,d=UD.computeUseDefInstriinUD.VS.iter(funvi->lvh_kill_vilvhvi)d;lvhend|VarDecl_->raise(Unimplemented"VarDecl")(* VarDecl instruction is not supported for availexpslv, to make availexpslv work for programs without VLA *)(* make sure to set alwaysGenerateVarDecl in cabs2cil.ml to false. To support VLA, implement this. *)moduleAvailableExps=structletname="Available Expressions"letdebug=debug(* mapping from var id to expression *)typet=expLvExpHash.tletcopy=LvExpHash.copyletstmtStartData=IH.create64letpretty=lvh_prettyletcomputeFirstPredecessorstmlvh=lvhletcombinePredecessors(stm:stmt)~(old:t)(lvh:t)=iftime"lvh_equals"(lvh_equalsold)lvhthenNoneelseSome(time"lvh_combine"(lvh_combineold)lvh)letdoInstrilvh=letaction=lvh_handle_instiinDF.Post(action)letdoStmtstmastate=DF.SDefaultletdoGuardcastate=DF.GDefaultletfilterStmtstm=trueendmoduleAE=DF.ForwardsDataFlow(AvailableExps)(*
Computes AEs for function fd.
*)letcomputeAEsfd=tryletslst=fd.sbody.bstmtsinletfirst_stm=List.hdslstin(*time "make_var_hash" make_var_hash fd;*)IH.clearAvailableExps.stmtStartData;IH.addAvailableExps.stmtStartDatafirst_stm.sid(LvExpHash.create4);time"compute"AE.compute[first_stm]withFailure_->if!debugthenignore(E.log"fn w/ no stmts?\n")|Not_found->if!debugthenignore(E.log"no data for first_stm?\n")(* get the AE data for a statement *)letgetAEssid=trySome(IH.findAvailableExps.stmtStartDatasid)withNot_found->None(* get the AE data for an instruction list *)letinstrAEsilsidlvhout=if!debugthenignore(E.log"instrAEs\n");letproc_onehili=matchhilwith[]->letlvh'=LvExpHash.copylvhinletlvh''=lvh_handle_instilvh'inlvh''::hil|lvh'::ehrstasl->letlvh'=LvExpHash.copylvh'inletlvh''=lvh_handle_instilvh'inlvh''::linletfolded=List.fold_leftproc_one[lvh]ilinletfoldednotout=List.rev(List.tlfolded)infoldednotoutclassaeVisitorClass=object(self)inheritnopCilVisitorvalmutablesid=-1valmutableae_dat_lst=[]valmutablecur_ae_dat=Nonemethod!vstmtstm=sid<-stm.sid;matchgetAEssidwithNone->if!debugthenignore(E.log"aeVis: stm %d has no data\n"sid);cur_ae_dat<-None;DoChildren|Someeh->matchstm.skindwithInstril->if!debugthenignore(E.log"aeVist: visit il\n");ae_dat_lst<-time"instrAEs"(instrAEsilstm.sideh)false;DoChildren|_->if!debugthenignore(E.log"aeVisit: visit non-il\n");cur_ae_dat<-None;DoChildrenmethod!vinsti=if!debugthenignore(E.log"aeVist: before %a, ae_dat_lst is %d long\n"d_instri(List.lengthae_dat_lst));tryletdata=List.hdae_dat_lstincur_ae_dat<-Some(data);ae_dat_lst<-List.tlae_dat_lst;if!debugthenignore(E.log"aeVisit: data is %a\n"lvh_prettydata);DoChildrenwithFailure_->if!debugthenignore(E.log"aeVis: il ae_dat_lst mismatch\n");DoChildrenmethodget_cur_eh()=matchcur_ae_datwithNone->getAEssid|Someeh->Someehend