Inferring object invariant method and system

• US 20060236305A1
• Filed: 04/15/2005
• Published: 10/19/2006
• Est. Priority Date: 04/15/2005
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Corporation
• Inventors: Leino, K. Rustan, Chang, Bor-Yuh Evan
• Granted Patent: US 7,590,978 B2
• Time in Patent Office: Days
• US Class Current: 717/106
• CPC Class Codes: G06F 8/433 Dependency analysis; Data or control flow analysis

Abstract

A local analysis analyzes the values of objects paying attention to program flow and a global analysis analyses the object independent of the flow. The local and global analysis interact to infer the invariants of objects used within a computer program. The local analysis is given the known invariants of an object by the global analysis when the object transitions from a valid to a mutable state. It then keeps track of all of the values of objects encountered until the object transitions from mutable to a valid state, when the information known to the local analysis is passed to the global analysis, which may use the new object values to add to the current list of invariants for the given object.

Claims

1. A computer implemented method for determining invariants within an object oriented program, comprising:

at least partially running a local analysis of the program wherein the local analysis notes at least one local value of at least one object field at at least one program point;

at least partially running a global analysis of the program, wherein an object is either mutable or valid;

wherein the global analysis stores at least one value which the object field has held when the object is valid; and

combining the local analysis and the global analysis to infer at least one invariant for at least one object,

wherein the combining comprises

the local analysis reaching a program point wherein the object transitions from mutable to valid, the local value of the at least one object field being given to the global analysis, this value within the global analysis comprising the global analysis information about the object.

2. The computer implemented method of claim 1 wherein the program point where the object transitions from mutable to valid is associated with a pack statement.

3. The computer implemented method of claim 1 wherein the local analysis analyzes the program at a subset of program points.

4. The computer implemented method of claim 1 wherein the object invariant for the object comprises at least one value held by an object field with an aliased name.

5. The computer implemented method of claim 1 wherein at least one value held by the object field when the object is mutable is not given to the global analysis.

6. The computer implemented method of claim 1 wherein the combining further comprises:

the local analysis reaching a program point where the object transitions from valid to mutable, at least a portion of the global analysis information about the object being given to the local analysis.

7. The computer implemented method of claim 6 wherein the program point where the object transitions from valid to mutable is an unpack statement.

8. The computer implemented method of claim 1 wherein a widen operator is used to add values to the invariant of an object.

9. The computer implemented method of claim 1 wherein a value held by the object field when the object is mutable are not reflected in an object invariant associated with the object.

10. At least one computer-readable medium having stored thereon a representation of invariant states of a sequential computer program, the invariant state representation comprising:

a representation of a flow-sensitive value state wherein the representation comprises a representation of the values of at least one object encountered between two program points; and

a representation of a flow-insensitive value state wherein the representation comprises a representation of substantially all of the values for substantially all of the objects encountered up to a given program point;

wherein the flow-sensitive analysis state and the flow-insensitive analysis state exchange information at least one exchange program point.

11. The at least one computer-readable medium of claim 10, further comprising a valid state where the object invariant holds, and wherein a flow insensitive analysis invariant state comprises all possible values discovered so far that the object has held when the object is in a valid state.

12. The at least one computer-readable medium of claim 10, wherein the flow-insensitive analysis state at the end of the analysis comprise the object invariants for the computer program.

13. The at least one computer-readable medium of claim 10, wherein the exchange program point comprises a pack or an unpack statement.

14. A computer system for inferring invariant states of objects, the computer system comprising

a compiler operable for generating the invariant states from a source code representation of the computer program, wherein the source code representation comprises one or more objects, each object comprising one or more fields with values;

a flow sensitive analysis module for generating at least a partial flow sensitive invariant storage which stores essentially all possible values of at least some object fields between two program points;

a flow insensitive analysis module for generating at least a partial flow insensitive invariant storage which stores essentially all possible values that at least some object fields have held from a first program point to an intermediate program point;

a mutable location module for during the generation locating a location wherein for an object O the object O is moving from a valid to a mutable state; and

a flow insensitive instantiation module which instantiates the partial flow insensitive analysis invariant state for object O within the at least partial flow sensitive analysis invariant state.

15. The computer system of claim 14 further comprising

a flow sensitive instantiation module which instantiates the partial flow sensitive analysis invariant state for object O within the at least partial flow insensitive analysis invariant state.

16. The computer system of claim 14 further comprising a backtrack module which backtracks to the location wherein the object O was moving from a valid to a mutable state.

17. The computer system of claim 14 wherein the object O moving from a valid to a mutable state is represented by an unpack statement.

18. The computer system of claim 17 wherein the pack statement is represented in an intermediate representation of the computer program.

19. The computer system of claim 17 wherein the flow-insensitive analysis module overapproximates the values held by at least one object.

20. The computer system of claim 14 further comprising a class wherein the object is a child of the class, and wherein to move the object O from a valid to a mutable state comprises initially moving the class from a valid to a mutable state.