静态代码分析.ppt

* * * * * * * * * * * * * * * * * * Example Forwards vs. backwards A forwards analysis is one that for each program point computes information about the past behavior. Examples of this are available expressions and reaching definitions. Calculation: predecessors of CFG nodes. A backwards analysis is one that for each program point computes information about the future behavior. Examples of this are liveness and very busy expressions. Calculation: successors of CFG nodes. May vs. Must A may analysis is one that describes information that may possibly be true and, thus, computes an upper approximation. Examples of this are liveness and reaching definitions. Calculation: union operator. A must analysis is one that describes information that must definitely be true and, thus, computes a lower approximation. Examples of this are available expressions and very busy expressions. Calculation: intersection operator. 静态代码分析 – 概念 Basic Blocks Control Flow Graph Dataflow Analysis Live Variable Analysis Reaching Definition Analysis Lattice Theory Basic Idea Information about program represented using values from algebraic structure called lattice Analysis produces lattice value for each program point Two flavors of analysis Forward dataflow analysis Backward dataflow analysis Partial Orders Set P Partial order ? such that ?x,y,z?P x ? x (reflexive) x ? y and y ? x implies x ? y (asymmetric) x ? y and y ? z implies x ? z (transitive) Can use partial order to define Upper and lower bounds Least upper bound Greatest lower bound Upper Bounds If S ? P then x?P is an upper bound of S if ?y?S. y ? x x?P is the least upper bound of S if x is an upper bound of S, and x ? y for all upper bounds y of S ? - join, least upper bound (lub), supremum, sup ? S is the least upper bound of S x ? y is the least upper bound of {x,y} Lower Bounds If S ? P then x?P is a lower bound of S if ?y?S. x ? y x?P is the greatest lower bound of S if x is a lower bound of S, and y ? x for all lowe