jvmlanguage-lawyerjvm-bytecode

Does the JVM operand stack have to be deterministic?

For clarification, this is a question regarding the specification of the bytecode verifier, especially when dealing with bytecode that isn't generated by javac.

Can the operand stack be modified in a non-deterministic way? In other words, is it possible to have conditional code transition the stack in a different state (size, types at the top of the stack, ...) depending on information that will only be known at runtime?

Examples of possibly non-validating methods (pseudo-code)

float f(boolean b) {
  if (b) {
    push 1.0 // float
  } else {
    push 2L // long
  }
  dup // generic instructions that work for both floats and longs
  pop
  if (b) {
    return // return the float
  } else {
    l2f // convert the long to float and return it
    return
  }
}

// Pushes a variable amount of ints on the stack, and pop them all after
void f(int n) {
  assert(n > 1)

  push 0
  push 1
  for (i from 0 to n) {
    dup
  }

  do {
    istore val // pop the int (1 or 0) and store it in the "val" local
  } while (val != 0); // stop once we've popped the original 0 at the base
}

Regarding the second example, I know that the operand stack is bounded, so having an arbitrarily large stack is already problematic in itself.

While both of these methods are semantically correct, I don't think it is really possible to check their correctness in constant time on non-trivial cases. I smell a bit of halting problem / Rice's theorem.

It could also have been possible for a Java runtime to fall back to an interpreter when it cannot prove the correctness of bytecode, but as far as I know, in Java, bytecode is always checked proactively (during link time).

Solution

  • In short, the operand stack has to be deterministic.

    There are two places in the specification addressing most of your question:

    §2.6.2. Operand Stacks:

    Values from the operand stack must be operated upon in ways appropriate to their types. It is not possible, for example, to push two int values and subsequently treat them as a long or to push two float values and subsequently add them with an iadd instruction. A small number of Java Virtual Machine instructions (the dup instructions (§dup) and swap (§swap)) operate on run-time data areas as raw values without regard to their specific types; these instructions are defined in such a way that they cannot be used to modify or break up individual values. These restrictions on operand stack manipulation are enforced through class file verification (§4.10).

    At any point in time, an operand stack has an associated depth, where a value of type long or double contributes two units to the depth and a value of any other type contributes one unit.

    Note the sentence “These restrictions on operand stack manipulation are enforced through class file verification” telling you that verification is mandatory.

    Further,

    §4.9.2. Structural Constraints:

    …

    • If an instruction can be executed along several different execution paths, the operand stack must have the same depth (§2.6.2) prior to the execution of the instruction, regardless of the path taken.

    So, there’s no way to push or pop a dynamic number of elements.

    Note that since Java 6, branch merge points must have a stack map frame describing the local variables and operand stack entries at this point and all code paths are verified against this description. This static description also rules out dynamic stack values on a technical level.

    Note further, that a type description in such a frame can express, int, long, float, double, and reference types, as well as “top”, the root of the verification type system, which denotes an unusable entry, but not “type 1” nor “type 2”.

    So, when the specification says that “dup can handle a value of a category 1 computational type”, it’s a short-hand for saying that it can equally handle int, float, and reference types, but it’s always either of them at a specific code location. There is no scenario where it could encounter an unspecific “type 1”.

    While it’s possible to have two branches, one pushing a float and the other pushing an int, merging both to an entry of the “top” type, it’s not possible to use it in any way, not even to use pop to drop the value, as the value’s type “top” is neither “type 1” nor “type 2”.

    The only thing, the subsequent code could do, is to ignore this value until exiting the method via return or throw.

    Before Java 6, there were no stack maps and branches had to be merged by the verifier, according to the following rules:

    To merge two operand stacks, the number of values on each stack must be identical. Then, corresponding values on the two stacks are compared and the value on the merged stack is computed, as follows:

    • If one value is a primitive type, then the corresponding value must be the same primitive type. The merged value is the primitive type.
    • If one value is a non-array reference type, then the corresponding value must be a reference type (array or non-array). The merged value is a reference to an instance of the first common supertype of the two reference types. …
    • If corresponding values are both array reference types, then their dimensions are examined. If the array types have the same dimensions, then the merged value is a reference to an instance of an array type which is first common supertype of both array types. …

    If the operand stacks cannot be merged, verification of the method fails.

    Note that there is no rule for merging different primitive types or merging a primitive type and a reference type, not even to something like “top”, as with newer class files.

    In other words, in older class files, two code paths like described above can’t merge at all.