diff --git a/checker/build.gradle b/checker/build.gradle index c30cd45fd9a2..61c24532cb23 100644 --- a/checker/build.gradle +++ b/checker/build.gradle @@ -1065,4 +1065,3 @@ publishing { signing { sign(publishing.publications.checker) } - diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java index d316d3aad509..bc0cbda0d994 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java @@ -50,6 +50,7 @@ import org.checkerframework.dataflow.cfg.node.Node; import org.checkerframework.dataflow.util.NodeUtils; import org.checkerframework.framework.flow.CFAbstractAnalysis; +import org.checkerframework.framework.qual.TypeUseLocation; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeFormatter; import org.checkerframework.framework.type.AnnotatedTypeMirror; @@ -953,6 +954,8 @@ public boolean isImmutable(TypeMirror type) { @Override public void wpiAdjustForUpdateField( Tree lhsTree, Element element, String fieldName, AnnotatedTypeMirror rhsATM) { + // Adjust initialization annotations first + wpiAdjustInitializationAnnotations(rhsATM, TypeUseLocation.FIELD); // Synthetic variable names contain "#". Ignore them. if (!rhsATM.hasPrimaryAnnotation(Nullable.class) || fieldName.contains("#")) { return; @@ -971,11 +974,42 @@ public void wpiAdjustForUpdateField( // then change rhs to @Nullable @Override public void wpiAdjustForUpdateNonField(AnnotatedTypeMirror rhsATM) { + // Adjust initialization annotations first + wpiAdjustInitializationAnnotations(rhsATM, TypeUseLocation.OTHERWISE); if (rhsATM.hasPrimaryAnnotation(MonotonicNonNull.class)) { rhsATM.replaceAnnotation(NULLABLE); } } + /** + * Changes the type of {@code rhsATM} when assigned to any pseudo-assignment, for use by + * whole-program inference. + * + *

If {@code rhsATM} is Nullable or MonotonicNonNull and has the UnknownInitialization + * annotation, replace it with {@code UnknownInitialization(java.lang.Object.class)}. This ensures + * that if there is a constructor where the type hasn't been initialized, its effect is + * considered. Otherwise, whole-program inference might get stuck in a loop. + * + * @param rhsATM the type of the right-hand side of the pseudo-assignment, which is side-effected + * by this method + * @param defLoc the location where the annotation will be added. It is either a FIELD or a + * non-field (OTHERWISE). + */ + public void wpiAdjustInitializationAnnotations( + AnnotatedTypeMirror rhsATM, TypeUseLocation defLoc) { + // defLoc is defined to be used in the future if needed to differentiate between field and + // non-field locations + if ((rhsATM.hasPrimaryAnnotation(Nullable.class) + || rhsATM.hasPrimaryAnnotation(MonotonicNonNull.class))) { + for (AnnotationMirror anno : rhsATM.getPrimaryAnnotations()) { + if (AnnotationUtils.areSameByName( + anno, "org.checkerframework.checker.initialization.qual" + ".UnknownInitialization")) { + rhsATM.replaceAnnotation(UNKNOWN_INITIALIZATION); + } + } + } + } + @Override public boolean wpiShouldInferTypesForReceivers() { // All receivers must be non-null, or the dereference involved in diff --git a/checker/src/main/java/org/checkerframework/checker/optional/OptionalImplVisitor.java b/checker/src/main/java/org/checkerframework/checker/optional/OptionalImplVisitor.java index 90e62ac116b8..0329fcb8b79d 100644 --- a/checker/src/main/java/org/checkerframework/checker/optional/OptionalImplVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/optional/OptionalImplVisitor.java @@ -65,7 +65,7 @@ * @checker_framework.manual #optional-checker Optional Checker */ public class OptionalImplVisitor - extends BaseTypeVisitor { + extends BaseTypeVisitor { /** The Collection type. */ private final TypeMirror collectionType; diff --git a/checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java b/checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java new file mode 100644 index 000000000000..60ef360cea82 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java @@ -0,0 +1,101 @@ +package org.checkerframework.checker.optional; + +import com.sun.source.tree.ExpressionTree; +import com.sun.source.tree.LambdaExpressionTree; +import com.sun.source.tree.MemberSelectTree; +import com.sun.source.tree.MethodInvocationTree; +import com.sun.source.tree.Tree; +import com.sun.source.tree.VariableTree; +import com.sun.source.util.TreePath; +import java.util.List; +import javax.annotation.processing.ProcessingEnvironment; +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.ExecutableElement; +import javax.lang.model.util.Elements; +import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.checker.optional.qual.Present; +import org.checkerframework.dataflow.cfg.UnderlyingAST; +import org.checkerframework.dataflow.cfg.UnderlyingAST.CFGLambda; +import org.checkerframework.dataflow.cfg.node.LocalVariableNode; +import org.checkerframework.dataflow.expression.JavaExpression; +import org.checkerframework.framework.flow.CFAbstractAnalysis; +import org.checkerframework.framework.flow.CFStore; +import org.checkerframework.framework.flow.CFTransfer; +import org.checkerframework.framework.flow.CFValue; +import org.checkerframework.javacutil.AnnotationBuilder; +import org.checkerframework.javacutil.TreeUtils; + +/** The transfer function for the Optional Checker. */ +public class OptionalTransfer extends CFTransfer { + + /** The {@link OptionalImplAnnotatedTypeFactory} instance for this transfer class. */ + private final OptionalImplAnnotatedTypeFactory optionalTypeFactory; + + /** The @{@link Present} annotation. */ + private final AnnotationMirror PRESENT; + + /** The element for java.util.Optional.ifPresent(). */ + private final ExecutableElement optionalIfPresent; + + /** The element for java.util.Optional.ifPresentOrElse(), or null. */ + private final @Nullable ExecutableElement optionalIfPresentOrElse; + + /** + * Create an OptionalTransfer. + * + * @param analysis the Optional Checker instance + */ + public OptionalTransfer(CFAbstractAnalysis analysis) { + super(analysis); + optionalTypeFactory = (OptionalImplAnnotatedTypeFactory) analysis.getTypeFactory(); + Elements elements = optionalTypeFactory.getElementUtils(); + PRESENT = AnnotationBuilder.fromClass(elements, Present.class); + ProcessingEnvironment env = optionalTypeFactory.getProcessingEnv(); + optionalIfPresent = TreeUtils.getMethod("java.util.Optional", "ifPresent", 1, env); + optionalIfPresentOrElse = + TreeUtils.getMethodOrNull("java.util.Optional", "ifPresentOrElse", 2, env); + } + + @Override + public CFStore initialStore(UnderlyingAST underlyingAST, List parameters) { + + CFStore result = super.initialStore(underlyingAST, parameters); + + if (underlyingAST.getKind() == UnderlyingAST.Kind.LAMBDA) { + // Check whether this lambda is an argument to `Optional.ifPresent()` or + // `Optional.ifPresentOrElse()`. If so, then within the lambda, the receiver of the + // `ifPresent*` method is @Present. + CFGLambda cfgLambda = (CFGLambda) underlyingAST; + LambdaExpressionTree lambdaTree = cfgLambda.getLambdaTree(); + List lambdaParams = lambdaTree.getParameters(); + if (lambdaParams.size() == 1) { + TreePath lambdaPath = optionalTypeFactory.getPath(lambdaTree); + Tree lambdaParent = lambdaPath.getParentPath().getLeaf(); + if (lambdaParent instanceof MethodInvocationTree) { + MethodInvocationTree invok = (MethodInvocationTree) lambdaParent; + ExecutableElement methodElt = TreeUtils.elementFromUse(invok); + if (methodElt.equals(optionalIfPresent) || methodElt.equals(optionalIfPresentOrElse)) { + // `underlyingAST` is an invocation of `Optional.ifPresent()` or + // `Optional.ifPresentOrElse()`. In the lambda, the receiver is @Present. + ExpressionTree methodSelectTree = TreeUtils.withoutParens(invok.getMethodSelect()); + ExpressionTree receiverTree = ((MemberSelectTree) methodSelectTree).getExpression(); + JavaExpression receiverJe = JavaExpression.fromTree(receiverTree); + result.insertValue(receiverJe, PRESENT); + } + } + } + } + + // TODO: Similar logic to the above can be applied in the Nullness Checker. + // Some methods take a function as an argument, guaranteeing that, if the function is + // called: + // * the value passed to the function is non-null + // * some other argument to the method is non-null + // Examples: + // * Jodd's `StringUtil.ifNotNull()` + // * `Opt.ifPresent()` + // * `Opt.map()` + + return result; + } +} diff --git a/checker/tests/ainfer-nullness/input-annotation-files/WPIUnknownInitializationLoopTest-org.checkerframework.checker.nullness.KeyForSubchecker.ajava b/checker/tests/ainfer-nullness/input-annotation-files/WPIUnknownInitializationLoopTest-org.checkerframework.checker.nullness.KeyForSubchecker.ajava new file mode 100644 index 000000000000..1641b30ad5a6 --- /dev/null +++ b/checker/tests/ainfer-nullness/input-annotation-files/WPIUnknownInitializationLoopTest-org.checkerframework.checker.nullness.KeyForSubchecker.ajava @@ -0,0 +1,91 @@ +@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker") +interface Game { + + @org.checkerframework.dataflow.qual.SideEffectFree + void newGame(); +} + +@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker") +class // package-private +GameImpl implements // package-private +Game { + + private MoveValidator moveValidator; + + @org.checkerframework.dataflow.qual.Impure + public GameImpl(MoveValidator mValidator) { + mValidator.setGame(this); + moveValidator = mValidator; + } + + @org.checkerframework.dataflow.qual.SideEffectFree + public GameImpl() { + } + + @org.checkerframework.dataflow.qual.SideEffectFree + public void newGame( // package-private + GameImpl this) { + // Implementation of starting a new game + } +} + +@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker") +interface MoveValidator { + + @org.checkerframework.dataflow.qual.Impure + void setGame( MoveValidator this, Game game); +} + +@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker") +class // package-private +PlayerDependentMoveValidator implements // package-private +MoveValidator { + + private Game game; + + private MoveValidator blackMoveValidator = new SimpleMoveValidator(); + + @org.checkerframework.dataflow.qual.Impure + public void setGame( // package-private + PlayerDependentMoveValidator this, Game game) { + this.game = game; + } + + @org.checkerframework.dataflow.qual.SideEffectFree + public PlayerDependentMoveValidator() { + } + + @org.checkerframework.dataflow.qual.Impure + public PlayerDependentMoveValidator( Game game) { + this.setGame(game); + blackMoveValidator.setGame(game); + } +} + +@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker") +class // package-private +SimpleMoveValidator implements // package-private +MoveValidator { + + private Game game; + + @org.checkerframework.dataflow.qual.Impure + public void setGame( // package-private + SimpleMoveValidator this, Game game) { + this.game = game; + } + + @org.checkerframework.dataflow.qual.SideEffectFree + public SimpleMoveValidator() { + } + + @org.checkerframework.dataflow.qual.Pure + public MoveValidator createMoveValidator() { + return new PlayerDependentMoveValidator(game); + } + public void test(){ + PlayerDependentMoveValidator g1 = + new PlayerDependentMoveValidator(game); + this.game = g1.game; + } +} diff --git a/checker/tests/ainfer-nullness/input-annotation-files/WPIUnknownInitializationLoopTest-org.checkerframework.checker.nullness.NullnessChecker.ajava b/checker/tests/ainfer-nullness/input-annotation-files/WPIUnknownInitializationLoopTest-org.checkerframework.checker.nullness.NullnessChecker.ajava new file mode 100644 index 000000000000..82c1429be032 --- /dev/null +++ b/checker/tests/ainfer-nullness/input-annotation-files/WPIUnknownInitializationLoopTest-org.checkerframework.checker.nullness.NullnessChecker.ajava @@ -0,0 +1,98 @@ +@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker") +interface Game { + + @org.checkerframework.dataflow.qual.SideEffectFree + void newGame(); +} + +@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker") +class // package-private +GameImpl implements // package-private +Game { + + private @org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.MonotonicNonNull MoveValidator moveValidator; + + @org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "this.moveValidator" }) + @org.checkerframework.dataflow.qual.Impure + public GameImpl(MoveValidator mValidator) { + mValidator.setGame(this); + moveValidator = mValidator; + } + + @org.checkerframework.dataflow.qual.SideEffectFree + public GameImpl() { + } + + @org.checkerframework.framework.qual.EnsuresQualifier(expression = { "this.moveValidator" }, qualifier = org.checkerframework.checker.nullness.qual.Nullable.class) + @org.checkerframework.dataflow.qual.SideEffectFree + public void newGame(@org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.NonNull // package-private + GameImpl this) { + // Implementation of starting a new game + } +} + +@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker") +interface MoveValidator { + + @org.checkerframework.dataflow.qual.Impure + void setGame(@org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.Nullable Game game); +} + +@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker") +class // package-private +PlayerDependentMoveValidator implements // package-private +MoveValidator { + + private @org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.Nullable Game game; + + private @org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.NonNull MoveValidator blackMoveValidator = new SimpleMoveValidator(); + + @org.checkerframework.framework.qual.EnsuresQualifier(expression = { "this.game" }, qualifier = org.checkerframework.checker.nullness.qual.Nullable.class) + @org.checkerframework.dataflow.qual.Impure + public void setGame(@org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.NonNull // package-private + PlayerDependentMoveValidator this, @org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.Nullable Game game) { + this.game = game; + } + + @org.checkerframework.dataflow.qual.SideEffectFree + public PlayerDependentMoveValidator() { + } + + @org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "#1" }) + @org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "this.game" }) + @org.checkerframework.dataflow.qual.Impure + public PlayerDependentMoveValidator(@org.checkerframework.checker.initialization.qual.UnknownInitialization(java.lang.Object.class) @org.checkerframework.checker.nullness.qual.Nullable Game game) { + this.setGame(game); + blackMoveValidator.setGame(game); + } +} + +@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker") +class // package-private +SimpleMoveValidator implements // package-private +MoveValidator { + + private @org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.MonotonicNonNull Game game; + + @org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "this.game" }) + @org.checkerframework.dataflow.qual.Impure + public void setGame(@org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.NonNull // package-private + SimpleMoveValidator this, @org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.NonNull Game game) { + this.game = game; + } + + @org.checkerframework.dataflow.qual.SideEffectFree + public SimpleMoveValidator() { + } + + @org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "this.game" }) + @org.checkerframework.dataflow.qual.Pure + public @org.checkerframework.checker.initialization.qual.UnderInitialization(PlayerDependentMoveValidator.class) @org.checkerframework.checker.nullness.qual.NonNull MoveValidator createMoveValidator() { + return new PlayerDependentMoveValidator(game); + } + public void test(){ + PlayerDependentMoveValidator g1 = + new PlayerDependentMoveValidator(game); + this.game = g1.game; + } +} diff --git a/checker/tests/ainfer-nullness/non-annotated/WPIUnknownInitializationLoopTest.java b/checker/tests/ainfer-nullness/non-annotated/WPIUnknownInitializationLoopTest.java new file mode 100644 index 000000000000..52ee5d1a6bbf --- /dev/null +++ b/checker/tests/ainfer-nullness/non-annotated/WPIUnknownInitializationLoopTest.java @@ -0,0 +1,75 @@ +// WPI gets stuck in a loop for codes like this because it +// does not currently consider the facts related to the absence of some initializations +// when there are multiple constructors for a class. A solution for this problem makes the +// ainfernullness test on this code pass. The current solution changes the UnknownInitialization +// annotations with all arguments for a Nullable or MonotonicNonNull object to +// UnknownInitialization(java.lang.Object.class). + +interface Game { + void newGame(); +} + +class GameImpl implements Game { + private MoveValidator moveValidator; + + public GameImpl(MoveValidator mValidator) { + mValidator.setGame(this); + moveValidator = mValidator; + } + + public GameImpl() {} + + @Override + public void newGame() {} +} + +interface MoveValidator { + void setGame(Game game); +} + +class PlayerDependentMoveValidator implements MoveValidator { + public Game game; + private MoveValidator blackMoveValidator = new SimpleMoveValidator(); + + @SuppressWarnings({"override.param", "contracts.postcondition"}) + @Override + public void setGame(Game game) { + this.game = game; + } + + public PlayerDependentMoveValidator() {} + + @SuppressWarnings({"contracts.postcondition", "argument", "method.invocation"}) + public PlayerDependentMoveValidator(Game game) { + this.setGame(game); + blackMoveValidator.setGame(game); + } +} + +class SimpleMoveValidator implements MoveValidator { + private Game game; + + @SuppressWarnings({"override.param", "contracts.postcondition"}) + @Override + public void setGame(Game game) { + this.game = game; + } + + public SimpleMoveValidator() {} + + @SuppressWarnings({ + "purity.not.deterministic.object.creation", + "purity" + ".not.sideeffectfree.call", + "contracts.postcondition", + "return" + }) + public MoveValidator createMoveValidator() { + return new PlayerDependentMoveValidator(game); + } + + public void test() { + PlayerDependentMoveValidator g1 = new PlayerDependentMoveValidator(game); + // :: warning: [assignment] + this.game = g1.game; + } +} diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java index 4743a3962a23..2a9367408f6b 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java @@ -581,8 +581,7 @@ protected boolean updateNodeValues(Node node, TransferResult transferResul * @param b the block to add to {@link #worklist} */ protected void addToWorklist(Block b) { - // TODO: This costs linear (!) time. Use a more efficient way to check if b is already - // present. + // TODO: This costs linear (!) time. Use a more efficient way to check if b is already present. // Two possibilities: // * add unconditionally, and detect duplicates when removing from the queue. // * maintain a HashSet of the elements that are already in the queue. diff --git a/docs/manual/contributors.tex b/docs/manual/contributors.tex index fc5a6d8872f5..541f55e364ba 100644 --- a/docs/manual/contributors.tex +++ b/docs/manual/contributors.tex @@ -39,6 +39,7 @@ Di Wang, Dilraj Singh, Dmitriy Shepelev, +Erfan Arvan, Eric Spishak, Ethan Koenig, Farzan Mirshekari, diff --git a/framework/tests/all-systems/java8/memberref/VarArgs.java b/framework/tests/all-systems/java8/memberref/VarArgs.java new file mode 100644 index 000000000000..a8d88392a86e --- /dev/null +++ b/framework/tests/all-systems/java8/memberref/VarArgs.java @@ -0,0 +1,40 @@ +interface VarArgsFunc { + void take(String... in); +} + +interface ArrayFunc { + void take(String[] in); +} + +class MemberRefVarArgsTest { + + static void myMethod(String... in) {} + + static void myMethodArray(String[] in) {} + + VarArgsFunc v1 = MemberRefVarArgsTest::myMethod; + VarArgsFunc v2 = MemberRefVarArgsTest::myMethodArray; + + ArrayFunc v3 = MemberRefVarArgsTest::myMethod; + ArrayFunc v4 = MemberRefVarArgsTest::myMethodArray; +} + +interface RegularFunc { + void take(Object o); +} + +interface RegularFunc2 { + void take(Object o, String s); +} + +interface RegularFunc3 { + void take(Object o, String s, String s2); +} + +class MoreVarAgrgsTest { + static void myObjectArgArg(Object o, String... vararg) {} + + RegularFunc v1 = MoreVarAgrgsTest::myObjectArgArg; + RegularFunc2 v2 = MoreVarAgrgsTest::myObjectArgArg; + RegularFunc3 v4 = MoreVarAgrgsTest::myObjectArgArg; +}