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

On 14 February 2014 at 13:18 Guido Wachsmuth removed tag @guidowachsmuth

On 14 February 2014 at 13:18 Guido Wachsmuth tagged mdsd14

On 21 February 2014 at 09:47 Richard van Heest tagged @richardvanheest

On 30 April 2014 at 14:47 Jeff Smits tagged 0.2

On 8 May 2014 at 16:21 Jeff Smits tagged @jeffsmits

On 8 May 2014 at 16:21 Jeff Smits tagged @reinierhartog

On 8 May 2014 at 16:26 Jeff Smits commented:

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.

On 15 May 2014 at 19:32 Jeff Smits commented:


  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).

Log in to post comments