Code verification system and method

• US 20020194579A1
• Filed: 06/01/2001
• Published: 12/19/2002
• Est. Priority Date: 06/01/2001
• Status: Active Grant

• Current Assignee: HTC Corporation
• Original Assignee: Hewlett-Packard Development Company, L.P. (HP Inc.)
• Inventors: Dollin, Christopher J., Gopalakrishnan, Vaideswar
• Granted Patent: US 7,036,111 B2
• Time in Patent Office: Days
• US Class Current: 717/126
• 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 code verification system is utilized to type check compiled code. The code verification system includes memory and a code verifier. The memory is utilized to store a compiled program. The code verifier analyzes instructions of the program and generates a plurality of type signatures based on the instructions The type signatures indicate the input type constraints and the output type descriptions of the instructions, and the code verifier analyzes the type signatures to detect a type error.

Claims

1. A code verification system, comprising:

memory for storing a compiled program; and

a code verifier configured to analyze instructions of said program and to generate a plurality of type signatures based on said instructions, each of said type signatures indicating each input type constraint and each output type description for a respective one of said instructions, wherein said code verifier is configured to detect a type error by analyzing said type signatures.

2. The system of claim 1, wherein said code verifier is configured to compose one of said type signatures with another of said type signatures to form a single composed signature, said code verifier further configured to make a determination as to whether an input type constraint of said one type signature is acceptable to an output type description of said other type signature, said code verifier further configured to detect said type error based on said determination.

3. The system of claim 1, wherein said code verifier is further configured to analyze said program and to group instructions of said program into a plurality of code blocks, wherein said code verifier is configured to translate said code blocks into type signature blocks, each of said type signature blocks having one or more type signatures, said code verifier further configured to compose the type signatures of each of said type signature blocks into a single respective composed type signature.

4. The system of claim 3, wherein said code verifier, in composing one of said type signature blocks, is configured to compose a first type signature with a second type signature to form a single composed signature, said first and second type signatures included within said one type signature block, said code verifier further configured to make a determination as to whether an input type constraint of said first type signature is acceptable to an output type description of said second type signature, said code verifier further configured to detect said type error based on said determination.

5. A code verification system, comprising:

memory for storing a compiled program; and

a code verifier configured to analyze a code block of said program and to translate instructions within said code block into a plurality of type signatures, said code verifier further configured to compose said type signatures into a single composed type signature and to detect a type error by analyzing said type signatures.

6. The system of claim 5, wherein one of said type signatures includes a type description indicative of a type of an input consumed by one of said instructions when said one instruction is executed, wherein another of said type signatures includes a type description indicative of a type of an output produced by another of said instruction when said other instruction is executed, and wherein said code verifier is further configured to detect said type error by comparing said type descriptions.

7. The system of claim 5, wherein said code verifier is further configured to analyze said program and to group instructions of said program into a plurality of code blocks, wherein said code verifier is configured to translate said code blocks into type signature blocks, each of said type signature blocks having one or more type signatures, said code verifier further configured to compose the type signatures of each of said type signature blocks into a single respective composed type signature.

8. A code verification method, comprising the steps of:

storing a compiled program;

generating a plurality of type signatures based on instructions within said program, each of said type signatures indicating each input type constraint and each output type description for a respective one of said instructions;

analyzing said type signatures; and

detecting a type error based on said analyzing step.

9. The method of claim 8, further comprising the steps of:

composing one of said type signatures with another of said type signatures thereby forming a single composed signature; and

determining whether an input type constraint of said one type signature is acceptable to an output type description of said other type signature,

wherein said detecting step is further based on said determining step.

10. The method of claim 8, further comprising the steps of:

grouping instructions of said program into a plurality of code blocks;

translating said code blocks into type signature blocks, each of said type signature blocks having one or more type signatures; and

composing the type signatures of each said type signature blocks into a single respective composed type signature.

11. A code verification method, comprising the steps of:

storing a compiled program, said compiled program having at least one code block that includes a plurality of instructions;

translating said instructions into a plurality of type signatures;

composing said type signatures into a single composed type signature;

analyzing said type signatures; and

detecting a type error based on said analyzing step.

12. The method of claim 11, wherein one of said type signatures includes a type description indicative of a type of an input consumed by one of said instructions when said one instruction is executed, wherein another of said type signatures includes a type description indicative of a type of an output produced by another of said instructions when said other instruction is executed, and wherein said analyzing step includes the step of comparing said type descriptions.

13. The method of claim 11, further comprising the steps of:

grouping instructions of said program into a plurality of code blocks;

translating said code blocks into type signature blocks, each of said type signature blocks having one or more type signatures; and

composing the type signatures of each of said signature blocks into a single respective composed type signature.