Skip to content
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.

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

ConstraintManager source tree fix #137

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open
Changes from all commits
Commits
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
42 changes: 28 additions & 14 deletions src/checkers/inference/model/ConstraintManager.java
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,9 @@
import org.checkerframework.framework.type.QualifierHierarchy;
import org.checkerframework.framework.type.VisitorState;
import org.checkerframework.javacutil.BugInCF;

import com.sun.source.tree.Tree;

import checkers.inference.InferenceAnnotatedTypeFactory;
import checkers.inference.VariableAnnotator;
import checkers.inference.model.ArithmeticConstraint.ArithmeticOperationKind;
Expand Down Expand Up @@ -91,7 +94,7 @@ public void stopIgnoringConstraints() {
* {@link AlwaysTrueConstraint}, {@link AlwaysFalseConstraint}, or {@link EqualityConstraint}.
*/
public Constraint createSubtypeConstraint(Slot subtype, Slot supertype) {
return SubtypeConstraint.create(subtype, supertype, getCurrentLocation(),
return SubtypeConstraint.create(subtype, supertype, getCurrentAnnotationLocation(),
realQualHierarchy);
}

Expand All @@ -100,38 +103,38 @@ public Constraint createSubtypeConstraint(Slot subtype, Slot supertype) {
* {@link AlwaysTrueConstraint} or {@link AlwaysFalseConstraint}.
*/
public Constraint createEqualityConstraint(Slot first, Slot second) {
return EqualityConstraint.create(first, second, getCurrentLocation());
return EqualityConstraint.create(first, second, getCurrentAnnotationLocation());
}

/**
* Creates an {@link InequalityConstraint} between the two slots, which may be normalized to
* {@link AlwaysTrueConstraint} or {@link AlwaysFalseConstraint}.
*/
public Constraint createInequalityConstraint(Slot first, Slot second) {
return InequalityConstraint.create(first, second, getCurrentLocation());
return InequalityConstraint.create(first, second, getCurrentAnnotationLocation());
}

/**
* Creates a {@link ComparableConstraint} between the two slots, which may be normalized to
* {@link AlwaysTrueConstraint} or {@link AlwaysFalseConstraint}.
*/
public Constraint createComparableConstraint(Slot first, Slot second) {
return ComparableConstraint.create(first, second, getCurrentLocation(), realQualHierarchy);
return ComparableConstraint.create(first, second, getCurrentAnnotationLocation(), realQualHierarchy);
}

/**
* Creates a {@link CombineConstraint} between the three slots.
*/
public CombineConstraint createCombineConstraint(Slot target, Slot decl, Slot result) {
return CombineConstraint.create(target, decl, result, getCurrentLocation());
return CombineConstraint.create(target, decl, result, getCurrentAnnotationLocation());
}

/**
* Creates a {@link PreferenceConstraint} for the given slots with the given weight.
*/
public PreferenceConstraint createPreferenceConstraint(VariableSlot variable, ConstantSlot goal,
int weight) {
return PreferenceConstraint.create(variable, goal, weight, getCurrentLocation());
return PreferenceConstraint.create(variable, goal, weight, getCurrentAnnotationLocation());
}

/**
Expand All @@ -140,11 +143,11 @@ public PreferenceConstraint createPreferenceConstraint(VariableSlot variable, Co
public ExistentialConstraint createExistentialConstraint(Slot slot,
List<Constraint> ifExistsConstraints, List<Constraint> ifNotExistsConstraints) {
return ExistentialConstraint.create((VariableSlot) slot, ifExistsConstraints,
ifNotExistsConstraints, getCurrentLocation());
ifNotExistsConstraints, getCurrentAnnotationLocation());
}

public Constraint createImplicationConstraint(List<Constraint> assumptions, Constraint conclusion) {
return ImplicationConstraint.create(assumptions, conclusion, getCurrentLocation());
return ImplicationConstraint.create(assumptions, conclusion, getCurrentAnnotationLocation());
}

/**
Expand All @@ -153,11 +156,11 @@ public Constraint createImplicationConstraint(List<Constraint> assumptions, Cons
public ArithmeticConstraint createArithmeticConstraint(ArithmeticOperationKind operation,
Slot leftOperand, Slot rightOperand, ArithmeticVariableSlot result) {
return ArithmeticConstraint.create(operation, leftOperand, rightOperand, result,
getCurrentLocation());
getCurrentAnnotationLocation());
}

// TODO: give location directly in Constraint.create() methods
private AnnotationLocation getCurrentLocation() {
private AnnotationLocation getCurrentAnnotationLocation() {
Copy link
Member Author

Choose a reason for hiding this comment

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

Javadoc

if (visitorState.getPath() != null) {
return VariableAnnotator.treeToLocation(inferenceTypeFactory,
visitorState.getPath().getLeaf());
Expand All @@ -166,6 +169,17 @@ private AnnotationLocation getCurrentLocation() {
}
}

// visitorState.getPath().getLeaf() caused NullPointerException on some real project
// and doesn't always return correct source tree. Using class tree at least shows which
Copy link
Member

@CharlesZ-Chen CharlesZ-Chen Jan 23, 2018

Choose a reason for hiding this comment

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

  1. "Using class tree at least shows " is ambiguous -- i.e. the code in this function actually only use class tree when visitorState.getPath() is null.
    Maybe only add a code comment on the else branch to document using class tree is a workaround for when visitorState.getPath() is null?

  2. " and doesn't always return correct source tree": do you have minimum code example for that? Should this be an issue instead of a code comment?

// Java source class there is such unsatisfiable error and also doesn't throw exception
private Tree getCurrentTreeLocation() {
Copy link
Member Author

Choose a reason for hiding this comment

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

Add Javadoc

if (visitorState.getPath() != null) {
return visitorState.getPath().getLeaf();
} else {
return visitorState.getClassTree();
Copy link
Member Author

Choose a reason for hiding this comment

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

Add TODOs for both methods - why hitting this case(else branch)?

Copy link
Member Author

Choose a reason for hiding this comment

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

Issue: find a minimum test case
Throw NPE in else branch, and find the project that causes exception.

}
}

// All addXXXConstraint methods create a (possibly normalized) constraint for the given slots.
// They also issue errors for unsatisfiable constraints, unless the method name has "NoErrorMsg"
// in it.
Expand All @@ -183,7 +197,7 @@ public void addSubtypeConstraint(Slot subtype, Slot supertype) {
// this subtype constraint originates from.
// Same for constraints below.
checker.report(Result.failure("subtype.constraint.unsatisfiable", subtype, supertype),
visitorState.getPath().getLeaf());
getCurrentTreeLocation());
} else {
add(constraint);
}
Expand Down Expand Up @@ -214,7 +228,7 @@ public void addEqualityConstraint(Slot first, Slot second) {
Constraint constraint = createEqualityConstraint(first, second);
if (constraint instanceof AlwaysFalseConstraint) {
checker.report(Result.failure("equality.constraint.unsatisfiable", first, second),
visitorState.getPath().getLeaf());
getCurrentTreeLocation());
} else {
add(constraint);
}
Expand All @@ -229,7 +243,7 @@ public void addInequalityConstraint(Slot first, Slot second) {
Constraint constraint = createInequalityConstraint(first, second);
if (constraint instanceof AlwaysFalseConstraint) {
checker.report(Result.failure("inequality.constraint.unsatisfiable", first, second),
visitorState.getPath().getLeaf());
getCurrentTreeLocation());
} else {
add(constraint);
}
Expand All @@ -244,7 +258,7 @@ public void addComparableConstraint(Slot first, Slot second) {
Constraint constraint = createComparableConstraint(first, second);
if (constraint instanceof AlwaysFalseConstraint) {
checker.report(Result.failure("comparable.constraint.unsatisfiable", first, second),
visitorState.getPath().getLeaf());
getCurrentTreeLocation());
} else {
add(constraint);
}
Expand Down