Static Stack Depth Property

Claim: if we apply translation above then the stack size at each point in the bytecode can be computed during compilation.

  • we can check for stack underflow and overflow

Why does it hold?

  • for each assignment statement
  • for if, while

Can JVM rely on this property?

  • what if bytecode is not compiled from java / tool ?
  • bytecode verifier checks the stack usage (including stack depth and initialization)

Consider depth computation for Compiled Factorial Example

How does this property relate to Translation Correctness for Expressions?

  • the property implies that compilation of expression only adds one value to the stack in the end
  • assignment will consume this value, so each assignment leaves stack unchanged!