Handle while true (Fixes #3249) (#3389)

This PR fixes both issue #3249 and issue #1727, by adapting the CFG in the following way:

If the loop condition is checked to be a constant true  (according to the same logic in javac flow analysis), then the loop condition does not have an else-branch, i.e. the block holding the loop condition is directly followed by the one holding the loop entry, instead of followed by a conditional block.

Fixes #1727 and Fixes #3249`

checker/tests/nullness/flow/Issue1727.java

@@ -0,0 +1,31 @@
+// Test case for Issue 1727:
+// https://github.com/typetools/checker-framework/issues/1727
+
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+class B {}
+
+public class Issue1727 {
+
+    private B foo() {
+        // Default type for local variable b is @UnknownInitialization @Nullable
+        B b;
+
+        while (true) {
+            B op = getB();
+            if (op == null) {
+                b = new B();
+                break;
+            } else {
+                b = op;
+                break;
+            }
+        }
+
+        return b;
+    }
+
+    private @Nullable B getB() {
+        return new B();
+    }
+}

checker/tests/nullness/flow/Issue3249.java

@@ -0,0 +1,64 @@
+// Test case for Issue 3249:
+// https://github.com/typetools/checker-framework/issues/3249
+
+public class Issue3249 {
+
+    private final double field;
+
+    Issue3249() {
+        double local;
+        while (true) {
+            local = 1;
+            break;
+        }
+        field = local;
+    }
+
+    Issue3249(int x) {
+        double local;
+        while (!false) {
+            local = 1;
+            break;
+        }
+        field = local;
+    }
+
+    Issue3249(float x) {
+        double local;
+        while (true || x > 0) {
+            local = 1;
+            break;
+        }
+        field = local;
+    }
+
+    Issue3249(double x) {
+        double local;
+        while (!false && true && !false) {
+            local = 1;
+            break;
+        }
+        field = local;
+    }
+
+    // Case for while conditions that contain final variables,
+    // which are treated as constant.
+    Issue3249(String x) {
+        double local;
+        final int i = 1;
+        while ((i > 0) && !false) {
+            local = 1;
+            break;
+        }
+        field = local;
+    }
+
+    Issue3249(boolean x) {
+        double local;
+        while (6 > 4) {
+            local = 1;
+            break;
+        }
+        field = local;
+    }
+}

dataflow/src/main/java/org/checkerframework/dataflow/cfg/CFGBuilder.java

@@ -61,6 +61,7 @@
 import com.sun.tools.javac.code.Symbol.MethodSymbol;
 import com.sun.tools.javac.code.Type;
 import com.sun.tools.javac.processing.JavacProcessingEnvironment;
+import com.sun.tools.javac.tree.TreeInfo;
 import com.sun.tools.javac.util.Context;
 import java.util.ArrayDeque;
 import java.util.ArrayList;
@@ -4913,15 +4914,32 @@ public Node visitWhileLoop(WhileLoopTree tree, Void p) {
             // Condition
             addLabelForNextNode(conditionStart);
             assert tree.getCondition() != null;
+            // Determine whether the loop condition has the constant value true, according to the
+            // compiler logic.
+            boolean isCondConstTrue = TreeUtils.isExprConstTrue(tree.getCondition());
+
             unbox(scan(tree.getCondition(), p));
-            ConditionalJump cjump = new ConditionalJump(loopEntry, loopExit);
-            extendWithExtendedNode(cjump);
+
+            if (!isCondConstTrue) {
+                // If the loop condition does not have the constant value true, the control flow is
+                // split into two branches.
+                ConditionalJump cjump = new ConditionalJump(loopEntry, loopExit);
+                extendWithExtendedNode(cjump);
+            }
 
             // Loop body
             addLabelForNextNode(loopEntry);
             assert tree.getStatement() != null;
             scan(tree.getStatement(), p);
-            extendWithExtendedNode(new UnconditionalJump(conditionStart));
+
+            if (isCondConstTrue) {
+                // The condition has the constant value true, so we can directly jump back to the
+                // loop entry.
+                extendWithExtendedNode(new UnconditionalJump(loopEntry));
+            } else {
+                // Otherwise, jump back to evaluate the condition.
+                extendWithExtendedNode(new UnconditionalJump(conditionStart));
+            }
 
             // Loop exit
             addLabelForNextNode(loopExit);

javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java

@@ -37,6 +37,8 @@
 import com.sun.tools.javac.tree.JCTree;
 import com.sun.tools.javac.tree.JCTree.JCAnnotatedType;
 import com.sun.tools.javac.tree.JCTree.JCAnnotation;
+import com.sun.tools.javac.tree.JCTree.JCBinary;
+import com.sun.tools.javac.tree.JCTree.JCExpression;
 import com.sun.tools.javac.tree.JCTree.JCExpressionStatement;
 import com.sun.tools.javac.tree.JCTree.JCLambda;
 import com.sun.tools.javac.tree.JCTree.JCLambda.ParameterKind;
@@ -1390,4 +1392,33 @@ public static boolean isImplicitlyTypedLambda(Tree tree) {
         return tree.getKind() == Kind.LAMBDA_EXPRESSION
                 && ((JCLambda) tree).paramKind == ParameterKind.IMPLICIT;
     }
+
+    /**
+     * Determine whether an expression {@link ExpressionTree} has the constant value true, according
+     * to the compiler logic.
+     *
+     * @param node the expression to be checked.
+     * @return true if {@code node} has the constant value true.
+     */
+    public static boolean isExprConstTrue(final ExpressionTree node) {
+        assert node instanceof JCExpression;
+        if (((JCExpression) node).type.isTrue()) {
+            return true;
+        }
+        ExpressionTree tree = TreeUtils.withoutParens(node);
+        if (tree instanceof JCTree.JCBinary) {
+            JCBinary binTree = (JCBinary) tree;
+            JCExpression ltree = binTree.lhs;
+            JCExpression rtree = binTree.rhs;
+            switch (binTree.getTag()) {
+                case AND:
+                    return isExprConstTrue(ltree) && isExprConstTrue(rtree);
+                case OR:
+                    return isExprConstTrue(ltree) || isExprConstTrue(rtree);
+                default:
+                    break;
+            }
+        }
+        return false;
+    }
 }