Skip to content

Support refinement for conditions of comparisons #389

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
d367wang wants to merge 8 commits into
base: master
Choose a base branch
from
Open

Support refinement for conditions of comparisons #389

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
2b01a93
support refinement for conditions of comparisons
d367wang Feb 20, 2022
58d9302
Merge branch 'master' of https://github.com/opprop/checker-framework-…
d367wang Mar 6, 2022
5ebcb2a
add doc; small refactor
d367wang Mar 7, 2022
eee0b78
Merge branch 'master' into value-patch-comparison
wmdietl Mar 12, 2022
61a9c0e
Merge branch 'master' of https://github.com/opprop/checker-framework-…
d367wang Mar 20, 2022
23f12b4
add comment
d367wang Mar 20, 2022
1d59b43
add comment
d367wang Mar 20, 2022
dc90cb8
Merge branch 'value-patch-comparison' of github.com:d367wang/checker-…
d367wang Mar 20, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
97 changes: 97 additions & 0 deletions src/checkers/inference/dataflow/InferenceTransfer.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,14 +1,18 @@
package checkers.inference.dataflow;

import org.checkerframework.dataflow.analysis.ConditionalTransferResult;
import org.checkerframework.dataflow.analysis.RegularTransferResult;
import org.checkerframework.dataflow.analysis.TransferInput;
import org.checkerframework.dataflow.analysis.TransferResult;
import org.checkerframework.dataflow.cfg.node.AssignmentNode;
import org.checkerframework.dataflow.cfg.node.EqualToNode;
import org.checkerframework.dataflow.cfg.node.FieldAccessNode;
import org.checkerframework.dataflow.cfg.node.LocalVariableNode;
import org.checkerframework.dataflow.cfg.node.Node;
import org.checkerframework.dataflow.cfg.node.NotEqualNode;
import org.checkerframework.dataflow.cfg.node.StringConcatenateAssignmentNode;
import org.checkerframework.dataflow.cfg.node.TernaryExpressionNode;
import org.checkerframework.dataflow.expression.JavaExpression;
import org.checkerframework.framework.flow.CFStore;
import org.checkerframework.framework.flow.CFTransfer;
import org.checkerframework.framework.flow.CFValue;
Expand All @@ -21,6 +25,7 @@
import java.util.Map;
import java.util.logging.Logger;

import javax.lang.model.element.AnnotationMirror;
import javax.lang.model.type.TypeKind;

