Back to course

The Verifier's Data

23 minadvancedModule 2: Members and CodeContinues from jvm-branches
23 min · Module 2: Members and Code · Algorithms

Why This Matters

Here is a genuinely strange thing about the class file format, and it is worth stating plainly before anything else: a compiler writes down the result of a type-checking analysis, in the file, where a verifier will check it. Not the code — the code is there to be executed. The conclusions are also there, as data, so that the virtual machine can check them cheaply.

The reason is a performance argument with a long history behind it. Before Java 6, the JVM verified bytecode by executing an abstract interpretation of it: it walked every instruction, tracked the type of every stack slot, and proved the method type-safe. That is sound and it is slow. Proving that a method is safe costs time proportional to the code, on every class, once per class loaded — and the result does not depend on anything at run time.

So the conclusion was hoisted out of the loop. The compiler, which has already done the analysis, writes a StackMapTable saying “at this offset, the frame is in this state”, and the verifier's job drops from proving to checking — following the frames and confirming each one is reachable and consistent. That is a large constant-factor win, and it is why the table exists. The price is that the file now contains a claim about the code, and the verifier's job has changed from proving the claim to trusting-with-checks.

A Simple Model

What a frame is, and then how the table encodes a sequence of them:

a FRAME at some point in the code is: locals[0 .. max_locals) each slot holds a type stack[0 .. stack_depth) each entry holds a type and a StackMapTable is a list of frames at chosen offsets: u2 number_of_entries then that many frames the frames are stored as DIFFERENCES from each other, and each frame_type byte says which of several shapes this frame is:

There are fifteen frame types, and they are not fifteen different kinds of frame. They are fifteen ways of saying “here is what changed since the last one”. The first frame is special because there is no previous one.

TypeRangeMeans
same_frame0–63nothing changed; the frame_type is the offset
same_locals_1_stack_item64–127locals unchanged, stack depth is 1; frame_type minus 64 is the offset delta
same_locals_1_stack_item_extended247as above, with a full 16-bit delta
chop_frame248–250locals unchanged, stack is empty, and 1 to 3 locals were chopped
same_frame_extended251nothing changed, with a full 16-bit delta
append_frame252–254locals unchanged, stack empty, 1 to 3 locals appended
full_frame255everything restated: all locals, then the stack

The compression is the whole design, and it is a delta encoding against the previous frame. A same_frame costs one byte and says nothing at all — the verifier already knows the state, because the previous frame told it and nothing has changed. That is what makes the table small enough to be worth having: most branch targets in real code are reached with the locals unchanged, because most branches are loops and conditionals that do not touch the frame.

And the range allocation is doing real work. Types 0 to 63 are free offsets, which covers small methods entirely in one byte per frame. 64 to 127 cost one byte of offset and buy a one-item stack, which is the single most common change in practice: a branch that just stored something. Everything else needs a second byte, and the two _extended types exist only because a method longer than 127 bytes runs out of the one-byte range.

The Actual Detail

The tableswitch method's table, in full. Eight bytes for six frames, and every byte accounted for:

  00 06 24 01 01 01 01 01
    |  |  |  |  |  |  +-- frame 5: 0x01
    |  |  |  |  |  +----- frame 4: 0x01
    |  |  |  |  +-------- frame 3: 0x01
    |  |  |  +----------- frame 2: 0x01
    |  |  +-------------- frame 1: 0x01
    |  +----------------- frame 0: 0x24 = 36, a same_frame at 36
    +-------------------- 6 frames

Six same_frames at one byte each. And here is the arithmetic, which is the detail that makes the encoding click:

frame 0: offset = 36 (0x24, the frame_type IS the offset) frame 1: offset = 36 + 1 + 1 = 38 (0x01, and the +1 is the rule) frame 2: offset = 38 + 1 + 1 = 40 frame 3: offset = 42 frame 4: offset = 44 frame 5: offset = 46

Why the +1. Every frame after the first is stored as a delta from the previous frame's offset, and the delta is one less than the actual difference. The reason is that a delta of zero would be ambiguous: 0x00 is same_frame with a zero delta, which would mean two frames at the same offset. Subtracting one makes every real difference representable in one byte, and it means a same_frame at the very next instruction has a delta of zero — which is legal and which is exactly what a loop back to the following instruction looks like.

And the payoff is the cross-check from the previous concept. Those six frame offsets are 36, 38, 40, 42, 44, 46, and the switch's six destinations are 36, 38, 40, 42, 44, 46 — the five cases plus the default, derived independently, matching to the byte. Six frames for six branch targets, one byte each, because at every one of those points the frame is identical to the one before.

What a frame that has to say something looks like

