Framework ignores annotations on outer types

[jwaataja]

If a class Outer contains an inner class Inner, then each instance of Inner has an instance of Outer separate from itself. This is often ignored, consider this class:

import org.checkerframework.checker.tainting.qual.*;

public class Outer {
    void outerMethod(@Untainted Outer this) {
    }

    class Inner {
        void innerMethod(@Untainted Outer. @Untainted Inner this) {
            Outer.this.outerMethod();
        }
    }
}

This seems like it should type check because everything is @Untainted. However, I get this error

Outer.java:9: error: [method.invocation.invalid] call to outerMethod() not allowed on the given receiver.
            Outer.this.outerMethod();
                                  ^
  found   : @Tainted Outer
  required: @Untainted Outer

Currently, there's no way to specify that the type of Outer.this is @Untainted rather than @Tainted. The checker is overly conservative in this case.

I propose that, for a type @A Outer. @B Inner, where @A and @B are annotations, that the type of Outer.this is @A and the type of Inner.this is @B. If implemented, this would mean the following:

• Member accesses are checked against the correct enclosing class type. For example, in the above code, the framework would recognize that in innerMethod where the receiver has type @Untainted Outer. @Untainted Inner, that the type of Outer.this is @Untainted Outer, and the class should type check.
• Outer types must be checked during inner class creation. In a method void myMethod(@Tainted Outer this), the line @Untainted Outer. @Untainted Inner o = new @Untainted Inner(). The reason is that the Outer instance for o is the receiver of the method it was created in, which has type @Tainted Outer, meaning the assignment would be invalid.
• New subtyping rules. For an inner class C_1 . C_2. ... . C_n, where each of C_1 through C_{n - 1} is an enclosing class of C_n, then the type @A1 C_1. @A_2 C_2. ... @A_n C_n is a subtype of @B_1 C_1. @B_2 C_2. ... . @B_n C_n if and only if @A_1 is a subtype of @B_1, @A_2 is a subtype of @B_2, ..., @A_n is a subtype of @B_n.

[smillst]

(I think this is a duplicate of #352, but keep this one open as it has more details.)