import com.sun.source.tree.Tree;
Expand All @@ -31,6 +36,8 @@
import checkers.inference.SlotManager;
import checkers.inference.VariableAnnotator;
import checkers.inference.model.AnnotationLocation;
import checkers.inference.model.ComparisonVariableSlot;
import checkers.inference.model.ConstraintManager;
import checkers.inference.model.ExistentialVariableSlot;
import checkers.inference.model.RefinementVariableSlot;
import checkers.inference.model.Slot;
Expand Down Expand Up @@ -401,4 +408,94 @@ private TransferResult<CFValue, CFStore> storeDeclaration(Node lhs,
private boolean isDeclarationWithInitializer(AssignmentNode assignmentNode) {
return (assignmentNode.getTree().getKind() == Tree.Kind.VARIABLE);
}

private void createComparisonVariableSlot(Node node, CFStore thenStore, CFStore elseStore) {
Comment thread
d367wang marked this conversation as resolved.
// Only create refinement comparison slot for variables
// TODO: deal with comparison between more complex expressions
Node var = node;
Comment thread
d367wang marked this conversation as resolved.
Outdated
if (node instanceof AssignmentNode) {
AssignmentNode a = (AssignmentNode) node;
var = a.getTarget();
}
if (!(var instanceof LocalVariableNode) && !(var instanceof FieldAccessNode)) {
return;
}
Tree tree = var.getTree();
ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager();

@wmdietl wmdietl Feb 23, 2022

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

@d367wang d367wang Mar 7, 2022

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

@wmdietl wmdietl Mar 12, 2022

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

@d367wang d367wang Mar 20, 2022 •
edited
Loading

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not all the constraints are created in xxxVisitor. E.g., the equality constraint associated with an assignment is created in the transfer function, as

checker-framework-inference/src/checkers/inference/DefaultSlotManager.java

Line 519 in 21dfba4

InferenceMain.getInstance().getConstraintManager().addEqualityConstraint(refinementVariableSlot, valueSlot);

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.

@d367wang d367wang Mar 20, 2022

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

SlotManager slotManager = getInferenceAnalysis().getSlotManager();

AnnotatedTypeMirror atm = typeFactory.getAnnotatedType(tree);

@wmdietl wmdietl Feb 23, 2022

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't this use getAnnotatedTypeLhs?

@d367wang d367wang Mar 7, 2022 •
edited
Loading

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

checker-framework-inference/src/checkers/inference/dataflow/InferenceTransfer.java

Line 222 in 8a29a0e

if (slotToRefine instanceof RefinementVariableSlot) {

@wmdietl wmdietl Mar 12, 2022

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the explanation! Let's try to clean this up with or after #362!

Slot slotToRefine = slotManager.getSlot(atm);

// TODO: Understand why there are null slots
if (InferenceMain.isHackMode(slotToRefine == null)) {
logger.fine("HackMode: slotToRefine is null !");
return;
}

if (slotToRefine instanceof RefinementVariableSlot) {
slotToRefine = ((RefinementVariableSlot) slotToRefine).getRefined();
assert !(slotToRefine instanceof RefinementVariableSlot);
}

AnnotationLocation location =
VariableAnnotator.treeToLocation(analysis.getTypeFactory(), tree);
// TODO: find out why there are missing location
if (InferenceMain.isHackMode(location == AnnotationLocation.MISSING_LOCATION)) {
logger.fine("HackMode: create ComparisonVariableSlot on MISSING_LOCATION !");
return;
}
ComparisonVariableSlot thenSlot = slotManager.createComparisonVariableSlot(location, slotToRefine, true);
constraintManager.addSubtypeConstraint(thenSlot, slotToRefine);
ComparisonVariableSlot elseSlot = slotManager.createComparisonVariableSlot(location, slotToRefine, false);
constraintManager.addSubtypeConstraint(elseSlot, slotToRefine);

if (slotToRefine instanceof VariableSlot) {
// ComparisonVariableSlots stores the refined value after comparison, so add it to the "refinedTo" list
((VariableSlot) slotToRefine).getRefinedToSlots().add(thenSlot);
((VariableSlot) slotToRefine).getRefinedToSlots().add(elseSlot);
}

AnnotationMirror thenAm = slotManager.getAnnotation(thenSlot);
AnnotationMirror elseAm = slotManager.getAnnotation(elseSlot);

// If node is assignment, iterate over lhs; otherwise, just node.
JavaExpression rec;
Comment thread
d367wang marked this conversation as resolved.
Outdated
rec = JavaExpression.fromNode(var);
thenStore.clearValue(rec);
thenStore.insertValue(rec, thenAm);
elseStore.clearValue(rec);
elseStore.insertValue(rec, elseAm);
}

@Override
public TransferResult<CFValue, CFStore> visitEqualTo(

@wmdietl wmdietl Mar 12, 2022

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These only handle equal and not-equal. Shouldn't other comparisons also be handled?

@d367wang d367wang Mar 20, 2022

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

EqualToNode n, TransferInput<CFValue, CFStore> in) {
TransferResult<CFValue, CFStore> result = super.visitEqualTo(n, in);
CFStore thenStore = result.getThenStore();
CFStore elseStore = result.getElseStore();

createComparisonVariableSlot(n.getLeftOperand(), thenStore, elseStore);
createComparisonVariableSlot(n.getRightOperand(), thenStore, elseStore);

CFValue newResultValue =
getInferenceAnalysis()
.createAbstractValue(typeFactory.getAnnotatedType(n.getTree()));
return new ConditionalTransferResult<>(newResultValue, thenStore, elseStore);
}

@Override
public TransferResult<CFValue, CFStore> visitNotEqual(
NotEqualNode n, TransferInput<CFValue, CFStore> in) {
TransferResult<CFValue, CFStore> result = super.visitNotEqual(n, in);
CFStore thenStore = result.getThenStore();
CFStore elseStore = result.getElseStore();

createComparisonVariableSlot(n.getLeftOperand(), thenStore, elseStore);
createComparisonVariableSlot(n.getRightOperand(), thenStore, elseStore);

CFValue newResultValue =
analysis.createAbstractValue(typeFactory.getAnnotatedType(n.getTree()));
return new ConditionalTransferResult<>(newResultValue, thenStore, elseStore);
}
}
14 changes: 12 additions & 2 deletions src/checkers/inference/dataflow/InferenceValue.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
package checkers.inference.dataflow;

import checkers.inference.model.ComparisonVariableSlot;
import checkers.inference.util.InferenceUtil;
import javax.lang.model.type.TypeVariable;
import org.checkerframework.framework.flow.CFValue;
Expand Down Expand Up @@ -153,9 +154,18 @@ public CFValue mostSpecificFromSlot(final Slot thisSlot, final Slot otherSlot, f
return other;
}

if (thisSlot instanceof ComparisonVariableSlot
&& ((ComparisonVariableSlot) thisSlot).getRefined().equals(otherSlot)) {
return this;
}
if (otherSlot instanceof ComparisonVariableSlot
&& ((ComparisonVariableSlot) otherSlot).getRefined().equals(thisSlot)) {
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()) {
for (VariableSlot slot : ((VariableSlot) thisSlot).getRefinedToSlots()) {
if (slot.isMergedTo(otherSlot)) {
return other;
}
Expand All @@ -164,7 +174,7 @@ public CFValue mostSpecificFromSlot(final Slot thisSlot, final Slot otherSlot, f

if (otherSlot instanceof VariableSlot) {
// Same as above
for (RefinementVariableSlot slot : ((VariableSlot) otherSlot).getRefinedToSlots()) {
for (VariableSlot slot : ((VariableSlot) otherSlot).getRefinedToSlots()) {
if (slot.isMergedTo(thisSlot)) {
return this;
}
Expand Down
4 changes: 2 additions & 2 deletions src/checkers/inference/model/VariableSlot.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ public abstract class VariableSlot extends Slot {
private AnnotationLocation location;

/** Refinement variables that refine this slot. */

@wmdietl wmdietl Feb 23, 2022

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What is the motivation for this change? Can you update the javadoc to explain what kinds of VariableSlots to expect?

@wmdietl wmdietl Feb 23, 2022

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should the name of the method and field be updated to reflect this change?

@d367wang d367wang Mar 7, 2022

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

private final Set<RefinementVariableSlot> refinedToSlots = new HashSet<>();
private final Set<VariableSlot> refinedToSlots = new HashSet<>();

/**
* Create a Slot with the given annotation location.
Expand All @@ -53,7 +53,7 @@ public void setLocation(AnnotationLocation location) {
this.location = location;
}

public Set<RefinementVariableSlot> getRefinedToSlots() {
public Set<VariableSlot> getRefinedToSlots() {
return refinedToSlots;
}

Expand Down
19 changes: 19 additions & 0 deletions testdata/ostrusted-inferrable-test/Comparison.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
import ostrusted.qual.OsTrusted;
import ostrusted.qual.OsUntrusted;

public class Comparison {

void foo(@OsUntrusted Object o) {
if (o == null) {
bar(o);
Comment thread
d367wang marked this conversation as resolved.
}
}

@OsTrusted
Object bar(Object o) {
// :: fixable-error: (return.type.incompatible)
return o;
}

}