Inferring object invariant method and system

• US 7,590,978 B2
• Filed: 04/15/2005
• Issued: 09/15/2009
• 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
• Primary Examiner(s): Kang; Insun
• Application Number:
  US11/107,276
• Publication Number:
  US 20060236305A1
• Time in Patent Office: 1,614 Days
• Field of Search: 717/9, 717/107, 717/130, 717/141, 717/155, 717/154, 715/215
• US Class Current: 717/155
• 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 in a computer, 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 of an object within the program at at least one program point wherein the state of the object is either mutable or valid;

at least partially running a global analysis of the program, wherein the global analysis stores invariants in a global analysis invariant storage which the at least one object field has held by the local analysis when the object is valid; and

combining the local analysis and the global analysis to infer at least one invariant that is not explicitly declared for the object within the program, wherein the combining comprises;

the local analysis reaching a program point marked by a pack statement where the object transitions from mutable to valid, the at least one local value of the at least one object field associated with the valid object being passed to the global analysis, and wherein if the at least one local value is not included within the current list of invariants in the global analysis invariant storage, the global analysis adds the at least one local value to the current list of invariants in the global analysis invariant storage for the object, and wherein the local analysis keeps track of the local values of the object encountered until the object transitions from mutable to valid;

and the local analysis reaching a program point marked by an unpack statement where the object transitions from valid to mutable, wherein the local values of the mutable object are recorded by the local analysis but the global analysis does not reflect the local values of the mutable object and the local values of the mutable object are not added to the current list of invariants in the global analysis invariant storage, and the global analysis passing information about the stored invariants for the object to the local analysis.

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

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

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

5. The computer implemented method of claim 1 wherein a widen operator is used to add the at least one local value to the current list of invariants of the object.

6. The computer implemented method of claim 1 wherein the at least one invariant comprises all possible values discovered so far that the object has held when the object is in a valid state.

7. The computer implemented method of claim 1, wherein the local analysis is run to end of the program, and wherein the invariant at end of the program run comprises the object invariants for the object.

8. The computer implemented method of claim 1, wherein at at least one unpack statement the global analysis passes a given invariant associated with a given object to the local analysis.

9. The computer implemented method of claim 8, wherein the given invariant for the given object does not hold after an unpack statement.

10. The computer implemented method of claim 9, further comprising backtracking to the program point wherein the given object was moving from a valid to a mutable state.

11. The computer implemented method of claim 1, wherein the global analysis of the program over approximates the values held by the object.

12. The computer implemented method of claim 1, further comprising a class wherein the object is a child of the class, and wherein to move the object from a valid to a mutable state comprises moving the class from a valid to a mutable state.

13. The computer implemented method of claim 1, wherein an aggregate is an object composed from representation objects and wherein the aggregate is made mutable prior to any of the representation objects being made mutable.

14. The computer implemented method of claim 1 wherein the local analysis provides at least one value to the at least one invariant at the pack statement.

15. A computer system having a processor for determining invariants within an object oriented program, comprising:

a compiler to at least partially run a local analysis of the program wherein the local analysis notes at least one local value of at least one object field of an object within the program at at least one program point wherein the state of the object is either mutable or valid;

the compiler to at least partially run a global analysis of the program, wherein the global analysis stores invariants in a global analysis invariant storage which the at least one object field has held by the local analysis when the object is valid; and

the compiler to combine the local analysis and the global analysis to infer at least one invariant that is not explicitly declared for the object within the program,

wherein the combining comprises;

the local analysis reaching a program point marked by a pack statement where the object transitions from mutable to valid, the at least one local value of the at least one object field associated with the valid object being given to the global analysis, and wherein if the at least one local value is not included within the current list of invariants in the global analysis invariant storage, the global analysis adds the at least one local value to the current list of invariants in the global analysis invariant storage for the object, and wherein the local analysis keeps track of the local values of the object encountered until the object transitions from mutable to valid;

and the local analysis reaching a program point marked by an unpack statement where the object transitions from valid to mutable, wherein the local values of the mutable object are recorded by the local analysis but the global analysis does not reflect the local values of the mutable object and the local values of the mutable object are not added to the current list of invariants in the global analysis invariant storage, and the global analysis passing information about the stored invariants for the object to the local analysis.