Support refinement for conditions of comparisons #389
Conversation
| return; | ||
| } | ||
| Tree tree = var.getTree(); | ||
| ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager(); |
There was a problem hiding this comment.
I think these are the first constraints that are created by InferenceTransfer - so far, this only created Slots.
Why is this needed for these constraints? Can you add a comment to the method explaining this? The method name should also reflect this.
There was a problem hiding this comment.
I think it works in either ways. I guess putting constraint creation here is just for convenience. I can move it to InferenceVisitor.visitBinary for consistency. In that case, we should (1) check if it's a comparison (2) retrieve the comparison slots associated from the cache.
There was a problem hiding this comment.
Did you get a chance to try whether this is nicer in InferenceVisitor? For refinement variables we seem to add the subtype constraints in InferenceVisitor. So maybe something similar would work for these ComparisonSlots.
There was a problem hiding this comment.
Not all the constraints are created in xxxVisitor. E.g., the equality constraint associated with an assignment is created in the transfer function, as
For refinement variables we add the subtype constraints in InferenceVisitor may be because we want to reuse the super method BaseTypeVisitor.visitAssignment, which checks if RHS <: LHS.
So it makes sense to put the type rule-based constraints in xxxVisitory, and add inherent constraints of a slot in xxxTransfer when the slot is created.
There was a problem hiding this comment.
Besides, regarding the comparison variable slot, I think the subtype constraints (compareSlot <: declareType) are not precise. It's more precise to create compareSlot <: typeBeforeComparison, i.e. line 443-446 can be removed.
| @@ -31,7 +31,7 @@ | |||
| private AnnotationLocation location; | |||
|
|
|||
| /** Refinement variables that refine this slot. */ | |||
There was a problem hiding this comment.
What is the motivation for this change? Can you update the javadoc to explain what kinds of VariableSlots to expect?
There was a problem hiding this comment.
Should the name of the method and field be updated to reflect this change?
There was a problem hiding this comment.
The comment for this field has been updated.
I think the current name refinedToSlots makes sense, considering that both RefinementVariableSlot and ComparisonVariableSlot can refine a `VariableSlot.
| ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager(); | ||
| SlotManager slotManager = getInferenceAnalysis().getSlotManager(); | ||
|
|
||
| AnnotatedTypeMirror atm = typeFactory.getAnnotatedType(tree); |
There was a problem hiding this comment.
Shouldn't this use getAnnotatedTypeLhs?
There was a problem hiding this comment.
We have a problem in getting the declared type using getAnnotatedTypeLhs in CFI, because of the mutable ATM in the elementToAtm cache (I have an open PR #362 intended to fix it by duplicating the ATM before writing or after reading).
The effect is, getAnnotatedTypeLhs give us the refined type right after initialization, no matter how many times the variable is reassigned.
A common workaround for this issue in CFI is to use getAnnotatedType (which is usually a RefinementVariableSlot), and then get the declared type of the RefinementVariableSlot, like Lines 436-439 in this file, and
There was a problem hiding this comment.
Thanks for the explanation! Let's try to clean this up with or after #362!
…inference into value-patch-comparison
| return; | ||
| } | ||
| Tree tree = var.getTree(); | ||
| ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager(); |
There was a problem hiding this comment.
Did you get a chance to try whether this is nicer in InferenceVisitor? For refinement variables we seem to add the subtype constraints in InferenceVisitor. So maybe something similar would work for these ComparisonSlots.
| ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager(); | ||
| SlotManager slotManager = getInferenceAnalysis().getSlotManager(); | ||
|
|
||
| AnnotatedTypeMirror atm = typeFactory.getAnnotatedType(tree); |
There was a problem hiding this comment.
Thanks for the explanation! Let's try to clean this up with or after #362!
| } | ||
|
|
||
| @Override | ||
| public TransferResult<CFValue, CFStore> visitEqualTo( |
There was a problem hiding this comment.
These only handle equal and not-equal. Shouldn't other comparisons also be handled?
There was a problem hiding this comment.
Comparison slots are created only when type refinement can be performed. For non-numeric types (general case in CFI), type refinement is only possible when the comparison is == or !=.
Other kinds of comparisons are only applicable for numeric types and can be defined in specific type system, like value-inference.
…inference into value-patch-comparison
…framework-inference into value-patch-comparison
A split of #331
Co-authored-by: Jenny Xiang j.tt.xiang@gmail.com