[Soot-list] java.lang.VerifyError and byte code execution trace

[John Jorgensen]

My knowledge of this topic is stale, but ten years ago when I modified
Soot's exceptional control flow analysis, I ran into circumstances where
improving the precision of exception analysis could lead Soot to generate
unverifiable code by basing its optimizations on more precise analyses than
those available to the bytecode verifier.

In that case, the unverifiable code resulted because the bytecode verifier
assumed that every instruction within the scope of an exception handler
might have that handler as its successor, even if the instruction could not
possibly throw an exception that the handler would catch.  That meant that
if Soot made optimizations based on knowing that some instructions could
not throw particular exceptions, it was possible that the verifier could
judge the resulting code unsafe, because it would think the code might lead
the exception handler to be executed with the VM in an improper state (for
example that some instruction in the handler might be executed when
"Register 3 contains wrong type").  See sections 2.6 and 3.4 of the Sable
Technical Report
2003-3<http://www.sable.mcgill.ca/publications/techreports/sable-tr-2003-3.pdf>for
more detail.

So in your example, it is conceivable that the verifier is not smart enough
to determine that astore_3 is always executed before aload_3, even though
you can see that it is.  Or maybe there is dead code that wants to read a
different type from register 3, but the verifier can't tell it is dead.

But as I said before, my knowledge of this subject is outdated (as I just
confirmed by  glancing at the current JVM spec's description of
verification: I don't remember it including any Prolog in the old days).




On Thu, Sep 12, 2013 at 11:29 PM, John Jorgensen
<jorgensen.john at gmail.com>wrote:

> My knowledge of this topic is stale, but ten years ago when I modified
> Soot's exceptional control flow analysis, I ran into circumstances where
> improving the precision of exception analysis could lead Soot to generate
> unverifiable code by basing its optimizations on more precise analyses than
> those available to the bytecode verifier.
>
> In that case, the unverifiable code resulted because the bytecode verifier
> assumed that every instruction within the scope of an exception handler
> might have that handler as its successor, even if the instruction could not
> possibly throw an exception that the handler would catch.  That meant that
> if Soot made optimizations based on knowing that some instructions could
> not throw particular exceptions, it was possible that the verifier could
> judge the resulting code unsafe, because it would think the code might lead
> the exception handler to be executed with the VM in an improper state (for
> example that some instruction in the handler might be executed when
> "Register 3 contains wrong type").  See sections 2.6 and 3.4 of the Sable
> Technical Report 2003-3<http://www.sable.mcgill.ca/publications/techreports/sable-tr-2003-3.pdf>for more detail.
>
> So in your example, it is conceivable that the verifier is not smart
> enough to determine that astore_3 is always executed before aload_3, even
> though you can see that it is.  Or maybe there is dead code that wants to
> read a different type from register 3, but the verifier can't tell it is
> dead.
>
> But as I said before, my knowledge of this subject is outdated (as I just
> confirmed by  glancing at the current JVM spec's description of
> verification: I don't remember it including any Prolog in the old days).
>
>
>
> On Thu, Sep 12, 2013 at 7:27 PM, Yongzhi Wang <wang.yongzhi2009 at gmail.com>wrote:
>
>> Dear All,
>>
>> I am stucked by the byte code that I generate with soot. I am using soot
>> to transform the control flow of java class. The transformed program should
>> behave same as the original program. However, my generated class file
>> cannot be executed  without the "-noverify" option.
>>
>> If I run the class file in java without "-noverify" option, I got the
>> following error message:
>> java.lang.VerifyError: (class: Test, method: main signature:
>> ([Ljava/lang/String;)V) Register 3 contains wrong type
>>
>> If I run the class file in java with "-noverify" option, some test
>> program will run correctly. But some test programs will be pending. I
>> suspect the program is in a dead loop given my transformed control flow.
>>
>> My question is:
>>
>> 1. What is the usual reason of "Register contains wrong type" error? I
>> can observe that my transformed class file has instruction aload_3 appears
>> before astore_3, even though I use goto instruction to control the control
>> flow to make sure astore_3 is executed before aloud_3. Is that the reason?
>> If so, what's the trick to fix this problem?
>>
>> 2. I suspect the test program is in a dead loop. How can I trace the
>> bytecode instruction execution sequence from JVM? Is there any tool or JVM
>> option I can use?
>>
>> Thanks!
>> Best regards,
>> Yongzhi
>>
>> _______________________________________________
>> Soot-list mailing list
>> Soot-list at sable.mcgill.ca
>> http://mailman.cs.mcgill.ca/mailman/listinfo/soot-list
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.mcgill.ca/pipermail/soot-list/attachments/20130912/b9f79408/attachment.html