fix typetools/checker-framework issue#3249 #132

d367wang · 2020-05-19T21:22:00Z

wmdietl

Thanks for working on this fix!
Can you add test cases for typetools#1727 and typetools#3249 to show that the issue is actually fixed?

wmdietl · 2020-05-21T01:00:46Z

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

+                        output += "boolean literal is true\n";
+                        isWhileTrue = true;
+                    } else {
+                        if (nodeList.size() > firstConditionPos + 1) {


Does javac treat while (!false) as a special case?
Is it really worth handling such unusual code?

wmdietl · 2020-05-21T01:02:26Z

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

+
+            boolean isWhileTrue = false;
+            int firstConditionPos = nodeList.size();
+            String output = "First condition position" + String.valueOf(firstConditionPos) + "\n";


You can remove the debug output and the commented-out assert below.

wmdietl · 2020-05-21T01:03:18Z

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

@@ -4878,8 +4878,34 @@ public Node visitWhileLoop(WhileLoopTree tree, Void p) {

            // Condition
            addLabelForNextNode(conditionStart);
+
+            boolean isWhileTrue = false;
+            int firstConditionPos = nodeList.size();


Instead of going through the converted nodes, wouldn't it be easier to just look at the condition tree and see whether it's the literal true?

…into issue-cfg-while-true

wmdietl · 2020-06-07T19:04:08Z

checker/tests/nullness/flow/Issue1727.java

+
+        while (true) {
+            B op = getB();
+            // :: warning: (known.nonnull)


Instead you could make the return type of getB @Nullable B. Otherwise the example isn't very convincing...

wmdietl · 2020-06-07T19:09:18Z

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

+
+            // Is condition constant true?
+            boolean isWhileTrue = false;
+
            if (tree.getCondition() != null) {


I don't think the condition tree could ever be null, could it?
So maybe change this to

if (tree.getCondition() == null) { raise error; }

Then you can move the declaration of isWhileTrue to line 4906 and simply have boolean isWhileTrue = condType.isTrue() and avoid the unnecessary initialization with false.

wmdietl · 2020-06-07T19:09:34Z

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

-                extendWithExtendedNode(cjump);
+
+                if (!isWhileTrue) {
+                    ConditionalJump cjump = new ConditionalJump(loopEntry, loopExit);


Add a comment here to explain why we do this.

wmdietl · 2020-06-07T19:10:28Z

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

-            extendWithExtendedNode(new UnconditionalJump(conditionStart));
+
+            // If the condition is constant true, the successor of loop end is loop entry, instead
+            // of condition start


End the sentence with .

wmdietl · 2020-06-07T19:10:52Z

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

            }

            // Loop body
            addLabelForNextNode(loopEntry);
            if (tree.getStatement() != null) {
                scan(tree.getStatement(), p);
            }
-            extendWithExtendedNode(new UnconditionalJump(conditionStart));
+
+            // If the condition is constant true, the successor of loop end is loop entry, instead


What is the effect of this change? Is it really necessary to skip the condition for a while true?

In fact, Javac bytecode generator merges the control flow at the end of the loop body with the condition start, so this change is just an optimization.

checker/tests/nullness/flow/Issue3249.java

…ases

wmdietl

A few more small comments to address.
Once they are and tests pass, please make a PR against typetools and we'll continue there.

wmdietl · 2020-06-09T00:21:38Z

checker/tests/nullness/flow/Issue3249.java

+            local = 1;
+            break;
+        }
+        // :: error: (assignment.type.incompatible)


Interesting that this isn't a constant... do you understand why? If you do, add a comment to explain.

wmdietl · 2020-06-09T00:22:42Z

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

-            if (tree.getCondition() != null) {
-                unbox(scan(tree.getCondition(), p));
+
+            // Is condition constant true?


This comment should go to the declaration of isWhileTrue a bit further down.

Actually, there is already documentation down there, so just remove this.

wmdietl · 2020-06-09T03:53:36Z

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

-                unbox(scan(tree.getCondition(), p));
+
+            // Is condition constant true?
+            assert tree.getCondition() != null : "while loop condition must not be null";


I've made this change throughout in typetools#3364
I didn't add descriptions, so to avoid a merge problem maybe remove the one here as well.

wmdietl · 2020-06-09T03:56:04Z

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

+
+            // Is condition constant true?
+            assert tree.getCondition() != null : "while loop condition must not be null";
+            // Check whether the loop condition is constant true, the criteria is consistent with


How about Determine whether loop condition is a constant true, according to the compiler logic.?

wmdietl · 2020-06-09T03:56:48Z

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

+
+            unbox(scan(tree.getCondition(), p));
+
+            // If the loop condition is not constant true, the control flow is split into two


Move this comment into the then block.

wmdietl · 2020-06-09T04:00:05Z

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

@@ -4908,7 +4919,15 @@ public Node visitWhileLoop(WhileLoopTree tree, Void p) {
            if (tree.getStatement() != null) {
                scan(tree.getStatement(), p);
            }
-            extendWithExtendedNode(new UnconditionalJump(conditionStart));
+
+            // If the condition is constant true, for the purpose of improving the dataflow analysis


I find the performance argument rather weak - it's a constant true expression.
I would add a brief comment to the then and else block, just stating something like:
then: The condition is constant true so we can directly jump back to the loop entry.
else: Otherwise, jump back to evaluate the condition.

… true

wmdietl

This looks very nice now! Please close the PR here and move it to typetools.

wmdietl · 2020-06-18T01:19:03Z

New PR is here typetools#3389

fix issue 3249

91cce6f

wmdietl requested changes May 21, 2020

View reviewed changes

wmdietl assigned d367wang May 21, 2020

d367wang added 3 commits June 6, 2020 03:43

add test cases

6f3c1a6

Merge branch 'master' of https://github.com/opprop/checker-framework …

f450ecb

…into issue-cfg-while-true

adapt test case for --warning-mode all

b0f3acd

wmdietl requested changes Jun 7, 2020

View reviewed changes

complete comments for logic of building CFG involving ; modify test c…

c369284

…ases

d367wang requested a review from wmdietl June 8, 2020 23:59

wmdietl requested changes Jun 9, 2020

View reviewed changes

d367wang added 2 commits June 15, 2020 04:47

adapt logic of determining whether a while loop condition is constant…

407e6c8

… true

fix error: missing default case for switch statement

39f3591

d367wang requested a review from wmdietl June 15, 2020 10:02

wmdietl added 2 commits June 15, 2020 13:52

Tweaks

85e5514

Tweaks

d494459

wmdietl approved these changes Jun 15, 2020

View reviewed changes

d367wang closed this Jun 17, 2020

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

fix typetools/checker-framework issue#3249 #132

fix typetools/checker-framework issue#3249 #132

d367wang commented May 19, 2020 •

edited

Loading

wmdietl left a comment

wmdietl May 21, 2020

wmdietl May 21, 2020

wmdietl May 21, 2020

wmdietl Jun 7, 2020

wmdietl Jun 7, 2020

wmdietl Jun 7, 2020

wmdietl Jun 7, 2020

wmdietl Jun 7, 2020

d367wang Jun 7, 2020

wmdietl left a comment

wmdietl Jun 9, 2020

wmdietl Jun 9, 2020

wmdietl Jun 9, 2020

wmdietl Jun 9, 2020

wmdietl Jun 9, 2020

wmdietl Jun 9, 2020

wmdietl Jun 9, 2020

wmdietl left a comment

wmdietl commented Jun 18, 2020


		unbox(scan(tree.getCondition(), p));

		// If the loop condition is not constant true, the control flow is split into two

fix typetools/checker-framework issue#3249 #132

fix typetools/checker-framework issue#3249 #132

Conversation

d367wang commented May 19, 2020 • edited Loading

wmdietl left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

wmdietl left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

wmdietl left a comment

Choose a reason for hiding this comment

wmdietl commented Jun 18, 2020

d367wang commented May 19, 2020 •

edited

Loading