Code verification by tree reconstruction

• US 6,594,783 B1
• Filed: 08/27/1999
• Issued: 07/15/2003
• Est. Priority Date: 08/27/1999
• Status: Expired due to Fees

• Current Assignee: Hewlett-Packard Development Company, L.P. (HP Inc.)
• Original Assignee: Hewlett-Packard Development Company, L.P. (HP Inc.)
• Inventors: Dollin, Christopher J, Dickey, Laura J., Oberhauser, Roy T., Knight Leach, Steven Frederick
• Primary Examiner(s): Iqbal, Nadeem
• Application Number:
  US09/384,812
• Time in Patent Office: 1,418 Days
• Field of Search: 714/38, 714/39, 714/47, 714/26, 714/25, 717/8-10, 717/7, 717/5
• US Class Current: 714/38.14
• CPC Class Codes: G06F 11/3608 using formal methods, e.g. model checking, abstract interpretation theorem proving G06N5/013
• CPC Class Codes: G06F 8/427 Parsing
• 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

A system and method are provided that allow for improved code sequence verification through the use of an abstract syntax tree. This is accomplished by first constructing an abstract syntax tree from the code sequence and then determining whether the abstract syntax tree satisfies a predefined set of conditions indicative of the code sequence being executable on the computer without generating a predefined class of execution errors. The abstract syntax tree is constructed by reassembling the code sequence into a plurality of instructions, combining the instructions into a plurality of blocks, examining the blocks to determine entry points of a plurality of loops, and tagging locations in the series of instructions where control is transferred at the end of each loop. The instructions, blocks, loops and tagged locations are then examined to generate a plurality of control structures (the coarse structure). Finally, the instructions, blocks, loops, tagged locations and control structures are examined to generate a plurality of form expressions (the fine structures).

Claims

1. A method for verifying a code sequence to be executed on a computer, the method comprising:

constructing an abstract syntax tree from the code sequence; and

determining whether the abstract syntax tree satisfies a predefined set of conditions, wherein the predefined set of conditions is indicative of the code sequence being executable on the computer without generating a predefined class of execution errors.

2. The method of claim 1, wherein constructing the abstract syntax tree further comprises:

reassembling the code sequence into a plurality of instructions;

combining the instructions into a plurality of blocks;

examining the blocks to determine entry points of a plurality of loops; and

tagging locations in the series of instructions where control is transferred at the end of each loop.

3. The method of claim 2, wherein constructing the abstract syntax tree further comprises:

examining the instructions, the blocks, the loops and the tagged locations to generate a plurality of control structures; and

examining the instructions, the blocks, the loops, the tagged locations and the control structures to generate a plurality of form expressions.

4. The method of claim 1, further comprising analyzing the abstract syntax tree to optimize the code sequence.

5. The method of claim 1, further comprising using the abstract syntax tree to generate recompiled source code from the code sequence.

6. The method of claim 1, further comprising adding tracing or debugging code segments to the code sequence at run time based on code abstract syntax tree.

7. The method of claim 1, further comprising adding resource monitoring code segments to the code sequence at run time based on the abstract syntax tree.

8. The method of claim 1, further comprising displaying a structure of the abstract syntax tree in graphical form.

9. The method of claim 1, further comprising generating a flow diagram from the abstract syntax tree representing a control flow of the code sequence.

10. The method of claim 1, further comprising analyzing the abstract syntax tree to ensure compliance of the code sequence with a set of predefined coding specifications.

11. A computer system connected to the Internet and executing a computer program for verifying computer code sequences downloaded from the Internet, the computer program comprising computer instructions for:

constructing an abstract syntax tree from the code sequence; and

determining whether the abstract syntax tree satisfies a predefined set of conditions, wherein the predefined set of conditions is indicative of the code sequence being executable on the computer without generating a predefined class of execution errors.

12. The computer system of claim 11, wherein the computer instructions for constructing the abstract syntax tree further comprise computer instructions for:

reassembling the code sequence into a plurality of instructions;

combining the instructions into a plurality of blocks;

examining the blocks to determine entry points of a plurality of loops; and

tagging locations in the series of instructions where control is transferred at the end of each loop.

13. The computer system of claim 12, wherein the computer instructions for constructing the abstract syntax tree further comprise computer instructions for:

examining the instructions, the blocks, the loops and the tagged locations to generate a plurality of control structures; and

examining the instructions, the blocks, the loops, the tagged locations and the control structures to generate a plurality of form expressions.

14. The computer system of claim 11, wherein the computer program further comprises computer instructions for analyzing the abstract syntax tree to optimize the code sequence.

15. The computer system of claim 11, wherein the computer program further comprises computer instructions for using the abstract syntax tree to generate recompiled source code from the code sequence.

16. The computer system of claim 11, wherein the computer program further comprises computer instructions for adding tracing or debugging code segments to the code sequence at run time based on the abstract syntax tree.

17. The computer system of claim 11, wherein the computer program further comprises computer instructions for adding resource monitoring code segments to the code sequence at run time based on the abstract syntax tree.

18. The computer system of claim 11, wherein the computer program further comprises computer instructions for displaying a structure of the abstract syntax tree in graphical form.

19. The computer system of claim 11, wherein the computer program further comprises computer instructions for generating a flow diagram from the abstract syntax tree representing a control flow of the code sequence.

20. The computer system of claim 11, wherein the computer program further comprises computer instructions for analyzing the abstract syntax tree to ensure compliance of the code sequence with a set of predefined coding specifications.

21. A computer-readable storage medium comprising a computer program for verifying computer code sequences downloaded from the Internet, wherein the computer program comprises computer instructions for:

constructing an abstract syntax tree from the code sequence; and

determining whether the abstract syntax tree satisfies a predefined set of conditions, wherein the predefined set of conditions is indicative of the code sequence being executable on the computer without generating a predefined class of execution errors.

22. The computer-readable storage medium of claim 21, wherein the computer instructions for constructing the abstract syntax tree further comprise computer instructions for:

reassembling the code sequence into a plurality of instructions;

combining the instructions into a plurality of blocks;

examining the blocks to determine entry points of a plurality of loops; and

tagging locations in the series of instructions where control is transferred at the end of each loop.

23. The computer-readable storage medium of claim 22, wherein the computer instructions for constructing the abstract syntax tree further comprise computer instructions for:

examining the instructions, the blocks, the loops and the tagged locations to generate a plurality of control structures; and

examining the instructions, the blocks, the loops, the tagged locations and the control structures to generate a plurality of form expressions.