淺論成本控制與財(cái)務(wù)管理目標(biāo)課件

靜態(tài)代碼分析梁廣泰2011-05-25靜態(tài)代碼分析梁廣泰提綱動機(jī)程序靜態(tài)分析（概念+實(shí)例）程序缺陷分析（科研工作）提綱動機(jī)動機(jī)云平臺特點(diǎn)應(yīng)用程序直接部署在云端服務(wù)器上，存在安全隱患直接操作破壞服務(wù)器文件系統(tǒng)存在安全漏洞時，可提供黑客入口資源共享，動態(tài)分配單個應(yīng)用的性能低下，會侵占其他應(yīng)用的資源解決方案之一：在部署應(yīng)用程序之前，對其進(jìn)行靜態(tài)代碼分析：是否存在違禁調(diào)用？（非法文件訪問）是否存在低效代碼？（未借助StringBuilder對String進(jìn)行大量拼接）是否存在安全漏洞？（SQL注入，跨站攻擊，拒絕服務(wù)）是否存在惡意病毒？……動機(jī)云平臺特點(diǎn)提綱動機(jī)程序靜態(tài)分析（概念+實(shí)例）程序缺陷分析（科研工作）提綱動機(jī)靜態(tài)代碼分析定義：程序靜態(tài)分析是在不執(zhí)行程序的情況下對其進(jìn)行分析的技術(shù)，簡稱為靜態(tài)分析。對比：程序動態(tài)分析：需要實(shí)際執(zhí)行程序程序理解：靜態(tài)分析這一術(shù)語一般用來形容自動化工具的分析，而人工分析則往往叫做程序理解用途：程序翻譯/編譯（編譯器），程序優(yōu)化重構(gòu)，軟件缺陷檢測等過程：大多數(shù)情況下，靜態(tài)分析的輸入都是源程序代碼或者中間碼（如Javabytecode），只有極少數(shù)情況會使用目標(biāo)代碼；以特定形式輸出分析結(jié)果靜態(tài)代碼分析定義：靜態(tài)代碼分析BasicBlocksControlFlowGraphDataflowAnalysisLiveVariableAnalysisReachingDefinitionAnalysisLatticeTheory靜態(tài)代碼分析BasicBlocksBasicBlocksAbasicblockisamaximalsequenceofconsecutivethree-addressinstructionswiththefollowingproperties:Theflowofcontrolcanonlyenterthebasicblockthruthe1stinstr.Controlwillleavetheblockwithouthaltingorbranching,exceptpossiblyatthelastinstr.Basicblocksbecomethenodesofaflowgraph,withedgesindicatingtheorder.BasicBlocksAbasicblockisaEABCDFBasicBlockExampleLeadersi=1j=1t1=10*it2=t1+jt3=8*t2t4=t3-88a[t4]=0.0j=j+1ifj<=10goto(3)i=i+1ifi<=10goto(2)i=1t5=i-1t6=88*t5a[t6]=1.0i=i+1ifi<=10goto(13)BasicBlocksEABCDFBasicBlockExampleLeadeControl-FlowGraphsControl-flowgraph:Node:aninstructionorsequenceofinstructions(abasicblock)Twoinstructionsi,jinsamebasicblock

iffexecutionofiguaranteesexecutionofjDirectededge:potential

