From 71024563a598426d35e3a2a2ce287115de7b2a2c Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sat, 25 Nov 2023 08:58:11 -0500 Subject: [PATCH 01/17] 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 68a9362ee9ea..a6b5890a1974 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 50bd076ed038..780d784c8e5e 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 6b61e7397a46..09a4e21b84b1 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 3b374bb91094..1fa3e9813ae2 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 b180997f2e23..1cf4732e3434 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 02/17] 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 a6b5890a1974..d5cf91ebac61 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 0478eb732e76..73261d6c8f80 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 09a4e21b84b1..6b11a2e45cbc 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 1fa3e9813ae2..233938659824 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 1cf4732e3434..7aabdd371817 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 03/17] 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 233938659824..c6cf6a9dc13c 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 04/17] 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 d5cf91ebac61..9a30cdfe4228 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 6b11a2e45cbc..2ce337799cd5 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 05/17] 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 0677e272f825..0c1cf5888023 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 06/17] 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 000000000000..f82b3cd8bba8 --- /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 000000000000..13d7f11e8e89 --- /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(); + } + } +} From 63920135a6190c14a18eb448566e2ff6273d3a46 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 16 Dec 2024 23:55:53 -0500 Subject: [PATCH 07/17] Address all comments --- .../checker/nullness/NullnessNoInitVisitor.java | 6 ++---- .../checker/test/junit/NullnessDeadBranchTest.java | 10 ++++------ .../DeadBranchNPE.java | 3 +-- docs/CHANGELOG.md | 5 ++--- docs/manual/introduction.tex | 2 ++ .../common/basetype/BaseTypeVisitor.java | 14 ++++++-------- .../framework/source/SourceChecker.java | 2 +- .../framework/type/AnnotatedTypeFactory.java | 2 +- .../type/GenericAnnotatedTypeFactory.java | 8 ++++---- 9 files changed, 23 insertions(+), 29 deletions(-) rename checker/tests/{nullness-deadbranch => nullness-ignoredeadcode}/DeadBranchNPE.java (88%) 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 7b11f203f3e0..b14832be5752 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java @@ -299,10 +299,8 @@ protected boolean commonAssignmentCheck( /** Case 1: Check for null dereferencing. */ @Override public Void visitMemberSelect(MemberSelectTree tree, Void p) { - if (ignoreCheckDeadCode) { - if (atypeFactory.isUnreachable(tree)) { - return super.visitMemberSelect(tree, p); - } + if (ignoreDeadCode && atypeFactory.isUnreachable(tree)) { + return super.visitMemberSelect(tree, p); } Element e = TreeUtils.elementFromUse(tree); if (e.getKind() == ElementKind.CLASS) { 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 index f82b3cd8bba8..6a8a09245247 100644 --- a/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessDeadBranchTest.java +++ b/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessDeadBranchTest.java @@ -6,9 +6,7 @@ import java.io.File; import java.util.List; -/** - * JUnit tests for the Nullness checker when -AignoreCheckDeadCode command-line argument is used. - */ +/** JUnit tests for the Nullness checker when -AignoreDeadCode command-line argument is used. */ public class NullnessDeadBranchTest extends CheckerFrameworkPerDirectoryTest { /** * Create a NullnessNullMarkedTest. @@ -19,12 +17,12 @@ public NullnessDeadBranchTest(List testFiles) { super( testFiles, org.checkerframework.checker.nullness.NullnessChecker.class, - "nullness-deadbranch", - "-AignoreCheckDeadCode"); + "nullness-ignoredeadcode", + "-AignoreDeadCode"); } @Parameterized.Parameters public static String[] getTestDirs() { - return new String[] {"nullness-deadbranch"}; + return new String[] {"nullness-ignoredeadcode"}; } } diff --git a/checker/tests/nullness-deadbranch/DeadBranchNPE.java b/checker/tests/nullness-ignoredeadcode/DeadBranchNPE.java similarity index 88% rename from checker/tests/nullness-deadbranch/DeadBranchNPE.java rename to checker/tests/nullness-ignoredeadcode/DeadBranchNPE.java index 13d7f11e8e89..fee6745beda3 100644 --- a/checker/tests/nullness-deadbranch/DeadBranchNPE.java +++ b/checker/tests/nullness-ignoredeadcode/DeadBranchNPE.java @@ -1,5 +1,3 @@ -// @skip-test until the bug is fixed - class DeadBranchNPE { void test1() { Object obj = null; @@ -15,6 +13,7 @@ void test2() { Object obj = null; // :: error: (dereference.of.nullable) obj.toString(); + // The following loop is dead code because the loop condition is false. for (int i = 0; i < 0; i++) { obj.toString(); } diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index aee477e523a0..a071807aab87 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -2,9 +2,8 @@ Version 3.42.0-eisop5 (November ??, 2024) ----------------------------------------- **User-visible changes:** - -Add a new command-line argument `-AignoreCheckDeadCode` disables the checker for code in dead expression. -This option is not enabled by default. +New command-line options: +* `-AignoreDeadCode`: Ignore unreachable code when running Checkers. Removed support for the `-Anocheckjdk` option, which was deprecated in version 3.1.1. Use `-ApermitMissingJdk` instead. diff --git a/docs/manual/introduction.tex b/docs/manual/introduction.tex index f5374c84eb6a..f06d0174ccc5 100644 --- a/docs/manual/introduction.tex +++ b/docs/manual/introduction.tex @@ -596,6 +596,8 @@ which is a javac argument to halt compilation if a warning is issued. \item \<-AignoreInvalidAnnotationLocations> Ignore annotations in bytecode that have invalid annotation locations. +\item \<-AignoreDeadCode> +Ignore unreachable code when running Checkers. \end{itemize} \label{unsound-by-default} 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 733159f2a9a3..03c199c16397 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -290,8 +290,8 @@ public class BaseTypeVisitor { From decd355f6bdb5d72d75deb364f85b031628c5fc8 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 16 Dec 2024 23:57:57 -0500 Subject: [PATCH 08/17] Rename Junit test file --- ...essDeadBranchTest.java => NullnessIgnoreDeadCodeTest.java} | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) rename checker/src/test/java/org/checkerframework/checker/test/junit/{NullnessDeadBranchTest.java => NullnessIgnoreDeadCodeTest.java} (84%) diff --git a/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessDeadBranchTest.java b/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessIgnoreDeadCodeTest.java similarity index 84% rename from checker/src/test/java/org/checkerframework/checker/test/junit/NullnessDeadBranchTest.java rename to checker/src/test/java/org/checkerframework/checker/test/junit/NullnessIgnoreDeadCodeTest.java index 6a8a09245247..a3b8e07068ec 100644 --- a/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessDeadBranchTest.java +++ b/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessIgnoreDeadCodeTest.java @@ -7,13 +7,13 @@ import java.util.List; /** JUnit tests for the Nullness checker when -AignoreDeadCode command-line argument is used. */ -public class NullnessDeadBranchTest extends CheckerFrameworkPerDirectoryTest { +public class NullnessIgnoreDeadCodeTest extends CheckerFrameworkPerDirectoryTest { /** * Create a NullnessNullMarkedTest. * * @param testFiles the files containing test code, which will be type-checked */ - public NullnessDeadBranchTest(List testFiles) { + public NullnessIgnoreDeadCodeTest(List testFiles) { super( testFiles, org.checkerframework.checker.nullness.NullnessChecker.class, From f7b1bb5d6ba62ac3673c695b3f7387bd6379b867 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 16 Dec 2024 22:32:00 -0800 Subject: [PATCH 09/17] Use getter and revert access modifier for root --- .../org/checkerframework/common/basetype/BaseTypeVisitor.java | 2 +- .../checkerframework/framework/type/AnnotatedTypeFactory.java | 2 +- .../framework/type/GenericAnnotatedTypeFactory.java | 3 ++- 3 files changed, 4 insertions(+), 3 deletions(-) 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 03c199c16397..823d1a28b01c 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -5201,7 +5201,7 @@ 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); + // System.out.printf("shouldSkipUses: %s: %s%n", exprTree.getClass(), exprTree); if (ignoreDeadCode && atypeFactory.isUnreachable(exprTree)) { return true; } 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 e0c20c12d9df..c8831335be35 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -181,7 +181,7 @@ public class AnnotatedTypeFactory implements AnnotationProvider { // TODO: when should root be null? What are the use cases? // None of the existing test checkers has a null root. // Should not be modified between calls to "visit". - protected @Nullable CompilationUnitTree root; + private @Nullable CompilationUnitTree root; /** The processing environment to use for accessing compiler internals. */ protected final ProcessingEnvironment processingEnv; 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 039643c57b00..f7bd07708848 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -1615,7 +1615,8 @@ protected void analyze( boolean updateInitializationStore, boolean isStatic, @Nullable Store capturedStore) { - ControlFlowGraph cfg = CFCFGBuilder.build(root, ast, checker, this, processingEnv); + ControlFlowGraph cfg = + CFCFGBuilder.build(this.getRoot(), ast, checker, this, processingEnv); if (ignoreDeadCode) { cfg.getAllNodes(this::isIgnoredExceptionType) .forEach( From a93748bbe550f34ca8af92cad566f24f2c9b820c Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 16 Dec 2024 22:36:40 -0800 Subject: [PATCH 10/17] Comment first... --- checker/tests/nullness-ignoredeadcode/DeadBranchNPE.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/checker/tests/nullness-ignoredeadcode/DeadBranchNPE.java b/checker/tests/nullness-ignoredeadcode/DeadBranchNPE.java index fee6745beda3..5c15646c08f6 100644 --- a/checker/tests/nullness-ignoredeadcode/DeadBranchNPE.java +++ b/checker/tests/nullness-ignoredeadcode/DeadBranchNPE.java @@ -5,7 +5,8 @@ void test1() { // :: error: (dereference.of.nullable) obj.toString(); } else { - obj.toString(); + // TODO: This is a dead branch should not issue error, the currently it does + // obj.toString(); } } From 1576672e61f70e392ccadcc07185f0da87a22a71 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Tue, 17 Dec 2024 07:30:08 -0800 Subject: [PATCH 11/17] Javadoc --- .../checker/test/junit/NullnessIgnoreDeadCodeTest.java | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessIgnoreDeadCodeTest.java b/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessIgnoreDeadCodeTest.java index a3b8e07068ec..7aaf9393b8b4 100644 --- a/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessIgnoreDeadCodeTest.java +++ b/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessIgnoreDeadCodeTest.java @@ -21,6 +21,11 @@ public NullnessIgnoreDeadCodeTest(List testFiles) { "-AignoreDeadCode"); } + /** + * Returns an array of test directory paths for parameterized testing. + * + * @return an array containing the test directory names + */ @Parameterized.Parameters public static String[] getTestDirs() { return new String[] {"nullness-ignoredeadcode"}; From fa183ecd6d32c7fe99bdf2a5afd2fb8596314fb6 Mon Sep 17 00:00:00 2001 From: Werner Dietl Date: Tue, 31 Dec 2024 13:03:52 -0500 Subject: [PATCH 12/17] Update CHANGELOG.md --- docs/CHANGELOG.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index f98634a75f19..03ba80004d10 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -3,6 +3,8 @@ Version 3.42.0-eisop6 (January ??, 2025) **User-visible changes:** +New command-line option `-AignoreDeadCode` to ignore unreachable code when running checkers. + **Implementation details:** **Closed issues:** @@ -14,8 +16,6 @@ Version 3.42.0-eisop5 (December 20, 2024) ----------------------------------------- **User-visible changes:** -New command-line options: -* `-AignoreDeadCode`: Ignore unreachable code when running Checkers. Removed support for the `-Anocheckjdk` option, which was deprecated in version 3.1.1. Use `-ApermitMissingJdk` instead. From f678255708474341cca13e27574c0021156e3bb9 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Tue, 31 Dec 2024 10:52:11 -0800 Subject: [PATCH 13/17] Wording Co-authored-by: Werner Dietl --- .../checker/test/junit/NullnessIgnoreDeadCodeTest.java | 4 ++-- docs/manual/introduction.tex | 2 +- .../org/checkerframework/framework/source/SourceChecker.java | 2 +- .../framework/type/GenericAnnotatedTypeFactory.java | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessIgnoreDeadCodeTest.java b/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessIgnoreDeadCodeTest.java index 7aaf9393b8b4..1273e81062d2 100644 --- a/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessIgnoreDeadCodeTest.java +++ b/checker/src/test/java/org/checkerframework/checker/test/junit/NullnessIgnoreDeadCodeTest.java @@ -6,10 +6,10 @@ import java.io.File; import java.util.List; -/** JUnit tests for the Nullness checker when -AignoreDeadCode command-line argument is used. */ +/** JUnit tests for the Nullness Checker when the -AignoreDeadCode command-line argument is used. */ public class NullnessIgnoreDeadCodeTest extends CheckerFrameworkPerDirectoryTest { /** - * Create a NullnessNullMarkedTest. + * Create a NullnessIgnoreDeadCodeTest. * * @param testFiles the files containing test code, which will be type-checked */ diff --git a/docs/manual/introduction.tex b/docs/manual/introduction.tex index 6a01a73f59fa..30382796f23b 100644 --- a/docs/manual/introduction.tex +++ b/docs/manual/introduction.tex @@ -600,7 +600,7 @@ Disables validating the target locations of qualifiers based on `@TargetLocations` meta-annotations. This option is not enabled by default. \item \<-AignoreDeadCode> -Ignore unreachable code when running Checkers. + Ignore unreachable code when running checkers. \end{itemize} \label{unsound-by-default} 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 dab420e21410..a06d1f39d001 100644 --- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java @@ -152,7 +152,7 @@ // org.checkerframework.framework.source.SourceChecker.report "warns", - // Make checker ignore the expression in dead branch + // Ignore dead code // org.checkerframework.framework.common.basetype.BaseTypeVisitor.shouldSkipUses "ignoreDeadCode", 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 ad3f3ba71e63..fc50adf15f63 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -275,7 +275,7 @@ public abstract class GenericAnnotatedTypeFactory< */ public final boolean hasOrIsSubchecker; - /** True if "-AigoreCheckDeadCode" was passed on the command line. */ + /** True if "-AignoreDeadCode" was passed on the command line. */ protected final boolean ignoreDeadCode; /** An empty store. */ From 2117ffcdb6412c19239e74bba95601899fe57ad0 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sat, 4 Jan 2025 21:53:27 -0500 Subject: [PATCH 14/17] Skip the test util we add dead branch analysis --- .../nullness-ignoredeadcode/DeadBranchNPE.java | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/checker/tests/nullness-ignoredeadcode/DeadBranchNPE.java b/checker/tests/nullness-ignoredeadcode/DeadBranchNPE.java index 5c15646c08f6..40ebf180d504 100644 --- a/checker/tests/nullness-ignoredeadcode/DeadBranchNPE.java +++ b/checker/tests/nullness-ignoredeadcode/DeadBranchNPE.java @@ -1,3 +1,4 @@ +// @skip-test until we add dead branch analysis class DeadBranchNPE { void test1() { Object obj = null; @@ -5,27 +6,28 @@ void test1() { // :: error: (dereference.of.nullable) obj.toString(); } else { - // TODO: This is a dead branch should not issue error, the currently it does - // obj.toString(); + obj.toString(); } } void test2() { - Object obj = null; + Object objOut = null; + object objInner = null; // :: error: (dereference.of.nullable) - obj.toString(); + objOut.toString(); // The following loop is dead code because the loop condition is false. for (int i = 0; i < 0; i++) { - obj.toString(); + objInner.toString(); } } void test3() { - Object obj = null; + Object objOut = null; + object objInner = null; // :: error: (dereference.of.nullable) - obj.toString(); + objOut.toString(); while (obj != null) { - obj.toString(); + objInner.toString(); } } } From aff74851a5f3ce607aee50720e118f8f2b994de5 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sat, 4 Jan 2025 21:54:18 -0500 Subject: [PATCH 15/17] Add test case for normal nullness checker --- checker/tests/nullness/DeadBranchNPE.java | 35 +++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 checker/tests/nullness/DeadBranchNPE.java diff --git a/checker/tests/nullness/DeadBranchNPE.java b/checker/tests/nullness/DeadBranchNPE.java new file mode 100644 index 000000000000..d952af88baa7 --- /dev/null +++ b/checker/tests/nullness/DeadBranchNPE.java @@ -0,0 +1,35 @@ +class DeadBranchNPE { + void test1() { + Object obj = null; + if (true) { + // :: error: (dereference.of.nullable) + obj.toString(); + } else { + // :: error: (dereference.of.nullable) + obj.toString(); + } + } + + void test2() { + Object objOut = null; + object objInner = null; + // :: error: (dereference.of.nullable) + objOut.toString(); + // The following loop is dead code because the loop condition is false. + for (int i = 0; i < 0; i++) { + // :: error: (dereference.of.nullable) + objInner.toString(); + } + } + + void test3() { + Object objOut = null; + object objInner = null; + // :: error: (dereference.of.nullable) + objOut.toString(); + while (obj != null) { + // :: error: (dereference.of.nullable) + objInner.toString(); + } + } +} From bf1652c13b0150d3d007060543dce2ac7045c0ac Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sat, 4 Jan 2025 22:36:16 -0500 Subject: [PATCH 16/17] Fixes the test cases --- checker/tests/nullness-ignoredeadcode/DeadBranchNPE.java | 9 ++++++--- checker/tests/nullness/DeadBranchNPE.java | 6 +++--- 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/checker/tests/nullness-ignoredeadcode/DeadBranchNPE.java b/checker/tests/nullness-ignoredeadcode/DeadBranchNPE.java index 40ebf180d504..d061a41fdb64 100644 --- a/checker/tests/nullness-ignoredeadcode/DeadBranchNPE.java +++ b/checker/tests/nullness-ignoredeadcode/DeadBranchNPE.java @@ -6,27 +6,30 @@ void test1() { // :: error: (dereference.of.nullable) obj.toString(); } else { + // :: error: (dereference.of.nullable) obj.toString(); } } void test2() { Object objOut = null; - object objInner = null; + Object objInner = null; // :: error: (dereference.of.nullable) objOut.toString(); // The following loop is dead code because the loop condition is false. for (int i = 0; i < 0; i++) { + // :: error: (dereference.of.nullable) objInner.toString(); } } void test3() { Object objOut = null; - object objInner = null; + Object objInner = null; // :: error: (dereference.of.nullable) objOut.toString(); - while (obj != null) { + while (objOut != null) { + // :: error: (dereference.of.nullable) objInner.toString(); } } diff --git a/checker/tests/nullness/DeadBranchNPE.java b/checker/tests/nullness/DeadBranchNPE.java index d952af88baa7..afcbea207089 100644 --- a/checker/tests/nullness/DeadBranchNPE.java +++ b/checker/tests/nullness/DeadBranchNPE.java @@ -12,7 +12,7 @@ void test1() { void test2() { Object objOut = null; - object objInner = null; + Object objInner = null; // :: error: (dereference.of.nullable) objOut.toString(); // The following loop is dead code because the loop condition is false. @@ -24,10 +24,10 @@ void test2() { void test3() { Object objOut = null; - object objInner = null; + Object objInner = null; // :: error: (dereference.of.nullable) objOut.toString(); - while (obj != null) { + while (objOut != null) { // :: error: (dereference.of.nullable) objInner.toString(); } From 85d3a9ae339c65eddf5b6325f0e8c6960a7aef54 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sat, 4 Jan 2025 22:47:37 -0500 Subject: [PATCH 17/17] Extra warning --- checker/tests/nullness/DeadBranchNPE.java | 1 + 1 file changed, 1 insertion(+) diff --git a/checker/tests/nullness/DeadBranchNPE.java b/checker/tests/nullness/DeadBranchNPE.java index afcbea207089..e51a98372262 100644 --- a/checker/tests/nullness/DeadBranchNPE.java +++ b/checker/tests/nullness/DeadBranchNPE.java @@ -27,6 +27,7 @@ void test3() { Object objInner = null; // :: error: (dereference.of.nullable) objOut.toString(); + // :: warning: (nulltest.redundant) while (objOut != null) { // :: error: (dereference.of.nullable) objInner.toString();