Method and apparatus for verifying invariant properties of data structures at run-time

• US 20040015897A1
• Filed: 05/15/2001
• Published: 01/22/2004
• Est. Priority Date: 05/15/2001
• Status: Active Grant

• Current Assignee: Hewlett-Packard Development Company, L.P. (HP Inc.)
• Original Assignee: Hewlett-Packard Development Company, L.P. (HP Inc.)
• Inventors: Thompson, Carlos L., Littfin, Jeff
• Granted Patent: US 7,013,460 B2
• Time in Patent Office: Days
• US Class Current: 717/140
• CPC Class Codes: G06F 11/0751 Error or fault detection not based on redundancy power supply failures G06F1/30; network fault management H04L41/06
• CPC Class Codes: G06F 11/3612 by runtime analysis performance monitoring G06F11/3466
• CPC Class Codes: G06F 9/44589 Program code verification, e.g. Java bytecode verification, proof-carrying code high-level semantic checks G06F8/43; testing and debugging software G06F11/36

Abstract

Method and apparatus for verifying at runtime an invariant property of a data structure. In various example embodiments, code that verifies whether a runtime value of the data structure is consistent with the invariant property is automatically generated in response to an annotation of the data structure in the source code. In executing the program, the runtime value of the data structure is compared to the invariant property in the automatically generated code. If the runtime property is inconsistent with the invariant property, the program branches to exception handler code.

Claims

1. A computer-implemented method for verifying at runtime an invariant property of a data structure of a computer program, comprising:

automatically generating a first code segment that verifies a runtime value of the data structure is consistent with the invariant property in response to an annotation of the data structure that defines the invariant property of the data structure;

comparing the runtime value of the data structure with the invariant property during execution of the program via execution of the first code segment; and

performing a programmed action if the runtime value is inconsistent with the invariant property.

2. The method of claim 1, wherein the invariant property is a range of data addresses and further comprising verifying that the runtime value of the data structure is within a range of data addresses specified in source code of the computer program.

3. The method of claim 1, wherein the invariant property is a range of data addresses and further comprising:

automatically generating during compilation a valid data address range including an upper bound and a lower bound for the range of data addresses, wherein the source code of the computer program does not include a specification of the upper bound and lower bound; and

verifying that the runtime value of the data structure is within the valid data address range.

4. The method of claim 1, wherein the invariant property is a range of instruction addresses and further comprising verifying that the runtime value of the data structure is within the range of instruction addresses specified in source code of the computer program.

5. The method of claim 1, wherein the invariant property is a range of instruction addresses and further comprising:

automatically generating during compilation a valid instruction address range including an upper bound and a lower bound for the range of addresses, wherein the source code of the computer program does not include a specification of the upper bound and lower bound; and

verifying that the runtime value of the data structure is within the valid instruction address range.

6. The method of claim 1, wherein the invariant property is a range of data values and further comprising the step of verifying that the runtime value of the data structure is within the range of data values.

7. The method of claim 1, further comprising communicating the invariant property from a compiler to a code generator.

8. The method of claim 7, further comprising storing the invariant property in a symbol table.

9. The method of claim 8, wherein the invariant property is a range of data addresses and further comprising verifying that the runtime value of the data structure is within a range of data addresses specified in source code of the computer program.

10. The method of claim 8, wherein the invariant property is a range of data addresses and further comprising:

automatically generating during compilation a valid data address range including an upper bound and a lower bound for the range of data addresses, wherein the source code of the computer program does not include a specification of the upper bound and lower bound; and

verifying that the runtime value of the data structure is within the valid data address range.

11. The method of claim 8, wherein the invariant property is a range of instruction addresses and further comprising verifying that the runtime value of the data structure is within the range of instruction addresses specified in source code of the computer program.

12. The method of claim 8, wherein the invariant property is a range of instruction addresses and further comprising:

automatically generating during compilation a valid instruction address range including an upper bound and a lower bound for the range of addresses, wherein the source code of the computer program does not include a specification of the upper bound and lower bound; and

verifying that the runtime value of the data structure is within the valid instruction address range.

13. The method of claim 8, wherein the invariant property is a range of data values and further comprising the step of verifying that the runtime value of the data structure is within the range of data values.

14. The method of claim 8, further comprising storing in the symbol table one or more code addresses associated with one or more updates to the data structure.

15. An apparatus for verifying at runtime an invariant property of a data structure of a computer program, comprising:

means for automatically generating a first code segment that verifies a runtime value of the data structure is consistent with the invariant property in response to an annotation of the data structure that defines the invariant property of the data structure;

means for comparing the runtime value of the data structure with the invariant property during execution of the program via execution of the first code segment; and

means for performing a programmed action if the runtime value is inconsistent with the invariant property.