Single pass intermediate language verification algorithm

• US 20040003380A1
• Filed: 06/26/2002
• Published: 01/01/2004
• Est. Priority Date: 06/26/2002
• Status: Abandoned Application

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Corporation
• Inventors: Fedorov, Vladimir
• Application Number:
  US10/180,733
• Publication Number:
  US 20040003380A1
• Time in Patent Office: Days
• US Class Current: 717/148
• 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

An intermediate language (IL) program is verified by processing the IL program in a single pass. Processed IL instructions may be provided to a just-in-time (JIT) compiler so that the IL program can be converted into a native language program of a targeted device. A verification apparatus may comprise a memory, a sequencing module, a memory updating module, and a rule logic module. The memory comprises an IL offset stack and a data structure that stores information of an IL stack corresponding to a processed IL instruction. The verification apparatus processes the IL program in a straight-line manner except when encountering IL instructions that correspond to designated op code types. In such cases, the verification apparatus may alter a sequencing of processing the IL program by utilizing the IL offset stack.

Claims

1. A method for verifying an intermediate language (IL) program in a single pass, the method comprising the steps of:

(a) encountering an IL instruction, wherein the IL instruction is associated with an IL offset;

(b) decode the IL instruction to determine an op code type;

(c) processing the IL instruction in accordance with the IL op code type and a rule set;

(d) updating a first data structure, a second data structure, and a third data structure, wherein the first data structure comprises an IL offset stack, the second data structure comprises a current IL stack, and the third data structure comprises a flag array;

(e) determining a next IL instruction.

2. The method of claim 1, wherein step (d) comprises the step of merging the current IL stack with an associated IL stack.

3. The method of claim 1, further comprising the step of:

(f) repeating steps (a)-(d) in response to step (e).

4. The method of claim 3, wherein an ordering of processing the IL program is rearranged so that a portion of the IL program is not processed.

5. The method of claim 1, wherein step (b) determines that the IL op code type corresponds to an unconditional branch and wherein a target IL instruction has already been processed, wherein step (d) comprises the step of merging the current IL stack with a target IL stack, and wherein step (e) comprises the step of popping the IL offset stack.

6. The method of claim 1, wherein step (b) determines that the IL op code type corresponds to an unconditional branch and wherein a target IL instruction has not already been processed, and wherein step (e) comprises the step of:

setting an instruction pointer to an offset of the target IL instruction, wherein the target IL instruction shall be subsequently processed.

7. The method of claim 1, wherein step (b) determines that the IL op code type corresponds to a conditional branch, wherein a target IL instruction has not already been processed, wherein step (d) comprises the step of pushing an offset of a following IL instruction on the IL offset stack, and wherein step (e) comprises the step of setting an instruction pointer to an offset of the target IL instruction, wherein the target IL instruction shall be subsequently processed.

8. The method of claim 1, wherein step (b) determines that the IL op code type corresponds to a conditional branch, wherein a target IL instruction has not already been processed, and wherein step (e) comprises the step of setting an instruction pointer to an offset of a following IL instruction, wherein the following IL instruction shall be subsequently processed.

9. The method of claim 1, wherein step (b) determines that the IL op code type corresponds to a conditional branch, wherein a target IL instruction has already been processed, and wherein step (d) comprises the step of merging the current IL stack with a target IL stack, and wherein step (e) comprises the step of popping the IL offset stack.

10. The method of claim 1, wherein step (b) determines that the IL op code type corresponds to a leave, wherein a target IL instruction is outside an exception handling block, wherein the target IL instruction has not been already processed, wherein step (d) comprises the step of inserting an IL offset of the target IL instruction in front of a first IL offset outside the exception handling block into the IL offset stack, and wherein step (e) comprises the step of popping the IL offset stack.

