diff --git a/src/checkers/inference/InferenceVisitor.java b/src/checkers/inference/InferenceVisitor.java index 789bff8b..459c1d75 100644 --- a/src/checkers/inference/InferenceVisitor.java +++ b/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); diff --git a/src/checkers/inference/dataflow/InferenceTransfer.java b/src/checkers/inference/dataflow/InferenceTransfer.java index ff93e405..ac168e6d 100644 --- a/src/checkers/inference/dataflow/InferenceTransfer.java +++ b/src/checkers/inference/dataflow/InferenceTransfer.java @@ -137,6 +137,15 @@ public TransferResult 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 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); diff --git a/src/checkers/inference/dataflow/InferenceValue.java b/src/checkers/inference/dataflow/InferenceValue.java index 9f290a80..96e98572 100644 --- a/src/checkers/inference/dataflow/InferenceValue.java +++ b/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; } } } diff --git a/src/checkers/inference/solver/backend/AbstractFormatTranslator.java b/src/checkers/inference/solver/backend/AbstractFormatTranslator.java index df1ad0cc..40ef503c 100644 --- a/src/checkers/inference/solver/backend/AbstractFormatTranslator.java +++ b/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. *

* In terms of "last step of initialization", different {@code FormatTranslator}s have different definitions. * For {@link checkers.inference.solver.backend.maxsat.MaxSatFormatTranslator} and diff --git a/testdata/ostrusted-inferrable-test/Refinement.java b/testdata/ostrusted-inferrable-test/Refinement.java new file mode 100644 index 00000000..618776f6 --- /dev/null +++ b/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; + } +} +