Introduce bottom store to improve dataflow analysis #167

d367wang · 2021-04-01T16:25:36Z

The bottom store has the following properties:

The LUB of a bottom store and a second store is the second store.
A bottom store is immutable once it's created. i.e. It doesn't support insertion, replacement and other forms of updating.
When getting value from a bottom store, it always returns the bottom value (consisted of bottom annotation and the underlying type).
With property 2, we maintain one single instance of bottom store for each type system involved at runtime.

…into bottom-store

framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java

…into bottom-store

framework/src/main/java/org/checkerframework/framework/flow/CFAbstractValue.java

…into bottom-store

zcai1

Most of the changes LGTM! 👍

zcai1 · 2021-09-29T04:05:47Z

checker/src/main/java/org/checkerframework/checker/lock/LockStore.java

+        AnnotationMirror guardBy = ((LockAnnotatedTypeFactory) analysis.getTypeFactory()).GUARDEDBY;
+        AnnotationMirror lockHeld = ((LockAnnotatedTypeFactory) analysis.getTypeFactory()).LOCKHELD;
+
+        return analysis.createAbstractValue(new HashSet<>(Arrays.asList(lockHeld, guardBy)), type);


new HashSet<>(Arrays.asList(lockHeld, guardBy)
Can we replace it with ImmutableSet.of(...)? Or should we store these bottom annotations instead of creating a new set each time this method is invoked?

Actually there is a final field bottomAnnos in the these store classes that represents the set of bottom annotations. That field is initialized in the constructor with AnnotatedTypeFactory.getBottomAnnotations().

But LockStore is special. We can't use the real bottom annotations, so here the getBottomValue is overriden.

zcai1 · 2021-09-29T04:07:42Z

checker/src/main/java/org/checkerframework/checker/nullness/NullnessStore.java

+        super(analysis, sequentialSemantics, isBottom);
        isPolyNullNonNull = false;
-        isPolyNullNull = false;
+        this.isPolyNullNull = false;


Why adding this. on line 49 while line 48 doesn't have this.?

zcai1 · 2021-09-29T04:36:48Z

framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java

+
+        // Is it necessary to consider `x = true ? y : z`
+        if (parentTree.getKind() == Tree.Kind.CONDITIONAL_EXPRESSION) {
+            return ((ConditionalExpressionTree) parentTree).getCondition() == tree;


What if the condition is wrapped by parentheses? For example, (x == true) ? y : z.

zcai1 · 2021-09-29T04:38:16Z

framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java

+            return ((ConditionalExpressionTree) parentTree).getCondition() == tree;
+        }
+
+        return parentTree.getKind() == Tree.Kind.IF


This logic may work as expected, but I think it's safer to compare with parentTree.getCondition() so we know it indeed is a condition.

zcai1 · 2021-09-29T05:04:17Z

checker/tests/index/LubIndex.java

-        // :: error: (assignment.type.incompatible)
        int @MinLen(10) [] res = arr;
        int @MinLen(4) [] res2 = arr;
-        // :: error: (assignment.type.incompatible)


These changes make sense, but they also alter the meaning of this test. Should we write a new test case for the merging of @BottomVal and @MinLen(4)?

zcai1 · 2021-09-29T05:10:54Z

checker/tests/initialization/TryFinallyContinue.java

        String ans = "x";
        while (true) {
            if (true) {
-                // :: error: (return.type.incompatible)


Same issue here: we are removing all occurences of // :: error: (return.type.incompatible) in this file, and we need some new test cases to cover issue typetools#548.

zcai1 · 2021-09-29T05:14:09Z

checker/tests/nullness/flow/DeadBranch.java

+
+class DeadBranch {
+
+    Object foo(@Nullable Object myObj, boolean x) {


Why do we need boolean x?

Thanks for pointing out! I need to add another case using x as the condition.

zcai1 · 2021-09-29T05:21:14Z

framework/tests/value/MinLenLUB.java

        } else {
            arr = arg2;
        }
-        // :: error: (assignment.type.incompatible)


Same issue here: I think we need to test LUB of @BottomVal and @MinLen(4), and LUB of @MinLen(10) and @MinLen(4).

d367wang · 2021-09-29T13:33:25Z

Thank you for the comments @zcai1

d367wang · 2021-09-29T13:36:31Z

framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java

+    public abstract S createBottomStore(boolean sequentialSemantics);
+
+    /**
+     * Get the singleton of the bottom store corresponding to the type.


... corresponding to the type system

d367wang · 2021-09-29T13:41:08Z

framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java

    @Override
    public S leastUpperBound(S other) {
+        if (this.isBottom) return other;
+        if (other != null && other.isBottom) return (S) this;


Do we need to test the nullness of other here? The dataflow code is nullness-type-safe guaranteed by NullnessChecker, isn't it?

zcai1 · 2021-09-29T14:28:23Z

checker/src/main/java/org/checkerframework/checker/nullness/KeyForAnalysis.java


+    @Override
+    public KeyForStore createBottomStore(boolean sequentialSemantics) {
+        return new KeyForStore(this, sequentialSemantics);


Maybe just return createEmptyStore(sequentialSemantics)?

return new KeyForStore(this, sequentialSemantics, true);

d367wang · 2021-09-29T14:32:55Z

checker/tests/nullness/Issue3622.java

-                "contracts.conditional.postcondition.not.satisfied" // TODO: `if` needs the
-        // BOTH_TO_THEN treatment that ?: gets.
-        )
+        @SuppressWarnings("contracts.conditional.postcondition.not.satisfied")


add comment for reason for suppressWarning

add another case return true in if and return false in else

d367wang · 2021-09-29T14:52:27Z

framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java

+     * @return ture if the given tree is a condition
+     */
+    @SuppressWarnings("interning:not.interned")
+    boolean isCondition(ExpressionTree tree) {


zcai1 · 2021-09-29T15:12:01Z

framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java

+     * @param type the input {@link TypeMirror}
+     * @return the bottom value
+     */
+    protected V getBottomValue(TypeMirror type) {


maybe createBottomValue?

d367wang added 2 commits April 1, 2021 12:23

initial bottom-store implementation

7e91f46

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

2237641

…into bottom-store

d367wang commented May 20, 2021

View reviewed changes

framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java Show resolved Hide resolved

d367wang added 9 commits July 6, 2021 11:52

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

6ec3d77

…into bottom-store

undo import *

0122edf

fix compile error

c276efa

fix bug

cceadf7

add lock bottom store; remove FPs involving if(true/false)

81c8059

NullnessBottom.getValue returns two qualifiers

887a888

xxxBottomStore.getValue returns abstract value with bottom annotations

9af8f2e

remove @nullable on xxxBottomStore.getValue

0a4adad

fix bug

6775dfa

d367wang commented Aug 5, 2021

View reviewed changes

framework/src/main/java/org/checkerframework/framework/flow/CFAbstractValue.java Outdated Show resolved Hide resolved

d367wang added 16 commits August 9, 2021 13:58

make bottom-store logic coherent to CFAbstract classes

68b238b

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

826d25a

…into bottom-store

adapt expected files

d6ddb82

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

ee35b60

…into bottom-store

remove BOTH_TO_THEN and BOTH_TO_ELSE

080ff48

fix bug and refactor

d70186b

hack CFAbastractValue.combineOneAnnotation

5b616d3

only use bottom store when the boolean literal is a condition on its own

e83dea7

suppress intern error

ea69c0a

adapt expected error

2e03227

change bottom value for lock type system

7408317

fix bug in bottom store, to resolve the must-call case

44c97a7

adapt bottom value for lock type system

a6509e5

no insertion to bottom store

9041117

add javadoc

40a27ca

apply default to void methodreturns

a131f41

d367wang mentioned this pull request Sep 28, 2021

Introduce "bottom store" to reduce false positive in dead branch eisop/checker-framework#101

Open

zcai1 reviewed Sep 29, 2021

View reviewed changes

d367wang commented Sep 29, 2021

View reviewed changes

zcai1 reviewed Sep 29, 2021

View reviewed changes

d367wang commented Sep 29, 2021

View reviewed changes

zcai1 reviewed Sep 29, 2021

View reviewed changes

zcai1 pushed a commit to zcai1/checker-framework that referenced this pull request Feb 8, 2022

Bump de.undercouch.download from 4.1.2 to 5.0.1 (opprop#167)

34657a1


		class DeadBranch {

		Object foo(@Nullable Object myObj, boolean x) {

Introduce bottom store to improve dataflow analysis #167

Are you sure you want to change the base?

Introduce bottom store to improve dataflow analysis #167

Uh oh!

Conversation

d367wang commented Apr 1, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

zcai1 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

zcai1 Sep 29, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

d367wang commented Sep 29, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

d367wang Sep 29, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

d367wang Sep 29, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

d367wang Sep 29, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

d367wang commented Apr 1, 2021 •

edited

Loading

zcai1 Sep 29, 2021 •

edited

Loading

d367wang commented Sep 29, 2021 •

edited

Loading

d367wang Sep 29, 2021 •

edited

Loading

d367wang Sep 29, 2021 •

edited

Loading

d367wang Sep 29, 2021 •

edited

Loading