Skip to content

Commit

Permalink
update pico, fix CF api rename, update gradle version
Browse files Browse the repository at this point in the history
  • Loading branch information
Haifeng Shi committed Feb 9, 2022
1 parent 472e75c commit 6e4e3c6
Show file tree
Hide file tree
Showing 11 changed files with 72 additions and 69 deletions.
17 changes: 8 additions & 9 deletions build.gradle
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ plugins {
apply plugin: 'java'

ext {
assert JavaVersion.current() == JavaVersion.VERSION_1_8: "Set JAVA_HOME to JDK 8. Current version is ${JavaVersion.current()}"
assert JavaVersion.current() == JavaVersion.VERSION_11: "Set JAVA_HOME to JDK 11. Current version is ${JavaVersion.current()}"
jsr308 = file(new File("..")).absolutePath
cfPath = "${jsr308}/checker-framework"
cfiPath = "${jsr308}/checker-framework-inference"
Expand All @@ -34,17 +34,16 @@ repositories {
}

dependencies {
compile fileTree(dir: "${cfPath}/checker/dist", include: "checker.jar")
compile fileTree(dir: "${cfiPath}/dist", include: "checker-framework-inference.jar")
implementation fileTree(dir: "${cfPath}/checker/dist", include: "checker.jar")
implementation fileTree(dir: "${cfiPath}/dist", include: "checker-framework-inference.jar")
// sat4j solver dependency
compile 'org.ow2.sat4j:org.ow2.sat4j.core:2.3.4'
compile 'org.ow2.sat4j:org.ow2.sat4j.maxsat:2.3.4'
implementation 'org.ow2.sat4j:org.ow2.sat4j.core:2.3.5'
implementation 'org.ow2.sat4j:org.ow2.sat4j.maxsat:2.3.5'
// The production code uses the SLF4J logging API at compile time
compile 'org.slf4j:slf4j-api:1.7.13'

implementation 'org.slf4j:slf4j-api:1.7.29'
// CF test lib dependency
testCompile fileTree(dir: "${cfPath}/framework-test/build/libs", include: "framework-test-*.jar")
testCompile 'junit:junit:4.12'
testImplementation fileTree(dir: "${cfPath}/framework-test/build/libs", include: "framework-test-*.jar")
testImplementation 'junit:junit:4.12'
}

sourceSets {
Expand Down
2 changes: 1 addition & 1 deletion gradle/wrapper/gradle-wrapper.properties
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,4 +2,4 @@ distributionBase=GRADLE_USER_HOME
distributionPath=wrapper/dists
zipStoreBase=GRADLE_USER_HOME
zipStorePath=wrapper/dists
distributionUrl=https\://services.gradle.org/distributions/gradle-4.5-bin.zip
distributionUrl=https\://services.gradle.org/distributions/gradle-7.3.3-bin.zip
21 changes: 11 additions & 10 deletions src/main/java/pico/common/PICOTypeUtil.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@
import org.checkerframework.javacutil.AnnotationUtils;
import org.checkerframework.javacutil.ElementUtils;
import org.checkerframework.javacutil.TreeUtils;
import org.checkerframework.javacutil.TreePathUtil;
import org.checkerframework.javacutil.TypesUtils;
import pico.typecheck.PICOVisitor;
import qual.Assignable;
Expand Down Expand Up @@ -119,12 +120,12 @@ public static AnnotatedDeclaredType getBoundTypeOfEnclosingTypeDeclaration(Tree
if (node instanceof MethodTree) {
MethodTree methodTree = (MethodTree) node;
ExecutableElement element = TreeUtils.elementFromDeclaration(methodTree);
typeElement = ElementUtils.enclosingClass(element);
typeElement = ElementUtils.enclosingTypeElement(element);
} else if(node instanceof VariableTree) {
VariableTree variableTree = (VariableTree) node;
VariableElement variableElement = TreeUtils.elementFromDeclaration(variableTree);
assert variableElement!= null && variableElement.getKind().isField();
typeElement = ElementUtils.enclosingClass(variableElement);
typeElement = ElementUtils.enclosingTypeElement(variableElement);
}

if (typeElement != null) {
Expand All @@ -135,7 +136,7 @@ public static AnnotatedDeclaredType getBoundTypeOfEnclosingTypeDeclaration(Tree
}

public static AnnotatedDeclaredType getBoundTypeOfEnclosingTypeDeclaration(Element element, AnnotatedTypeFactory atypeFactory) {
TypeElement typeElement = ElementUtils.enclosingClass(element);
TypeElement typeElement = ElementUtils.enclosingTypeElement(element);
if (typeElement != null) {
return getBoundTypeOfTypeDeclaration(typeElement, atypeFactory);
}
Expand Down Expand Up @@ -255,7 +256,7 @@ public static void addDefaultForField(AnnotatedTypeFactory annotatedTypeFactory,

// add RDM if bound=M and enclosingBound=M/RDM
Set<AnnotationMirror> enclosingBound = annotatedTypeFactory.getTypeDeclarationBounds(
Objects.requireNonNull(ElementUtils.enclosingClass(element)).asType());
Objects.requireNonNull(ElementUtils.enclosingTypeElement(element)).asType());
Set<AnnotationMirror> declBound = annotatedTypeFactory.getTypeDeclarationBounds(element.asType());
if (AnnotationUtils.containsSameByName(declBound, MUTABLE)) {
if (AnnotationUtils.containsSameByName(enclosingBound, RECEIVER_DEPENDANT_MUTABLE) ||
Expand Down Expand Up @@ -311,7 +312,7 @@ public static void applyConstant(AnnotatedTypeMirror type, AnnotationMirror am)
// Might be null. It's normal. In typechecking side, we use addMissingAnnotations(). Only if
// there is existing annotation in code, then here is non-null. Otherwise, VariableAnnotator
// hasn't come into the picture yet, so no VarAnnot exists here, which is normal.
Slot shouldBeAppliedTo = slotManager.getVariableSlot(type);
Slot shouldBeAppliedTo = slotManager.getSlot(type);
ConstantSlot constant = slotManager.createConstantSlot(am);
if (shouldBeAppliedTo == null) {
// Here, we are adding VarAnnot that represents @Immutable. There won't be solution for this ConstantSlot for this type,
Expand Down Expand Up @@ -380,7 +381,7 @@ public static boolean isAssigningAssignableField(ExpressionTree node, Annotation
public static boolean isEnclosedByAnonymousClass(Tree tree, AnnotatedTypeFactory atypeFactory) {
TreePath path = atypeFactory.getPath(tree);
if (path != null) {
ClassTree classTree = TreeUtils.enclosingClass(path);
ClassTree classTree = TreePathUtil.enclosingClass(path);
return classTree != null && InferenceUtil.isAnonymousClass(classTree);
}
return false;
Expand All @@ -392,7 +393,7 @@ public static AnnotatedDeclaredType getBoundOfEnclosingAnonymousClass(Tree tree,
return null;
}
AnnotatedDeclaredType enclosingType = null;
Tree newclassTree = TreeUtils.enclosingOfKind(path, Tree.Kind.NEW_CLASS);
Tree newclassTree = TreePathUtil.enclosingOfKind(path, Tree.Kind.NEW_CLASS);
if (newclassTree != null) {
enclosingType = (AnnotatedDeclaredType) atypeFactory.getAnnotatedType(newclassTree);
}
Expand All @@ -407,10 +408,10 @@ public static AnnotationMirror createEquivalentVarAnnotOfRealQualifier(final Ann

public static boolean inStaticScope(TreePath treePath) {
boolean in = false;
if (TreeUtils.isTreeInStaticScope(treePath)) {
if (TreePathUtil.isTreeInStaticScope(treePath)) {
in = true;
// Exclude case in which enclosing class is static
ClassTree classTree = TreeUtils.enclosingClass(treePath);
ClassTree classTree = TreePathUtil.enclosingClass(treePath);
if (classTree != null && classTree.getModifiers().getFlags().contains((Modifier.STATIC))) {
in = false;
}
Expand Down Expand Up @@ -454,7 +455,7 @@ public static boolean isArrayType(AnnotatedDeclaredType type, AnnotatedTypeFacto
// If it is a user-declared "Array" class without package, a class / source file should be there.
// Otherwise, it is the java inner type.
return ele instanceof Symbol.ClassSymbol
&& ElementUtils.getVerboseName(ele).equals("Array")
&& ElementUtils.getQualifiedName(ele).equals("Array")
&& ((Symbol.ClassSymbol) ele).classfile == null
&& ((Symbol.ClassSymbol) ele).sourcefile == null;
}
Expand Down
5 changes: 3 additions & 2 deletions src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@
import org.checkerframework.javacutil.AnnotationUtils;
import org.checkerframework.javacutil.Pair;
import org.checkerframework.javacutil.TreeUtils;
import org.checkerframework.javacutil.TreePathUtil;
import pico.common.ExtendedViewpointAdapter;
import pico.common.ViewpointAdapterGettable;
import pico.typecheck.PICOAnnotatedTypeFactory.PICODefaultForTypeAnnotator;
Expand Down Expand Up @@ -114,7 +115,7 @@ VariableAnnotator getVariableAnnotator() {
*/
public AnnotatedDeclaredType getSelfType(Tree tree) {
TreePath path = getPath(tree);
ClassTree enclosingClass = TreeUtils.enclosingClass(path);
ClassTree enclosingClass = TreePathUtil.enclosingClass(path);
if (enclosingClass == null) {
// I hope this only happens when tree is a fake tree that
// we created, e.g. when desugaring enhanced-for-loops.
Expand All @@ -123,7 +124,7 @@ public AnnotatedDeclaredType getSelfType(Tree tree) {
// "type" is right now VarAnnot inserted to the bound of "enclosingClass"
AnnotatedDeclaredType type = getAnnotatedType(enclosingClass);

MethodTree enclosingMethod = TreeUtils.enclosingMethod(path);
MethodTree enclosingMethod = TreePathUtil.enclosingMethod(path);
if (enclosingClass.getSimpleName().length() != 0 && enclosingMethod != null) {
AnnotatedTypeMirror.AnnotatedDeclaredType methodReceiver;
if (TreeUtils.isConstructor(enclosingMethod)) {
Expand Down
5 changes: 3 additions & 2 deletions src/main/java/pico/inference/PICOInferenceRealTypeFactory.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@
import org.checkerframework.javacutil.AnnotationUtils;
import org.checkerframework.javacutil.BugInCF;
import org.checkerframework.javacutil.TreeUtils;
import org.checkerframework.javacutil.TreePathUtil;

import com.sun.source.tree.Tree;

Expand Down Expand Up @@ -115,7 +116,7 @@ protected TypeAnnotator createTypeAnnotator() {
// annotated.
typeAnnotators.add(
new IrrelevantTypeAnnotator(
this, getQualifierHierarchy().getTopAnnotations(), classes));
this, getQualifierHierarchy().getTopAnnotations()));
}
typeAnnotators.add(new PropagationTypeAnnotator(this));
/*Copied code ends*/
Expand Down Expand Up @@ -215,7 +216,7 @@ protected DefaultQualifierForUseTypeAnnotator createDefaultForUseTypeAnnotator()
@Override
public AnnotatedTypeMirror getTypeOfExtendsImplements(Tree clause) {
// add default anno from class main qual, if no qual present
AnnotatedTypeMirror enclosing = getAnnotatedType(TreeUtils.enclosingClass(getPath(clause)));
AnnotatedTypeMirror enclosing = getAnnotatedType(TreePathUtil.enclosingClass(getPath(clause)));

// workaround for anonymous class.
// TypesUtils::isAnonymous won't work when annotation presents on new class tree!
Expand Down
9 changes: 4 additions & 5 deletions src/main/java/pico/inference/PICOInferenceValidator.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@
import com.sun.source.tree.Tree;
import com.sun.source.tree.VariableTree;
import org.checkerframework.common.basetype.BaseTypeChecker;
import org.checkerframework.framework.source.Result;
import org.checkerframework.framework.type.AnnotatedTypeFactory;
import org.checkerframework.framework.type.AnnotatedTypeMirror;
import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedArrayType;
Expand Down Expand Up @@ -37,7 +36,7 @@ public Void visitDeclared(AnnotatedDeclaredType type, Tree tree) {
checkOnlyOneAssignabilityModifierOnField(tree);
// AnnotatedDeclaredType defaultType =
// (AnnotatedDeclaredType) atypeFactory.getAnnotatedType(type.getUnderlyingType().asElement());
// // TODO for defaulted super clause: should top anno be checked? (see shouldCheckTopLevelDeclaredType())
// // TODO for defaulted super clause: should top anno be checked? (see shouldCheckTopLevelDeclaredOrPrimitiveType())
// if (defaultType.getAnnotationInHierarchy(READONLY) == null && !PICOTypeUtil.isEnumOrEnumConstant(defaultType)) {
// defaultType = defaultType.deepCopy();
// defaultType.replaceAnnotation(MUTABLE);
Expand All @@ -64,11 +63,11 @@ public Void visitPrimitive(AnnotatedPrimitiveType type, Tree tree) {
}

@Override
protected boolean shouldCheckTopLevelDeclaredType(AnnotatedTypeMirror type, Tree tree) {
protected boolean shouldCheckTopLevelDeclaredOrPrimitiveType(AnnotatedTypeMirror type, Tree tree) {
if (TreeUtils.isLocalVariable(tree)) {
return true;
}
return super.shouldCheckTopLevelDeclaredType(type, tree);
return super.shouldCheckTopLevelDeclaredOrPrimitiveType(type, tree);
}

private void checkStaticReceiverDependantMutableError(AnnotatedTypeMirror type, Tree tree) {
Expand Down Expand Up @@ -121,7 +120,7 @@ private void checkOnlyOneAssignabilityModifierOnField(Tree tree) {
}

private void reportFieldMultipleAssignabilityModifiersError(VariableElement field) {
checker.report(Result.failure("one.assignability.invalid", field), field);
checker.reportError(field, "one.assignability.invalid", field);
isValid = false;
}

Expand Down
Loading

0 comments on commit 6e4e3c6

Please sign in to comment.