Adding notcheckdeadcode option

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 (ignoreCheckDeadCode) {
+            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())) {

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<File> testFiles) {
+        super(
+                testFiles,
+                org.checkerframework.checker.nullness.NullnessChecker.class,
+                "nullness-deadbranch",
+                "-AignoreCheckDeadCode");
+    }
+
+    @Parameterized.Parameters
+    public static String[] getTestDirs() {
+        return new String[] {"nullness-deadbranch"};
+    }
+}

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();
+        }
+    }
+}

docs/CHANGELOG.md

@@ -3,6 +3,9 @@ Version 3.40.0-eisop3 (November ??, 2023)
 
 **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.
+
 **Implementation details:**
 
 **Closed issues:**

framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java

@@ -286,6 +286,9 @@ public class BaseTypeVisitor<Factory extends GenericAnnotatedTypeFactory<?, ?, ?
     /** True if "-AcheckEnclosingExpr" was passed on the command line. */
     private final boolean checkEnclosingExpr;
 
+    /** True if "-AigoreCheckDeadCode" was passed on the command line. */
+    protected final boolean ignoreCheckDeadCode;
+
     /** The tree of the enclosing method that is currently being visited. */
     protected @Nullable MethodTree methodTree = null;
 
@@ -346,6 +349,7 @@ protected BaseTypeVisitor(BaseTypeChecker checker, @Nullable Factory typeFactory
         checkCastElementType = checker.hasOption("checkCastElementType");
         conservativeUninferredTypeArguments =
                 checker.hasOption("conservativeUninferredTypeArguments");
+        ignoreCheckDeadCode = checker.hasOption("ignoreCheckDeadCode");
     }
 
     /** An array containing just {@code BaseTypeChecker.class}. */
@@ -5181,10 +5185,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 (ignoreCheckDeadCode) {
+            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);
     }

framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java

@@ -150,6 +150,10 @@
     // org.checkerframework.framework.source.SourceChecker.report
     "warns",
 
+    // Make checker ignore the expression in dead branch
+    // org.checkerframework.framework.common.basetype.BaseTypeVisitor.shouldSkipUses
+    "ignoreCheckDeadCode",
+
     ///
     /// More sound (strict checking): enable errors that are disabled by default
     ///

framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java

@@ -273,6 +273,9 @@ public abstract class GenericAnnotatedTypeFactory<
      */
     public final boolean hasOrIsSubchecker;
 
+    /** True if "-AigoreCheckDeadCode" was passed on the command line. */
+    protected final boolean ignoreCheckDeadCode;
+
     /** An empty store. */
     // Set in postInit only
     protected Store emptyStore;
@@ -394,6 +397,7 @@ protected GenericAnnotatedTypeFactory(BaseTypeChecker checker, boolean useFlow)
         hasOrIsSubchecker =
                 !this.getChecker().getSubcheckers().isEmpty()
                         || this.getChecker().getParentChecker() != null;
+        ignoreCheckDeadCode = checker.hasOption("ignoreCheckDeadCode");
 
         // Every subclass must call postInit, but it must be called after
         // all other initialization is finished.
@@ -458,7 +462,9 @@ public void setRoot(@Nullable CompilationUnitTree root) {
 
         super.setRoot(root);
         this.scannedClasses.clear();
-        // this.reachableNodes.clear();
+        if (ignoreCheckDeadCode) {
+            this.reachableNodes.clear();
+        }
         this.flowResult = null;
         this.regularExitStores.clear();
         this.exceptionalExitStores.clear();
@@ -1071,13 +1077,13 @@ public IPair<JavaExpression, String> 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) {
             return false;
@@ -1096,7 +1102,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
@@ -1112,15 +1117,15 @@ protected enum ScanState {
     /** Map from ClassTree to their dataflow analysis state. */
     protected final Map<ClassTree, ScanState> 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.
      *
      * <p>This cannot be a set of Nodes, because two LocalVariableNodes are equal if they have the
      * 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<Tree> reachableNodes = new HashSet<>();
+    private final Set<Tree> reachableNodes = new HashSet<>();
 
     /**
      * The result of the flow analysis. Invariant:
@@ -1598,15 +1603,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 (ignoreCheckDeadCode) {
+            cfg.getAllNodes(this::isIgnoredExceptionType)
+                    .forEach(
+                            node -> {
+                                if (node.getTree() != null) {
+                                    reachableNodes.add(node.getTree());
+                                }
+                            });
+        }
         if (isInitializationCode) {
             Store initStore = !isStatic ? initializationStore : initializationStaticStore;
             if (initStore != null) {