Bytecode Verification and Stack Map Frames

A class file arrives from somewhere else. It may have been produced by a compiler that is not trusted, by a bytecode transformer that rewrote an existing class, or by hand. Before the runtime executes it, the runtime must establish that the code cannot corrupt the virtual machine’s state: that it never pops more values than it pushed, never stores an int where an object reference is expected, never jumps into the middle of an instruction, and never reaches a point where the operand stack’s contents are ambiguous between two paths.

Verification is the proof of those properties. It runs once at load time, and its conclusions let the interpreter skip checks that would otherwise be needed on every instruction. The facts it establishes about operand types are also what lets the interpreter skip checking kinds when a constant pool entry is resolved lazily, since the instruction that names the entry has already been shown to name it with the right kind.

The dataflow formulation

The verifier models each program point with an abstract state: an array of types for the local variables and a list of types for the operand stack. Each instruction has a transfer function from input state to output state, derived from its opcode and, when the opcode carries an index into the constant pool, from the entry that index names. iload_1 reads local slot one, requires it to be an integer, and pushes an integer. invokevirtual pops a receiver and arguments according to the descriptor and pushes the result type.

The analysis propagates these states along control flow edges. At an offset reachable from several predecessors, the incoming states are merged: two states are compatible if their stacks have the same depth and each corresponding type pair has a common supertype. The merged state is the pointwise join, and it replaces the previous state at that offset. If the join changes, the analysis must revisit the successors. This is a standard forward dataflow problem with a lattice of types, and it terminates because the lattice has finite height: each slot’s type can only move upward toward a supertype, and there are finitely many classes.

The old verifier implemented exactly this, iterating over the code until no state changed. It was correct but expensive: a method with many branches could require several passes, each walking the code, and each merge could trigger a class hierarchy query to compute the common supertype. Loading a large application meant doing this for every method, and the cost fell on class loading.

Stack map frames move the analysis to compile time

The current class file format inverts the responsibility. Instead of computing the merge at load time, the compiler computes it and writes the result into the class file as a stack map table. Each frame entry names an offset and declares the full state at that offset: the types of the locals that are not Top and the types on the stack.

The verifier then does a single linear pass. At an offset with a stack map entry, it checks that the declared state is consistent with what the code reaching that offset would produce, but it does not have to iterate to find the fixpoint. At an offset without an entry, the state is derived from the preceding instruction, and the verifier requires that no branch targets that offset.

This converts an iterative analysis into a checking pass, and it converts the cost from load time to compile time. The idea is the lightweight version of proof-carrying code: the producer of the artifact supplies the evidence the consumer needs, and the checker verifies the evidence instead of deriving it. The price is that the compiler must produce correct frames, and a compiler bug becomes a VerifyError at load. Bytecode transformers must also maintain the frames, which is why libraries that rewrite class files have to recompute the stack map table rather than just patching instructions.

The frame encoding is compressed. Rather than writing a full state per offset, each entry is a delta from the previous entry’s state. One form records that nothing changed, others append or chop locals, one appends a single stack item, and a full frame form exists for the cases the deltas cannot express. A method whose branches all occur with the same locals and a growing stack therefore needs only one or two bytes per branch. The compression matters because the stack map table is part of the class file and counts against its size.

What the verifier refuses

The properties enforced are specific. Every instruction must be reachable at an offset that is a valid instruction boundary; a branch to the middle of a multi-byte instruction is rejected. Every local read must have a type that is not Top, meaning the slot has been definitely assigned on all paths reaching the read. Every invoke must see an operand stack whose top entries match the descriptor exactly. Every return must match the method’s declared return type.

Three rules catch most hand-crafted or transformed code. First, the operand stack depth must be identical at every point where control flow merges. Second, a reference may only be used as a reference: it cannot be stored to an integer local and later read as an integer. Third, an uninitialized object may only be used in limited ways until its constructor has run. The third rule is the subtlest, and the verifier tracks it with a distinct type that names both the object and the offset of the new instruction that created it, so that a constructor call can be matched to the specific allocation.

The uninitialized-object rule exists because the type of a freshly allocated object is not yet the type of its class: the constructor has not run, so no invariant that the class establishes can be relied on. Without the rule, code could invoke an overridable method on an object whose fields are still default, or hand it to code that assumes a fully constructed receiver. The rule restricts the object to being stored in a local, passed as a receiver to a constructor of the same class or a superclass, or duplicated on the stack. Anything else is rejected.

Structured control flow avoids the problem

WebAssembly takes the other route: it does not have stack maps because it does not allow arbitrary jumps. Control flow is expressed with block, loop, and if, each carrying a function type that declares the stack shape at entry and exit. A branch names a label, and the validator knows the stack height at that label from the block’s type. Validation is therefore a single pass with no fixpoint and no merge: the stack shape at every label is a static fact of the nesting structure.

The trade is expressiveness. Irreducible control flow, where two loops share a header, cannot be expressed directly and must be restructured, which is why compilers targeting WebAssembly run a relooper-style transformation over the control-flow graph. That transformation sometimes introduces a state variable and a dispatch loop, costing a few instructions per iteration. The JVM’s arbitrary jumps avoid that cost but require the frames.

Both designs reject the same class of errors. A stack underflow is caught in WebAssembly by the validator’s height accounting; in the JVM by the frame check. A type mismatch is caught by the same pointwise comparison. The difference is where the information comes from: shipped metadata in one case, the structure of the code in the other.

Verification is not a sandbox

A verified class file is guaranteed to respect the virtual machine’s type discipline, but it is not guaranteed to be safe to run in an adversarial sense. A verified method can loop forever, allocate until memory is exhausted, or recurse until the stack overflows. Verification constrains what the code can do to the machine’s internal state, not what it can do to the machine’s resources.

That distinction matters when the runtime hosts untrusted code. Resource limits are enforced separately: instruction budgets, allocation quotas, and stack depth limits. The JVM’s verifier also does not check that a method’s code is semantically related to its name, so a method called hashCode can return a constant. Verification is a memory-safety and type-safety property, not a correctness property.

The interaction with the class loader is the other limit. Verification resolves class references, and resolution can load classes, which can run code, which can throw. The JVM specification constrains when a VerifyError must surface relative to the loading of referenced classes, because a verifier that eagerly resolves can trigger loading of classes the program never uses. Implementations that verify lazily, at first execution of a method, avoid loading unused classes but expose a VerifyError later than the program might expect. Lazy verification also defers the failure: a class can be loaded, and its other methods executed, before the one method that would fail verification is ever called, so a VerifyError surfaces at the call site rather than at load. To keep that safe, the check has to complete before any instruction of the offending method executes.

What the metadata costs and what it buys

Stack map tables add bytes to every class file, and for a method with many branches the table can rival the code in size. The compression mitigates this, but a method with hundreds of distinct branch targets and varying local states still carries a full frame per target. That is the price of moving the analysis.

What it buys is predictable load time and a simpler verifier, which matters for a runtime that loads classes on demand during execution. It also buys a stable interface for bytecode transformers: a tool that inserts instructions knows exactly what it must recompute. And it lets the interpreter omit checks: a verified iadd can assume its operands are integers, and a verified invokevirtual can assume the receiver is a reference of a type that has the method.

The specialization that builds on that assumption, rewriting verified instructions into faster forms once they have been executed, is covered under superinstructions and opcode quickening.