The trycatch method, where the frames are same_locals_1_stack_item and so carry a type. Fourteen bytes for three frames:

  00 03 4a 07 00 07  47 07 00 09  48 07 00 15
    |  |  |  |  |  |  +------- 0x0015 = 21 -> Throwable
    |  |  |  |  |  +---------- 0x07: an OBJECT type
    |  |  |  |  +------------- 0x48 = 72, a same_locals_1_stack_item
    |  |  |  +--------------- 0x0009 -> RuntimeException
    |  |  +------------------ 0x07: an OBJECT type
    |  +--------------------- 0x47 = 71, a same_locals_1_stack_item
    |  +----------------------- 0x0007 -> ArithmeticException
    +-------------------------- 0x07: an OBJECT type
    +---------------------------- 0x4a = 74, a same_locals_1_stack_item
    +------------------------------ 3 frames

The structure of each entry is three bytes of overhead plus a type: a one-byte frame type, then a verification type consisting of a one-byte tag and a two-byte pool index. And the three frame types, 74, 71 and 72, have to be read as 64 plus an offset delta:

  frame 0:  74 - 64 = 10  -> offset 10        ArithmeticException
  frame 1:  71 - 64 =  7  -> 10 + 7 + 1 = 18  RuntimeException
  frame 2:  72 - 64 =  8  -> 18 + 8 + 1 = 27  Throwable

And those three offsets are 10, 18 and 27 — the three exception handler targets from the previous concept, exactly. So the frames are the type checker's note that at each handler, the stack holds one value of the caught type, and the locals are whatever they were.

A hypothesis this course formed, tested, and had to discard. Seeing 74, 71 and 72 as raw bytes gives 0x4A, 0x47, 0x48 — and those are the astore, astore_0 and astore_1 opcodes. That is a coincidence worth chasing, because the specification really does say a same_locals_1_stack_item frame always follows an astore-family instruction, and the frame's single stack item is whatever that store put there. The connection looked like a lovely piece of encoding economy: the frame type is the instruction that produced the item, so the verifier does not have to be told twice. It is wrong, and the bytes say so. The instructions at offsets 10, 18 and 27 in that method are astore_2, astore_2 and astore 4 — opcodes 0x4D, 0x4D and 0x3A, none of which is 0x4A, 0x47 or 0x48. The frame type is 64 plus an offset delta and nothing else; the astore opcodes merely occupy the same numeric range. Recording this matters more than the finding it replaced, because a plausible story that survives a glance is exactly what this course keeps warning about — the 64-to-127 range was allocated to this frame type, and the astore family happens to live at 64 to 127 too, and those two facts are unrelated.

The verification type tags

The second half of a frame entry is a type, and its tag byte is a second, smaller tag space:

  tag  meaning
    0   TOP                 the unusable half of a long or double
    1   INTEGER             int, short, byte, char, boolean
    2   FLOAT
    3   DOUBLE
    4   LONG
    5   NULL                the type of a null reference
    6   UNINITIALIZED_THIS  in a constructor, before super() runs
    7   OBJECT              + a u2 pool index to a Class
    8   UNINITIALIZED      + a u2 offset: a new that has not completed

Two of those are worth pausing on, because they are the verifier's internal states leaking into the file.

TOP is the unusable half of a 64-bit value — the same two-slot rule a third time. A long occupies two local slots, the second holds no value, and the type checker needs a name for that slot, so it invents one and writes it in the file. It is the local-frame twin of the constant pool's second index, and the reason is the same: a 64-bit value is two 32-bit units, and everything that tracks such a value has to account for both.

And UNINITIALIZED_THIS exists because of a language rule, not a machine one. Java requires a superclass constructor to run before the object is usable, so the verifier tracks an object whose superclass constructor has not yet been called. The source is super() being mandatory as the first statement of a constructor, and it is the reason a verifier exists at all: without the check, a subclass could read a field before the superclass set it, and the failure would be a silent wrong value rather than a crash.

A Real Example

What the verifier actually does with the table, and why the change from proving to checking is safe:

verify(method):

    # NOT: walk every instruction tracking every type
    #      (that is the pre-Java-6 verifier, and it is what this
    #       table exists to avoid)

    frame = implicit_initial_frame()     # from the descriptor
    pending_targets = every branch destination in the method

    for each frame in the StackMapTable:
        offset = frame.offset
        assert offset is in pending_targets
            the table must only claim positions the code
            actually branches to. A frame anywhere else is
            rejected -- it is a claim about a path that does
            not exist.

        # apply the DELTA, not a description
        frame.locals = previous.locals + frame's local changes
        frame.stack  = previous.stack  + frame's stack changes

        walk the code from the last frame's offset to here,
        simulating only the INSTRUCTIONS, and check that the
        simulation arrives at exactly the state the frame claims

        pending_targets -= destinations inside the range just walked

    assert pending_targets is empty
        every branch in the method was covered by some frame