11. The method of claim 1, wherein step (b) determines that the IL op code type corresponds to a leave, wherein a target IL instruction is outside an exception handling block, wherein the target IL instruction has already been processed, wherein step (d) comprises the step of merging the current IL stack with a target IL stack, and wherein step (e) comprises the step of popping the IL offset stack.

12. The method of claim 1, wherein step (b) determines that the IL op code type corresponds to a leave, wherein a target IL instruction is inside an exception handling block, wherein the target IL instruction has not already been processed, and wherein step (e) comprises the step of setting an instruction pointer to an offset of the target IL instruction, wherein the target IL instruction shall be subsequently processed.

13. The method of claim 1, wherein step (b) determines that the IL op code type corresponds to a leave, wherein a target IL instruction is inside an exception handling block, wherein the target IL instruction has already been processed, and wherein step (d) comprises the step of merging the current IL stack with a target IL stack, and wherein step (e) comprises the step of popping the IL offset stack.

14. The method of claim 1, wherein step (b) determines that the IL instruction corresponds to a start of a try block, wherein step (d) comprises the step of pushing a current IL offset on the IL offset stack and the step of pushing IL offsets of associated exception handlers on the IL offset stack, wherein a highest IL offset is first, and wherein step (e) comprises the step of popping the IL offset stack.

15. The method of claim 1, wherein step (b) determines that the IL op code corresponds to a throw, a return, a rethrow, or a last instruction in an exception handling block, wherein step (e) comprises the step of popping the IL offset stack.

16. The method of claim 1, wherein step (e) determines that the IL op code type corresponds to a switch, wherein step (c) comprises the step of validating the IL offset of each clause, wherein step (d) comprises the step of pushing the IL offset of each clause on the IL offset stack, and wherein step (e) comprises the step of popping the IL offset stack.

17. The method of claim 1, wherein step (e) causes sequencing the IL program in a straight-line manner except when the IL instruction has an op code type selected from the group consisting of an unconditional branch, a conditional branch, a leave, a throw, a return, and a switch.

19. A computer-readable medium having computer-executable instructions for performing the steps recited in claim 1.

18. The method of method 1, further comprising the step of:

(f) determining that a verification of the IL program has been completed when the IL offset stack is empty and popping the IL offset stack is attempted.

20. A verification module for verifying an intermediate language (IL) program in a single pass, the IL program comprising a plurality of IL instructions, the verification module comprising:

(a) a memory comprising;

a data structure that stores information about an IL stack entry for a first IL instruction corresponding to a first IL offset;

an IL offset stack that stores a second IL offset corresponding to a second IL instruction; and

a flag entry that indicates if the first IL instruction has been processed;

(b) a sequencing module that determines a next IL instruction that is to be processed in accordance with an op code type that is associated with the first IL instruction;

(c) a memory updating module that updates the data structure with the state information about the first IL instruction and updates the IL offset stack; and

(d) rule logic module that processes the first IL instruction in accordance with the op code type.

21. The verification module of claim 20, further comprising:

(e) a status module that obtains results from the rule logic module; and

(f) a display unit that is instructed by the status module to control an indicator in accordance with the results.

22. The verification module of claim 20, further comprising:

(e) a status module that obtains results from the rule logic module and informs a server to reload another version of the IL program.

23. The verification module of claim 20, wherein the information that is stored in the IL stack entry is differentially characterized between the IL instruction and another IL instruction.

24. The verification module of claim 20, wherein the rule logic module is in accordance with European Computer Manufacturer'"'"'s Association (ECMA) standards for an intermediate language.

25. The verification module of claim 20, wherein the verification module is coupled to a compiler module.

26. The verification module of claim 20 that is implemented with a component selected from the group consisting of:

a general purpose computer, a microprocessor, a discrete logic circuitry, and an application specific integrated circuit (ASIC).

27. The verification module of claim 20, wherein the EL program is obtained from a high-level program that is written in a high-level language that is selected from the group consisting of:

a visual basic language, a C++ language, and a C# language.