Skip to content

Commit

Permalink
commits for fixing PICO-TypeCheck and part of PICO-Infer
Browse files Browse the repository at this point in the history
  • Loading branch information
@AndrewShf
AndrewShf committed Jul 13, 2022
1 parent 6e4e3c6 commit e4ced88
Show file tree
Hide file tree
Showing 21 changed files with 338 additions and 298 deletions.
4 changes: 4 additions & 0 deletions build.gradle
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,8 @@ sourceSets {
main {
java {
srcDirs = ["src/main/java"]
exclude "pico/inference/**"

}

resources {
Expand All @@ -62,6 +64,8 @@ sourceSets {
java {
// TODO: we shouldn't need source level dependency on CFITest
srcDirs = ["src/test/java", "${cfiPath}/tests/checkers/inference/test"]
exclude "pico/ImmutabilityInferenceInitialTypecheckTest.java","pico/ImmutabilityReImInferenceTest.java",
"pico/ImmutabilityInferenceTest.java"
}
}
}
Expand Down
9 changes: 2 additions & 7 deletions src/main/java/pico/inference/PICOInferenceChecker.java
View file
Original file line number Diff line number Diff line change
@@ -1,11 +1,6 @@
package pico.inference;

import checkers.inference.BaseInferrableChecker;
import checkers.inference.InferenceAnnotatedTypeFactory;
import checkers.inference.InferenceChecker;
import checkers.inference.InferenceVisitor;
import checkers.inference.InferrableChecker;
import checkers.inference.SlotManager;
import checkers.inference.*;
import checkers.inference.model.ConstraintManager;
import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
import org.checkerframework.framework.source.SupportedOptions;
Expand All @@ -24,7 +19,7 @@ public void initChecker() {
}

@Override
public BaseAnnotatedTypeFactory createRealTypeFactory() {
public BaseInferenceRealTypeFactory createRealTypeFactory(boolean infer) {
return new PICOInferenceRealTypeFactory(this, true);
}

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 @@ -16,6 +16,7 @@
import javax.lang.model.type.TypeMirror;
import javax.lang.model.util.Elements;

import checkers.inference.BaseInferenceRealTypeFactory;
import com.sun.tools.javac.tree.JCTree;
import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
import org.checkerframework.common.basetype.BaseTypeChecker;
Expand Down Expand Up @@ -58,7 +59,7 @@
* to InitializationAnnotatedTypeFactory as if there is only one mutability qualifier hierarchy.
* This class has lots of copied code from PICOAnnotatedTypeFactory. The two should be in sync.
*/
public class PICOInferenceRealTypeFactory extends BaseAnnotatedTypeFactory implements ViewpointAdapterGettable {
public class PICOInferenceRealTypeFactory extends BaseInferenceRealTypeFactory implements ViewpointAdapterGettable {

private static final List<String> IMMUTABLE_ALIASES = Arrays.asList(
"com.google.errorprone.annotations.Immutable",
Expand Down Expand Up @@ -226,7 +227,7 @@ public AnnotatedTypeMirror getTypeOfExtendsImplements(Tree clause) {

}
AnnotationMirror mainBound = enclosing.getAnnotationInHierarchy(READONLY);
AnnotatedTypeMirror fromTypeTree = this.fromTypeTree(clause);
AnnotatedTypeMirror fromTypeTree = this.getAnnotatedTypeFromTypeTree(clause);
if (!fromTypeTree.isAnnotatedInHierarchy(READONLY)) {
fromTypeTree.addAnnotation(mainBound);
}
Expand Down
28 changes: 22 additions & 6 deletions src/main/java/pico/inference/PICOInferenceVisitor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -148,6 +148,7 @@ private boolean isAdaptedSubtype(AnnotatedTypeMirror lhs, AnnotatedTypeMirror rh
if (extractVarAnnot(lhs).equals(extractVarAnnot(rhs))) {
return true;
}
// todo: haifeng we should do the viewpointAdapt in baseTypeValidator.java#visitDeclared 299 function:getTypeDeclarationBounds
ExtendedViewpointAdapter vpa = ((ViewpointAdapterGettable)atypeFactory).getViewpointAdapter();
AnnotatedTypeMirror adapted = vpa.rawCombineAnnotationWithType(extractVarAnnot(lhs),
rhs);
Expand Down Expand Up @@ -494,7 +495,22 @@ public Void visitMethod(MethodTree node, Void p) {
// TODO Object identity check
return super.visitMethod(node, p);
}

/*
* @RDM
* class A <T> {
*
* void foo(T) {
*
* }
* }
* class B extends @Immutable A<@X String> {
*
* @Override
* void foo(@Y String) { // string is compatible to bound of T. Adapt the signature of Class A to the use of class B.
* }
* }
*
* */
private void flexibleOverrideChecker(MethodTree node) {
// Method overriding checks
// TODO Copied from super, hence has lots of duplicate code with super. We need to
Expand All @@ -520,7 +536,7 @@ private void flexibleOverrideChecker(MethodTree node) {
types, atypeFactory, enclosingType, pair.getValue());
// Viewpoint adapt super method executable type to current class bound(is this always class bound?)
// to allow flexible overriding
atypeFactory.getViewpointAdapter().viewpointAdaptMethod(enclosingType, pair.getValue() , overriddenMethod);
atypeFactory.getViewpointAdapter().viewpointAdaptMethod(enclosingType, pair.getValue() , overriddenMethod); // todo: should we cast it?
AnnotatedExecutableType overrider = atypeFactory.getAnnotatedType(node);
if (!checkOverride(node, overrider, enclosingType, overriddenMethod, overriddenType)) {
// Stop at the first mismatch; this makes a difference only if
Expand Down Expand Up @@ -707,7 +723,7 @@ private void checkAssignableField(ExpressionTree node, ExpressionTree variable,
}
}

private void checkInitializingObject(ExpressionTree node, ExpressionTree variable, AnnotatedTypeMirror receiverType) {
private void checkInitializingObject(ExpressionTree node, ExpressionTree variable, AnnotatedTypeMirror receiverType) { // todo: haifeng we only need to do this in one statement
// TODO rm infer after mainIsNot returns bool
if (infer) {
// Can be anything from mutable, immutable or receiverdependantmutable
Expand All @@ -718,7 +734,7 @@ private void checkInitializingObject(ExpressionTree node, ExpressionTree variabl
}
}
}

// todo: haifeng: the deciding factor seems to be if it is array or not. Not infer.
private void checkMutableReceiverCase(ExpressionTree node, ExpressionTree variable, AnnotatedTypeMirror receiverType) {
// TODO rm infer after mainIs returns bool
if (infer) {
Expand Down Expand Up @@ -1004,7 +1020,7 @@ private boolean checkCompatabilityBetweenBoundAndSuperClassesBounds(ClassTree no
*/
@Override
protected void commonAssignmentCheck(
Tree varTree, ExpressionTree valueExp, String errorKey) {
Tree varTree, ExpressionTree valueExp, String errorKey, Object... extraArgs) {
AnnotatedTypeMirror var = atypeFactory.getAnnotatedTypeLhs(varTree);
assert var != null : "no variable found for tree: " + varTree;

Expand Down Expand Up @@ -1043,7 +1059,7 @@ protected void commonAssignmentCheck(
@Override
protected void commonAssignmentCheck(AnnotatedTypeMirror varType,
AnnotatedTypeMirror valueType, Tree valueTree,
String errorKey) {
String errorKey, Object... extraArgs) {
// TODO: WORKAROUND: anonymous class handling
if (TypesUtils.isAnonymous(valueType.getUnderlyingType())) {
AnnotatedTypeMirror newValueType = varType.deepCopy();
Expand Down
177 changes: 87 additions & 90 deletions src/main/java/pico/inference/PICOVariableAnnotator.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,80 +45,80 @@ public PICOVariableAnnotator(InferenceAnnotatedTypeFactory typeFactory, Annotate
super(typeFactory, realTypeFactory, realChecker, slotManager, constraintManager);
}

@Override
protected void handleClassDeclaration(AnnotatedDeclaredType classType, ClassTree classTree) {
super.handleClassDeclaration(classType, classTree);
int interfaceIndex = 1;
for(Tree implementsTree : classTree.getImplementsClause()) {
final AnnotatedTypeMirror implementsType = inferenceTypeFactory.getAnnotatedTypeFromTypeTree(implementsTree);
AnnotatedTypeMirror supertype = classType.directSuperTypes().get(interfaceIndex);
assert supertype.getUnderlyingType() == implementsType.getUnderlyingType();
visit(supertype, implementsTree);
interfaceIndex++;
}
}

@Override
protected void handleClassDeclarationBound(AnnotatedDeclaredType classType) {
TypeElement classElement = (TypeElement) classType.getUnderlyingType().asElement();
if (classDeclAnnos.containsKey(classElement)) {
classType.addAnnotation(slotManager.getAnnotation(classDeclAnnos.get(classElement)));
classType.addAnnotation(READONLY);
return;
}
AnnotatedDeclaredType bound = inferenceTypeFactory.fromElement(classElement);

VariableSlot boundSlot;

// Insert @Immutable VarAnnot directly to enum bound
// if (PICOTypeUtil.isEnumOrEnumConstant(bound)) {
// boundSlot = slotManager.createConstantSlot(IMMUTABLE);
// classType.addAnnotation(slotManager.getAnnotation(boundSlot));
// classDeclAnnos.put(classElement, boundSlot);
// @Override
// protected void handleClassDeclaration(AnnotatedDeclaredType classType, ClassTree classTree) {
// super.handleClassDeclaration(classType, classTree);
// int interfaceIndex = 1;
// for(Tree implementsTree : classTree.getImplementsClause()) {
// final AnnotatedTypeMirror implementsType = inferenceTypeFactory.getAnnotatedTypeFromTypeTree(implementsTree);
// AnnotatedTypeMirror supertype = classType.directSupertypes().get(interfaceIndex);
// assert supertype.getUnderlyingType() == implementsType.getUnderlyingType();
// visit(supertype, implementsTree);
// interfaceIndex++;
// }
// }

// @Override
// protected void handleClassDeclarationBound(AnnotatedDeclaredType classType) {
// TypeElement classElement = (TypeElement) classType.getUnderlyingType().asElement();
// if (classDeclAnnos.containsKey(classElement)) {
// classType.addAnnotation(slotManager.getAnnotation(classDeclAnnos.get(classElement)));
// classType.addAnnotation(READONLY);
// return;
// }

Tree classTree = inferenceTypeFactory.declarationFromElement(classElement);
if (classTree != null) {
// Have source tree
if (bound.isAnnotatedInHierarchy(READONLY)) {
// Have bound annotation -> convert to equivalent ConstantSlot
boundSlot = slotManager.createConstantSlot(bound.getAnnotationInHierarchy(READONLY));
} else {
// No existing annotation -> create new VariableSlot
boundSlot = createVariable(treeToLocation(classTree));
}
} else {
// No source tree: bytecode classes
if (bound.isAnnotatedInHierarchy(READONLY)) {
// Have bound annotation in stub file
boundSlot = slotManager.createConstantSlot(bound.getAnnotationInHierarchy(READONLY));
} else {
// No stub file
if (PICOTypeUtil.isImplicitlyImmutableType(classType)) {
// Implicitly immutable
boundSlot = slotManager.createConstantSlot(IMMUTABLE);
} else {
// None of the above applies: use conservative @Mutable
boundSlot = slotManager.createConstantSlot(MUTABLE);
}
}
}
classType.addAnnotation(slotManager.getAnnotation(boundSlot));
classDeclAnnos.put(classElement, boundSlot);
}
// AnnotatedDeclaredType bound = inferenceTypeFactory.fromElement(classElement);
//
// VariableSlot boundSlot;
//
// // Insert @Immutable VarAnnot directly to enum bound
//// if (PICOTypeUtil.isEnumOrEnumConstant(bound)) {
//// boundSlot = slotManager.createConstantSlot(IMMUTABLE);
//// classType.addAnnotation(slotManager.getAnnotation(boundSlot));
//// classDeclAnnos.put(classElement, boundSlot);
//// return;
//// }
//
// Tree classTree = inferenceTypeFactory.declarationFromElement(classElement);
// if (classTree != null) {
// // Have source tree
// if (bound.isAnnotatedInHierarchy(READONLY)) {
// // Have bound annotation -> convert to equivalent ConstantSlot
// boundSlot = slotManager.createConstantSlot(bound.getAnnotationInHierarchy(READONLY));
// } else {
// // No existing annotation -> create new VariableSlot
// boundSlot = createVariable(treeToLocation(classTree));
// }
// } else {
// // No source tree: bytecode classes
// if (bound.isAnnotatedInHierarchy(READONLY)) {
// // Have bound annotation in stub file
// boundSlot = slotManager.createConstantSlot(bound.getAnnotationInHierarchy(READONLY));
// } else {
// // No stub file
// if (PICOTypeUtil.isImplicitlyImmutableType(classType)) {
// // Implicitly immutable
// boundSlot = slotManager.createConstantSlot(IMMUTABLE);
// } else {
// // None of the above applies: use conservative @Mutable
// boundSlot = slotManager.createConstantSlot(MUTABLE);
// }
// }
// }
// classType.addAnnotation(slotManager.getAnnotation(boundSlot));
// classDeclAnnos.put(classElement, boundSlot);
// }

@Override
protected VariableSlot getOrCreateDeclBound(AnnotatedDeclaredType type) {
TypeElement classDecl = (TypeElement) type.getUnderlyingType().asElement();

VariableSlot declSlot = classDeclAnnos.get(classDecl);
AnnotationMirror declSlot = getClassDeclVarAnnot(classDecl);
if (declSlot == null) {
// if a explicit annotation presents on the class DECL, use that directly
if (type.isDeclaration() && type.isAnnotatedInHierarchy(READONLY) && !type.hasAnnotation(READONLY)) {
VariableSlot constantSlot = (VariableSlot) slotManager.getSlot(type.getAnnotationInHierarchy(READONLY));
// TypeElement classDecl = (TypeElement) type.getUnderlyingType().asElement();
classDeclAnnos.put(classDecl, constantSlot);
super.getOrCreateDeclBound(type);
// // avoid duplicate annos
// type.removeAnnotationInHierarchy(READONLY);
return constantSlot;
Expand All @@ -134,21 +134,21 @@ protected VariableSlot getOrCreateDeclBound(AnnotatedDeclaredType type) {
return (VariableSlot) slotManager.getSlot(type.getAnnotation(VarAnnot.class));
}
}
return super.getOrCreateDeclBound(type);
return (VariableSlot) super.getOrCreateDeclBound(type);
}

@Override
protected void handleExplicitExtends(Tree extendsTree) {
// PICO cannot use base extends handling: not simply subtype relationship because of RDM
// Constraints already generated in processClassTree
}
// @Override
// protected void handleExplicitExtends(Tree extendsTree) {
// // PICO cannot use base extends handling: not simply subtype relationship because of RDM
// // Constraints already generated in processClassTree
// }

@Override
public void storeElementType(Element element, AnnotatedTypeMirror atm) {
// this method is override the behavior of super.handleClassDeclaration before storing
// find a better way

Slot slot = slotManager.getVariableSlot(atm);
Slot slot = slotManager.getSlot(atm);
// do not use potential slot generated on the class decl annotation
// PICO always have a annotation on the class bound, so Existential should always exist
// TODO make VariableAnnotator::getOrCreateDeclBound protected and override that instead of this method
Expand All @@ -167,22 +167,22 @@ public void storeElementType(Element element, AnnotatedTypeMirror atm) {
}

// Don't generate subtype constraint between use type and bound type
@Override
protected void handleInstantiationConstraint(AnnotatedTypeMirror.AnnotatedDeclaredType adt, VariableSlot instantiationSlot, Tree tree) {
return;
}

@Override
protected VariableSlot addPrimaryVariable(AnnotatedTypeMirror atm, Tree tree) {
// if (PICOTypeUtil.isEnumOrEnumConstant(atm)) {
// // Don't add new VarAnnot to type use of enum type
// PICOTypeUtil.applyConstant(atm, IMMUTABLE);
// @Override
// protected void handleInstantiationConstraint(AnnotatedTypeMirror.AnnotatedDeclaredType adt, VariableSlot instantiationSlot, Tree tree) {
// return;
// }

// @Override
// protected VariableSlot addPrimaryVariable(AnnotatedTypeMirror atm, Tree tree) {
//// if (PICOTypeUtil.isEnumOrEnumConstant(atm)) {
//// // Don't add new VarAnnot to type use of enum type
//// PICOTypeUtil.applyConstant(atm, IMMUTABLE);
//// }
// if (atm instanceof AnnotatedTypeMirror.AnnotatedNullType) {
// PICOTypeUtil.applyConstant(atm, BOTTOM);
// }
if (atm instanceof AnnotatedTypeMirror.AnnotatedNullType) {
PICOTypeUtil.applyConstant(atm, BOTTOM);
}
return super.addPrimaryVariable(atm, tree);
}
// return super.addPrimaryVariable(atm, tree);
// }

// Generates inequality constraint between every strict VariableSlot and @Bottom so that @Bottom is not inserted
// back to source code, but can be within the internal state because of dataflow refinement
Expand Down Expand Up @@ -285,7 +285,7 @@ public Void visitWildcard(AnnotatedTypeMirror.AnnotatedWildcardType wildcardType

@Override
public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) {
if (atm.isAnnotatedInHierarchy(varAnnot)) {
if (atm.isAnnotatedInHierarchy(inferenceTypeFactory.getVarAnnot())) {
// Happens for binary trees whose atm is implicitly immutable and already handled by
// PICOInferencePropagationTreeAnnotator
return;
Expand All @@ -294,15 +294,12 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) {
}

public AnnotationMirror getClassDeclAnno(Element ele) {
if (classDeclAnnos.get(ele) != null) {
return slotManager.getAnnotation(classDeclAnnos.get(ele));
}
return null;
return getClassDeclVarAnnot((TypeElement) ele); // todo: solved
}


@Override
protected void addDeclarationConstraints(VariableSlot declSlot, VariableSlot instanceSlot) {
protected void addDeclarationConstraints(Slot declSlot, Slot instanceSlot) {
// RDM-related constraints cannot use subtype.
// Necessary constraints added in visitor instead.
}
Expand Down
Loading

0 comments on commit e4ced88

Please sign in to comment.