Week 1 progress report

[Aditya Singh]

Hi everyone!

This is my week report from 21st May 2020 to 28th May 2020.

This week, I worked on a feature request #3313 (https://github.com/typetools/checker-framework/issues/3313) as my first task, in order to introduce me to the Checker Framework and the formal procedure for code submission. Concerning with the aliasing checker, the request proposed the idea of a new checker @AlwaysUnique. An object or a class X annotated with @AlwaysUnique could never be leaked/aliased. However, such an objective can be incorporated by the existing framework by declaring @Unique as an upper bound.

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

@Unique class Test{

            @SuppressWarnings("unique.leaked") // Inconvenient @SuppressWarnings

            Test(){}

            void check(Test x){

                        Test y = x;   // Expected error

            }

}

This code should ideally give an error on Test y = x; since, a unique object x is leaked. However, this doesn't give an error at all. The "unique.leaked" error on the constructor return is also not helpful.

After setting up my system to test, modify and debug the checker framework, I started looking for possible solutions.

The reason for the error in the constructor class is because the Aliasing checker checks whether the parent of a @Unique class is also @Unique. Otherwise, data can be leaked in the unique class' super() method. This is useful for classes inheriting from other classes but not so much for parent classes. If a class is a top parent class (inherits from no other classes), then, by default, it is a subclass of the java Object class, which is @MaybeAliased according to the Aliasing checker. The solution is to either bypass this condition by treating it as an exception in the source code or by using an .astub file to annotate Object class constructor as @Unique.

For the latter problem, this is caused due to the fact that the Aliasing checker checks for explicit @Unique annotations when dealing with local variables. Hence, even if the local variables are unique, they don't report the error until explicitly stated so. Removing this restriction (using hasAnnotation() instead of hasExplicitAnnotation() in the AliasingVisitor.java file) fixes the problem and gives the proper expected result.

Regards,

Aditya Singh