Cast annotation is not properly generated in the class file

[GoogleCodeExporter]

from whq1238000@gmail.com:

 have found a possible bug in the checker-framework. After compiling with its javac I found the cast (target type 0x47) annotation contains offset which has value 0. It turns out the cast annotation is not properly generated in the class file. 
     Annotation : 0x47000000 (b1 b2 b3 b4). where b1 is 0x47 and b2<<<8 + b3 is the offset. 

The checker I am using is 1.8.10 version and I have attached the source and 
compiled byte code. To be more specific, the problem is when we attach an cast 
annotation to a range of byte code, the offset doesn't  point to the last byte 
code within range. Instead the checker attach the cast annotation to the 
nearest byte code.
    In the example I attached, the getSource() method should put a cast at offset 3 in principle while the checker put it at offset 2. 
   This type of bugs happen in places where we evaluate a non-static method call or get field instructions.For example, in (@Untainted int) x. f and (@Untainted int) x.get(), the cast is by mistake attached to x as opposed to the actual evaluated value of type int.

Original issue reported on code.google.com by mcart...@cs.washington.edu on 12 Mar 2015 at 9:30

Attachments:

• MyTest.java
• MyTest.out

[GoogleCodeExporter]

Original comment by mcart...@cs.washington.edu on 12 Mar 2015 at 9:31

• Changed state: New

[GoogleCodeExporter]

Original comment by mcart...@cs.washington.edu on 12 Mar 2015 at 9:31

[GoogleCodeExporter]

Is this really specific to the Checker Framework?
From the description this sounds like:
https://bugs.openjdk.java.net/browse/JDK-8033803

Original comment by wdi...@gmail.com on 12 Mar 2015 at 9:38

[GoogleCodeExporter]

Hi Werner, Haoqing from UCLA (working for Jens Palsberg) reported this to us. I 
was wonder if we could figure out a workaround for them so they can continue 
with their work.

"But for our purpose of doing dynamic analysis combined with annotation, the 
bug inhibits us from enabling dynamic cast check which will complement your 
static checker."

I am trying to determine if there is an issue with the spec.

From the spec
"The value of the offset item specifies the code array offset of either the 
bytecode instruction corresponding to the cast expression ..."

They intentionally didn't mention the checkcast bytecode (since it is not 
always generated). His code does not insert a checkcast bytecode because the 
types are the same.

Currently, the offset points to the first instruction in the cast, which seems 
to correspond to the spec (offset 2 below):

class MyTest{       
        public int d;

        public @Untainted int getSource(int input, @Tainted MyTest a){          
                int re =   input;
                int p = (@Untainted int) a.d;
                return p;
        }

 public int getSource(int, MyTest);
    Code:
       0: iload_1       
       1: istore_3      
       2: aload_2       // cast offset here ?  
       3: getfield      #10                 // Field d:I
       6: istore        4
       8: iload         4
      10: ireturn       

However, is there any way to differentiate that from:

        public @Untainted int getSource(int input, @Tainted MyTest a){          
                int re =   input;
                int p = ((@Untainted Mytest) a).d;
                return p;
        }

    Code:
      stack=1, locals=5, args_size=3
         0: iload_1
         1: istore_3
         2: aload_2
         3: getfield      #2                  // Field d:Ljava/lang/Object;
         6: astore        4
         8: return

Which will also point to an offset of 2.

Original comment by mcart...@cs.washington.edu on 17 Mar 2015 at 9:27