| 摘要 |
In general, in one aspect, the invention relates to a method for static analysis. The method includes: obtaining source code; constructing a control flow graph (CFG) corresponding to the source code, by identifying control structures within the source code, creating a set of graph nodes of the CFG, and creating a set of directed graph edges of the CFG connecting the set of graph nodes; assigning a first Boolean flow value to a selected node of the set of graph nodes; backward traversing the CFG from the selected node to a target node; computing, by a computer processor and while backward traversing the CFG, disjoint predicate expressions representing flow values at the set of directed graph edges; computing, based on the disjoint predicate expressions, a resulting disjoint predicate expression; and identifying, based on the resulting disjoint predicate expression, a potential program property in the source code. |
| 主权项 |
1. A method for static analysis to identify a potential program property, comprising:
obtaining a plurality of source code; constructing a control flow graph (CFG) corresponding to the plurality of source code, by:
identifying a plurality of control structures within the plurality of source code;identifying, based on the plurality of control structures, a plurality of basic blocks of reachable code within the plurality of source code;creating a plurality of graph nodes of the CFG representing the plurality of basic blocks, wherein the plurality of graph nodes comprises a first graph node and a second graph node; andcreating, based on the plurality of control structures, a plurality of directed graph edges of the CFG connecting the plurality of graph nodes,wherein the plurality of directed graph edges comprises a first directed graph edge outgoing from the second graph node and a second directed graph edge outgoing from the second graph node, andwherein the plurality of directed graph edges further comprises a third directed graph edge outgoing from the first graph node to the second graph node; extracting, from at least one of the plurality of control structures, a first edge predicate for the first directed graph edge and a second edge predicate for the second directed graph edge, wherein the first edge predicate evaluates to TRUE if the first directed graph edge is taken, and wherein the second edge predicate evaluates to TRUE if the second directed graph edge is taken; assigning a first Boolean flow value corresponding to the potential program property to a selected node of the plurality of graph nodes; backward traversing the CFG from the selected node to a target node of the CFG; computing, by a computer processor and while backward traversing the CFG, a plurality of disjoint predicate expressions representing flow values corresponding to the potential program property at the plurality of directed graph edges, wherein the plurality of disjoint predicate expressions comprises a first disjoint predicate expression for the first directed graph edge, a second disjoint predicate expression for the second directed graph edge, and a third disjoint predicate expression for the third directed graph edge, wherein the third disjoint predicate expression is computed by:
computing a first conjunction of the first disjoint predicate expression and the first edge predicate;computing a second conjunction of the second disjoint predicate expression and the second edge predicate; andcomputing a disjunction of the first conjunction and the second conjunction,wherein the third disjoint predicate expression is the disjunction of the first conjunction and the second conjunction; computing, by the computer processor and based on the plurality of disjoint predicate expressions, a resulting disjoint predicate expression representing a resulting flow value at the target node; and identifying, based on the resulting disjoint predicate expression, the potential program property in the source code, wherein identification of the potential program property indicates that source code corresponding to the traversed portion of the CFG can be subjected to at least one selected from a group consisting of redundant code reduction and an optimization technique. |
