A number of cases where the Frames stored in JustIce's InstructionContext instances disagree with what Sun's Preverifier produces have been found. Most of these cases are related to the way that JustIce verifies Exception handlers. It seems that JustIce verifies Exception handlers more often than the specification requires, which results in inconsistencies between JustIce and Sun's code.
The problem is understood. Implementing a solution would be non-trivial.
| Package | Class | Method | Method # | Effect | Source |
|---|---|---|---|---|---|
| com.markcrocker.purifier.testcases | ProblemCases | unresolvedNullObject() | 6 | Passes despite issue. | Purifier project |
| remove2(int) | 14 | ||||
| remove(int) | 14 | Fails due to issue. |
The Purifier, occasionally disagrees with what Sun's preverifier produces because the algorithms are not identical. In an effort to understand these cases, the JustIce Verifier, which is included in the BCEL library, was used as a window into the algorithm in the JVM Specification section 4.9.2, The Bytecode Verifier. JustIce was designed to follow Sun's JVM Specification and it was rumoured that Sun's J2ME preverifier was created by modifying their existing verifier. Consequently, JustIce aught to provide a way to see how Sun's preverifier arrives at certain results. However, modifying JustIce's Verifier to log certain internal operations to the console revealed that there were cases where JustIce disagrees with Sun's preverifier.
This situation represents a hidden bug in the JustIce Pass3bVerifier. It is the sort of thing were the bug is not really noticible when running JustIce, but does appear when looking into the internal behaviour of JustIce. It is unknown if any invalid classes are passed by JustIce or valid classes failed by JustIce due to this problem. All that is known is that the internal state of JustIce occationally disagrees with the StackMap produced by Sun's preverifier.
The cause of this problem is related to the way that JustIce verifies Exception handlers in the Pass3bVerifier class. In the Pass3bVerifier.circulationPump method, every InstructionContext that is inside a try block has it's outFrame checked against the inFrame of the first InstructionContext of each of the corresponding Exception handlers. This is accomplished by using the InstructionContext.execute method of the handler's first InstructionContext with the inFrame set to the current InstructionContext's outFrame (actually a clone with a modified OperandStack holding the Exception type). This, in turn, causes the two Frames to be merged at the first InstructionContext of the Exception handler. If the merging process indicates that a change had to be made, then the Pass3bVerifier.circulationPump will add the Exception handler to the InstructionContext queue of branches to be traversed.
This behaviour is a misinterpretation of a somewhat vague section in the specification (section 4.9.2) regarding how Exception handlers are to be checked. The section, exerpted from the original is:
Determine the instructions that can follow the current instruction. Successor instructions can be one of the following:
The next instruction, if the current instruction is not an unconditional control transfer instruction (for instance goto, return, or athrow). Verification fails if it is possible to "fall off" the last instruction of the method.
The target(s) of a conditional or unconditional branch or switch.
Any exception handlers for this instruction.
Merge the state of the operand stack and local variable array at the end of the execution of the current instruction into each of the successor instructions. In the special case of control transfer to an exception handler, the operand stack is set to contain a single object of the exception type indicated by the exception handler information.
If this is the first time the successor instruction has been visited, record that the operand stack and local variable values calculated in steps 2 and 3 are the state of the operand stack and local variable array prior to executing the successor instruction. Set the "changed" bit for the successor instruction.
If the successor instruction has been seen before, merge the operand stack and local variable values calculated in steps 2 and 3 into the values already there. Set the "changed" bit if there is any modification to the values.
Although the Pass3bVerifier does seem to follow these steps, it is my contention that the JustIce's interpretation of the third point of item 3, Any exception handlers for this instruction, is too broad. Not all instructions can throw an Exception. Therefore, it is not be reasonable to check every instruction in a try block against the handler as JustIce does. JustIce does make an effort to only add branches to the queue when the branch would cause a merge change. This does reduce thrashing significantly, but is still overkill because not all instructions inside of a try block can cause a branch to the handler.
This theory rests on the assumption that Sun's preverifier uses the same algorithm as their JVM verifier as described in the specification. Since the Purifier1 project is an open source project and I am not a Sun licensee and do not know if this assumption is correct. However, the preponderance of evidence makes it seem extremely likely that I'm right about this.
ProblemCases.remove method provides an example of this issue and is shown below.
204: public void remove(int index) { 205: Object object = null; 206: try { 207: object = vector.elementAt(index); 208: } catch (ArrayIndexOutOfBoundsException aioobe) { 209: object = null; 210: } 211: if (object != null) { 212: vector.removeElementAt(index); 213: } 214: }
The following byte code is from the compiled and preverified class file created from the source in the previous section. The StackMap has been reformatted for readability.
public void remove(int arg1)
Code(max_stack = 2, max_locals = 4, code_length = 30)
0: aconst_null
1: astore_2
2: aload_0
3: getfield com.markcrocker.purifier.testcases.ProblemCases.vector Ljava/util/Vector; (20)
6: iload_1
7: invokevirtual java.util.Vector.elementAt (I)Ljava/lang/Object; (21)
10: astore_2
11: goto #17
14: astore_3
15: aconst_null
16: astore_2
17: aload_2
18: ifnull #29
21: aload_0
22: getfield com.markcrocker.purifier.testcases.ProblemCases.vector Ljava/util/Vector; (20)
25: iload_1
26: invokevirtual java.util.Vector.removeElementAt (I)V (22)
29: return
Exception handler(s) =
From To Handler Type
2 11 14 java.lang.ArrayIndexOutOfBoundsException(13)
Attribute(s) = StackMap(
(
offset = 14,
locals = {
(type=Object, (28)class=com.markcrocker.purifier.testcases.ProblemCases),
(type=Integer),
(type=Null)
},
stack items = {
(type=Object, (13)class=java.lang.ArrayIndexOutOfBoundsException)
}
)
(
offset = 17,
locals = {
(type=Object, (28)class=com.markcrocker.purifier.testcases.ProblemCases),
(type=Integer),
(type=Object, (93)class=java.lang.Object)
}
)
(
offset = 29,
locals = {
(type=Object, (28)class=com.markcrocker.purifier.testcases.ProblemCases),
(type=Integer),
(type=Object, (93)class=java.lang.Object)
}
)
)
The aload_0 instruction at offset 2 is also the start of the try block that is protected by the Exception handler, which starts at offset 14. Clearly, the outgoing Frame of that aload_0 instruction should be the incoming Frame at the start of the handler. The early part of the log from Pass3bVerifier confirms this:
DEBUG: Investigating instruction 2: aload_0[42](1) DEBUG: Frame of normal successor is: Local Variables: 0: com.markcrocker.purifier.testcases.ProblemCases 1: int 2: <null object> 3: <unknown object> OperandStack: Slots used: 1 MaxStack: 2. com.markcrocker.purifier.testcases.ProblemCases (Size: 1) DEBUG: Checking Exception handler at offset 14 DEBUG: Incoming Frame changed, so add Exception handler to icq.
This leads to a first pass through the Exception handler featuring log entries of:
DEBUG: Instruction 14: astore_3[78](1) DEBUG: inFrame is: Local Variables: 0: com.markcrocker.purifier.testcases.ProblemCases 1: int 2: <null object> 3: <unknown object> OperandStack: Slots used: 1 MaxStack: 2. java.lang.ArrayIndexOutOfBoundsException (Size: 1)
This agrees completely with the StackMapEntry for offset 14 produced by Sun's preverifier (after the astore_3 has been processed). However, further traversal of the main branch of execution eventually leads to the astore_2 instruction at offset 10, which does cause an inFrame merge change because it adds a java.lang.Object reference to LocalVariables slot 2. This is the correct type for this slot at that point of execution, so this isn't wrong, but the merge change of the offset 14 InstructionContext incoming frame does cause a problem. It also gets added to the InstructionContext queue, which re-verifies the Exception handler at offset 14 with a different incoming Frame. This merge and second verification pass through the Exception handler results in an incoming frame at offset 14 of:
DEBUG: Instruction 14: astore_3[78](1) DEBUG: inFrame is: Local Variables: 0: com.markcrocker.purifier.testcases.ProblemCases 1: int 2: java.lang.Object 3: <unknown object> OperandStack: Slots used: 1 MaxStack: 2. java.lang.ArrayIndexOutOfBoundsException (Size: 1)
this disagrees with the StackMapEntry for offset 14! So, this merge and second pass verification messes up the stored frames. Although LocalVariables slot is indeed intended to store a java.lang.Object, that fact is not known by any instruction in the try block that can actually throw an Exception, which is supposed to be the only way into the Exception handler, so it makes sense that the StackMapType for this slot should resolve to an ITEM_Null. Later on in the execution, starting at offset 7, the type is known to be a java.lang.object, so it makes sense that the StackMapEntry's include a java.lang.Object for later offsets, but not for offset 14.
ProblemCases.remove2 method provides a counter example of this issue and is shown below.
236: public void remove2(int index) { 237: Object object = null; 238: try { 239: object = vector.elementAt(index); /* can throw an exception, but object = null */ 240: object = vector.elementAt(index+1); /* can throw exception, now object = Object */ 241: } catch (ArrayIndexOutOfBoundsException aioobe) { 242: object = null; 243: } 244: if (object != null) { 245: vector.removeElementAt(index); 246: } 247: }
Note that the only real difference is that there is an extra line that can also throw an ArrayIndexOutOfBoundsException after a line that definitively establishes that the variable 'object' is a java.lang.Object. This is a significant change because, now there is a second entry point into the Exception handler where the type is now known to be something higher up on the merging hierarchy than a Null object.
The following byte code is from the compiled and preverified class file created from the source in the previous section. The StackMap has been reformatted for readability.
public void remove2(int arg1)
Code(max_stack = 3, max_locals = 4, code_length = 41)
0: aconst_null
1: astore_2
2: aload_0
3: getfield com.markcrocker.purifier.testcases.ProblemCases.vector Ljava/util/Vector; (20)
6: iload_1
7: invokevirtual java.util.Vector.elementAt (I)Ljava/lang/Object; (21)
10: astore_2
11: aload_0
12: getfield com.markcrocker.purifier.testcases.ProblemCases.vector Ljava/util/Vector; (20)
15: iload_1
16: iconst_1
17: iadd
18: invokevirtual java.util.Vector.elementAt (I)Ljava/lang/Object; (21)
21: astore_2
22: goto #28
25: astore_3
26: aconst_null
27: astore_2
28: aload_2
29: ifnull #40
32: aload_0
33: getfield com.markcrocker.purifier.testcases.ProblemCases.vector Ljava/util/Vector; (20)
36: iload_1
37: invokevirtual java.util.Vector.removeElementAt (I)V (22)
40: return
Exception handler(s) =
From To Handler Type
2 22 25 java.lang.ArrayIndexOutOfBoundsException(13)
Attribute(s) =
StackMap(
(
offset = 25,
locals = {
(type=Object, (28)class=com.markcrocker.purifier.testcases.ProblemCases),
(type=Integer),
(type=Object, (94)class=java.lang.Object)
},
stack items = {
(type=Object, (13)class=java.lang.ArrayIndexOutOfBoundsException)
}
)
(
offset = 28,
locals = {
(type=Object, (28)class=com.markcrocker.purifier.testcases.ProblemCases),
(type=Integer),
(type=Object, (94)class=java.lang.Object)
}
)
(
offset = 40,
locals = {
(type=Object, (28)class=com.markcrocker.purifier.testcases.ProblemCases),
(type=Integer),
(type=Object, (94)class=java.lang.Object)
}
)
)
Although very similar to the DFA for the previous example, the key thing to notice here is that, now, the StackMapEntry at offset 25 (equivalent to offset 14 in the previous example) has a java.lang.Object in LocalVariables slot 2. Clearly, the fact that there is now a second instruction that can throw an ArrayIndexOutOfBoundsException after an instruction that clearly establishes that LocalVariables slot 2 holds a java.lang.Object convinces Sun's preverifier that the incoming frame at the start of the Exception handler should also have a java.lang.Object in slot 2 of the LocalVariables.
The JustIce Pass3bVerifier also comes to the same conclusion, but not for the correct reasons. JustIce flags the astore_2 instruction at offset 10 as having a successor of 25. This is incorrect, but does, by chance, happen to have the correct Frame for merging with the Exception handler's incoming Frame. What it should be doing is flagging the invokevirtual instruction at offset 18 as being the instruction that can throw an ArrayIndexOutOfBoundsException and, therefore, have a successor of offset 25. JustIce does not notice the merge change at the astore_2 instruction at offset 21 because the previous merge from the astore_2 at offset 10 has already created an incoming Frame at offset 25 that doesn't need to be merged with the outgoing Frame at offset 21.
Modify the Pass3bVerifier.circulationPump method to only consider Exception handlers as possible successors when the current instruction can actually throw a type of Exception that the handler is designed to catch. This is a non-trivial exercise.
One key point is that it is not reasonable, and in some cases not possible, to calculate all possible Exceptions an instruction can throw and only consider the handler to be a successor if there is a match between what the instruction can throw and what the handler can catch. Instead, it seems that the preverifier considers any instruction that can throw an Exception of any type as having the handler as a successor. JustIce has an Interface, ExceptionThrower, that can be used to identify instructions that can throw an exception. In addition, the preverifier seems to indicate that the first and last instruction in protected code have the handler as a successor even if they can't normally throw an Exception. Throwables like VirtualMachineError, that any instruction can throw are not considered.
Back to Developer's Guide Purifier Home Page
