Java bytecode verification analyses the types of instructions by symbolic execution, maintaining a stack of types instead of a stack of values. You should implement such a type analysis for Jasmin. Read Xavier Leroy’s paper “Java bytecode verification: algorithms and formalisations” as a starting point.

Submitted by Guido Wachsmuth on 14 February 2014 at 13:18

Ok, so first we will define some static properties about instructions, things like what is popped from the stack, what is pushed onto it, what instruction is next, what locals variables are used etc..
The next step would be desugaring all instructions to have unique names, then eliminate label instructions. Now all calculated stack information can be manually added to the index from stratego after name/type analysis, where we use the static properties.

Options:

1. A plain type-level interpreter would run into the halting problem. (so not really an option)
2. A fixed-point linear-pass type-level interpreter can fail early on different stack-sizes or bad Least Upper Bounds and therefore halt. It can also probably give a fairly coherent reason for failing. However taskifying is likely difficult.
3. Fairly close to the above option is constraint-collection and solving those constraints. The elegant part is only walking through the code once. And once the constraint-solving works, changing from pure Stratego to tasks will map more easily this way. But you probably lose some of the info of where constraints came from and what exactly causes the constraints to fail.

The idea is to go for option #3. I quickly wrote some code to put a few things more concretely. See my last commit on the typeAnalysis branch (76663b8).