Boolean variables in dataflow #6661
Conversation
|
Testing on the case study now.
… On Jun 6, 2024, at 1:04 PM, Michael Ernst ***@***.***> wrote:
@mernst approved this pull request.
LGTM
—
Reply to this email directly, view it on GitHub <#6661 (review)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AFZ3EEHANMZRUPQQEH5WXVTZGC6ELAVCNFSM6AAAAABI5LZLX2VHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMZDCMBTGEYDGNZXGE>.
You are receiving this because you were mentioned.
|
framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java
Outdated
Show resolved
Hide resolved
framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java
Outdated
Show resolved
Hide resolved
framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java
Outdated
Show resolved
Hide resolved
| @@ -1253,6 +1347,32 @@ private V upperBoundOfValues(V otherVal, V thisVal, boolean shouldWiden) { | |||
| return shouldWiden ? thisVal.widenUpperBound(otherVal) : thisVal.leastUpperBound(otherVal); | |||
| } | |||
|
|
|||
| /** | |||
| * Creates a new store that has all the values from both {@code this} and {@code other}. If a node | |||
| * has a value in both stores, then the most specific one is used. | |||
There was a problem hiding this comment.
Why is the most specific one used rather than the glb?
It might be helpful to add a comment to the declaration of mostSpecific indicating when it should be called and when glb should be called.
| @@ -68,6 +68,12 @@ public abstract class CFAbstractValue<V extends CFAbstractValue<V>> implements A | |||
| /** The annotations in this abstract value. */ | |||
| protected final AnnotationMirrorSet annotations; | |||
|
|
|||
| /** The then store. */ | |||
There was a problem hiding this comment.
Please say more here. The pull request doesn't seem to have any comments about the feature being implemented or the purpose of the code, and I think that will make it unnecessarily hard for readers of the code to understand the feature and its implementation.
| return analysis.createAbstractValue(mostSpecific, mostSpecifTypeMirror); | ||
| V mostSpecificVal = analysis.createAbstractValue(mostSpecific, mostSpecifTypeMirror); | ||
| if (this.getThenStore() != null) { | ||
| mostSpecificVal.setStores(thenStore, elseStore); |
There was a problem hiding this comment.
Why is it OK to ignore other's stores if this has a store? Might it have information that should be retained?
| @@ -529,7 +574,23 @@ protected V upperBound(@Nullable V other, TypeMirror upperBoundTypeMirror, boole | |||
| other.getUnderlyingType(), | |||
| other.getAnnotations(), | |||
| canBeMissingAnnotations(upperBoundTypeMirror)); | |||
| return analysis.createAbstractValue(lub, upperBoundTypeMirror); | |||
| V upperBound = analysis.createAbstractValue(lub, upperBoundTypeMirror); | |||
| if (this.getThenStore() != null && other.getThenStore() != null) { | |||
There was a problem hiding this comment.
What if one of this and other has a thenStore, but the other does not? What should be done in that case? The behavior is different than in mostSpecific() above, which always uses exactly one if either one is set.
|
This is a really cool PR! Is there any idea what the performance impact will be? In NullAway, local type inference is one of the most expensive parts of checking, and I imagine the same could be true with the Checker Framework. Might be worth doing some sanity checks on large programs to make sure this doesn't lead to a significant regression. |
|
There are bugs in this implementation that once fixed cause infinite recursion, so I'm closing this pull request in favor of #6797 |
This is a rough draft of the fix for #406. @jyoo980 can you see if this fixes the error in the case study?
Fixes #406.