Method and apparatus for finding errors in software programs using satisfiability of constraints
First Claim
1. A computer-implemented method for analyzing a software program, said method comprising the steps of:
- receiving input constraints for a path in said software program to be feasible;
applying one or more rewrite rules to a flow graph of said software program defining how said flow graph can change;
adding at least one new node or new edge to said flow graph based on said rewrite rules;
deriving new constraints by arithmetic constraint solving from said input constraints, said flow graph and one or more existing constraints; and
adding said one or more new constraints to said existing constraints.
1 Assignment
0 Petitions
Accused Products
Abstract
A method and apparatus are provided for analyzing software programs. The invention combines data flow analysis and symbolic execution with a new constraint solver to create a more efficient and accurate static software analysis tool. The disclosed constraint solver combines rewrite rules with arithmetic constraint solving to provide a constraint solver that is efficient, flexible and capable of satisfactorily expressing semantics and handling arithmetic constraints. The disclosed constraint solver comprises a number of data structures to remember existing range, equivalence and inequality constraints and incrementally add new constraints. The constraint solver returns an inconsistent indication only if the range constraints, equivalence constraints, and inequality constraints are mutually inconsistent.
-
Citations
21 Claims
-
1. A computer-implemented method for analyzing a software program, said method comprising the steps of:
-
receiving input constraints for a path in said software program to be feasible; applying one or more rewrite rules to a flow graph of said software program defining how said flow graph can change; adding at least one new node or new edge to said flow graph based on said rewrite rules; deriving new constraints by arithmetic constraint solving from said input constraints, said flow graph and one or more existing constraints; and adding said one or more new constraints to said existing constraints. - View Dependent Claims (2, 3, 4, 5, 6)
-
-
7. A computer-implemented method of performing static software analysis comprising:
-
parsing source code and creating a parse tree; performing semantic analysis on said parse tree to create a flow graph; performing data flow analysis on said flow graph to identify potential errors; and performing symbolic execution of paths corresponding to said potential errors to identify confirmed errors, wherein at least one of said semantic analysis, data flow analysis and symbolic execution interact with a constraint solver. - View Dependent Claims (8, 9, 10)
-
-
11. A computer-implemented method for solving constraints when analyzing a software program, comprising:
-
receiving at least one inequality constraint for a path in said software program to be feasible, wherein said inequality constraint is represented by a first and second integer number i0 and i1, a first and second node Na and Nb and a range of numbers R; and storing said at least one inequality constraint in an inequality data structure having at least one inequality record, each inequality record defining an inequality constraint, the inequality constraint being that the product of the first integer number and said first node added to the product of the second integer number and said second node is within an inequality range. - View Dependent Claims (12)
-
-
13. A computer-implemented constraint solver for analyzing a software program, said constraint solver comprising:
-
a range-constraint data structure having at least one node record corresponding to a range constraint, each node record having a node identifier identifying a node that is an operation in a flow graph of the software program and zero or more intervals associated with the respective node, the intervals including all of the possible values that the node can have during the execution of the software program; an equivalence data structure having at least one record that identifies zero or more sets of equivalent nodes that have an equivalence constraint, the equivalence constraint indicating that each of said nodes in one of the sets of equivalent nodes have the same value during a time in an execution of the software program; an inequality data structure having at least one inequality record, each defining an inequality constraint, the inequality constraint being that the product of a first value and a first node added to the product of a second value and a second node is within an inequality range; and a processor that returns an inconsistent indication only if the at least one range constraint, at least one equivalence constraint, and at least one inequality constraint are inconsistent. - View Dependent Claims (14, 15, 16)
-
-
17. A computer-implemented constraint solver for analyzing a software program, said constraint solver comprising:
-
a range-constraint data structure having at least one node record corresponding to a range constraint, each node record having a node identifier identifying a node that is an operation in a flow graph of the software program and zero or more intervals associated with the respective node, the intervals including all of the possible values that the node can have during the execution of the software program; an equivalence data structure having at least one record that identifies zero or more sets of equivalent nodes that have an equivalence constraint, the equivalence constraint indicating that each of said nodes in one of the sets of equivalent nodes have the same value during a time in an execution of the software program; an inequality data structure having at least one inequality record, each defining an inequality constraint, the inequality constraint being that the product of a first value and a first node added to the product of a second value and a second node is within an inequality range; a rule base having one or more rules that define how the flow graph can change; and a constraint solver that returns an “
inconsistent”
indication only if the range constraints, the equivalence constraints, and the inequality constraints are inconsistent.
-
-
18. An apparatus for analyzing a software program, comprising:
-
a memory; and at least one processor, coupled to the memory, operative to; receive input constraints for a path in said software program to be feasible; apply one or more rewrite rules to a flow graph of said software program defining how said flow graph can change; add at least one new node or new edge to said flow graph based on said rewrite rules; derive new constraints by arithmetic constraint solving from said input constraints, said flow graph and one or more existing constraints; and add said one or more new constraints to said existing constraints.
-
-
19. An apparatus for performing static software analysis, comprising:
-
a memory; and at least one processor, coupled to the memory, operative to; parse source code to create a parse tree; perform semantic analysis on said parse tree to create a flow graph; perform data flow analysis on said flow graph to identify potential errors; and perform symbolic execution of paths corresponding to said potential errors to identify confirmed errors, wherein at least one of said semantic analysis, data flow analysis and symbolic execution interact with a constraint solver.
-
-
20. An article of manufacture for analyzing a software program, comprising a machine readable medium containing one or more programs which when executed implement the steps of:
-
a memory; and at least one processor, coupled to the memory, operative to; receiving input constraints for a path in said software program to be feasible; applying one or more rewrite rules to a flow graph of said software program defining how said flow graph can change; adding at least one new node or new edge to said flow graph based on said rewrite rules; deriving new constraints by arithmetic constraint solving from said input constraints, said flow graph and one or more existing constraints; and adding said one or more new constraints to said existing constraints.
-
-
21. An article of manufacture for performing static software analysis, comprising:
-
a memory; and at least one processor, coupled to the memory, operative to; parsing source code to create a parse tree; performing semantic analysis on said parse tree to create a flow graph; performing data flow analysis on said flow graph to identify potential errors; and performing symbolic execution of paths corresponding to said potential errors to identify confirmed errors, wherein at least one of said semantic analysis, data flow analysis and symbolic execution interact with a constraint solver.
-
Specification