Monday Aug 23, 2010

Yet another offline Java bytecode verifier

When directly manipulating or generating Java bytecode, it's not too hard to end up with bytecode that will not verify. The JVM will catch this code at runtime. However, the verifier in a JVM exists primarily to ensure secure execution of Java code, not to assist with bytecode-level programming. As a result, the verification error messages printed by a JVM are typically not so useful when trying to figure out why exactly your manipulated/generated bytecode does not verify. This is a well known problem and there already exists a number of standalone verifiers that provide very informative error messages. The ASM Java bytecode manipulation and analysis framework includes a builtin class verifier as does the BCEL library.

In the Maxine VM project, we use bytecode generation/manipulation as an alternative to writing assembler code. For example, we implement JNI stubs via generated bytecode (using a couple of bytecode extensions specific to Maxine). As such, we run into the usual issues of ensuring that the bytecode we generated was verifiable. Initially, we considered using one of the aforementioned libraries to address this. However, given that our goal is to develop a specification compliant JVM implementation we had to implement a verifier anyway. So, with the help of a sharp intern (thanks Dave!) we wrote one. Actually, we wrote two - one that performs type inferencing for class files with a version number less than 50 and one that does type checking for more recent class files (those compliant with the class file changes specified in JSR202). Now we have a verifier that not only passes the relevant JCK tests but is also a development aid whenever we do bytecode-level programming in the VM.

Useful functionality in the Maxine code base that can be made to work standalone is exposed by the max script. So, for anyone wanting yet another offline verifier, this script includes a verify sub-command. Here's how to get the usage message for this command:

~/maxine$ max help verify
max verify [options] patterns...

verifies a set methods using the Maxine bytecode verifier

    Run the Maxine verifier over a set of specified methods available
    on the class path. To extend the class path, use one of the global
    "-cp/p:" or "-cp/a:" options.

    See Patterns below for a description of the format expected for "patterns..."

    Use "max verify -help" to see what other options this command accepts.
    
    --- Patterns ---
    
    A pattern is a class name pattern followed by an optional method name...

Here's the output of using it to verify a negative-test (i.e. expected to cause a failure) from the JCK:

~/maxine$ max -cp/a:/Volumes/JCK-runtime-6/classes verify javasoft.sqe.tests.vm.classfmt.ins.instr_006.instr_00601m1t.instr_00601m1tn:m
Initializing verifier system...
Initialized verifier system
Finding specified methods...
Found 1 methods
Exception in thread "main" VerifyError: Missing stackmap frame for bytecode position 26 (branch target)
    while verifying javasoft.sqe.tests.vm.classfmt.ins.instr_006.instr_00601m1t.instr_00601m1tn.m() at bytecode position 1
        at com.sun.max.vm.classfile.ErrorContext.verifyError(ErrorContext.java:179)
        at com.sun.max.vm.verifier.MethodVerifier.verifyError(MethodVerifier.java:124)
        at com.sun.max.vm.verifier.TypeCheckingMethodVerifier.frameAt(TypeCheckingMethodVerifier.java:209)
        at com.sun.max.vm.verifier.TypeCheckingMethodVerifier.performBranch(TypeCheckingMethodVerifier.java:317)
        at com.sun.max.vm.verifier.TypeCheckingMethodVerifier$Interpreter.lookupswitch(TypeCheckingMethodVerifier.java:1579)
        at com.sun.max.vm.bytecode.BytecodeScanner.scanInstruction(BytecodeScanner.java:991)
        at com.sun.max.vm.bytecode.BytecodeScanner.scan(BytecodeScanner.java:1197)
        at com.sun.max.vm.verifier.TypeCheckingMethodVerifier.verifyBytecodes(TypeCheckingMethodVerifier.java:145)
        at com.sun.max.vm.verifier.TypeCheckingMethodVerifier.verify(TypeCheckingMethodVerifier.java:112)
        at com.sun.max.vm.verifier.TypeCheckingVerifier.verify(TypeCheckingVerifier.java:71)
        at test.com.sun.max.vm.verifier.CommandLineVerifier.main(CommandLineVerifier.java:106)

To see the abstract interpreter in action, use the -verbose option:

~/maxine$ max -cp/a:/Volumes/JCK-runtime-6/classes verify -verbose=3 javasoft.sqe.tests.vm.classfmt.ins.instr_006.instr_00601m1t.instr_00601m1tn:m
Initializing verifier system... 
Initialized verifier system
Finding specified methods...
Found 2 methods

Verifying javasoft.sqe.tests.vm.classfmt.ins.instr_006.instr_00601m1t.instr_00601m1tn.m()
Input bytecode:
Stack=1, Locals=1
0: iconst_1 | 4
1: lookupswitch default:20 1:26 | 171 0 0 0 0 0 19 0 0 0 1 0 0 0 1 0 0 0 25
20: return | 177
StackMapTable: number of entries = 1
  20: frame_type = 255 /\* full_frame \*/
    offset_delta = 20
    number_of_locals = 1
    locals = [ javasoft.sqe.tests.vm.classfmt.ins.instr_006.instr_00601m1t.instr_00601m1tn ]
    number_of_stack_items = 0
    stack = [  ]

StackMapTable frames:
0: local[0] = javasoft.sqe.tests.vm.classfmt.ins.instr_006.instr_00601m1t.instr_00601m1tn
20: local[0] = javasoft.sqe.tests.vm.classfmt.ins.instr_006.instr_00601m1t.instr_00601m1tn

Interpreting bytecode:
    local[0] = javasoft.sqe.tests.vm.classfmt.ins.instr_006.instr_00601m1t.instr_00601m1tn
0: iconst_1

    stack[0] = int
    local[0] = javasoft.sqe.tests.vm.classfmt.ins.instr_006.instr_00601m1t.instr_00601m1tn
1: lookupswitch

Exception in thread "main" VerifyError: Missing stackmap frame for bytecode position 26 (branch target)
    while verifying javasoft.sqe.tests.vm.classfmt.ins.instr_006.instr_00601m1t.instr_00601m1tn.m() at bytecode position 1
        at com.sun.max.vm.classfile.ErrorContext.verifyError(ErrorContext.java:179)
        at com.sun.max.vm.verifier.MethodVerifier.verifyError(MethodVerifier.java:122)
        at com.sun.max.vm.verifier.TypeCheckingMethodVerifier.frameAt(TypeCheckingMethodVerifier.java:209)
        at com.sun.max.vm.verifier.TypeCheckingMethodVerifier.performBranch(TypeCheckingMethodVerifier.java:317)
        at com.sun.max.vm.verifier.TypeCheckingMethodVerifier$Interpreter.lookupswitch(TypeCheckingMethodVerifier.java:1579)
        at com.sun.max.vm.bytecode.BytecodeScanner.scanInstruction(BytecodeScanner.java:991)
        at com.sun.max.vm.bytecode.BytecodeScanner.scan(BytecodeScanner.java:1197)
        at com.sun.max.vm.verifier.TypeCheckingMethodVerifier.verifyBytecodes(TypeCheckingMethodVerifier.java:145)
        at com.sun.max.vm.verifier.TypeCheckingMethodVerifier.verify(TypeCheckingMethodVerifier.java:112)
        at com.sun.max.vm.verifier.TypeCheckingVerifier.verify(TypeCheckingVerifier.java:71)
        at test.com.sun.max.vm.verifier.CommandLineVerifier.main(CommandLineVerifier.java:106)

The verify sub-command is available as of version 4278 in the main Maxine repository.

About

Doug Simon

Search

Categories
Archives
« April 2014
SunMonTueWedThuFriSat
  
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
   
       
Today