diff --git a/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/IfNullThrows.java b/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/IfNullThrows.java new file mode 100644 index 000000000000..5e55baafb6b4 --- /dev/null +++ b/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/IfNullThrows.java @@ -0,0 +1,35 @@ +package org.checkerframework.checker.nullness.qual; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; + +/** + * A parameter annotation indicating that the method throws an exception if this parameter is null. + * + *

When the CFG is built, calls to methods with {@code @IfNullThrows} on a parameter are + * translated into an explicit branch: if the argument is null, the method throws; otherwise + * execution continues. This enables flow-sensitive refinement in type checkers (e.g., the Nullness + * Checker refines the argument to non-null on the continue path). + * + *

Semantic meaning: {@code @IfNullThrows} means: if this parameter is null, then the + * method throws. Equivalently: when the method returns normally, the parameter was non-null. + * + *

Example: + * + * 


+ * public static <T> T requireNonNull(@IfNullThrows @Nullable T obj) {
+ *   if (obj == null) throw new NullPointerException();
+ *   return obj;
+ * }
+ *
+ * + * @checker_framework.manual #type-refinement Automatic type refinement (flow-sensitive type + * qualifier inference) + */ +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target(ElementType.PARAMETER) +public @interface IfNullThrows {} diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java index f2ba3a3abb7a..59d706fcdab5 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java @@ -6,6 +6,7 @@ import com.sun.source.tree.ArrayTypeTree; import com.sun.source.tree.AssertTree; import com.sun.source.tree.BinaryTree; +import com.sun.source.tree.BlockTree; import com.sun.source.tree.CaseTree; import com.sun.source.tree.CatchTree; import com.sun.source.tree.ClassTree; @@ -35,9 +36,11 @@ import com.sun.source.tree.VariableTree; import com.sun.source.tree.WhileLoopTree; import com.sun.source.util.TreePath; +import com.sun.source.util.TreeScanner; import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey; import org.checkerframework.checker.formatter.qual.FormatMethod; +import org.checkerframework.checker.nullness.qual.IfNullThrows; import org.checkerframework.checker.nullness.qual.NonNull; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.common.basetype.BaseTypeChecker; @@ -600,9 +603,51 @@ public void processMethodTree(String className, MethodTree tree) { } } + // @IfNullThrows well-formedness: method must throw (e.g. on null param) + checkIfNullThrowsEnforced(tree); + super.processMethodTree(className, tree); } + /** + * Reports an error if the method has {@link IfNullThrows} on any parameter but its body does + * not contain a throw statement (so the contract cannot be satisfied). + */ + private void checkIfNullThrowsEnforced(MethodTree tree) { + ExecutableElement methodElement = TreeUtils.elementFromDeclaration(tree); + if (methodElement.getModifiers().contains(javax.lang.model.element.Modifier.ABSTRACT) + || methodElement + .getModifiers() + .contains(javax.lang.model.element.Modifier.NATIVE)) { + return; + } + boolean hasIfNullThrows = false; + for (Element param : methodElement.getParameters()) { + if (atypeFactory.getDeclAnnotation(param, IfNullThrows.class) != null) { + hasIfNullThrows = true; + break; + } + } + if (!hasIfNullThrows) { + return; + } + BlockTree body = tree.getBody(); + if (body == null) { + return; + } + boolean[] hasThrow = new boolean[] {false}; + new TreeScanner() { + @Override + public Void visitThrow(ThrowTree node, Void p) { + hasThrow[0] = true; + return super.visitThrow(node, p); + } + }.scan(body, null); + if (!hasThrow[0]) { + checker.reportError(tree, "if.null.throws.must.throw"); + } + } + @Override public Void visitMethodInvocation(MethodInvocationTree tree, Void p) { if (!permitClearProperty) { diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/messages.properties b/checker/src/main/java/org/checkerframework/checker/nullness/messages.properties index 5867ce7a919f..0bcde4f3278b 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/messages.properties +++ b/checker/src/main/java/org/checkerframework/checker/nullness/messages.properties @@ -22,6 +22,7 @@ nulltest.redundant=redundant test against null; "%s" is non-null instanceof.nullable=instanceof is only true for a non-null expression instanceof.nonnull.redundant=redundant @NonNull annotation on instanceof new.array.type.invalid=annotations %s may not be applied as component type for array "%s" +if.null.throws.must.throw=method has @IfNullThrows on parameter but body does not throw when parameter is null nullness.on.constructor=do not write nullness annotations on a constructor, whose result is always non-null nullness.on.new.array=do not write nullness annotations on an array creation, which is always non-null nullness.on.new.object=do not write nullness annotations on an object creation, which is always non-null diff --git a/checker/tests/nullness/IfNullThrowsTest.java b/checker/tests/nullness/IfNullThrowsTest.java new file mode 100644 index 000000000000..237cbf370557 --- /dev/null +++ b/checker/tests/nullness/IfNullThrowsTest.java @@ -0,0 +1,60 @@ +// Test that @IfNullThrows (parameter-level postcondition: if null then throw) is respected by the +// Nullness Checker. + +import org.checkerframework.checker.nullness.qual.IfNullThrows; +import org.checkerframework.checker.nullness.qual.Nullable; + +public class IfNullThrowsTest { + + // requireNonNull-style: if param is null, throws; so when returns, param is non-null + public static T requireNonNull(@IfNullThrows @Nullable T obj) { + if (obj == null) { + throw new NullPointerException(); + } + return obj; + } + + void useRequireNonNull(@Nullable String s) { + requireNonNull(s); + s.toString(); // OK: s refined to non-null after requireNonNull returns + } + + // With message parameter + public static T requireNonNull(@IfNullThrows @Nullable T obj, String msg) { + if (obj == null) { + throw new NullPointerException(msg); + } + return obj; + } + + void useRequireNonNullWithMsg(@Nullable String s) { + requireNonNull(s, "s must not be null"); + s.toString(); // OK + } + + // Multiple parameters with @IfNullThrows - validates both must be non-null to return + public static void requireBothNonNull( + @IfNullThrows @Nullable Object a, @IfNullThrows @Nullable Object b) { + if (a == null || b == null) { + throw new NullPointerException(); + } + } + + void useRequireBothNonNull(@Nullable Object x, @Nullable Object y) { + requireBothNonNull(x, y); + x.toString(); // OK + y.toString(); // OK + } + + // Incorrect: has @IfNullThrows but never throws + // :: error: (if.null.throws.must.throw) + public static T badNoThrow(@IfNullThrows @Nullable T obj) { + return obj; + } + + // Incorrect: has @IfNullThrows but only returns, no throw + // :: error: (if.null.throws.must.throw) + public static String badJustReturn(@IfNullThrows @Nullable String s) { + return s == null ? "" : s; + } +} diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java index 15d3e920dc90..6ad14ac048ac 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java @@ -58,6 +58,7 @@ import com.sun.source.util.TreeScanner; import com.sun.source.util.Trees; import com.sun.tools.javac.code.Type; +import com.sun.tools.javac.code.TypeTag; import org.checkerframework.checker.interning.qual.FindDistinct; import org.checkerframework.checker.nullness.qual.Nullable; @@ -1367,7 +1368,8 @@ protected List convertCallArguments( int numFormals = formals.size(); ArrayList convertedNodes = new ArrayList<>(numFormals); - AssertMethodTuple assertMethodTuple = getAssertMethodTuple(executable); + List conditionalThrowSpecs = + getParameterConditionalThrowSpecs(executable); int numActuals = actualExprs.size(); if (executable.isVarArgs()) { @@ -1382,15 +1384,27 @@ protected List convertCallArguments( // invocation conversion to all arguments. for (int i = 0; i < numActuals; i++) { Node actualVal = scan(actualExprs.get(i), null); - if (i == assertMethodTuple.booleanParam) { - treatMethodAsAssert( - (MethodInvocationTree) tree, assertMethodTuple, actualVal); - } if (actualVal == null) { throw new BugInCF( "CFGBuilder: scan returned null for %s [%s]", actualExprs.get(i), actualExprs.get(i).getClass()); } + for (ParameterConditionalThrowSpec spec : conditionalThrowSpecs) { + if (spec.parameterIndex == i) { + Node conditionNode = + buildConditionNodeForParameterThrow( + (MethodInvocationTree) tree, actualVal, spec); + boolean throwWhenConditionTrue = + spec.compareValue == ConditionalThrowCompareValue.TRUE + || spec.compareValue + == ConditionalThrowCompareValue.NULL; + emitConditionalThrow( + (MethodInvocationTree) tree, + conditionNode, + throwWhenConditionTrue, + spec.exceptionType); + } + } convertedNodes.add(methodInvocationConvert(actualVal, formals.get(i))); } } else { @@ -1417,9 +1431,26 @@ protected List convertCallArguments( // remaining ones to initialize an array. for (int i = 0; i < lastArgIndex; i++) { Node actualVal = scan(actualExprs.get(i), null); - if (i == assertMethodTuple.booleanParam) { - treatMethodAsAssert( - (MethodInvocationTree) tree, assertMethodTuple, actualVal); + if (actualVal == null) { + throw new BugInCF( + "CFGBuilder: scan returned null for %s [%s]", + actualExprs.get(i), actualExprs.get(i).getClass()); + } + for (ParameterConditionalThrowSpec spec : conditionalThrowSpecs) { + if (spec.parameterIndex == i) { + Node conditionNode = + buildConditionNodeForParameterThrow( + (MethodInvocationTree) tree, actualVal, spec); + boolean throwWhenConditionTrue = + spec.compareValue == ConditionalThrowCompareValue.TRUE + || spec.compareValue + == ConditionalThrowCompareValue.NULL; + emitConditionalThrow( + (MethodInvocationTree) tree, + conditionNode, + throwWhenConditionTrue, + spec.exceptionType); + } } convertedNodes.add(methodInvocationConvert(actualVal, formals.get(i))); } @@ -1450,8 +1481,25 @@ protected List convertCallArguments( } else { for (int i = 0; i < numActuals; i++) { Node actualVal = scan(actualExprs.get(i), null); - if (i == assertMethodTuple.booleanParam) { - treatMethodAsAssert((MethodInvocationTree) tree, assertMethodTuple, actualVal); + if (actualVal == null) { + throw new BugInCF( + "CFGBuilder: scan returned null for %s [%s]", + actualExprs.get(i), actualExprs.get(i).getClass()); + } + for (ParameterConditionalThrowSpec spec : conditionalThrowSpecs) { + if (spec.parameterIndex == i) { + Node conditionNode = + buildConditionNodeForParameterThrow( + (MethodInvocationTree) tree, actualVal, spec); + boolean throwWhenConditionTrue = + spec.compareValue == ConditionalThrowCompareValue.TRUE + || spec.compareValue == ConditionalThrowCompareValue.NULL; + emitConditionalThrow( + (MethodInvocationTree) tree, + conditionNode, + throwWhenConditionTrue, + spec.exceptionType); + } } convertedNodes.add(methodInvocationConvert(actualVal, formals.get(i))); } @@ -1461,71 +1509,117 @@ protected List convertCallArguments( } /** - * Returns the AssertMethodTuple for {@code method}. If {@code method} is not an assert method, - * then {@link AssertMethodTuple#NONE} is returned. + * Returns the list of parameter conditional-throw specs for {@code method} from dataflow + * annotations (e.g. {@link AssertMethod}). When the CFG is built through the Checker Framework, + * additional specs may be merged by framework-specific phase-one subclasses. * - * @param method a method element that might be an assert method - * @return the AssertMethodTuple for {@code method} + * @param method the method or constructor + * @return specs for parameters that trigger a throw when compared to a value */ - protected AssertMethodTuple getAssertMethodTuple(ExecutableElement method) { + protected List getParameterConditionalThrowSpecs( + ExecutableElement method) { + List result = new ArrayList<>(); + + // AssertMethod: one spec (boolean param, throw when true or false) AnnotationMirror assertMethodAnno = annotationProvider.getDeclAnnotation(method, AssertMethod.class); - if (assertMethodAnno == null) { - return AssertMethodTuple.NONE; + if (assertMethodAnno != null) { + int booleanParam = + AnnotationUtils.getElementValueNotOnClasspath( + assertMethodAnno, "parameter", Integer.class, 1) + - 1; + TypeMirror exceptionType = + AnnotationUtils.getElementValueNotOnClasspath( + assertMethodAnno, + "value", + Type.ClassType.class, + (Type.ClassType) assertionErrorType); + boolean isAssertFalse = + AnnotationUtils.getElementValueNotOnClasspath( + assertMethodAnno, "isAssertFalse", Boolean.class, false); + result.add( + new ParameterConditionalThrowSpec( + booleanParam, + isAssertFalse + ? ConditionalThrowCompareValue.TRUE + : ConditionalThrowCompareValue.FALSE, + exceptionType)); } - // Dataflow does not require checker-qual.jar to be on the users classpath, so - // AnnotationUtils.getElementValue(...) cannot be used. - - int booleanParam = - AnnotationUtils.getElementValueNotOnClasspath( - assertMethodAnno, "parameter", Integer.class, 1) - - 1; - - TypeMirror exceptionType = - AnnotationUtils.getElementValueNotOnClasspath( - assertMethodAnno, - "value", - Type.ClassType.class, - (Type.ClassType) assertionErrorType); - boolean isAssertFalse = - AnnotationUtils.getElementValueNotOnClasspath( - assertMethodAnno, "isAssertFalse", Boolean.class, false); - return new AssertMethodTuple(booleanParam, exceptionType, isAssertFalse); + return result; } - /** Holds the elements of an {@link AssertMethod} annotation. */ - protected static class AssertMethodTuple { - - /** A tuple representing the lack of an {@link AssertMethodTuple}. */ - protected static final AssertMethodTuple NONE = new AssertMethodTuple(-1, null, false); - - /** - * 0-based index of the parameter of the expression that is tested by the assert method. (Or - * -1 if this isn't an assert method.) - */ - public final int booleanParam; + /** + * Builds the condition node for a parameter conditional throw: for {@link + * ConditionalThrowCompareValue#NULL}, returns (argNode == null); for {@link + * ConditionalThrowCompareValue#TRUE} or {@link ConditionalThrowCompareValue#FALSE}, returns the + * argument node itself (boolean). + * + * @param tree the method invocation tree (for artificial tree context) + * @param argNode the argument value node + * @param spec the spec describing the comparison + * @return the condition node to branch on + */ + protected Node buildConditionNodeForParameterThrow( + MethodInvocationTree tree, Node argNode, ParameterConditionalThrowSpec spec) { + if (spec.compareValue == ConditionalThrowCompareValue.NULL) { + TypeMirror booleanType = types.getPrimitiveType(TypeKind.BOOLEAN); + LiteralTree nullTree = + TreeUtils.createLiteral(TypeTag.BOT, null, types.getNullType(), env); + handleArtificialTree(nullTree); + Node nullNode = new NullLiteralNode(nullTree); + extendWithNode(nullNode); + + ExpressionTree argTree = (ExpressionTree) argNode.getTree(); + BinaryTree eqTree = + treeBuilder.buildBinary(booleanType, Tree.Kind.EQUAL_TO, argTree, nullTree); + handleArtificialTree(eqTree); + + Node condition = new EqualToNode(eqTree, argNode, nullNode); + extendWithNode(condition); + return condition; + } + // TRUE or FALSE: condition is the argument (boolean) itself; already in CFG from scan/unbox + return unbox(argNode); + } - /** The type of the exception thrown by the assert method. */ - public final TypeMirror exceptionType; + /** + * Emits CFG nodes for a conditional throw: branch on {@code conditionNode}; when {@code + * throwWhenConditionTrue} is true, take the throw branch when the condition is true, else when + * the condition is false. Then emit the throw and the continue label. + * + * @param tree the method invocation tree (for the AssertionErrorNode) + * @param conditionNode the boolean condition node (already extended) + * @param throwWhenConditionTrue true to throw when condition is true, false to throw when + * condition is false + * @param exceptionType the exception type to throw + */ + protected void emitConditionalThrow( + MethodInvocationTree tree, + Node conditionNode, + boolean throwWhenConditionTrue, + TypeMirror exceptionType) { + // conditionNode is already in the CFG (extended in buildConditionNodeForParameterThrow for + // NULL, or from scan/unbox for TRUE/FALSE) + + Label throwLabel = new Label(); + Label continueLabel = new Label(); + ConditionalJump cjump = + throwWhenConditionTrue + ? new ConditionalJump(throwLabel, continueLabel) + : new ConditionalJump(continueLabel, throwLabel); + extendWithExtendedNode(cjump); - /** Is this an assert false method? */ - public final boolean isAssertFalse; + addLabelForNextNode(throwLabel); + AssertionErrorNode assertNode = + new AssertionErrorNode(tree, conditionNode, null, exceptionType); + extendWithNode(assertNode); + NodeWithExceptionsHolder exNode = + extendWithNodeWithException( + new ThrowNode(null, assertNode, env.getTypeUtils()), exceptionType); + exNode.setTerminatesExecution(true); - /** - * Creates an AssertMethodTuple. - * - * @param booleanParam 0-based index of the parameter of the expression that is tested by - * the assert method - * @param exceptionType the type of the exception thrown by the assert method - * @param isAssertFalse is this an assert false method - */ - public AssertMethodTuple( - int booleanParam, TypeMirror exceptionType, boolean isAssertFalse) { - this.booleanParam = booleanParam; - this.exceptionType = exceptionType; - this.isAssertFalse = isAssertFalse; - } + addLabelForNextNode(continueLabel); } /** @@ -1807,35 +1901,6 @@ protected void translateAssertWithAssertionsEnabled(AssertTree tree) { addLabelForNextNode(assertEnd); } - /** - * Translates a method marked as {@link AssertMethod} into CFG nodes corresponding to an {@code - * assert} statement. - * - * @param tree the method invocation tree for a method marked as {@link AssertMethod} - * @param assertMethodTuple the assert method tuple for the method - * @param condition the boolean expression node for the argument that the method tests - */ - protected void treatMethodAsAssert( - MethodInvocationTree tree, AssertMethodTuple assertMethodTuple, Node condition) { - // all necessary labels - Label thenLabel = new Label(); - Label elseLabel = new Label(); - ConditionalJump cjump = new ConditionalJump(thenLabel, elseLabel); - extendWithExtendedNode(cjump); - - addLabelForNextNode(assertMethodTuple.isAssertFalse ? thenLabel : elseLabel); - AssertionErrorNode assertNode = - new AssertionErrorNode(tree, condition, null, assertMethodTuple.exceptionType); - extendWithNode(assertNode); - NodeWithExceptionsHolder exNode = - extendWithNodeWithException( - new ThrowNode(null, assertNode, env.getTypeUtils()), - assertMethodTuple.exceptionType); - exNode.setTerminatesExecution(true); - - addLabelForNextNode(assertMethodTuple.isAssertFalse ? elseLabel : thenLabel); - } - @Override public Node visitAssignment(AssignmentTree tree, Void p) { diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/ConditionalThrowCompareValue.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/ConditionalThrowCompareValue.java new file mode 100644 index 000000000000..8ff0ea92697d --- /dev/null +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/ConditionalThrowCompareValue.java @@ -0,0 +1,13 @@ +package org.checkerframework.dataflow.cfg.builder; + +/** + * Value to compare a formal parameter against when inserting conditional throw edges in the CFG. + */ +public enum ConditionalThrowCompareValue { + /** Throw when the boolean parameter is true (e.g. assert-false style methods). */ + TRUE, + /** Throw when the boolean parameter is false (e.g. assert-true style methods). */ + FALSE, + /** Throw when the reference parameter is null (e.g. {@code @IfNullThrows} on a parameter). */ + NULL +} diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/ParameterConditionalThrowSpec.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/ParameterConditionalThrowSpec.java new file mode 100644 index 000000000000..2fc9b49ca475 --- /dev/null +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/ParameterConditionalThrowSpec.java @@ -0,0 +1,34 @@ +package org.checkerframework.dataflow.cfg.builder; + +import javax.lang.model.type.TypeMirror; + +/** + * One parameter position that may cause the callee to throw when the argument compares equal to + * {@link #compareValue}. + */ +public class ParameterConditionalThrowSpec { + /** 0-based parameter index. */ + public final int parameterIndex; + + /** Value to compare against; throw when (argument equals this comparison kind). */ + public final ConditionalThrowCompareValue compareValue; + + /** Exception type thrown when the condition holds. */ + public final TypeMirror exceptionType; + + /** + * Creates a spec. + * + * @param parameterIndex 0-based index + * @param compareValue comparison kind + * @param exceptionType exception type thrown when the condition holds + */ + public ParameterConditionalThrowSpec( + int parameterIndex, + ConditionalThrowCompareValue compareValue, + TypeMirror exceptionType) { + this.parameterIndex = parameterIndex; + this.compareValue = compareValue; + this.exceptionType = exceptionType; + } +} diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFCFGBuilder.java b/framework/src/main/java/org/checkerframework/framework/flow/CFCFGBuilder.java index 9a4b064933be..98aff6b17828 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFCFGBuilder.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFCFGBuilder.java @@ -3,38 +3,26 @@ import com.sun.source.tree.AssertTree; import com.sun.source.tree.CompilationUnitTree; import com.sun.source.tree.ExpressionTree; -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 org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.dataflow.cfg.ControlFlowGraph; import org.checkerframework.dataflow.cfg.UnderlyingAST; import org.checkerframework.dataflow.cfg.builder.CFGBuilder; -import org.checkerframework.dataflow.cfg.builder.CFGTranslationPhaseOne; import org.checkerframework.dataflow.cfg.builder.CFGTranslationPhaseThree; import org.checkerframework.dataflow.cfg.builder.CFGTranslationPhaseTwo; import org.checkerframework.dataflow.cfg.builder.PhaseOneResult; import org.checkerframework.framework.type.AnnotatedTypeFactory; -import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.GenericAnnotatedTypeFactory; -import org.checkerframework.javacutil.ElementUtils; -import org.checkerframework.javacutil.TreeUtils; import org.checkerframework.javacutil.UserError; import java.util.Collection; import javax.annotation.processing.ProcessingEnvironment; -import javax.lang.model.element.Element; -import javax.lang.model.element.VariableElement; -import javax.lang.model.type.ArrayType; -import javax.lang.model.type.TypeKind; -import javax.lang.model.type.TypeMirror; /** * A control-flow graph builder (see {@link CFGBuilder}) that knows about the Checker Framework - * annotations and their representation as {@link AnnotatedTypeMirror}s. + * annotations and their representation as {@link + * org.checkerframework.framework.type.AnnotatedTypeMirror}s. */ public class CFCFGBuilder extends CFGBuilder { /** This class should never be instantiated. Protected to still allow subclasses. */ @@ -90,13 +78,13 @@ public static ControlFlowGraph build( } /** - * Given a SourceChecker and an AssertTree, returns whether the AssertTree uses - * an @AssumeAssertion string that is relevant to the SourceChecker. + * Given a SourceChecker and an AssertTree, returns whether the AssertTree uses an + * {@code @AssumeAssertion} string that is relevant to the SourceChecker. * * @param checker the checker * @param tree an assert tree - * @return true if the assert tree contains an @AssumeAssertion(checker) message string for any - * subchecker of the given checker's ultimate parent checker + * @return true if the assert tree contains an {@code @AssumeAssertion(checker)} message string + * for any subchecker of the given checker's ultimate parent checker */ public static boolean assumeAssertionsActivatedForAssertTree( BaseTypeChecker checker, AssertTree tree) { @@ -115,115 +103,4 @@ public static boolean assumeAssertionsActivatedForAssertTree( return false; } - - /** - * A specialized phase-one CFG builder, with a few modifications that make use of the type - * factory. It is responsible for: 1) translating foreach loops so that the declarations of - * their iteration variables have the right annotations, 2) registering the containing elements - * of artificial trees with the relevant type factories, and 3) generating appropriate assertion - * CFG structure in the presence of @AssumeAssertion assertion strings which mention the checker - * or its supercheckers. - */ - protected static class CFCFGTranslationPhaseOne extends CFGTranslationPhaseOne { - /** The associated checker. */ - protected final BaseTypeChecker checker; - - /** Type factory to provide types used during CFG building. */ - protected final AnnotatedTypeFactory atypeFactory; - - public CFCFGTranslationPhaseOne( - CFTreeBuilder builder, - BaseTypeChecker checker, - AnnotatedTypeFactory atypeFactory, - boolean assumeAssertionsEnabled, - boolean assumeAssertionsDisabled, - ProcessingEnvironment env) { - super(builder, atypeFactory, assumeAssertionsEnabled, assumeAssertionsDisabled, env); - this.checker = checker; - this.atypeFactory = atypeFactory; - } - - @Override - protected boolean assumeAssertionsEnabledFor(AssertTree tree) { - if (assumeAssertionsActivatedForAssertTree(checker, tree)) { - return true; - } - return super.assumeAssertionsEnabledFor(tree); - } - - /** - * {@inheritDoc} - * - *

