Method and apparatus for finding errors in software programs using satisfiability of constraints

• US 7,089,542 B2
• Filed: 12/13/2002
• Issued: 08/08/2006
• Est. Priority Date: 12/13/2002
• Status: Expired due to Fees

• Current Assignee: International Business Machines Corporation
• Original Assignee: International Business Machines Corporation
• Inventors: Brand, Daniel, Krohm, Florian, Darringer, John A.
• Primary Examiner(s): Khatri, Anil
• Application Number:
  US10/318,823
• Publication Number:
  US 20040117772A1
• Time in Patent Office: 1,334 Days
• Field of Search: 717141-145, 717154-157, 706 45- 46
• US Class Current: 717/143
• CPC Class Codes: G06F 11/3608 using formal methods, e.g. model checking, abstract interpretation theorem proving G06N5/013

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.

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.

2. The method of claim 1, wherein said input constraints include a range constraint.

3. The method of claim 1, wherein said step of adding said one or more new constraints incrementally adds said one or more new constraints to said one or more existing contraints.

4. The method of claim 1, wherein said method interacts with a semantic analyzer to eliminate paths through said software program that will not be traversed during execution of said software program.

5. The method of claim 1, wherein said method interacts with a data flow analyzer to eliminate paths through said flow graph that will not be traversed during execution of said software program.

6. The method of claim 1, wherein said method interacts with a symbolic executor to eliminate paths through said flow graph that will not be traversed during execution of said software program.

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.

8. The method of claim 7, wherein said constraint solver receives input constraints for a path in said software program to be feasible;

applies rewrite rules to a flow graph of said software program;

adds at least one new node or new edge to said flow graph based on said rewrite rules;

derives new constraints by arithmetic constraint solving from said input constraints, said flow graph and one or more existing constraints; and

adds said one or more new constraints to said existing constraints.

9. The method of claim 8, wherein said input constraints include one or more range constraints.

10. The method of claim 8, wherein said constraint solver is further configured to incrementally add said one or more new constraints to said one or more existing contraints.

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 i₀ and i₁, a first and second node N_a and N_b 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.

12. The method of claim 11, wherein execution of said software program is constrained to parameters where said first and second nodes have integer values which satisfy the equation:

i₀×

N_a+i₁×

N_bε

R.

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.

14. The constraint solver of claim 13, wherein said processor incrementally adds said one or more new constraints to said at least one range constraint, at least one equivalence constraint, and at least one inequality constraint.

15. The constraint solver of claim 13, wherein at least one of the data structures is persistent.

16. The constraint solver of claim 13, wherein the range constraint is provided from one or more of an invocation from a semantic analyzer, a data flow analysis or a symbolic executor.

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.