@@ -2798,14 +2798,13 @@ class TranslatedJvmInvoke extends TranslatedJvmInstruction, TTranslatedJvmInvoke
27982798 or
27992799 // Rest of the stack has the arguments removed
28002800 i > 0 and
2801- result = getTranslatedJvmInstruction ( instr .getABackwardPredecessor ( ) )
2802- . getStackElement ( i - 1 + instr .getNumberOfArguments ( ) )
2801+ instr .hasReturnValue ( ) and
2802+ result = this . getInputStackVariable ( i - 1 + instr .getNumberOfArguments ( ) )
28032803 or
2804- // If no return value, shift the indices
2804+ // If no return value, shift the indices (only arguments removed)
28052805 i >= 0 and
28062806 not instr .hasReturnValue ( ) and
2807- result = getTranslatedJvmInstruction ( instr .getABackwardPredecessor ( ) )
2808- .getStackElement ( i + instr .getNumberOfArguments ( ) )
2807+ result = this .getInputStackVariable ( i + instr .getNumberOfArguments ( ) )
28092808 }
28102809}
28112810
@@ -2888,11 +2887,13 @@ class TranslatedJvmLoadLocal extends TranslatedJvmInstruction, TTranslatedJvmLoa
28882887 override Variable getResultVariable ( ) { result = this .getTempVariable ( JvmLoadLocalResultVarTag ( ) ) }
28892888
28902889 final override Variable getStackElement ( int i ) {
2890+ // Load pushes a value onto the stack
28912891 i = 0 and
28922892 result = this .getInstruction ( JvmLoadLocalTag ( ) ) .getResultVariable ( )
28932893 or
2894+ // Rest of stack is unchanged (shifted by 1)
28942895 i > 0 and
2895- result = getTranslatedJvmInstruction ( instr . getABackwardPredecessor ( ) ) . getStackElement ( i - 1 )
2896+ result = this . getInputStackVariable ( i - 1 )
28962897 }
28972898
28982899 override predicate hasLocalVariable ( LocalVariableTag tag ) {
@@ -2937,7 +2938,8 @@ class TranslatedJvmStoreLocal extends TranslatedJvmInstruction, TTranslatedJvmSt
29372938 override Variable getResultVariable ( ) { none ( ) }
29382939
29392940 final override Variable getStackElement ( int i ) {
2940- result = getTranslatedJvmInstruction ( instr .getABackwardPredecessor ( ) ) .getStackElement ( i + 1 )
2941+ // Store pops the top value, so stack shifts down by 1
2942+ result = this .getInputStackVariable ( i + 1 )
29412943 }
29422944
29432945 override predicate hasLocalVariable ( LocalVariableTag tag ) {
@@ -2978,7 +2980,8 @@ class TranslatedJvmNop extends TranslatedJvmInstruction, TTranslatedJvmNop {
29782980 override Variable getResultVariable ( ) { none ( ) }
29792981
29802982 final override Variable getStackElement ( int i ) {
2981- result = getTranslatedJvmInstruction ( instr .getABackwardPredecessor ( ) ) .getStackElement ( i )
2983+ // Nop doesn't change the stack
2984+ result = this .getInputStackVariable ( i )
29822985 }
29832986}
29842987
@@ -3037,11 +3040,11 @@ class TranslatedJvmBranch extends TranslatedJvmInstruction, TTranslatedJvmBranch
30373040 final override Variable getStackElement ( int i ) {
30383041 // After a unary branch, one element is consumed
30393042 instr instanceof Raw:: JvmUnaryConditionalBranch and
3040- result = getTranslatedJvmInstruction ( instr . getABackwardPredecessor ( ) ) . getStackElement ( i + 1 )
3043+ result = this . getInputStackVariable ( i + 1 )
30413044 or
30423045 // After a binary branch, two elements are consumed
30433046 instr instanceof Raw:: JvmBinaryConditionalBranch and
3044- result = getTranslatedJvmInstruction ( instr . getABackwardPredecessor ( ) ) . getStackElement ( i + 2 )
3047+ result = this . getInputStackVariable ( i + 2 )
30453048 }
30463049}
30473050
@@ -3078,7 +3081,8 @@ class TranslatedJvmGoto extends TranslatedJvmInstruction, TTranslatedJvmGoto {
30783081 override Variable getResultVariable ( ) { none ( ) }
30793082
30803083 final override Variable getStackElement ( int i ) {
3081- result = getTranslatedJvmInstruction ( instr .getABackwardPredecessor ( ) ) .getStackElement ( i )
3084+ // Goto doesn't change the stack
3085+ result = this .getInputStackVariable ( i )
30823086 }
30833087}
30843088
@@ -3139,8 +3143,9 @@ class TranslatedJvmArithmetic extends TranslatedJvmInstruction, TTranslatedJvmAr
31393143 i = 0 and
31403144 result = this .getInstruction ( JvmArithOpTag ( ) ) .getResultVariable ( )
31413145 or
3146+ // Rest of the stack shifts down by 1 (2 consumed, 1 produced)
31423147 i > 0 and
3143- result = getTranslatedJvmInstruction ( instr . getABackwardPredecessor ( ) ) . getStackElement ( i + 1 )
3148+ result = this . getInputStackVariable ( i + 1 )
31443149 }
31453150}
31463151
@@ -3249,31 +3254,32 @@ class TranslatedJvmFieldAccess extends TranslatedJvmInstruction, TTranslatedJvmF
32493254 }
32503255
32513256 final override Variable getStackElement ( int i ) {
3252- // For getfield: consumes object ref, pushes field value
3257+ // For getfield: consumes object ref, pushes field value (net: no change in stack depth)
32533258 instr instanceof Raw:: JvmGetfield and
32543259 (
32553260 i = 0 and result = this .getInstruction ( JvmFieldLoadTag ( ) ) .getResultVariable ( )
32563261 or
3262+ // Stack unchanged below the result (1 consumed, 1 produced)
32573263 i > 0 and
3258- result = getTranslatedJvmInstruction ( instr . getABackwardPredecessor ( ) ) . getStackElement ( i )
3264+ result = this . getInputStackVariable ( i )
32593265 )
32603266 or
3261- // For getstatic: pushes field value (no object ref consumed)
3267+ // For getstatic: pushes field value (no object ref consumed, stack grows by 1 )
32623268 instr instanceof Raw:: JvmGetstatic and
32633269 (
32643270 i = 0 and result = this .getInstruction ( JvmFieldLoadTag ( ) ) .getResultVariable ( )
32653271 or
32663272 i > 0 and
3267- result = getTranslatedJvmInstruction ( instr . getABackwardPredecessor ( ) ) . getStackElement ( i - 1 )
3273+ result = this . getInputStackVariable ( i - 1 )
32683274 )
32693275 or
3270- // For putfield: consumes object ref and value
3276+ // For putfield: consumes object ref and value (stack shrinks by 2)
32713277 instr instanceof Raw:: JvmPutfield and
3272- result = getTranslatedJvmInstruction ( instr . getABackwardPredecessor ( ) ) . getStackElement ( i + 2 )
3278+ result = this . getInputStackVariable ( i + 2 )
32733279 or
3274- // For putstatic: consumes value only
3280+ // For putstatic: consumes value only (stack shrinks by 1)
32753281 instr instanceof Raw:: JvmPutstatic and
3276- result = getTranslatedJvmInstruction ( instr . getABackwardPredecessor ( ) ) . getStackElement ( i + 1 )
3282+ result = this . getInputStackVariable ( i + 1 )
32773283 }
32783284}
32793285
@@ -3316,8 +3322,9 @@ class TranslatedJvmNew extends TranslatedJvmInstruction, TTranslatedJvmNew {
33163322 i = 0 and
33173323 result = this .getInstruction ( JvmNewInitTag ( ) ) .getResultVariable ( )
33183324 or
3325+ // Rest of the stack is unchanged (shifted by 1)
33193326 i > 0 and
3320- result = getTranslatedJvmInstruction ( instr . getABackwardPredecessor ( ) ) . getStackElement ( i - 1 )
3327+ result = this . getInputStackVariable ( i - 1 )
33213328 }
33223329}
33233330
@@ -3366,10 +3373,11 @@ class TranslatedJvmDup extends TranslatedJvmInstruction, TTranslatedJvmDup {
33663373 or
33673374 // The original element is still there at position 1
33683375 i = 1 and
3369- result = getTranslatedJvmInstruction ( instr . getABackwardPredecessor ( ) ) . getStackElement ( 0 )
3376+ result = this . getInputStackVariable ( 0 )
33703377 or
3378+ // Rest of the stack is shifted by 1
33713379 i > 1 and
3372- result = getTranslatedJvmInstruction ( instr . getABackwardPredecessor ( ) ) . getStackElement ( i - 1 )
3380+ result = this . getInputStackVariable ( i - 1 )
33733381 }
33743382}
33753383
@@ -3408,10 +3416,10 @@ class TranslatedJvmPop extends TranslatedJvmInstruction, TTranslatedJvmPop {
34083416 final override Variable getStackElement ( int i ) {
34093417 // pop removes the top element (pop removes 1, pop2 removes 2)
34103418 instr instanceof Raw:: JvmPop and
3411- result = getTranslatedJvmInstruction ( instr . getABackwardPredecessor ( ) ) . getStackElement ( i + 1 )
3419+ result = this . getInputStackVariable ( i + 1 )
34123420 or
34133421 instr instanceof Raw:: JvmPop2 and
3414- result = getTranslatedJvmInstruction ( instr . getABackwardPredecessor ( ) ) . getStackElement ( i + 2 )
3422+ result = this . getInputStackVariable ( i + 2 )
34153423 }
34163424}
34173425
@@ -3454,7 +3462,8 @@ class TranslatedJvmLoadConstant extends TranslatedJvmInstruction, TTranslatedJvm
34543462 i = 0 and
34553463 result = this .getInstruction ( JvmConstTag ( ) ) .getResultVariable ( )
34563464 or
3465+ // Rest of the stack is unchanged (shifted by 1)
34573466 i > 0 and
3458- result = getTranslatedJvmInstruction ( instr . getABackwardPredecessor ( ) ) . getStackElement ( i - 1 )
3467+ result = this . getInputStackVariable ( i - 1 )
34593468 }
34603469}
0 commit comments