flowofcontrolDistinguishedstartnodeEntry&ExitFirst&lastinstructioninprogramControl-FlowGraphsControl-floControl-FlowEdgesBasicblocks=nodesEdges:AdddirectededgebetweenB1andB2if:BranchfromlaststatementofB1tofirststatementofB2(B2isaleader),orB2immediatelyfollowsB1inprogramorderandB1doesnotendwithunconditionalbranch(goto)DefinitionofpredecessorandsuccessorB1isapredecessorofB2B2isasuccessorofB1Control-FlowEdgesBasicblocksCFGExampleCFGExample靜態(tài)代碼分析BasicBlocksControlFlowGraphDataflowAnalysisLiveVariableAnalysisReachingDefinitionAnalysisLatticeTheory靜態(tài)代碼分析BasicBlocksDataflowAnalysisCompile-TimeReasoningAboutRun-TimeValuesofVariablesorExpressionsAtDifferentProgramPointsWhichassignmentstatementsproducedvalueofvariableatthispoint?Whichvariablescontainvaluesthatarenolongerusedafterthisprogrampoint?Whatistherangeofpossiblevaluesofvariableatthisprogrampoint?……DataflowAnalysisCompile-TimeProgramPointsOneprogrampointbeforeeachnodeOneprogrampointaftereachnodeJoinpoint–pointwithmultiplepredecessorsSplitpoint–pointwithmultiplesuccessorsProgramPointsOneprogrampoinLiveVariableAnalysisAvariablevisliveatpointpifvisusedalongsomepathstartingatp,andnodefinitionofvalongthepathbeforetheuse.Whenisavariablevdeadatpointp?Nouseofvonanypathfromptoexitnode,orIfallpathsfrompredefinevbeforeusingv.LiveVariableAnalysisAvariabWhatUseisLivenessInformation?Registerallocation.Ifavariableisdead,canreassignitsregisterDeadcodeelimination.Eliminateassignmentstovariablesnotreadlater.Butmustnoteliminatelastassignmenttovariable(suchasinstancevariable)visibleoutsideCFG.Caneliminateotherdeadassignments.HandlebymakingallexternallyvisiblevariablesliveonexitfromCFGWhatUseisLivenessInformatiConceptualIdeaofAnalysisstartfromexitandgobackwardsinCFGComputelivenessinformationfromendtobeginningofbasicblocksConceptualIdeaofAnalysisstaLivenessExamplea=x+y;t=a;c=a+x;x==0b=t+z;

c=y+1;11001001110000Assumea,b,cvisibleoutsidemethodSoareliveonexitAssumex,y,z,tnotvisibleRepresentLivenessUsingBitVectororderisabcxyzt1100111100011111001000101110abcxyztabcxyztabcxyztLivenessExamplea=x+y;1100FormalizingAnalysisEachbasicblockhasIN-setofvariablesliveatstartofblockOUT-setofvariablesliveatendofblockUSE-setofvariableswithupwardsexposedusesinblock(usepriortodefinition)DEF-setofvariablesdefinedinblockpriortouseUSE[x=z;x=x+1;]={z}(xnotinUSE)DEF[x=z;x=x+1;y=1;]={x,y}CompilerscanseachbasicblocktoderiveUSEandDEFsetsFormalizingAnalysisEachbasicAlgorithmforallnodesninN-{Exit} IN[n]=emptyset;OUT[Exit]=emptyset;IN[Exit]=use[Exit];Changed=N-{Exit};while(Changed!=emptyset) chooseanodeninChanged; Changed=Changed-{n};

OUT[n]=emptyset; forallnodessinsuccessors(n) OUT[n]=OUT[n]UIN[p]; IN[n]=use[n]U(out[n]-def[n]); if(IN[n]changed) forallnodespinpredecessors(n) Changed=ChangedU{p};AlgorithmforallnodesninN靜態(tài)代碼分析–概念BasicBlocksControlFlowGraphDataflowAnalysisLiveVariableAnalysisReachingDefinitionAnalysisLatticeTheory靜態(tài)代碼分析–概念BasicBlocksReachingDefinitionsConceptofdefinitionandusea=x+yisadefinitionofaisauseofxandyAdefinitionreachesauseifvaluewrittenbydefinition

maybereadbyuseReachingDefinitionsConceptofReachingDefinitionss=0;a=4;i=0;k==0b=1;b=2;i<ns=s+a*b;i=i+1;returnsReachingDefinitionss=0;bReachingDefinitionsandConstantPropagationIsauseofavariableaconstant?CheckallreachingdefinitionsIfallassignvariabletosameconstantThenuseisinfactaconstantCanreplacevariablewithconstantReachingDefinitionsandConstIsaConstantins=s+a*b?s=0;a=4;i=0;k==0b=1;b=2;i<ns=s+a*b;i=i+1;returnsYes!Onallreachingdefinitionsa=4

IsaConstantins=s+a*b?sConstantPropagationTransforms=0;a=4;i=0;k==0b=1;b=2;i<ns=s+4*b;i=i+1;returnsYes!Onallreachingdefinitionsa=4

