Re: Verify classfile

[Ondrej LHOTAK <olhotak@sable.mcgill.ca>]

I think it should be quite easy to implement some verification phases in
Soot, since they are exactly the kinds of analyses that Soot was
designed for. I also think it would be nice to include them in Soot if
someone were to implement and contribute them.

Jimple prevents stack height mismatches, except when there are
assignment statements with mismatched types, or when there are bugs in
Baf. In the past two months, I had to debug two stack height mismatches
for these two reasons, and they are really tough to debug. So, a phase
that checks for assignment statements with mismatched types would be
really helpful (the Baf bugs are already fixed). Another two phases that
would be helpful would be one to check for uninitialized variables, and
another to check that <init> methods are called on all allocated
objects. Both should be quite doable with Soot's flow analysis
framework.

Ondrej

On Mon, May 19, 2003 at 10:24:24PM -0400, Amit Manjhi wrote:
> 
> Thanks for the help. Even though not thinking about the stack simplifies many 
> transformations, I agree with James that it is possible to generate 
> non-verifying bytecode using SOOT. For example, one pathological example would 
> be having the following code fragment
> 
> tmp1 = new Java.Util.Vector;
> virtualinvoke tmp1.<java.util.Vector: void addElement(java.lang.Object)>($foo);
> 
> in which case the verifier would complain - trying to using a vector instance 
> without initializing it.
> 
> -amit
> 
> > Patrick LAM wrote:
> > > Soot doesn't really provide any tools to check that the output of your
> > > transformation's going to have any desirable properties.  At least,
> > > being 3-address code, you can't generate stack height imbalances and
> > > non-verifying bytecode, if that's any consolation at all.
> > 
> > Not sure this is true - I've generated non-verifying bytecode using SOOT.
> > 
> > - James
> > 
> 
>