Feature request: @AlwaysUnique (?) to mark classes whose instances must always be @Unique

[PawelLipski]

Checker: Aliasing Checker

Annotation name: @AlwaysUnique or @OnlyUnique or @Require{d,s,}Unique

Annotation target: class and interface declarations

Proposed behavior:

All instances of the class/interface X marked (possibly via stubs) as @AlwaysUnique must be @Unique (i.e. no instance of @MaybeAliased X type is ever allowed in the checked code).

Use cases:

Certain mutable objects are inherently unsafe when leaked. A good example might be JGit's org.eclipse.jgit.revwalk.RevCommit (as of v5.7.0), which has a mutable internal state. When the instance is leaked, the original holder of the reference may experience an unexpected behavior unless it calls RevCommit#reset.

[wmdietl]

Thanks for the suggestion!
This feature effectively should already exist, by declaring @Unique as upper bound for the type: https://checkerframework.org/manual/#upper-bound-for-use

However, I think the Aliasing Checker needs a few improvements to correctly work with this feature.
The following example:

import org.checkerframework.common.aliasing.qual.Unique;
import org.checkerframework.framework.qual.DefaultQualifierForUse;

@Unique
class Data {
    @SuppressWarnings("unique.leaked")
    Data() {}    
}

class Demo {
    void foo(Data p) {
        Data y = p;
        y.toString();
    }
}

Doesn't raise an error when the parameter is not annotated, but does when we add a @Unique explicitly.

The unique.leaked error on the constructor return is also not helpful.

Also, by default the CF allows top annotations for local variables, which is not useful for this type system.

So instead of adding a new annotation, we should look into making the upper bound feature work correctly for the Aliasing Checker.

[PawelLipski]

Yeah, most likely lifting this limitation of DefaultQualifier would be useful:

This annotation currently has no effect in stub files.

coz then with DefaultQualifier we could override CLIMB-to-top default for local variables that can't be overridden when simply annotating the class as @Unique in the stub.

[PawelLipski]

Actually! even more prominent candidate for being marked as always @Unique is Java 8+ Stream due to https://www.baeldung.com/java-stream-operated-upon-or-closed-exception