[Soot-list] Problems with nested try..catch..finally?

[Etienne M. Gagnon]

In case anyone is insterested, here's a link to Jamal's thesis (in French):
http://www.archipel.uqam.ca/1809/1/M10697.pdf

Etienne

Etienne M. Gagnon a écrit :
> Hi there,
>
> As far as I remember, Soot did inline the code of JSRs to get rid of 
> jsr/ret instructions. One problem is that inlining could be trickier 
> than one would intuitively think, as you can get out of a "subroutine" 
> without going through a RET instruction. So, I wouldn't be surprised 
> if there were some corner cases that are improperly handled in Soot. 
> The name "JSR" was a poor choice for this instruction, as the 
> instruction does a "branch and store address on the stack" operation, 
> nothing more; it does not always invoke a "subroutine". (Another 
> problem, which is not real in practice, is that, in the worst case, 
> inlining can exponentially expand the size of the code).
>
> Jamal Lazaar has developed a theoretical framework that allows the 
> analysis of bytecode instructions in presence of JSR/RET instructions, 
> in polynonimal time. He actually shows (and proves) how to verify Java 
> bytecode. Separately, he uses the computed results (about 
> "subroutimes" and JSR/RET relations) to also statically verify that 
> each MONITORENTER is properly closed with MONITOREXIT instructions.
>
> I think that the first steps of his algorithm could help in finding 
> the appropriate code to duplicate when inlining JSR instructions.
>
> Example (valid bytecode):
>
> static int foo(int) {
>
> Label_1:
>  ILOAD_0
>  ICONST_0
>  IF_ICMPEQ Label_3
>  JSR Label_2
> Label_2:
>  ASTORE_1
>  GOTO Label_1
> Label3:
>  ICONST_1
>  IRETURN
>
> }
>
> Yep, I know: this doesn't look like it was generated from Java code. 
> Yet, it does match all the rules of Java verification. Have fun 
> inlining the JSR. :)
>
> Etienne
>

-- 
Etienne M. Gagnon, Ph.D.
SableCC:                                            http://sablecc.org