Skip to content

Commit

Permalink
Changes for updates from eisop (#391)
Browse files Browse the repository at this point in the history
  • Loading branch information
zcai1 authored Mar 13, 2022
1 parent 0d3e5a4 commit 21dfba4
Show file tree
Hide file tree
Showing 5 changed files with 31 additions and 16 deletions.
2 changes: 1 addition & 1 deletion scripts/inference-dev
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ libDir="$cfiDir"/lib
CFBuild="${cfDir}"/dataflow/"${classes}":"${cfDir}"/javacutil/"${classes}":"${cfDir}"/framework/"${classes}":"${cfDir}"/framework/"${resources}"
CFBuild="${CFBuild}":"${cfDir}"/checker/"${classes}":"${cfDir}"/checker/"${resources}":"${annoToolsDir}"/scene-lib/bin

CFDepJars="${stubparserDir}"/javaparser-core/target/stubparser-3.22.1.jar:"${afuDir}"/annotation-file-utilities-all.jar
CFDepJars="${stubparserDir}"/javaparser-core/target/stubparser-3.24.0.jar:"${afuDir}"/annotation-file-utilities-all.jar

# sanity check: ensure each jar in CFDepJars actually exists in the file system
# total number of jars
Expand Down
4 changes: 2 additions & 2 deletions src/checkers/inference/InferenceAnnotatedTypeFactory.java
Original file line number Diff line number Diff line change
Expand Up @@ -314,7 +314,7 @@ public void postAsMemberOf(final AnnotatedTypeMirror type,
@Override
public ParameterizedExecutableType methodFromUse(final MethodInvocationTree methodInvocationTree) {
assert methodInvocationTree != null : "MethodInvocationTree in methodFromUse was null. " +
"Current path:\n" + this.visitorState.getPath();
"Current path:\n" + getVisitorTreePath();
final ExecutableElement methodElem = TreeUtils.elementFromUse(methodInvocationTree);

// TODO: Used in comb constraints, going to leave it in to ensure the element has been visited
Expand Down Expand Up @@ -375,7 +375,7 @@ public Boolean visitDeclared(AnnotatedDeclaredType type, Void p) {
@Override
public ParameterizedExecutableType constructorFromUse(final NewClassTree newClassTree) {
assert newClassTree != null : "NewClassTree was null when attempting to get constructorFromUse. " +
"Current path:\n" + this.visitorState.getPath();
"Current path:\n" + getVisitorTreePath();

final ExecutableElement constructorElem = TreeUtils.constructor(newClassTree);;
final AnnotatedTypeMirror constructorReturnType = fromNewClass(newClassTree);
Expand Down
36 changes: 25 additions & 11 deletions src/checkers/inference/model/ConstraintManager.java
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,10 @@
import java.util.HashSet;
import java.util.List;
import java.util.Set;

import com.sun.source.util.TreePath;
import org.checkerframework.framework.source.SourceChecker;
import org.checkerframework.framework.type.QualifierHierarchy;
import org.checkerframework.framework.type.VisitorState;
import org.checkerframework.javacutil.BugInCF;
import checkers.inference.InferenceAnnotatedTypeFactory;
import checkers.inference.VariableAnnotator;
Expand All @@ -30,12 +31,9 @@ public class ConstraintManager {

private QualifierHierarchy realQualHierarchy;

private VisitorState visitorState;

public void init(InferenceAnnotatedTypeFactory inferenceTypeFactory) {
this.inferenceTypeFactory = inferenceTypeFactory;
this.realQualHierarchy = inferenceTypeFactory.getRealQualifierHierarchy();
this.visitorState = inferenceTypeFactory.getVisitorState();
this.checker = inferenceTypeFactory.getChecker();
}

Expand Down Expand Up @@ -166,9 +164,9 @@ public ArithmeticConstraint createArithmeticConstraint(ArithmeticOperationKind o

// TODO: give location directly in Constraint.create() methods
private AnnotationLocation getCurrentLocation() {
if (visitorState.getPath() != null) {
return VariableAnnotator.treeToLocation(inferenceTypeFactory,
visitorState.getPath().getLeaf());
TreePath path = inferenceTypeFactory.getVisitorTreePath();
if (path != null) {
return VariableAnnotator.treeToLocation(inferenceTypeFactory, path.getLeaf());
} else {
return AnnotationLocation.MISSING_LOCATION;
}
Expand All @@ -190,7 +188,11 @@ public void addSubtypeConstraint(Slot subtype, Slot supertype) {
// relevant error message (eg assignment.type.incompatible) at the precise code AST node
// this subtype constraint originates from.
// Same for constraints below.
checker.reportError(visitorState.getPath().getLeaf(), "subtype.constraint.unsatisfiable", subtype, supertype);
checker.reportError(
inferenceTypeFactory.getVisitorTreePath().getLeaf(),
"subtype.constraint.unsatisfiable",
subtype,
supertype);
} else {
add(constraint);
}
Expand Down Expand Up @@ -220,7 +222,11 @@ public boolean addSubtypeConstraintNoErrorMsg(Slot subtype, Slot supertype) {
public void addEqualityConstraint(Slot first, Slot second) {
Constraint constraint = createEqualityConstraint(first, second);
if (constraint instanceof AlwaysFalseConstraint) {
checker.reportError(visitorState.getPath().getLeaf(), "equality.constraint.unsatisfiable", first, second);
checker.reportError(
inferenceTypeFactory.getVisitorTreePath().getLeaf(),
"equality.constraint.unsatisfiable",
first,
second);
} else {
add(constraint);
}
Expand All @@ -234,7 +240,11 @@ public void addEqualityConstraint(Slot first, Slot second) {
public void addInequalityConstraint(Slot first, Slot second) {
Constraint constraint = createInequalityConstraint(first, second);
if (constraint instanceof AlwaysFalseConstraint) {
checker.reportError(visitorState.getPath().getLeaf(), "inequality.constraint.unsatisfiable", first, second);
checker.reportError(
inferenceTypeFactory.getVisitorTreePath().getLeaf(),
"inequality.constraint.unsatisfiable",
first,
second);
} else {
add(constraint);
}
Expand All @@ -248,7 +258,11 @@ public void addInequalityConstraint(Slot first, Slot second) {
public void addComparableConstraint(Slot first, Slot second) {
Constraint constraint = createComparableConstraint(first, second);
if (constraint instanceof AlwaysFalseConstraint) {
checker.reportError(visitorState.getPath().getLeaf(), "comparable.constraint.unsatisfiable", first, second);
checker.reportError(
inferenceTypeFactory.getVisitorTreePath().getLeaf(),
"comparable.constraint.unsatisfiable",
first,
second);
} else {
add(constraint);
}
Expand Down
2 changes: 1 addition & 1 deletion src/interning/InterningVisitor.java
Original file line number Diff line number Diff line change
Expand Up @@ -428,7 +428,7 @@ private boolean suppressInsideComparison(final BinaryTree node) {
return false; // The if statement is not the first statement in the method.
}

ExecutableElement enclosing = TreeUtils.elementFromDeclaration(visitorState.getMethodTree());
ExecutableElement enclosing = TreeUtils.elementFromDeclaration(methodTree);
assert enclosing != null;

final Element lhs = TreeUtils.elementFromUse((IdentifierTree)left);
Expand Down
3 changes: 2 additions & 1 deletion src/nninf/NninfAnnotatedTypeFactory.java
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@
import nninf.qual.Nullable;
import nninf.qual.PolyNull;
import org.checkerframework.javacutil.ElementUtils;
import org.checkerframework.javacutil.TreePathUtil;
import org.checkerframework.javacutil.TreeUtils;

import javax.lang.model.element.Element;
Expand Down Expand Up @@ -96,7 +97,7 @@ public final boolean isMostEnclosingThisDeref(ExpressionTree tree) {
Element element = TreeUtils.elementFromUse(tree);
TypeElement typeElt = ElementUtils.enclosingTypeElement(element);

ClassTree enclosingClass = getCurrentClassTree(tree);
ClassTree enclosingClass = TreePathUtil.enclosingClass(getPath(tree));
if (enclosingClass != null
&& isSubtype(TreeUtils.elementFromDeclaration(enclosingClass), typeElt)) {
return true;
Expand Down

0 comments on commit 21dfba4

Please sign in to comment.