Code verification system and method

• US 7,036,111 B2
• Filed: 06/01/2001
• Issued: 04/25/2006
• Est. Priority Date: 06/01/2001
• Status: Expired due to Term

• Current Assignee: HTC Corporation
• Original Assignee: Hewlett-Packard Development Company, L.P. (HP Inc.)
• Inventors: Gopalakrishnan, Vaideswar, Dollin, Christopher J
• Primary Examiner(s): Zhen, Wei Y.
• Assistant Examiner(s): RAMPURIA, SATISH
• Application Number:
  US09/871,778
• Publication Number:
  US 20020194579A1
• Time in Patent Office: 1,789 Days
• Field of Search: 717124-129, 717/148, 717/114, 717/143, 717/173, 714/332, 714/38, 714/15, 711/6, 713/2, 713/200, 365/185.04
• 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,

wherein said code verifier is further configured to analyze said program and to group said 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 of said plurality of 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.

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 one of the single composed type signatures, 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, 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.

4. The system of claim 1, 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.

5. A code verification method, comprising to 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;

detecting a type error based an said analyzing step;

grouping said 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 of said plurality of type signatures; and

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

6. The method of claim 5, further comprising the steps of:

composing one of said type signatures with another of said type signatures thereby forming a single composed type signature of said composed type signatures; 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.

7. 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;

detecting a type error based on said analyzing step 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 signature; and

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

8. The method of claim 7, 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.

9. A code verifier comprising:

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

means for analyzing said type signatures; and

means for detecting a type error based on said analyzing step;

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

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

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

10. The code verifier of claim 9, further comprising:

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

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