Create refinement slots for variable declarations with initialization (#287)

Co-authored-by: txiang61 <[email protected]>

Author: d367wang

src/checkers/inference/InferenceVisitor.java

@@ -448,11 +448,17 @@ protected void commonAssignmentCheck(Tree varTree, ExpressionTree valueExp,
             return;
         }
 
-        // commonAssignmentCheck eventually create an equality constraint between varTree and valueExp.
-        // For inference, we need this constraint to be between the RefinementVariable and the value.
-        // Refinement variables come from flow inference, so we need to call getAnnotatedType instead of getDefaultedAnnotatedType
         AnnotatedTypeMirror var;
-        if (this.infer) {
+        if (infer && varTree.getKind() == Kind.TYPE_PARAMETER) {
+            // When the lhs is a type variable, due to the partially resolved issue
+            // https://github.com/opprop/checker-framework-inference/issues/316,
+            // currently it is still "commonAssignmentCheck" who creates the refinement constraint.
+            // We need this constraint to be between the refinement variable and the rhs value.
+            // Since refinement variables come from flow inference, we must call "getAnnotatedType"
+            // instead of "getAnnotatedTypeLhs".
+            // TODO: use "getAnnotatedTypeLhs" uniformly when issue 316 is completely resolved.
+            //  (In that way, the refinement constraints are uniformly created during dataflow analysis, so
+            //  "commonAssignmentCheck" only needs to enforce the general type rule regarding assignment.)
             var = atypeFactory.getAnnotatedType(varTree);
         } else {
             var = atypeFactory.getAnnotatedTypeLhs(varTree);

src/checkers/inference/dataflow/InferenceTransfer.java

@@ -137,6 +137,15 @@ public TransferResult<CFValue, CFStore> visitAssignment(AssignmentNode assignmen
                 assert false;
             }
 
+            if (assignmentNode.getTarget() instanceof LocalVariableNode
+                    && atm.getKind() != TypeKind.TYPEVAR) {
+                // Get the rhs value and pass it to slot manager to generate the equality constraint
+                // as "refinement variable == rhs value"
+                Tree valueTree = assignmentNode.getExpression().getTree();
+                AnnotatedTypeMirror valueType = typeFactory.getAnnotatedType(valueTree);
+                return createRefinementVar(assignmentNode.getTarget(), assignmentNode.getTree(), store, atm, valueType);
+            }
+
             return storeDeclaration(lhs, (VariableTree) assignmentNode.getTree(), store, typeFactory);
 
         } else if (lhs.getTree().getKind() == Tree.Kind.IDENTIFIER
@@ -217,6 +226,14 @@ private TransferResult<CFValue, CFStore> createRefinementVar(Node lhs,
 
         SlotManager slotManager = getInferenceAnalysis().getSlotManager();
         Slot slotToRefine = slotManager.getSlot(atm);
+
+        // Make sure the refinement slot is created on the declared type
+        if (slotToRefine instanceof RefinementVariableSlot) {
+            // Getting the declared type of a RefinementVariableSlot
+            // getRefined() always returns the slot of the declared type value
+            slotToRefine = ((RefinementVariableSlot)slotToRefine).getRefined();
+        }
+
         Slot refineTo = slotManager.getSlot(valueAtm);
 
         logger.fine("Creating refinement variable for tree: " + assignmentTree);

src/checkers/inference/dataflow/InferenceValue.java

@@ -119,31 +119,54 @@ public CFValue mostSpecific(CFValue other, CFValue backup) {
      *
      */
     public CFValue mostSpecificFromSlot(final Slot thisSlot, final Slot otherSlot, final CFValue other, final CFValue backup) {
-        // TODO: refactor this method
-        if (thisSlot instanceof VariableSlot && otherSlot instanceof VariableSlot) {
-            if (thisSlot.isMergedTo(otherSlot)) {
-                return other;
-            } else if (otherSlot.isMergedTo(thisSlot)) {
-                return this;
-            } else if (thisSlot instanceof RefinementVariableSlot
-                    && ((RefinementVariableSlot) thisSlot).getRefined().equals(otherSlot)) {
-
-                return this;
-            } else if (otherSlot instanceof RefinementVariableSlot
-                    && ((RefinementVariableSlot) otherSlot).getRefined().equals(thisSlot)) {
-
-                return other;
-            } else {
-                // Check if one of these has refinement variables that were merged to the other.
-                for (RefinementVariableSlot slot : ((VariableSlot) thisSlot).getRefinedToSlots()) {
-                    if (slot.isMergedTo(otherSlot)) {
-                        return other;
-                    }
+        if (thisSlot.isMergedTo(otherSlot)) {
+            return other;
+        }
+
+        if (otherSlot.isMergedTo(thisSlot)) {
+            return this;
+        }
+
+        if (thisSlot instanceof RefinementVariableSlot
+                && ((RefinementVariableSlot) thisSlot).getRefined().equals(otherSlot)) {
+            return this;
+        }
+
+        if (otherSlot instanceof RefinementVariableSlot
+                && ((RefinementVariableSlot) otherSlot).getRefined().equals(thisSlot)) {
+            return other;
+        }
+
+        if (thisSlot instanceof RefinementVariableSlot
+                && otherSlot instanceof RefinementVariableSlot
+                && ((RefinementVariableSlot) thisSlot).getRefined().equals(((RefinementVariableSlot) otherSlot).getRefined())) {
+            // This happens when a local variable is declared with initializer, and is reassigned afterwards. E.g.
+            //      Object obj = null;
+            //      obj = new Object();
+            //      return obj;
+            // Suppose RefinementVar(1) is created at variable declaration, RefinementVar(2) is created at re-assignment.
+            // Then at the return point, when getting the most specific type of obj,
+            // "thisSlot" is RefinementVar(1), coming from "getValueFromFactory".
+            // "otherSlot" is RefinementVar(2), coming from the store value.
+            // The store value is more precise, so we choose "other" as the most specific type.
+            assert thisSlot.getId() <= otherSlot.getId();
+            return other;
+        }
+
+        if (thisSlot instanceof VariableSlot) {
+            // Check if one of these has refinement variables that were merged to the other.
+            for (RefinementVariableSlot slot : ((VariableSlot) thisSlot).getRefinedToSlots()) {
+                if (slot.isMergedTo(otherSlot)) {
+                    return other;
                 }
-                for (RefinementVariableSlot slot : ((VariableSlot) otherSlot).getRefinedToSlots()) {
-                    if (slot.isMergedTo(thisSlot)) {
-                        return this;
-                    }
+            }
+        }
+
+        if (otherSlot instanceof VariableSlot) {
+            // Same as above
+            for (RefinementVariableSlot slot : ((VariableSlot) otherSlot).getRefinedToSlots()) {
+                if (slot.isMergedTo(thisSlot)) {
+                    return this;
                 }
             }
         }

src/checkers/inference/solver/backend/AbstractFormatTranslator.java

@@ -53,9 +53,9 @@
  * For example, {@link checkers.inference.solver.backend.maxsat.encoder.MaxSATConstraintEncoderFactory}
  * depends on {@link checkers.inference.solver.backend.maxsat.MaxSatFormatTranslator#typeToInt typeToInt}
  * filed in {@link checkers.inference.solver.backend.maxsat.MaxSatFormatTranslator}. So only after those
- * dependant fields are initialized in subclasses constructors, encoders can be then initialized.
+ * dependent fields are initialized in subclasses constructors, encoders can be then initialized.
  * Calling {@link #finishInitializingEncoders()} at the last step of initialization makes sure all the
- * dependant fields are already initialized.
+ * dependent fields are already initialized.
  * <p>
  * In terms of "last step of initialization", different {@code FormatTranslator}s have different definitions.
  * For {@link checkers.inference.solver.backend.maxsat.MaxSatFormatTranslator} and

testdata/ostrusted-inferrable-test/Refinement.java

@@ -0,0 +1,26 @@
+import ostrusted.qual.OsUntrusted;
+import ostrusted.qual.OsTrusted;
+
+public class Refinement {
+
+    void foo(Object in1, Object in2) {
+        Object o = in1;
+        // :: fixable-error: (argument.type.incompatible)
+        bar(o);
+
+        o = in2;
+        // :: fixable-error: (argument.type.incompatible) 
+        bar(o);
+    }
+
+    void bar(@OsTrusted Object in) {}
+
+
+    @OsTrusted Object m(@OsUntrusted Object untrusted, Object trusted) {
+        Object obj = untrusted;
+        obj = trusted;
+        // :: fixable-error: (return.type.incompatible)
+        return obj;
+    }
+}
+