Assigns a path to the artificial tree. - * - * @param tree the newly created Tree - */ - @Override - public void handleArtificialTree(Tree tree) { - // Create a new child of the current path and assign to the artificial tree. - // Although intuitively, using the sibling of the current path as the artificial tree - // path makes more sense, it has the risk of improperly changing the defaulting scope - // of the artificial tree. - TreePath artificialPath = new TreePath(getCurrentPath(), tree); - atypeFactory.setPathForArtificialTree(tree, artificialPath); - } - - @Override - protected VariableTree createEnhancedForLoopIteratorVariable( - MethodInvocationTree iteratorCall, VariableElement variableElement) { - Tree annotatedIteratorTypeTree = - ((CFTreeBuilder) treeBuilder) - .buildAnnotatedType(TreeUtils.typeOf(iteratorCall)); - handleArtificialTree(annotatedIteratorTypeTree); - - // Declare and initialize a new, unique iterator variable - VariableTree iteratorVariable = - treeBuilder.buildVariableDecl( - annotatedIteratorTypeTree, - uniqueName("iter"), - variableElement.getEnclosingElement(), - iteratorCall); - return iteratorVariable; - } - - @Override - protected VariableTree createEnhancedForLoopArrayVariable( - ExpressionTree expression, VariableElement variableElement) { - - TypeMirror type = null; - if (TreeUtils.isLocalVariable(expression)) { - // It is necessary to get the elt because just getting the type of expression - // directly (via TreeUtils.typeOf) doesn't include annotations on the declarations - // of local variables, for some reason. - Element elt = TreeUtils.elementFromTree(expression); - if (elt != null) { - type = ElementUtils.getType(elt); - } - } - - // In all other cases, instead get the type of the expression. This case is - // also triggered when the type from the element is not an array, which can occur - // if the declaration of the local is a generic, such as in - // framework/tests/all-systems/java8inference/Issue1775.java. - // Getting the type from the expression itself guarantees the result will be an array. - if (type == null || type.getKind() != TypeKind.ARRAY) { - TypeMirror expressionType = TreeUtils.typeOf(expression); - type = expressionType; - } - - assert (type instanceof ArrayType) : "array types must be represented by ArrayType"; - - Tree annotatedArrayTypeTree = ((CFTreeBuilder) treeBuilder).buildAnnotatedType(type); - handleArtificialTree(annotatedArrayTypeTree); - - // Declare and initialize a temporary array variable - VariableTree arrayVariable = - treeBuilder.buildVariableDecl( - annotatedArrayTypeTree, - uniqueName("array"), - variableElement.getEnclosingElement(), - expression); - return arrayVariable; - } - } } diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFCFGTranslationPhaseOne.java b/framework/src/main/java/org/checkerframework/framework/flow/CFCFGTranslationPhaseOne.java new file mode 100644 index 000000000000..fdeabf043ce7 --- /dev/null +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFCFGTranslationPhaseOne.java @@ -0,0 +1,141 @@ +package org.checkerframework.framework.flow; + +import com.sun.source.tree.AssertTree; +import com.sun.source.tree.ExpressionTree; +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 org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.dataflow.cfg.builder.CFGTranslationPhaseOne; +import org.checkerframework.dataflow.cfg.builder.ParameterConditionalThrowSpec; +import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.javacutil.ElementUtils; +import org.checkerframework.javacutil.TreeUtils; + +import java.util.ArrayList; +import java.util.List; + +import javax.annotation.processing.ProcessingEnvironment; +import javax.lang.model.element.Element; +import javax.lang.model.element.ExecutableElement; +import javax.lang.model.element.VariableElement; +import javax.lang.model.type.ArrayType; +import javax.lang.model.type.TypeKind; +import javax.lang.model.type.TypeMirror; + +/** + * Checker Framework phase-one CFG translation: uses the {@link AnnotatedTypeFactory} during + * translation (e.g. foreach, artificial trees, assertion-related CFG structure) and merges + * {@linkplain AnnotatedTypeFactory#getAdditionalParameterConditionalThrowSpecs(ExecutableElement) + * additional conditional-throw specs} from the type system. + */ +public class CFCFGTranslationPhaseOne extends CFGTranslationPhaseOne { + + /** The associated checker. */ + protected final BaseTypeChecker checker; + + /** Type factory to provide types used during CFG building. */ + protected final AnnotatedTypeFactory atypeFactory; + + /** + * Creates a Checker Framework phase-one CFG translator. + * + * @param builder tree builder (typically a {@link CFTreeBuilder}) + * @param checker the checker + * @param atypeFactory type factory (also the {@link + * org.checkerframework.javacutil.AnnotationProvider}) + * @param assumeAssertionsEnabled whether assertions may be assumed enabled + * @param assumeAssertionsDisabled whether assertions may be assumed disabled + * @param env processing environment + */ + public CFCFGTranslationPhaseOne( + CFTreeBuilder builder, + BaseTypeChecker checker, + AnnotatedTypeFactory atypeFactory, + boolean assumeAssertionsEnabled, + boolean assumeAssertionsDisabled, + ProcessingEnvironment env) { + super(builder, atypeFactory, assumeAssertionsEnabled, assumeAssertionsDisabled, env); + this.checker = checker; + this.atypeFactory = atypeFactory; + } + + @Override + protected List getParameterConditionalThrowSpecs( + ExecutableElement method) { + List result = + new ArrayList<>(super.getParameterConditionalThrowSpecs(method)); + result.addAll(atypeFactory.getAdditionalParameterConditionalThrowSpecs(method)); + return result; + } + + @Override + protected boolean assumeAssertionsEnabledFor(AssertTree tree) { + if (CFCFGBuilder.assumeAssertionsActivatedForAssertTree(checker, tree)) { + return true; + } + return super.assumeAssertionsEnabledFor(tree); + } + + /** + * {@inheritDoc} + * + *

Assigns a path to the artificial tree. + * + * @param tree the newly created Tree + */ + @Override + public void handleArtificialTree(Tree tree) { + TreePath artificialPath = new TreePath(getCurrentPath(), tree); + atypeFactory.setPathForArtificialTree(tree, artificialPath); + } + + @Override + protected VariableTree createEnhancedForLoopIteratorVariable( + MethodInvocationTree iteratorCall, VariableElement variableElement) { + Tree annotatedIteratorTypeTree = + ((CFTreeBuilder) treeBuilder).buildAnnotatedType(TreeUtils.typeOf(iteratorCall)); + handleArtificialTree(annotatedIteratorTypeTree); + + VariableTree iteratorVariable = + treeBuilder.buildVariableDecl( + annotatedIteratorTypeTree, + uniqueName("iter"), + variableElement.getEnclosingElement(), + iteratorCall); + return iteratorVariable; + } + + @Override + protected VariableTree createEnhancedForLoopArrayVariable( + ExpressionTree expression, VariableElement variableElement) { + + TypeMirror type = null; + if (TreeUtils.isLocalVariable(expression)) { + Element elt = TreeUtils.elementFromTree(expression); + if (elt != null) { + type = ElementUtils.getType(elt); + } + } + + if (type == null || type.getKind() != TypeKind.ARRAY) { + TypeMirror expressionType = TreeUtils.typeOf(expression); + type = expressionType; + } + + assert (type instanceof ArrayType) : "array types must be represented by ArrayType"; + + Tree annotatedArrayTypeTree = ((CFTreeBuilder) treeBuilder).buildAnnotatedType(type); + handleArtificialTree(annotatedArrayTypeTree); + + VariableTree arrayVariable = + treeBuilder.buildVariableDecl( + annotatedArrayTypeTree, + uniqueName("array"), + variableElement.getEnclosingElement(), + expression); + return arrayVariable; + } +} diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java index d066bdc37389..a552d00e65ef 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -45,6 +45,7 @@ import org.checkerframework.common.reflection.MethodValChecker; import org.checkerframework.common.reflection.ReflectionResolver; import org.checkerframework.common.reflection.qual.MethodVal; +import org.checkerframework.dataflow.cfg.builder.ParameterConditionalThrowSpec; import org.checkerframework.dataflow.qual.SideEffectFree; import org.checkerframework.framework.qual.AnnotatedFor; import org.checkerframework.framework.qual.EnsuresQualifier; @@ -901,6 +902,19 @@ public BaseTypeChecker getChecker() { return checker; } + /** + * Extra conditional-parameter throw specs merged during CFG construction (phase one). The + * default implementation returns none; {@link GenericAnnotatedTypeFactory} merges self-only + * contributions from composite checkers. + * + * @param method method or constructor being called + * @return additional {@link ParameterConditionalThrowSpec} entries + */ + public List getAdditionalParameterConditionalThrowSpecs( + ExecutableElement method) { + return Collections.emptyList(); + } + /** * Returns the names of the annotation processors that are being run. * @@ -4038,7 +4052,7 @@ public void setVisitorTreePath(@Nullable TreePath visitorTreePath) { * Set the tree path for the given artificial tree. * *

See {@code - * org.checkerframework.framework.flow.CFCFGBuilder.CFCFGTranslationPhaseOne.handleArtificialTree(Tree)}. + * org.checkerframework.framework.flow.CFCFGTranslationPhaseOne#handleArtificialTree(Tree)}. * * @param tree the artificial {@link Tree} to set the path for * @param path the {@link TreePath} for the artificial tree diff --git a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java index b4ba882f9aaf..6c1af7a24f27 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -31,6 +31,8 @@ import org.checkerframework.dataflow.cfg.UnderlyingAST.CFGLambda; import org.checkerframework.dataflow.cfg.UnderlyingAST.CFGMethod; import org.checkerframework.dataflow.cfg.UnderlyingAST.CFGStatement; +import org.checkerframework.dataflow.cfg.builder.ConditionalThrowCompareValue; +import org.checkerframework.dataflow.cfg.builder.ParameterConditionalThrowSpec; import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; import org.checkerframework.dataflow.cfg.node.Node; import org.checkerframework.dataflow.cfg.node.ObjectCreationNode; @@ -114,11 +116,13 @@ import java.util.Queue; import java.util.Set; import java.util.StringJoiner; +import java.util.WeakHashMap; import java.util.regex.Pattern; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; import javax.lang.model.element.ElementKind; +import javax.lang.model.element.ExecutableElement; import javax.lang.model.element.Modifier; import javax.lang.model.element.TypeElement; import javax.lang.model.element.VariableElement; @@ -263,6 +267,30 @@ public abstract class GenericAnnotatedTypeFactory< */ private final Map initializerCache; + /** + * Caches merged conditional-throw specs per callee declaration for the current compilation + * unit, so repeated call sites avoid re-discovering hook annotations. + */ + private final Map> + additionalParameterConditionalThrowSpecsCache; + + /** + * Name of nullness's declaration annotation that indicates a parameter throws when null. + * + *

Using the binary name avoids introducing a framework->checker module dependency. + */ + private static final String IF_NULL_THROWS_ANNOTATION_NAME = + "org.checkerframework.checker.nullness.qual.IfNullThrows"; + + /** + * Cross-factory cache of parameter indexes annotated with framework-level null-throw hooks. + * + *

Keys are weak to avoid retaining elements beyond javac rounds. + */ + private static final Map> + frameworkIfNullThrowsParameterIndexesCache = + Collections.synchronizedMap(new WeakHashMap<>()); + /** * Should the analysis assume that side effects to a value can change the type of aliased * references? @@ -370,9 +398,12 @@ protected GenericAnnotatedTypeFactory(BaseTypeChecker checker, boolean useFlow) int cacheSize = getCacheSize(); flowResultAnalysisCaches = CollectionsPlume.createLruCache(cacheSize); initializerCache = CollectionsPlume.createLruCache(cacheSize); + additionalParameterConditionalThrowSpecsCache = + CollectionsPlume.createLruCache(cacheSize); } else { flowResultAnalysisCaches = null; initializerCache = null; + additionalParameterConditionalThrowSpecsCache = null; } RelevantJavaTypes relevantJavaTypesAnno = @@ -424,6 +455,88 @@ protected boolean getUseFlow() { return useFlow; } + @Override + public List getAdditionalParameterConditionalThrowSpecs( + ExecutableElement method) { + GenericAnnotatedTypeFactory ultimateAtf = + checker.getUltimateParentChecker().getTypeFactory(); + if (this != ultimateAtf) { + return ultimateAtf.getAdditionalParameterConditionalThrowSpecs(method); + } + if (shouldCache) { + List cached = + additionalParameterConditionalThrowSpecsCache.get(method); + if (cached != null) { + return cached; + } + } + List result = new ArrayList<>(); + result.addAll(getFrameworkParameterConditionalThrowSpecs(method)); + result.addAll(getAdditionalParameterConditionalThrowSpecsSelfOnly(method)); + if (hasOrIsSubchecker) { + for (SourceChecker sub : checker.getSubcheckers()) { + if (sub instanceof BaseTypeChecker) { + result.addAll( + ((BaseTypeChecker) sub) + .getTypeFactory() + .getAdditionalParameterConditionalThrowSpecsSelfOnly(method)); + } + } + } + List immutableResult = Collections.unmodifiableList(result); + if (shouldCache) { + additionalParameterConditionalThrowSpecsCache.put(method, immutableResult); + } + return immutableResult; + } + + /** + * Returns framework-level conditional throw specs that are independent of a specific checker. + * + * @param method method or constructor + * @return framework-level specs for the callee declaration + */ + private List getFrameworkParameterConditionalThrowSpecs( + ExecutableElement method) { + List parameterIndexes = frameworkIfNullThrowsParameterIndexesCache.get(method); + if (parameterIndexes == null) { + parameterIndexes = new ArrayList<>(); + List params = method.getParameters(); + for (int i = 0; i < params.size(); i++) { + VariableElement param = params.get(i); + for (AnnotationMirror anno : param.getAnnotationMirrors()) { + if (AnnotationUtils.areSameByName(anno, IF_NULL_THROWS_ANNOTATION_NAME)) { + parameterIndexes.add(i); + break; + } + } + } + parameterIndexes = Collections.unmodifiableList(parameterIndexes); + frameworkIfNullThrowsParameterIndexesCache.put(method, parameterIndexes); + } + + List result = new ArrayList<>(); + TypeMirror npeType = TypesUtils.typeFromClass(NullPointerException.class, types, elements); + for (int index : parameterIndexes) { + result.add( + new ParameterConditionalThrowSpec( + index, ConditionalThrowCompareValue.NULL, npeType)); + } + return result; + } + + /** + * Conditional throw specs contributed only by this type factory. The merged list used during + * CFG construction is {@link #getAdditionalParameterConditionalThrowSpecs(ExecutableElement)}. + * + * @param method method or constructor + * @return specs for this factory alone + */ + public List getAdditionalParameterConditionalThrowSpecsSelfOnly( + ExecutableElement method) { + return Collections.emptyList(); + } + @Override protected void postInit( @UnderInitialization(GenericAnnotatedTypeFactory.class) GenericAnnotatedTypeFactory @@ -494,6 +607,7 @@ public void setRoot(@Nullable CompilationUnitTree root) { if (shouldCache) { this.flowResultAnalysisCaches.clear(); this.initializerCache.clear(); + this.additionalParameterConditionalThrowSpecsCache.clear(); this.defaultQualifierForUseTypeAnnotator.clearCache(); if (this.checker.getParentChecker() == null) {