-
Notifications
You must be signed in to change notification settings - Fork 13
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
base: master
Are you sure you want to change the base?
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -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; | ||
|
@@ -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); | ||
} | ||
|
||
|
@@ -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()); | ||
} | ||
|
||
/** | ||
|
@@ -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()); | ||
} | ||
|
||
/** | ||
|
@@ -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() { | ||
if (visitorState.getPath() != null) { | ||
return VariableAnnotator.treeToLocation(inferenceTypeFactory, | ||
visitorState.getPath().getLeaf()); | ||
|
@@ -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 | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
|
||
// Java source class there is such unsatisfiable error and also doesn't throw exception | ||
private Tree getCurrentTreeLocation() { | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe 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(); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Add TODOs for both methods - why hitting this case(else branch)? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Issue: find a minimum test case |
||
} | ||
} | ||
|
||
// 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. | ||
|
@@ -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); | ||
} | ||
|
@@ -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); | ||
} | ||
|
@@ -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); | ||
} | ||
|
@@ -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); | ||
} | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Javadoc