From 5071e451ca61493aac095e8629e1db0495f11922 Mon Sep 17 00:00:00 2001
From: Suzanne Millstein <smillst@cs.washington.edu>
Date: Fri, 6 Dec 2024 12:28:22 -0800
Subject: [PATCH] Initialize implicit this

---
 checker/tests/nonempty/SizeInIsEmpty.java            | 12 ++++++++++++
 .../framework/flow/CFAbstractStore.java              | 11 +++++++----
 .../framework/flow/CFAbstractTransfer.java           | 11 ++++++++++-
 3 files changed, 29 insertions(+), 5 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<Object> 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);
       }
     }
 
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..cfa27246eb9 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 values from field initialization and, if analyzing a
+   * lambda, final local variables.
+   */
   private @Nullable S fixedInitialStore = null;
 
   /**
@@ -268,6 +271,12 @@ public S initialStore(UnderlyingAST underlyingAST, List<LocalVariableNode> param
         store.initializeMethodParameter(p, analysis.createAbstractValue(anno));
       }
 
+      AnnotatedTypeMirror implicitThis = atypeFactory.getSelfType(underlyingAST.getCode());
+      if (implicitThis != null) {
+        V thisSelf = analysis.createAbstractValue(implicitThis);
+        store.thisValue = thisSelf.mostSpecific(store.thisValue, null);
+      }
+
       // add properties known through precondition
       CFGMethod method = (CFGMethod) underlyingAST;
       MethodTree methodDeclTree = method.getMethod();