From 71024563a598426d35e3a2a2ce287115de7b2a2c Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sat, 25 Nov 2023 08:58:11 -0500 Subject: [PATCH 1/6] initial commit for adding notcheckdeadcode option --- .../nullness/NullnessNoInitVisitor.java | 8 +++--- docs/CHANGELOG.md | 3 +++ .../common/basetype/BaseTypeVisitor.java | 10 ++++--- .../framework/source/SourceChecker.java | 3 +++ .../type/GenericAnnotatedTypeFactory.java | 26 ++++++++++--------- 5 files changed, 31 insertions(+), 19 deletions(-) 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 68a9362ee9e..a6b5890a197 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java @@ -290,9 +290,11 @@ protected boolean commonAssignmentCheck( /** Case 1: Check for null dereferencing. */ @Override public Void visitMemberSelect(MemberSelectTree tree, Void p) { - // if (atypeFactory.isUnreachable(tree)) { - // return super.visitMemberSelect(tree, p); - // } + if (checker.hasOption("notCheckDeadCode")) { + if (atypeFactory.isUnreachable(tree)) { + return super.visitMemberSelect(tree, p); + } + } Element e = TreeUtils.elementFromUse(tree); if (e.getKind() == ElementKind.CLASS) { if (atypeFactory.containsNullnessAnnotation(null, tree.getExpression())) { diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 50bd076ed03..780d784c8e5 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -3,6 +3,9 @@ Version 3.40.0-eisop2 (November ??, 2023) **User-visible changes:** +Add a new command-line argument `-AnotCheckDeadCode` disables the checker for code in dead expression. +This option is not enabled by default. + **Implementation details:** **Closed issues:** diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index 6b61e7397a4..09a4e21b84b 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -5181,10 +5181,12 @@ protected TypeValidator createTypeValidator() { * @return true if checker should not test exprTree */ protected final boolean shouldSkipUses(ExpressionTree exprTree) { - // System.out.printf("shouldSkipUses: %s: %s%n", exprTree.getClass(), exprTree); - // if (atypeFactory.isUnreachable(exprTree)) { - // return true; - // } + if (checker.hasOption("notCheckDeadCode")) { + System.out.printf("shouldSkipUses: %s: %s%n", exprTree.getClass(), exprTree); + if (atypeFactory.isUnreachable(exprTree)) { + return true; + } + } Element elm = TreeUtils.elementFromTree(exprTree); return checker.shouldSkipUses(elm); } diff --git a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java index 3b374bb9109..1fa3e9813ae 100644 --- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java @@ -150,6 +150,9 @@ // org.checkerframework.framework.source.SourceChecker.report "warns", + // Make checker ignore the expression in dead branch + "notCheckDeadCode", + /// /// More sound (strict checking): enable errors that are disabled by default /// 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 b180997f2e2..1cf4732e343 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -458,7 +458,9 @@ public void setRoot(@Nullable CompilationUnitTree root) { super.setRoot(root); this.scannedClasses.clear(); - // this.reachableNodes.clear(); + if (checker.hasOption("notCheckDeadCode")) { + this.reachableNodes.clear(); + } this.flowResult = null; this.regularExitStores.clear(); this.exceptionalExitStores.clear(); @@ -1078,6 +1080,7 @@ public IPair getExpressionAndOffsetFromJavaExpressionStr * @param exprTree an expression tree * @return true if the {@code exprTree} is unreachable * + */ public boolean isUnreachable(ExpressionTree exprTree) { if (!everUseFlow) { return false; @@ -1096,7 +1099,6 @@ public boolean isUnreachable(ExpressionTree exprTree) { // None of the corresponding nodes is reachable, so this tree is dead. return true; } - */ /** * Track the state of org.checkerframework.dataflow analysis scanning for each class tree in the @@ -1120,7 +1122,7 @@ protected enum ScanState { * same name but represent different uses of the variable. So instead of storing Nodes, it * stores the result of {@code Node#getTree}. */ - // private final Set reachableNodes = new HashSet<>(); + private final Set reachableNodes = new HashSet<>(); /** * The result of the flow analysis. Invariant: @@ -1598,15 +1600,15 @@ protected void analyze( boolean isStatic, @Nullable Store capturedStore) { ControlFlowGraph cfg = CFCFGBuilder.build(root, ast, checker, this, processingEnv); - /* - cfg.getAllNodes(this::isIgnoredExceptionType) - .forEach( - node -> { - if (node.getTree() != null) { - reachableNodes.add(node.getTree()); - } - }); - */ + if (checker.hasOption("notCheckDeadCode")) { + cfg.getAllNodes(this::isIgnoredExceptionType) + .forEach( + node -> { + if (node.getTree() != null) { + reachableNodes.add(node.getTree()); + } + }); + } if (isInitializationCode) { Store initStore = !isStatic ? initializationStore : initializationStaticStore; if (initStore != null) { From 58f4773275dfa60da4457ce76be60d3cb19b24aa Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sat, 25 Nov 2023 13:27:06 -0500 Subject: [PATCH 2/6] change option name to ignoreCheckDeadCode --- .../checker/nullness/NullnessNoInitVisitor.java | 2 +- docs/CHANGELOG.md | 2 +- .../org/checkerframework/common/basetype/BaseTypeVisitor.java | 2 +- .../org/checkerframework/framework/source/SourceChecker.java | 2 +- .../framework/type/GenericAnnotatedTypeFactory.java | 4 ++-- 5 files changed, 6 insertions(+), 6 deletions(-) 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 a6b5890a197..d5cf91ebac6 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java @@ -290,7 +290,7 @@ protected boolean commonAssignmentCheck( /** Case 1: Check for null dereferencing. */ @Override public Void visitMemberSelect(MemberSelectTree tree, Void p) { - if (checker.hasOption("notCheckDeadCode")) { + if (checker.hasOption("ignoreCheckDeadCode")) { if (atypeFactory.isUnreachable(tree)) { return super.visitMemberSelect(tree, p); } diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 0478eb732e7..73261d6c8f8 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -3,7 +3,7 @@ Version 3.40.0-eisop3 (November ??, 2023) **User-visible changes:** -Add a new command-line argument `-AnotCheckDeadCode` disables the checker for code in dead expression. +Add a new command-line argument `-AignoreCheckDeadCode` disables the checker for code in dead expression. This option is not enabled by default. **Implementation details:** diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index 09a4e21b84b..6b11a2e45cb 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -5181,7 +5181,7 @@ protected TypeValidator createTypeValidator() { * @return true if checker should not test exprTree */ protected final boolean shouldSkipUses(ExpressionTree exprTree) { - if (checker.hasOption("notCheckDeadCode")) { + if (checker.hasOption("ignoreCheckDeadCode")) { System.out.printf("shouldSkipUses: %s: %s%n", exprTree.getClass(), exprTree); if (atypeFactory.isUnreachable(exprTree)) { return true; diff --git a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java index 1fa3e9813ae..23393865982 100644 --- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java @@ -151,7 +151,7 @@ "warns", // Make checker ignore the expression in dead branch - "notCheckDeadCode", + "ignoreCheckDeadCode", /// /// More sound (strict checking): enable errors that are disabled by default 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 1cf4732e343..7aabdd37181 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -458,7 +458,7 @@ public void setRoot(@Nullable CompilationUnitTree root) { super.setRoot(root); this.scannedClasses.clear(); - if (checker.hasOption("notCheckDeadCode")) { + if (checker.hasOption("ignoreCheckDeadCode")) { this.reachableNodes.clear(); } this.flowResult = null; @@ -1600,7 +1600,7 @@ protected void analyze( boolean isStatic, @Nullable Store capturedStore) { ControlFlowGraph cfg = CFCFGBuilder.build(root, ast, checker, this, processingEnv); - if (checker.hasOption("notCheckDeadCode")) { + if (checker.hasOption("ignoreCheckDeadCode")) { cfg.getAllNodes(this::isIgnoredExceptionType) .forEach( node -> { From 1d1c348e3d69bddc0c98407c486c819a8990c69c Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sat, 25 Nov 2023 13:48:33 -0500 Subject: [PATCH 3/6] add comment for entry point of the option --- .../org/checkerframework/framework/source/SourceChecker.java | 1 + 1 file changed, 1 insertion(+) diff --git a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java index 23393865982..c6cf6a9dc13 100644 --- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java @@ -151,6 +151,7 @@ "warns", // Make checker ignore the expression in dead branch + // org.checkerframework.framework.common.basetype.BaseTypeVisitor.shouldSkipUses "ignoreCheckDeadCode", /// From 2540cd301a1c598113e63b6555284a7e971228d8 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sat, 25 Nov 2023 13:49:15 -0500 Subject: [PATCH 4/6] add protect variable of checker option --- .../checker/nullness/NullnessNoInitVisitor.java | 2 +- .../checkerframework/common/basetype/BaseTypeVisitor.java | 6 +++++- .../framework/type/GenericAnnotatedTypeFactory.java | 8 ++++++-- 3 files changed, 12 insertions(+), 4 deletions(-) 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 d5cf91ebac6..9a30cdfe422 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java @@ -290,7 +290,7 @@ protected boolean commonAssignmentCheck( /** Case 1: Check for null dereferencing. */ @Override public Void visitMemberSelect(MemberSelectTree tree, Void p) { - if (checker.hasOption("ignoreCheckDeadCode")) { + if (ignoreCheckDeadCode) { if (atypeFactory.isUnreachable(tree)) { return super.visitMemberSelect(tree, p); } diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index 6b11a2e45cb..2ce337799cd 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -286,6 +286,9 @@ public class BaseTypeVisitor { From 02c69a8be518a51301734257c7d5a69be976e5dd Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sat, 25 Nov 2023 13:51:07 -0500 Subject: [PATCH 5/6] add * make javadoc happy --- .../framework/type/GenericAnnotatedTypeFactory.java | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) 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 0677e272f82..0c1cf588802 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -1077,13 +1077,12 @@ public IPair getExpressionAndOffsetFromJavaExpressionStr return value != null ? value.getAnnotations().iterator().next() : null; } - /* + /** * Returns true if the {@code exprTree} is unreachable. This is a conservative estimate and may * return {@code false} even though the {@code exprTree} is unreachable. * * @param exprTree an expression tree * @return true if the {@code exprTree} is unreachable - * */ public boolean isUnreachable(ExpressionTree exprTree) { if (!everUseFlow) { @@ -1118,7 +1117,7 @@ protected enum ScanState { /** Map from ClassTree to their dataflow analysis state. */ protected final Map scannedClasses = new HashMap<>(); - /* + /** * A set of trees whose corresponding nodes are reachable. This is not an exhaustive set of * reachable trees. Use {@link #isUnreachable(ExpressionTree)} instead of this set directly. * From 73de62f76aa5945cc59e6a7660cf0beaaa4023f7 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 27 Nov 2023 23:05:08 -0500 Subject: [PATCH 6/6] add deadbranch test case and skip the test first --- .../test/junit/NullnessDeadBranchTest.java | 30 ++++++++++++++++++ .../nullness-deadbranch/DeadBranchNPE.java | 31 +++++++++++++++++++ 2 files changed, 61 insertions(+) create mode 100644 checker/src/test/java/org/checkerframework/checker/test/junit/NullnessDeadBranchTest.java create mode 100644 checker/tests/nullness-deadbranch/DeadBranchNPE.java diff --git a/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessDeadBranchTest.java b/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessDeadBranchTest.java new file mode 100644 index 00000000000..f82b3cd8bba --- /dev/null +++ b/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessDeadBranchTest.java @@ -0,0 +1,30 @@ +package org.checkerframework.checker.test.junit; + +import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest; +import org.junit.runners.Parameterized; + +import java.io.File; +import java.util.List; + +/** + * JUnit tests for the Nullness checker when -AignoreCheckDeadCode command-line argument is used. + */ +public class NullnessDeadBranchTest extends CheckerFrameworkPerDirectoryTest { + /** + * Create a NullnessNullMarkedTest. + * + * @param testFiles the files containing test code, which will be type-checked + */ + public NullnessDeadBranchTest(List testFiles) { + super( + testFiles, + org.checkerframework.checker.nullness.NullnessChecker.class, + "nullness-deadbranch", + "-AignoreCheckDeadCode"); + } + + @Parameterized.Parameters + public static String[] getTestDirs() { + return new String[] {"nullness-deadbranch"}; + } +} diff --git a/checker/tests/nullness-deadbranch/DeadBranchNPE.java b/checker/tests/nullness-deadbranch/DeadBranchNPE.java new file mode 100644 index 00000000000..13d7f11e8e8 --- /dev/null +++ b/checker/tests/nullness-deadbranch/DeadBranchNPE.java @@ -0,0 +1,31 @@ +// @skip-test until the bug is fixed + +class DeadBranchNPE { + void test1() { + Object obj = null; + if (true) { + // :: error: (dereference.of.nullable) + obj.toString(); + } else { + obj.toString(); + } + } + + void test2() { + Object obj = null; + // :: error: (dereference.of.nullable) + obj.toString(); + for (int i = 0; i < 0; i++) { + obj.toString(); + } + } + + void test3() { + Object obj = null; + // :: error: (dereference.of.nullable) + obj.toString(); + while (obj != null) { + obj.toString(); + } + } +}