From 89cf2e7380d9986f3c2c3ea055b738b2b918516a Mon Sep 17 00:00:00 2001 From: Henry Xi Date: Mon, 2 Mar 2026 00:39:17 -0500 Subject: [PATCH 1/3] Add @IfNullThrows parameter annotation --- .../dataflow/qual/IfNullThrows.java | 35 +++++++++ checker/tests/nullness/IfNullThrowsTest.java | 48 ++++++++++++ .../cfg/builder/CFGTranslationPhaseOne.java | 73 +++++++++++++++++++ 3 files changed, 156 insertions(+) create mode 100644 checker-qual/src/main/java/org/checkerframework/dataflow/qual/IfNullThrows.java create mode 100644 checker/tests/nullness/IfNullThrowsTest.java diff --git a/checker-qual/src/main/java/org/checkerframework/dataflow/qual/IfNullThrows.java b/checker-qual/src/main/java/org/checkerframework/dataflow/qual/IfNullThrows.java new file mode 100644 index 000000000000..8acd930edca3 --- /dev/null +++ b/checker-qual/src/main/java/org/checkerframework/dataflow/qual/IfNullThrows.java @@ -0,0 +1,35 @@ +package org.checkerframework.dataflow.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/tests/nullness/IfNullThrowsTest.java b/checker/tests/nullness/IfNullThrowsTest.java new file mode 100644 index 000000000000..59315fddefdd --- /dev/null +++ b/checker/tests/nullness/IfNullThrowsTest.java @@ -0,0 +1,48 @@ +// Test that @IfNullThrows (parameter-level postcondition: if null then throw) is respected by the +// Nullness Checker. + +import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.dataflow.qual.IfNullThrows; + +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 + } +} 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..be01cfde7ade 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; @@ -139,6 +140,7 @@ import org.checkerframework.dataflow.cfg.node.VariableDeclarationNode; import org.checkerframework.dataflow.cfg.node.WideningConversionNode; import org.checkerframework.dataflow.qual.AssertMethod; +import org.checkerframework.dataflow.qual.IfNullThrows; import org.checkerframework.dataflow.qual.TerminatesExecution; import org.checkerframework.javacutil.AnnotationProvider; import org.checkerframework.javacutil.AnnotationUtils; @@ -1368,6 +1370,7 @@ protected List convertCallArguments( ArrayList convertedNodes = new ArrayList<>(numFormals); AssertMethodTuple assertMethodTuple = getAssertMethodTuple(executable); + Set ifNullThrowsParams = getIfNullThrowsParameterIndices(executable); int numActuals = actualExprs.size(); if (executable.isVarArgs()) { @@ -1386,6 +1389,9 @@ protected List convertCallArguments( treatMethodAsAssert( (MethodInvocationTree) tree, assertMethodTuple, actualVal); } + if (ifNullThrowsParams.contains(i)) { + treatMethodAsIfNullThrows((MethodInvocationTree) tree, actualVal); + } if (actualVal == null) { throw new BugInCF( "CFGBuilder: scan returned null for %s [%s]", @@ -1421,6 +1427,9 @@ protected List convertCallArguments( treatMethodAsAssert( (MethodInvocationTree) tree, assertMethodTuple, actualVal); } + if (ifNullThrowsParams.contains(i)) { + treatMethodAsIfNullThrows((MethodInvocationTree) tree, actualVal); + } convertedNodes.add(methodInvocationConvert(actualVal, formals.get(i))); } @@ -1453,6 +1462,9 @@ protected List convertCallArguments( if (i == assertMethodTuple.booleanParam) { treatMethodAsAssert((MethodInvocationTree) tree, assertMethodTuple, actualVal); } + if (ifNullThrowsParams.contains(i)) { + treatMethodAsIfNullThrows((MethodInvocationTree) tree, actualVal); + } convertedNodes.add(methodInvocationConvert(actualVal, formals.get(i))); } } @@ -1494,6 +1506,67 @@ protected AssertMethodTuple getAssertMethodTuple(ExecutableElement method) { return new AssertMethodTuple(booleanParam, exceptionType, isAssertFalse); } + /** + * Returns the 0-based indices of parameters annotated with {@link IfNullThrows}. Such + * parameters cause the method to throw when null; the CFG is modified to add an explicit + * branch. + * + * @param method the method or constructor + * @return indices of parameters with {@code @IfNullThrows} + */ + protected Set getIfNullThrowsParameterIndices(ExecutableElement method) { + Set result = new HashSet<>(); + List params = method.getParameters(); + for (int i = 0; i < params.size(); i++) { + if (annotationProvider.getDeclAnnotation(params.get(i), IfNullThrows.class) != null) { + result.add(i); + } + } + return result; + } + + /** + * Translates a method call with {@link IfNullThrows} on a parameter into CFG nodes: if the + * argument is null, the method throws; otherwise execution continues. + * + * @param tree the method invocation tree + * @param argNode the node for the argument (the parameter value) + */ + protected void treatMethodAsIfNullThrows(MethodInvocationTree tree, Node argNode) { + // Create (arg == null) condition + 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); + + // When (arg == null) is true, throw; else continue + Label throwLabel = new Label(); + Label continueLabel = new Label(); + ConditionalJump cjump = new ConditionalJump(throwLabel, continueLabel); + extendWithExtendedNode(cjump); + + addLabelForNextNode(throwLabel); + AssertionErrorNode assertNode = + new AssertionErrorNode(tree, condition, null, nullPointerExceptionType); + extendWithNode(assertNode); + NodeWithExceptionsHolder exNode = + extendWithNodeWithException( + new ThrowNode(null, assertNode, env.getTypeUtils()), + nullPointerExceptionType); + exNode.setTerminatesExecution(true); + + addLabelForNextNode(continueLabel); + } + /** Holds the elements of an {@link AssertMethod} annotation. */ protected static class AssertMethodTuple { From 1c4a67644dd0fdbe085c51e9c9b7afec0e5dfec7 Mon Sep 17 00:00:00 2001 From: Henry Xi Date: Tue, 10 Mar 2026 21:27:08 -0400 Subject: [PATCH 2/3] Unify AssertMethod and IfNullThrows in CFG, move IfNullThrows to Nullness, Ensure qualifer is enforced --- .../nullness}/qual/IfNullThrows.java | 2 +- .../nullness/NullnessNoInitVisitor.java | 45 +++ .../checker/nullness/messages.properties | 1 + checker/tests/nullness/IfNullThrowsTest.java | 14 +- .../cfg/builder/CFGTranslationPhaseOne.java | 320 ++++++++++-------- 5 files changed, 237 insertions(+), 145 deletions(-) rename checker-qual/src/main/java/org/checkerframework/{dataflow => checker/nullness}/qual/IfNullThrows.java (96%) diff --git a/checker-qual/src/main/java/org/checkerframework/dataflow/qual/IfNullThrows.java b/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/IfNullThrows.java similarity index 96% rename from checker-qual/src/main/java/org/checkerframework/dataflow/qual/IfNullThrows.java rename to checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/IfNullThrows.java index 8acd930edca3..5e55baafb6b4 100644 --- a/checker-qual/src/main/java/org/checkerframework/dataflow/qual/IfNullThrows.java +++ b/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/IfNullThrows.java @@ -1,4 +1,4 @@ -package org.checkerframework.dataflow.qual; +package org.checkerframework.checker.nullness.qual; import java.lang.annotation.Documented; import java.lang.annotation.ElementType; 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 index 59315fddefdd..237cbf370557 100644 --- a/checker/tests/nullness/IfNullThrowsTest.java +++ b/checker/tests/nullness/IfNullThrowsTest.java @@ -1,8 +1,8 @@ // 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; -import org.checkerframework.dataflow.qual.IfNullThrows; public class IfNullThrowsTest { @@ -45,4 +45,16 @@ void useRequireBothNonNull(@Nullable Object x, @Nullable Object 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 be01cfde7ade..7a21612236e0 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 @@ -61,6 +61,7 @@ import com.sun.tools.javac.code.TypeTag; import org.checkerframework.checker.interning.qual.FindDistinct; +import org.checkerframework.checker.nullness.qual.IfNullThrows; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.dataflow.analysis.Store.FlowRule; import org.checkerframework.dataflow.cfg.UnderlyingAST; @@ -140,7 +141,6 @@ import org.checkerframework.dataflow.cfg.node.VariableDeclarationNode; import org.checkerframework.dataflow.cfg.node.WideningConversionNode; import org.checkerframework.dataflow.qual.AssertMethod; -import org.checkerframework.dataflow.qual.IfNullThrows; import org.checkerframework.dataflow.qual.TerminatesExecution; import org.checkerframework.javacutil.AnnotationProvider; import org.checkerframework.javacutil.AnnotationUtils; @@ -1369,8 +1369,8 @@ protected List convertCallArguments( int numFormals = formals.size(); ArrayList convertedNodes = new ArrayList<>(numFormals); - AssertMethodTuple assertMethodTuple = getAssertMethodTuple(executable); - Set ifNullThrowsParams = getIfNullThrowsParameterIndices(executable); + List conditionalThrowSpecs = + getParameterConditionalThrowSpecs(executable); int numActuals = actualExprs.size(); if (executable.isVarArgs()) { @@ -1385,18 +1385,26 @@ 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 (ifNullThrowsParams.contains(i)) { - treatMethodAsIfNullThrows((MethodInvocationTree) tree, 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 == CompareValue.TRUE + || spec.compareValue == CompareValue.NULL; + emitConditionalThrow( + (MethodInvocationTree) tree, + conditionNode, + throwWhenConditionTrue, + spec.exceptionType); + } + } convertedNodes.add(methodInvocationConvert(actualVal, formals.get(i))); } } else { @@ -1423,12 +1431,25 @@ 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()); } - if (ifNullThrowsParams.contains(i)) { - treatMethodAsIfNullThrows((MethodInvocationTree) tree, actualVal); + for (ParameterConditionalThrowSpec spec : conditionalThrowSpecs) { + if (spec.parameterIndex == i) { + Node conditionNode = + buildConditionNodeForParameterThrow( + (MethodInvocationTree) tree, actualVal, spec); + boolean throwWhenConditionTrue = + spec.compareValue == CompareValue.TRUE + || spec.compareValue == CompareValue.NULL; + emitConditionalThrow( + (MethodInvocationTree) tree, + conditionNode, + throwWhenConditionTrue, + spec.exceptionType); + } } convertedNodes.add(methodInvocationConvert(actualVal, formals.get(i))); } @@ -1459,11 +1480,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()); } - if (ifNullThrowsParams.contains(i)) { - treatMethodAsIfNullThrows((MethodInvocationTree) tree, actualVal); + for (ParameterConditionalThrowSpec spec : conditionalThrowSpecs) { + if (spec.parameterIndex == i) { + Node conditionNode = + buildConditionNodeForParameterThrow( + (MethodInvocationTree) tree, actualVal, spec); + boolean throwWhenConditionTrue = + spec.compareValue == CompareValue.TRUE + || spec.compareValue == CompareValue.NULL; + emitConditionalThrow( + (MethodInvocationTree) tree, + conditionNode, + throwWhenConditionTrue, + spec.exceptionType); + } } convertedNodes.add(methodInvocationConvert(actualVal, formals.get(i))); } @@ -1473,134 +1508,162 @@ protected List convertCallArguments( } /** - * Returns the AssertMethodTuple for {@code method}. If {@code method} is not an assert method, - * then {@link AssertMethodTuple#NONE} is returned. - * - * @param method a method element that might be an assert method - * @return the AssertMethodTuple for {@code method} + * Value to compare the parameter against; when the condition (param equals this value) holds, + * the method throws. Used for both {@link AssertMethod} (TRUE/FALSE) and {@link IfNullThrows} + * (NULL). */ - protected AssertMethodTuple getAssertMethodTuple(ExecutableElement method) { - AnnotationMirror assertMethodAnno = - annotationProvider.getDeclAnnotation(method, AssertMethod.class); - if (assertMethodAnno == null) { - return AssertMethodTuple.NONE; - } + protected enum CompareValue { + /** Throw when the boolean parameter is true (e.g. assert false methods). */ + TRUE, + /** Throw when the boolean parameter is false (e.g. assert methods). */ + FALSE, + /** Throw when the reference parameter is null ({@link IfNullThrows}). */ + NULL + } - // 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); + /** + * Spec for one parameter that triggers a conditional throw: when the parameter compares equal + * to {@link #compareValue}, the method throws {@link #exceptionType}. Unifies {@link + * AssertMethod} (one per method) and {@link IfNullThrows} (one per annotated parameter). + */ + protected static class ParameterConditionalThrowSpec { + /** 0-based parameter index. */ + public final int parameterIndex; + + /** Value to compare against; throw when (param equals this). */ + public final CompareValue compareValue; + + /** Exception type thrown when the condition holds. */ + public final TypeMirror exceptionType; + + public ParameterConditionalThrowSpec( + int parameterIndex, CompareValue compareValue, TypeMirror exceptionType) { + this.parameterIndex = parameterIndex; + this.compareValue = compareValue; + this.exceptionType = exceptionType; + } } /** - * Returns the 0-based indices of parameters annotated with {@link IfNullThrows}. Such - * parameters cause the method to throw when null; the CFG is modified to add an explicit - * branch. + * Returns the list of parameter conditional-throw specs for {@code method}: one from {@link + * AssertMethod} if present, plus one per parameter annotated with {@link IfNullThrows}. * * @param method the method or constructor - * @return indices of parameters with {@code @IfNullThrows} + * @return specs for parameters that trigger a throw when compared to a value */ - protected Set getIfNullThrowsParameterIndices(ExecutableElement method) { - Set result = new HashSet<>(); + 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) { + 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 ? CompareValue.TRUE : CompareValue.FALSE, + exceptionType)); + } + + // IfNullThrows: one spec per annotated parameter List params = method.getParameters(); for (int i = 0; i < params.size(); i++) { if (annotationProvider.getDeclAnnotation(params.get(i), IfNullThrows.class) != null) { - result.add(i); + result.add( + new ParameterConditionalThrowSpec( + i, CompareValue.NULL, nullPointerExceptionType)); } } + return result; } /** - * Translates a method call with {@link IfNullThrows} on a parameter into CFG nodes: if the - * argument is null, the method throws; otherwise execution continues. + * Builds the condition node for a parameter conditional throw: for {@link CompareValue#NULL}, + * returns (argNode == null); for {@link CompareValue#TRUE} or {@link CompareValue#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 == CompareValue.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); + } + + /** + * 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 - * @param argNode the node for the argument (the parameter value) + * @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 treatMethodAsIfNullThrows(MethodInvocationTree tree, Node argNode) { - // Create (arg == null) condition - 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); - - // When (arg == null) is true, throw; else continue + 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 = new ConditionalJump(throwLabel, continueLabel); + ConditionalJump cjump = + throwWhenConditionTrue + ? new ConditionalJump(throwLabel, continueLabel) + : new ConditionalJump(continueLabel, throwLabel); extendWithExtendedNode(cjump); addLabelForNextNode(throwLabel); AssertionErrorNode assertNode = - new AssertionErrorNode(tree, condition, null, nullPointerExceptionType); + new AssertionErrorNode(tree, conditionNode, null, exceptionType); extendWithNode(assertNode); NodeWithExceptionsHolder exNode = extendWithNodeWithException( - new ThrowNode(null, assertNode, env.getTypeUtils()), - nullPointerExceptionType); + new ThrowNode(null, assertNode, env.getTypeUtils()), exceptionType); exNode.setTerminatesExecution(true); addLabelForNextNode(continueLabel); } - /** 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; - - /** The type of the exception thrown by the assert method. */ - public final TypeMirror exceptionType; - - /** Is this an assert false method? */ - public final boolean isAssertFalse; - - /** - * 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; - } - } - /** * Convert an operand of a conditional expression to the type of the whole expression. * @@ -1880,35 +1943,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) { From 549178e968882313f434d0e9a3a0d42e0ad94dad Mon Sep 17 00:00:00 2001 From: Henry Xi Date: Wed, 15 Apr 2026 12:01:18 -0400 Subject: [PATCH 3/3] Cache conditional-throw hook discovery across CFG builds --- .../cfg/builder/CFGTranslationPhaseOne.java | 80 +++------- .../builder/ConditionalThrowCompareValue.java | 13 ++ .../ParameterConditionalThrowSpec.java | 34 +++++ .../framework/flow/CFCFGBuilder.java | 135 +---------------- .../flow/CFCFGTranslationPhaseOne.java | 141 ++++++++++++++++++ .../framework/type/AnnotatedTypeFactory.java | 16 +- .../type/GenericAnnotatedTypeFactory.java | 114 ++++++++++++++ 7 files changed, 342 insertions(+), 191 deletions(-) create mode 100644 dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/ConditionalThrowCompareValue.java create mode 100644 dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/ParameterConditionalThrowSpec.java create mode 100644 framework/src/main/java/org/checkerframework/framework/flow/CFCFGTranslationPhaseOne.java 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 7a21612236e0..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 @@ -61,7 +61,6 @@ import com.sun.tools.javac.code.TypeTag; import org.checkerframework.checker.interning.qual.FindDistinct; -import org.checkerframework.checker.nullness.qual.IfNullThrows; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.dataflow.analysis.Store.FlowRule; import org.checkerframework.dataflow.cfg.UnderlyingAST; @@ -1396,8 +1395,9 @@ protected List convertCallArguments( buildConditionNodeForParameterThrow( (MethodInvocationTree) tree, actualVal, spec); boolean throwWhenConditionTrue = - spec.compareValue == CompareValue.TRUE - || spec.compareValue == CompareValue.NULL; + spec.compareValue == ConditionalThrowCompareValue.TRUE + || spec.compareValue + == ConditionalThrowCompareValue.NULL; emitConditionalThrow( (MethodInvocationTree) tree, conditionNode, @@ -1442,8 +1442,9 @@ protected List convertCallArguments( buildConditionNodeForParameterThrow( (MethodInvocationTree) tree, actualVal, spec); boolean throwWhenConditionTrue = - spec.compareValue == CompareValue.TRUE - || spec.compareValue == CompareValue.NULL; + spec.compareValue == ConditionalThrowCompareValue.TRUE + || spec.compareValue + == ConditionalThrowCompareValue.NULL; emitConditionalThrow( (MethodInvocationTree) tree, conditionNode, @@ -1491,8 +1492,8 @@ protected List convertCallArguments( buildConditionNodeForParameterThrow( (MethodInvocationTree) tree, actualVal, spec); boolean throwWhenConditionTrue = - spec.compareValue == CompareValue.TRUE - || spec.compareValue == CompareValue.NULL; + spec.compareValue == ConditionalThrowCompareValue.TRUE + || spec.compareValue == ConditionalThrowCompareValue.NULL; emitConditionalThrow( (MethodInvocationTree) tree, conditionNode, @@ -1508,45 +1509,9 @@ protected List convertCallArguments( } /** - * Value to compare the parameter against; when the condition (param equals this value) holds, - * the method throws. Used for both {@link AssertMethod} (TRUE/FALSE) and {@link IfNullThrows} - * (NULL). - */ - protected enum CompareValue { - /** Throw when the boolean parameter is true (e.g. assert false methods). */ - TRUE, - /** Throw when the boolean parameter is false (e.g. assert methods). */ - FALSE, - /** Throw when the reference parameter is null ({@link IfNullThrows}). */ - NULL - } - - /** - * Spec for one parameter that triggers a conditional throw: when the parameter compares equal - * to {@link #compareValue}, the method throws {@link #exceptionType}. Unifies {@link - * AssertMethod} (one per method) and {@link IfNullThrows} (one per annotated parameter). - */ - protected static class ParameterConditionalThrowSpec { - /** 0-based parameter index. */ - public final int parameterIndex; - - /** Value to compare against; throw when (param equals this). */ - public final CompareValue compareValue; - - /** Exception type thrown when the condition holds. */ - public final TypeMirror exceptionType; - - public ParameterConditionalThrowSpec( - int parameterIndex, CompareValue compareValue, TypeMirror exceptionType) { - this.parameterIndex = parameterIndex; - this.compareValue = compareValue; - this.exceptionType = exceptionType; - } - } - - /** - * Returns the list of parameter conditional-throw specs for {@code method}: one from {@link - * AssertMethod} if present, plus one per parameter annotated with {@link IfNullThrows}. + * 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 the method or constructor * @return specs for parameters that trigger a throw when compared to a value @@ -1575,27 +1540,20 @@ protected List getParameterConditionalThrowSpecs( result.add( new ParameterConditionalThrowSpec( booleanParam, - isAssertFalse ? CompareValue.TRUE : CompareValue.FALSE, + isAssertFalse + ? ConditionalThrowCompareValue.TRUE + : ConditionalThrowCompareValue.FALSE, exceptionType)); } - // IfNullThrows: one spec per annotated parameter - List params = method.getParameters(); - for (int i = 0; i < params.size(); i++) { - if (annotationProvider.getDeclAnnotation(params.get(i), IfNullThrows.class) != null) { - result.add( - new ParameterConditionalThrowSpec( - i, CompareValue.NULL, nullPointerExceptionType)); - } - } - return result; } /** - * Builds the condition node for a parameter conditional throw: for {@link CompareValue#NULL}, - * returns (argNode == null); for {@link CompareValue#TRUE} or {@link CompareValue#FALSE}, - * returns the argument node itself (boolean). + * 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 @@ -1604,7 +1562,7 @@ protected List getParameterConditionalThrowSpecs( */ protected Node buildConditionNodeForParameterThrow( MethodInvocationTree tree, Node argNode, ParameterConditionalThrowSpec spec) { - if (spec.compareValue == CompareValue.NULL) { + if (spec.compareValue == ConditionalThrowCompareValue.NULL) { TypeMirror booleanType = types.getPrimitiveType(TypeKind.BOOLEAN); LiteralTree nullTree = TreeUtils.createLiteral(TypeTag.BOT, null, types.getNullType(), env); 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) {