From 1ba21efece58e037bc9482f3f5fd0b67fd5deb36 Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Tue, 3 Dec 2024 10:49:50 -0800 Subject: [PATCH 1/4] Initialize implicit this. --- .../checkerframework/framework/flow/CFAbstractTransfer.java | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java index daf06e94669..a1249c90fed 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -268,6 +268,11 @@ public S initialStore(UnderlyingAST underlyingAST, List param store.initializeMethodParameter(p, analysis.createAbstractValue(anno)); } + AnnotatedTypeMirror implicitThis = atypeFactory.getSelfType(underlyingAST.getCode()); + if (implicitThis != null) { + store.thisValue = analysis.createAbstractValue(implicitThis); + } + // add properties known through precondition CFGMethod method = (CFGMethod) underlyingAST; MethodTree methodDeclTree = method.getMethod(); From ba3ccd40ff3ed0ddb8e830b4032d9c13b079aac6 Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Wed, 4 Dec 2024 11:54:41 -0800 Subject: [PATCH 2/4] False positive. --- checker/tests/nonempty/SizeInIsEmpty.java | 12 ++++++++++++ .../framework/flow/CFAbstractStore.java | 11 +++++++---- 2 files changed, 19 insertions(+), 4 deletions(-) diff --git a/checker/tests/nonempty/SizeInIsEmpty.java b/checker/tests/nonempty/SizeInIsEmpty.java index 5b9ea07ae3c..31ca40ea5d2 100644 --- a/checker/tests/nonempty/SizeInIsEmpty.java +++ b/checker/tests/nonempty/SizeInIsEmpty.java @@ -1,5 +1,7 @@ import java.util.AbstractSet; +import java.util.HashSet; import java.util.Iterator; +import java.util.Set; import org.checkerframework.checker.nonempty.qual.EnsuresNonEmptyIf; import org.checkerframework.checker.nonempty.qual.PolyNonEmpty; import org.checkerframework.dataflow.qual.Pure; @@ -31,9 +33,19 @@ public boolean isEmpty() { @EnsuresNonEmptyIf(result = false, expression = "this") public boolean isEmpty2() { + // :: error: contracts.conditional.postcondition return size() == 0 ? true : false; } + Set set = new HashSet<>(); + + @EnsuresNonEmptyIf(result = false, expression = "this.set") + public boolean isEmpty2B() { + // TODO: this is a false positive + // :: error: contracts.conditional.postcondition + return set.size() == 0 ? true : false; + } + @EnsuresNonEmptyIf(result = false, expression = "this") public boolean isEmpty3() { return size() == 0; diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java index 93f96d70c87..8f31f26841b 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java @@ -772,7 +772,9 @@ public void clearValue(JavaExpression expr) { } else if (expr instanceof ClassName) { ClassName c = (ClassName) expr; classValues.remove(c); - } else { // thisValue ... + } else if (expr instanceof ThisReference) { + thisValue = null; + } else { // No other types of expressions are stored. } } @@ -1190,9 +1192,10 @@ private S upperBound(S other, boolean shouldWiden) { { V otherVal = other.thisValue; V myVal = thisValue; - V mergedVal = myVal == null ? null : upperBoundOfValues(otherVal, myVal, shouldWiden); - if (mergedVal != null) { - newStore.thisValue = mergedVal; + if (myVal == null || otherVal == null) { + newStore.thisValue = null; + } else { + newStore.thisValue = upperBoundOfValues(otherVal, myVal, shouldWiden); } } From 701e53d3503163283d3def8374821f9c24c8904e Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Fri, 6 Dec 2024 09:47:56 -0800 Subject: [PATCH 3/4] Fix test failure. --- .../framework/flow/CFAbstractTransfer.java | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java index a1249c90fed..72330f55b3f 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -226,7 +226,10 @@ protected V getValueFromFactory(Tree tree, Node node) { return analysis.createAbstractValue(at); } - /** The fixed initial store. */ + /** + * The fixed initial store which includes initialized fields and, if analyzing a lambda, final + * local variables. + */ private @Nullable S fixedInitialStore = null; /** @@ -270,7 +273,8 @@ public S initialStore(UnderlyingAST underlyingAST, List param AnnotatedTypeMirror implicitThis = atypeFactory.getSelfType(underlyingAST.getCode()); if (implicitThis != null) { - store.thisValue = analysis.createAbstractValue(implicitThis); + V thisSelf = analysis.createAbstractValue(implicitThis); + store.thisValue = thisSelf.mostSpecific(store.thisValue, null); } // add properties known through precondition From 267c8efe09df670f3252d4f711c60e48ee9928b8 Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Fri, 6 Dec 2024 09:49:27 -0800 Subject: [PATCH 4/4] Tweak javadoc. --- .../checkerframework/framework/flow/CFAbstractTransfer.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java index 72330f55b3f..cfa27246eb9 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -227,8 +227,8 @@ protected V getValueFromFactory(Tree tree, Node node) { } /** - * The fixed initial store which includes initialized fields and, if analyzing a lambda, final - * local variables. + * The fixed initial store which includes values from field initialization and, if analyzing a + * lambda, final local variables. */ private @Nullable S fixedInitialStore = null;