Three assertions in that, and each one is a place a malformed file is caught. The table may only claim positions that are real branch targets, so a table that describes a path the code does not have is rejected rather than ignored. The simulation must agree with the claim — so the table cannot assert a type the code would not produce, which means a compiler cannot lie about a method being safe when it is not. And every branch must be covered, so omitting a frame for a real target is an error rather than a gap.

That last one is what stops the whole scheme from being a security hole. If a method contained a branch target with no frame, a lazy verifier would simply not check it — and the method's type safety would rest on nothing. So the verifier's first act is to enumerate the branch targets itself, independently, and then require the table to match. It is a checksum over the control-flow graph, written by the compiler and verified by the machine, and that is why the table can be trusted to have skipped nothing.

Why the delta encoding is safe is the more interesting question, and the answer is that it is not a claim about correctness at all — only about effort. A full_frame restates the locals, so a table of only full frames would carry exactly the same information in more bytes. The deltas are a compression with no loss, and they are safe because the verifier reconstructs the full state before checking anything against it. What changed in Java 6 was not what the verifier knows; it is how much work the compiler does to let the verifier skip.

And the cost falls on the producer, which is worth naming because it is unusual. The class file is now larger — a StackMapTable is a real cost in every method with a branch. And the compiler must compute the frames even when nothing will ever verify the result, because the table is not optional for a version 50 or later class file. A tool that generates class files has to implement the analysis whether or not it cares about type safety, which is why class file generators are rare and bytecode libraries are not.

Try It Yourself

$ javap -v -p out/Shapes.class
$ python3 courses/jvm/assets/samples/class_decode.py out/Shapes.class

Check Your Understanding

Without looking back: a method's StackMapTable holds six frames, all same_frame, with frame type bytes 36, 1, 1, 1, 1, 1. What are the six frame offsets, how many bytes does the whole table occupy, and what does the fact that all six are same_frame tell you about those six points in the code?

Apply It

A third-party bytecode library generates class files. Everything works until it hits a method with more than 127 bytes of code containing a forward branch. At that point the JVM rejects the class with Expecting a stackmap frame at branch target. Methods under that size are fine, including ones with branches. The library was written against a version 50 target. What is the defect, and what is the change that fixes it that is not simply “emit more frames”?

The general habit: a range-limited encoding has a threshold, and a producer that has never crossed it has no evidence its logic is right. Construct the boundary case deliberately — it is the only test that distinguishes “correct” from “correct on this data”.

Connect

A verifier that trusts a producer's conclusions while still checking them is a distinctive arrangement, and the collection has three other examples of the same shape at different levels of trust. A PE load config records the security cookie size and the guard flags, and the loader checks them. An ELF sh_flags records what a section is, and the loader believes it. The difference here is that the checked claim is about the code in the same file, which makes the arrangement unusually strong: a producer cannot lie, because the verifier re-derives the claim by simulating the code and comparing. The load config is trusted on the producer's word; the stack map is checked against the very bytes it describes.

The delta encoding is the same technique as a DWARF .debug_loc list and the same as a COFF line-number run: store what changed, not the state. All three exist because the states are highly repetitive and a consumer already holds the previous one. DWARF is the closest in spirit, because a location list also answers “where does this type apply” and also encodes a transition rather than a snapshot — and a DWARF consumer that ignored the deltas would report the wrong variable type at exactly the points where a variable changes, which is where anyone debugging cares.

The TOP tag is the strongest thread back to the constant pool. This course has now found the same 64-bit rule in three separate places: two pool indices, two local slots, two stack slots, and a TOP verification type for the unusable half. The first was a fetch-uniformity decision and the second a frame-sizing one, but the third is the clearest statement of the underlying reason: the type system itself models the gap. A verifier that tracks a long has to have a name for the slot the value does not occupy, and rather than leaving it implicit the format gives it a tag and writes it in the file. That is a format choosing to make its own internal bookkeeping explicit, and it is the same instinct as the two-byte NUL: represent the awkward case rather than hope tools handle it.

And the honest limit of this module belongs here, because it is where the difficulty is. A StackMapTable is a proof sketch the verifier checks rather than a proof it derives, and the whole design rests on the compiler having done the analysis. Any class file writer is a type checker whether it admits it or not, which is a real barrier to entry for a format that is otherwise remarkably easy to read. Every format with a verifier has some version of this — control flow guard requires a linker to compute a bitmap — but the JVM is the case where the requirement is unavoidable, because the verifier's speed depends on it.

That completes Module 2. Every part of a class file outside the constant pool has now been covered: the members and their types, the frame declaration, the instruction encoding, the offsets, and the verifier's own conclusions. What is left in the format is a long list of attributes — InnerClasses and the $1 numbering, Signature for generics, annotations, records, sealed classes, and modules — and the question of how a format that has no section table accommodates twenty years of new features. Back to the start for the whole shape.