ConstantPropagationTransformComputingReachingDefinitionsComputewithsetsofdefinitionsrepresentsetsusingbitvectorseachdefinitionhasapositioninbitvectorAteachbasicblock,computedefinitionsthatreachstartofblockdefinitionsthatreachendofblockDocomputationbysimulatingexecutionofprogramuntilreachfixedpointComputingReachingDefinitions

1:s=0;2:a=4;3:i=0;k==04:b=1;5:b=2;0000000111000011100001111100111110011111001111111111111111111111234567123456712345671234567123456712345671110000111100011101001111100010111111111001111111i<n1111111returns6:s=s+a*b;7:i=i+1;

1:s=0;4:b=1;5:b=2;0FormalizingReachingDefinitionsEachbasicblockhasIN-setofdefinitionsthatreachbeginningofblockOUT-setofdefinitionsthatreachendofblockGEN-setofdefinitionsgeneratedinblockKILL-setofdefinitionskilledinblockGEN[s=s+a*b;i=i+1;]=0000011KILL[s=s+a*b;i=i+1;]=1010000CompilerscanseachbasicblocktoderiveGENandKILLsetsFormalizingReachingDefinitioExampleExampleForwardsvs.backwardsAforwardsanalysisisonethatforeachprogrampointcomputesinformationaboutthepastbehavior.Examplesofthisareavailableexpressionsandreachingdefinitions.Calculation:predecessorsofCFGnodes.Abackwardsanalysisisonethatforeachprogrampointcomputesinformationaboutthefuturebehavior.Examplesofthisarelivenessandverybusyexpressions.Calculation:successorsofCFGnodes.Forwardsvs.backwardsAforwarMayvs.MustAmayanalysisisonethatdescribesinformationthatmaypossiblybetrueand,thus,computesanupperapproximation.Examplesofthisarelivenessandreachingdefinitions.Calculation:unionoperator.Amustanalysisisonethatdescribesinformationthatmustdefinitelybetrueand,thus,computesalowerapproximation.Examplesofthisareavailableexpressionsandverybusyexpressions.Calculation:intersectionoperator.Mayvs.MustAmayanalysisis靜態(tài)代碼分析–概念BasicBlocksControlFlowGraphDataflowAnalysisLiveVariableAnalysisReachingDefinitionAnalysisLatticeTheory靜態(tài)代碼分析–概念BasicBlocksBasicIdeaInformationaboutprogramrepresentedusingvaluesfromalgebraicstructurecalledlatticeAnalysisproduceslatticevalueforeachprogrampointTwoflavorsofanalysisForwarddataflowanalysisBackwarddataflowanalysisBasicIdeaInformationaboutprPartialOrdersSetPPartialordersuchthatx,y,zPxx (reflexive)xyandyximpliesxy (asymmetric)xyandyzimpliesxz (transitive)CanusepartialordertodefineUpperandlowerboundsLeastupperboundGreatestlowerboundPartialOrdersSetPUpperBoundsIfSPthenxPisanupperboundofSifyS.yxxPistheleastupperboundofSifxisanupperboundofS,andxyforallupperboundsyofS-join,leastupperbound(lub),supremum,supSistheleastupperboundofSxyistheleastupperboundof{x,y}UpperBoundsIfSPthenLower

