Optional checker: implicit `@MaybePresent` annotations are inserted in `.ajava` files

[jyoo980]

Summary

An execution of WPI on a Java project with the Optional Checker will yield a set of .ajava files where the implicit @MaybePresent annotation is inserted for most (if not all) method arguments and return types, e.g.,

@org.checkerframework.dataflow.qual.Impure
public @org.checkerframework.checker.optional.qual.MaybePresent ResolvedReferenceTypeDeclaration toTypeDeclaration(@org.checkerframework.checker.optional.qual.MaybePresent JavaSymbolSolver this, @org.checkerframework.checker.optional.qual.MaybePresent Node node)

A research discussion with @mernst and @rjust showed that this was not an error; since .ajava files are not meant to be human-read.

That said, I am opening this issue to at least document the possibility that @MaybePresent annotations will no longer be inserted into the .ajava files. The manual suggests that the

[MaybePresent] type is a default value, so programmers do not have to write it

See this manual section for details.

[kelloggm]

@jyoo980 This is expected (though not really desirable) WPI behavior: effectively, WPI writes all "true" annotations, even those that are equivalent to the default.

WPI makes an effort to avoid doing this when it can: see

checker-framework/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java

Line 1081 in 05863eb

// Do not print invisible qualifiers, to avoid cluttering the output.

. This code only works for qualifiers that are marked as @InvisibleQualifer, so it's only useful for qualifiers that the type system designer genuinely intended to never be written. It would be great if WPI could do a better job of filtering "default" qualifiers than this.

[mernst]

A good first step would be for .ajava files not to contain annotations that do not satisfy the @RelevantJavaTypes meta-annotation.

[mernst]

#6254 will not solve the problem of inserting implicit annotations, but it makes a big step by not inserting irrelevant annotations.