BoundsIfSPthenxPisalowerboundofSifyS.xyxPisthegreatestlowerboundofSifxisalowerboundofS,andyxforalllowerboundsyofS-meet,greatestlowerbound(glb),infimum,infSisthegreatestlowerboundofSxyisthegreatestlowerboundof{x,y}LowerBoundsIfSPthenCoveringxyifxyandxyxiscoveredbyy(ycoversx)ifxy,andxzyimpliesxzConceptually,ycoversxiftherearenoelementsbetweenxandyCoveringxyifxyandxyExampleP={000,001,010,011,100,101,110,111}(standardBooleanlattice,alsocalledhypercube)xyif(xbitwiseandy)=x111011101110010001000100HasseDiagramIfycoversxLinefromytoxyabovexindiagramExampleP={000,001,010,01LatticesIfxyandxyexistforallx,yP, thenPisalattice.IfSandSexistforallSP, thenPisacompletelattice.AllfinitelatticesarecompleteLatticesIfxyandxyexiLatticesIfxyandxyexistforallx,yP, thenPisalattice.IfSandSexistforallSP, thenPisacompletelattice.AllfinitelatticesarecompleteExampleofalatticethatisnotcompleteIntegersIForanyx,yI,xy=max(x,y),xy=min(x,y)ButIandIdonotexistI{,}isacompletelatticeLatticesIfxyandxyexiLatticeExamplesLatticesNon-latticesLatticeExamplesLatticesSemi-LatticeOnlyoneofthetwobinaryoperations(meetorjoin)existMeet-semilatticeIfxyexistforallx,yPJoin-semilatticeIfxyexistforallx,yPSemi-LatticeOnlyoneofthetwMonotonicFunction&FixedpointLetLbealattice.Afunctionf:L→Lismonotonicif?x,y∈S:x

y?f(x)

f(y)LetAbeaset,f:A→Aafunction,a∈A. Iff(a)=a,thenaiscalledafixedpointoffonAMonotonicFunction&FixedpoiExistenceofFixedPointsTheheightofalatticeisdefinedtobethelengthofthelongestpathfrom⊥to?InacompletelatticeLwithfiniteheight,everymonotonicfunctionf:L→Lhasaunique

leastfixed-point:

ExistenceofFixedPointsThehKnaster-Tarski

FixedPointTheoremSuppose(L,)isacompletelattice,f:LLisamonotonicfunction.ThenthefixedpointmoffcanbedefinedasKnaster-Tarski

FixedPointThCalculatingFixedPointThetimecomplexityofcomputingafixed-pointdependsonthreefactors:Theheightofthelattice,sincethisprovidesaboundfori;Thecostofcomputingf;Thecostoftestingequality.Thecomputationofafixed-pointcanbeillustratedasawalkupthelatticestartingat⊥:CalculatingFixedPointThetimApplicationtoDataflowAnalysisDataflowinformationwillbelatticevaluesTransferfunctionsoperateonlatticevaluesSolutionalgorithmwillgenerateincreasingsequenceofvaluesateachprogrampointAscendingchainconditionwillensureterminationWillusetocombinevaluesatcontrol-flowjoinpointsApplicationtoDataflowAnalysTransferFunctionsTransferfunctionf:PPforeachnodeincontrolflowgraphfmodelseffectofthenodeontheprograminformationTransferFunctionsTransferfunTransferFunctionsEachdataflowanalysisproblemhasasetFoftransferfunctionsf:PPIdentityfunctioniFFmustbeclosedundercomposition: f,gF.thefunctionh=x.f(g(x))FEachfFmustbemonotone: xyimpliesf(x)f(y)SometimesallfFaredistributive: f(xy)=f(x)f(y)DistributivityimpliesmonotonicityTransferFunctionsEachdataflo課程考核方式作業(yè)（提交到課程平臺/，并演示）+課程報告作業(yè)選題：代碼注釋提取，文檔生成代碼信息統(tǒng)計(jì)：總行數(shù)，代碼行數(shù)，類數(shù)量，方法數(shù)，方法長度等Latex格式文檔自動轉(zhuǎn)成PDF代碼在線diffExecutableJar轉(zhuǎn)換成帶有特定icon的exe程序代碼各類缺陷檢測：內(nèi)存泄漏，空指針異常Testcase自動生成腳本缺陷分析：Javascript，Python，Ruby，PHP……C#代碼缺陷分析在線壓縮，解壓縮，加密，解密……課程考核方式作業(yè)（提交到課程平臺http://sase.seQuestions?

Thankyou!Questions?

Thankyou!靜態(tài)代碼分析梁廣泰2011-05-25靜態(tài)代碼分析梁廣泰提綱動機(jī)程序靜態(tài)分析（概念+實(shí)例）程序缺陷分析（科研工作）提綱動機(jī)動機(jī)云平臺特點(diǎn)應(yīng)用程序直接部署在云端服務(wù)器上，存在安全隱患直接操作破壞服務(wù)器文件系統(tǒng)存在安全漏洞時，可提供黑客入口資源共享，動態(tài)分配單個應(yīng)用的性能低下，會侵占其他應(yīng)用的資源解決方案之一：在部署應(yīng)用程序之前，對其進(jìn)行靜態(tài)代碼分析：是否存在違禁調(diào)用？（非法文件訪問）是否存在低效代碼？（未借助StringBuilder對String進(jìn)行大量拼接）是否存在安全漏洞？（SQL注入，跨站攻擊，拒絕服務(wù)）是否存在惡意病毒？……動機(jī)云平臺特點(diǎn)提綱動機(jī)程序靜態(tài)分析（概念+實(shí)例）程序缺陷分析（科研工作）提綱動機(jī)靜態(tài)代碼分析定義：程序靜態(tài)分析是在不執(zhí)行程序的情況下對其進(jìn)行分析的技術(shù)，簡稱為靜態(tài)分析。對比：程序動態(tài)分析：需要實(shí)際執(zhí)行程序程序理解：靜態(tài)分析這一術(shù)語一般用來形容自動化工具的分析，而人工分析則往往叫做程序理解用途：程序翻譯/編譯（編譯器），程序優(yōu)化重構(gòu)，軟件缺陷檢測等過程：大多數(shù)情況下，靜態(tài)分析的輸入都是源程序代碼或者中間碼（如Javabytecode），只有極少數(shù)情況會使用目標(biāo)代碼；以特定形式輸出分析結(jié)果靜態(tài)代碼分析定義：靜態(tài)代碼分析BasicBlocksControlFlowGraphDataflowAnalysisLiveVariableAnalysisReachingDefinitionAnalysisLatticeTheory靜態(tài)代碼分析BasicBlocksBasicBlocksAbasicblockisamaximalsequenceofconsecutivethree-addressinstructionswiththefollowingproperties:Theflowofcontrolcanonlyenterthebasicblockthruthe1stinstr.Controlwillleavetheblockwithouthaltingorbranching,exceptpossiblyatthelastinstr.Basicblocksbecomethenodesofaflowgraph,withedgesindicatingtheorder.BasicBlocksAbasicblockisaEABCDFBasicBlockExampleLeadersi=1j=1t1=10*it2=t1+jt3=8*t2t4=t3-88a[t4]=0.0j=j+1ifj<=10goto(3)i=i+1ifi<=10goto(2)i=1t5=i-1t6=88*t5a[t6]=1.0i=i+1ifi<=10goto(13)BasicBlocksEABCDFBasicBlockExampleLeadeControl-FlowGraphsControl-flowgraph:Node:aninstructionorsequenceofinstructions(abasicblock)Twoinstructionsi,jinsamebasicblock

iffexecutionofiguaranteesexecutionofjDirectededge:potential

flowofcontrolDistinguishedstartnodeEntry&ExitFirst&lastinstructioninprogramControl-FlowGraphsControl-floControl-FlowEdgesBasicblocks=nodesEdges:AdddirectededgebetweenB1andB2if:BranchfromlaststatementofB1tofirststatementofB2(B2isaleader),orB2immediatelyfollowsB1inprogramorderandB1doesnotendwithunconditionalbranch(goto)DefinitionofpredecessorandsuccessorB1isapredecessorofB2B2isasuccessorofB1Control-FlowEdgesBasicblocksCFGExampleCFGExample靜態(tài)代碼分析BasicBlocksControlFlowGraphDataflowAnalysisLiveVariableAnalysisReachingDefinitionAnalysisLatticeTheory靜態(tài)代碼分析BasicBlocksDataflowAnalysisCompile-TimeReasoningAboutRun-TimeValuesofVariablesorExpressionsAtDifferentProgramPointsWhichassignmentstatementsproducedvalueofvariableatthispoint?Whichvariablescontainvaluesthatarenolongerusedafterthisprogrampoint?Whatistherangeofpossiblevaluesofvariableatthisprogrampoint?……DataflowAnalysisCompile-TimeProgramPointsOneprogrampointbeforeeachnodeOneprogrampointaftereachnodeJoinpoint–pointwithmultiplepredecessorsSplitpoint–pointwithmultiplesuccessorsProgramPointsOneprogrampoinLiveVariableAnalysisAvariablevisliveatpointpifvisusedalongsomepathstartingatp,andnodefinitionofvalongthepathbeforetheuse.Whenisavariablevdeadatpointp?Nouseofvonanypathfromptoexitnode,orIfallpathsfrompredefinevbeforeusingv.LiveVariableAnalysisAvariabWhatUseisLivenessInformation?Registerallocation.Ifavariableisdead,canreassignitsregisterDeadcodeelimination.Eliminateassignmentstovariablesnotreadlater.Butmustnoteliminatelastassignmenttovariable(suchasinstancevariable)visibleoutsideCFG.Caneliminateotherdeadassignments.HandlebymakingallexternallyvisiblevariablesliveonexitfromCFGWhatUseisLivenessInformatiConceptualIdeaofAnalysisstartfromexitandgobackwardsinCFGComputelivenessinformationfromendtobeginningofbasicblocksConceptualIdeaofAnalysisstaLivenessExamplea=x+y;t=a;c=a+x;x==0b=t+z;

c=y+1;11001001110000Assumea,b,cvisibleoutsidemethodSoareliveonexitAssumex,y,z,tnotvisibleRepresentLivenessUsingBitVectororderisabcxyzt1100111100011111001000101110abcxyztabcxyztabcxyztLivenessExamplea=x+y;1100FormalizingAnalysisEachbasicblockhasIN-setofvariablesliveatstartofblockOUT-setofvariablesliveatendofblockUSE-setofvariableswithupwardsexposedusesinblock(usepriortodefinition)DEF-setofvariablesdefinedinblockpriortouseUSE[x=z;x=x+1;]={z}(xnotinUSE)DEF[x=z;x=x+1;y=1;]={x,y}CompilerscanseachbasicblocktoderiveUSEandDEFsetsFormalizingAnalysisEachbasicAlgorithmforallnodesninN-{Exit} IN[n]=emptyset;OUT[Exit]=emptyset;IN[Exit]=use[Exit];Changed=N-{Exit};while(Changed!=emptyset) chooseanodeninChanged; Changed=Changed-{n};

OUT[n]=emptyset; forallnodessinsuccessors(n) OUT[n]=OUT[n]UIN[p]; IN[n]=use[n]U(out[n]-def[n]); if(IN[n]changed) forallnodespinpredecessors(n) Changed=ChangedU{p};AlgorithmforallnodesninN靜態(tài)代碼分析–概念BasicBlocksControlFlowGraphDataflowAnalysisLiveVariableAnalysisReachingDefinitionAnalysisLatticeTheory靜態(tài)代碼分析–概念BasicBlocksReachingDefinitionsConceptofdefinitionandusea=x+yisadefinitionofaisauseofxandyAdefinitionreachesauseifvaluewrittenbydefinition

maybereadbyuseReachingDefinitionsConceptofReachingDefinitionss=0;a=4;i=0;k==0b=1;b=2;i<ns=s+a*b;i=i+1;returnsReachingDefinitionss=0;bReachingDefinitionsandConstantPropagationIsauseofavariableaconstant?CheckallreachingdefinitionsIfallassignvariabletosameconstantThenuseisinfactaconstantCanreplacevariablewithconstantReachingDefinitionsandConstIsaConstantins=s+a*b?s=0;a=4;i=0;k==0b=1;b=2;i<ns=s+a*b;i=i+1;returnsYes!Onallreachingdefinitionsa=4

IsaConstantins=s+a*b?sConstantPropagationTransforms=0;a=4;i=0;k==0b=1;b=2;i<ns=s+4*b;i=i+1;returnsYes!Onallreachingdefinitionsa=4

ConstantPropagationTransformComputingReachingDefinitionsComputewithsetsofdefinitionsrepresentsetsusingbitvectorseachdefinitionhasapositioninbitvectorAteachbasicblock,computedefinitionsthatreachstartofblockdefinitionsthatreachendofblockDocomputationbysimulatingexecutionofprogramuntilreachfixedpointComputingReachingDefinitions

1:s=0;2:a=4;3:i=0;k==04:b=1;5:b=2;0000000111000011100001111100111110011111001111111111111111111111234567123456712345671234567123456712345671110000111100011101001111100010111111111001111111i<n1111111returns6:s=s+a*b;7:i=i+1;

1:s=0;4:b=1;5:b=2;0FormalizingReachingDefinitionsEachbasicblockhasIN-setofdefinitionsthatreachbeginningofblockOUT-setofdefinitionsthatreachendofblockGEN-setofdefinitionsgeneratedinblockKILL-setofdefinitionskilledinblockGEN[s=s+a*b;i=i+1;]=0000011KILL[s=s+a*b;i=i+1;]=1010000CompilerscanseachbasicblocktoderiveGENandKILLsetsFormalizingReachingDefinitioExampleExampleForwardsvs.backwardsAforwardsanalysisisonethatforeachprogrampointcomputesinformationaboutthepastbehavior.Examplesofthisareavailableexpressionsandreachingdefinitions.Calculation:predecessorsofCFGnodes.Abackwardsanalysisisonethatforeachprogrampointcomputesinformationaboutthefuturebehavior.Examplesofthisarelivenessandverybusyexpressions.Calculation:successorsofCFGnodes.Forwardsvs.backwardsAforwarMayvs.MustAmayanalysisisonethatdescribesinformationthatmaypossiblybetrueand,thus,computesanupperapproximation.Examplesofthisarelivenessandreachingdefinitions.Calculation:unionoperator.Amustanalysisisonethatdescribesinformationthatmustdefinitelybetrueand,thus,computesalowerapproximation.Examplesofthisareavailableexpressionsandverybusyexpressions.Calculation:intersectionoperator.Mayvs.MustAmayanalysisis靜態(tài)代碼分析–概念BasicBlocksControlFlowGraphDataflowAnalysisLiveVariableAnalysisReachingDefinitionAnalysisLatticeTheory靜態(tài)代碼分析–概念BasicBlocksBasicIdeaInformationaboutprogramrepresentedusingvaluesfromalgebraicstructurecalledlatticeAnalysisproduceslatticevalueforeachprogrampointTwoflavorsofanalysisForwarddataflowanalysisBackwarddataflowanalysisBasicIdeaInformationaboutprPartialOrdersSetPPartialordersuchthatx,y,zPxx (reflexive)xyandyximpliesxy (asymmetric)xyandyzimpliesxz (transitive)CanusepartialordertodefineUpperandlowerboundsLeastupperboundGreatestlowerboundPartialOrdersSetPUpperBoundsIfSPthenxPisanupperboundofSifyS.yxxPistheleastupperboundofSifxisanupperboundofS,andxyforallupperboundsyofS-join,leastupperbound(lub),supremum,supSistheleastupperboundofSxyistheleastupperboundof{x,y}UpperBoundsIfSPthenLower

BoundsIfSPthenxPisalowerboundofSifyS.xyxPisthegreatestlowerboundofSifxisalowerboundofS,andyxforalllowerboundsyofS-meet,greatestlowerbound(glb),infimum,infSisthegreatestlowerboundofSxyisthegreatestlowerboundof{x,y}LowerBoundsIfSPthenCoveringxyifxyandxyxiscoveredbyy(ycoversx)ifxy,andxzyimpliesxzConceptually,ycoversxiftherearenoelementsbetweenxandyCoveringxyifxyandxyExampleP={000,001,010,011,100,101,110,111}(standardBooleanlattice,alsocalledhypercube)xyif(xbitwiseandy)=x111011101110010001000100HasseDiagramIfycoversxLinefromytoxyabovexindiagramExampleP={000,001,010,01LatticesIfxyandxyexistforallx,yP, thenPisalattice.IfSandSexistforallSP, thenPisacompletelattice.AllfinitelatticesarecompleteLatticesIfxyandxyexiLatticesIfxyandxyexistforallx,yP, thenPisalattice.IfSandSexistforallSP, thenPisacompletelattice.AllfinitelatticesarecompleteExampleofalatticethatisnotcompleteIntegersIForanyx,yI,xy=max(x,y),xy=min(x,y)ButIandIdonotexistI{,}isacompletelatticeLatticesIfxyandxyexiLat