Skip to content

Commit

Permalink
Further clean up
Browse files Browse the repository at this point in the history
  • Loading branch information
Ao-senXiong committed May 8, 2024
1 parent ac169f1 commit d5c155c
Show file tree
Hide file tree
Showing 2 changed files with 17 additions and 86 deletions.
47 changes: 11 additions & 36 deletions src/main/java/pico/typecheck/PICONoInitAnnotatedTypeFactory.java
Original file line number Diff line number Diff line change
Expand Up @@ -130,10 +130,7 @@ public QualifierHierarchy createQualifierHierarchy() {

@Override
public ParameterizedExecutableType constructorFromUse(NewClassTree tree) {
boolean hasExplicitAnnos = false;
if (!getExplicitNewClassAnnos(tree).isEmpty()) {
hasExplicitAnnos = true;
}
boolean hasExplicitAnnos = !getExplicitNewClassAnnos(tree).isEmpty();
ParameterizedExecutableType mType = super.constructorFromUse(tree);
AnnotatedExecutableType method = mType.executableType;
if (!hasExplicitAnnos && method.getReturnType().hasAnnotation(RECEIVER_DEPENDANT_MUTABLE)) {
Expand Down Expand Up @@ -173,10 +170,7 @@ public PICOPropagationTreeAnnotator(AnnotatedTypeFactory atypeFactory) {
public Void visitNewArray(NewArrayTree tree, AnnotatedTypeMirror type) {
AnnotatedTypeMirror componentType =
((AnnotatedTypeMirror.AnnotatedArrayType) type).getComponentType();
boolean noExplicitATM = false;
if (!componentType.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE)) {
noExplicitATM = true;
}
boolean noExplicitATM = !componentType.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE);
super.visitNewArray(tree, type);
// if new explicit anno before, but RDM after, the RDM must come from the type
// declaration bound
Expand All @@ -189,30 +183,14 @@ public Void visitNewArray(NewArrayTree tree, AnnotatedTypeMirror type) {

@Override
public Void visitTypeCast(TypeCastTree node, AnnotatedTypeMirror type) {
boolean hasExplicitAnnos = false;
if (!type.getAnnotations().isEmpty()) {
hasExplicitAnnos = true;
}
boolean hasExplicitAnnos = !type.getAnnotations().isEmpty();
super.visitTypeCast(node, type);
if (!hasExplicitAnnos && type.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE)) {
type.replaceAnnotation(MUTABLE);
}
return null;
}

//
/**
* Because TreeAnnotator runs before DefaultForTypeAnnotator, implicitly immutable types are
* not guaranteed to always have immutable annotation. If this happens, we manually add
* immutable to type. We use addMissingAnnotations because we want to respect existing
* annotation on type
*/
private void applyImmutableIfImplicitlyImmutable(AnnotatedTypeMirror type) {
if (PICOTypeUtil.isImplicitlyImmutableType(type)) {
type.addMissingAnnotations(new HashSet<>(Collections.singletonList(IMMUTABLE)));
}
}

@Override
public Void visitBinary(BinaryTree node, AnnotatedTypeMirror type) {
return null;
Expand Down Expand Up @@ -360,17 +338,14 @@ public Void visitExecutable(AnnotatedExecutableType t, Void p) {
// for now: default array in receiver, parameter and return type to RDM
if (t.getReceiverType() != null) {
if (PICOTypeUtil.isArrayType(t.getReceiverType(), atypeFactory)) {
switch (t.toString()) {
case "Object clone(Array this)":
// Receiver type will not be viewpoint adapted:
// SyntheticArrays.replaceReturnType() will rollback the viewpoint adapt
// result.
// Use readonly to allow all invocations.
if (!t.getReceiverType().hasAnnotationInHierarchy(READONLY))
t.getReceiverType().replaceAnnotation(READONLY);
// The return type will be fixed by SyntheticArrays anyway.
// Qualifiers added here will not have effect.
break;
if (t.toString().equals("Object clone(Array this)")) {// Receiver type will not be viewpoint adapted:
// SyntheticArrays.replaceReturnType() will rollback the viewpoint adapt
// result.
// Use readonly to allow all invocations.
if (!t.getReceiverType().hasAnnotationInHierarchy(READONLY))
t.getReceiverType().replaceAnnotation(READONLY);
// The return type will be fixed by SyntheticArrays anyway.
// Qualifiers added here will not have effect.
}
}
}
Expand Down
56 changes: 6 additions & 50 deletions src/main/java/pico/typecheck/PICONoInitVisitor.java
Original file line number Diff line number Diff line change
Expand Up @@ -51,15 +51,13 @@
import pico.common.PICOTypeUtil;
import pico.common.ViewpointAdapterGettable;

/** Created by mier on 20/06/17. Enforce PICO type rules. */
public class PICONoInitVisitor extends BaseTypeVisitor<PICONoInitAnnotatedTypeFactory> {

private final boolean shouldOutputFbcError;
final Map<String, Integer> fbcViolatedMethods;

public PICONoInitVisitor(BaseTypeChecker checker) {
super(checker);
shouldOutputFbcError = checker.hasOption("printFbcErrors");
boolean shouldOutputFbcError = checker.hasOption("printFbcErrors");
fbcViolatedMethods = shouldOutputFbcError ? new HashMap<>() : null;
}

Expand Down Expand Up @@ -107,33 +105,6 @@ public boolean isValidUse(AnnotatedTypeMirror.AnnotatedArrayType type, Tree tree
return !AnnotationUtils.areSame(used, BOTTOM);
}

private static boolean isAnnoValidUse(AnnotationMirror declared, AnnotationMirror used) {
if (AnnotationUtils.areSame(declared, RECEIVER_DEPENDANT_MUTABLE)
|| AnnotationUtils.areSame(declared, READONLY)) {
// Element is declared with @ReceiverDependantMutable bound, any instantiation is
// allowed. We don't use
// a subtype check to validate the correct usage here. Because @Readonly is the super
// type of
// @ReceiverDependantMutable, but it's still considered valid usage.
return true;
}

if (AnnotationUtils.areSame(declared, MUTABLE)
&& !(AnnotationUtils.areSame(used, IMMUTABLE)
|| AnnotationUtils.areSame(used, RECEIVER_DEPENDANT_MUTABLE))) {
return true;
}

if (AnnotationUtils.areSame(declared, IMMUTABLE)
&& !(AnnotationUtils.areSame(used, MUTABLE)
|| AnnotationUtils.areSame(used, RECEIVER_DEPENDANT_MUTABLE))) {
return true;
}

// All valid cases are listed above. So returns false here.
return false;
}

private boolean isAdaptedSubtype(AnnotationMirror lhs, AnnotationMirror rhs) {
ExtendedViewpointAdapter vpa =
((ViewpointAdapterGettable) atypeFactory).getViewpointAdapter();
Expand Down Expand Up @@ -362,17 +333,13 @@ private boolean allowWrite(AnnotatedTypeMirror receiverType, ExpressionTree vari
// the field
// is declared as final, Java compiler will catch that, and we couldn't have reached this
// point
// If the receiver is mutable, we allow assigning/reassigning
// } else if (TreeUtils.elementFromUse(variable)) {
// // If the field is not initialized, we allow assigning/reassigning
// return true;
if (PICOTypeUtil.isAssigningAssignableField(variable, atypeFactory)) {
return isAllowedAssignableField(receiverType, variable);
} else if (receiverType.hasAnnotation(MUTABLE)) {
// If the receiver is mutable, we allow assigning/reassigning
return true;
// } else if (TreeUtils.elementFromUse(variable)) {
// // If the field is not initialized, we allow assigning/reassigning
// return true;
}

return false;
} else return receiverType.hasAnnotation(MUTABLE);
}

private boolean isAllowedAssignableField(
Expand Down Expand Up @@ -495,17 +462,6 @@ public Void visitMethodInvocation(MethodInvocationTree node, Void p) {
return null;
}

private void saveFbcViolatedMethods(
ExecutableElement method, String actualReceiver, String declaredReceiver) {
if (actualReceiver.contains("@UnderInitialization")
&& declaredReceiver.contains("@Initialized")) {
String key = ElementUtils.enclosingTypeElement(method) + "#" + method;
Integer times =
fbcViolatedMethods.get(key) == null ? 1 : fbcViolatedMethods.get(key) + 1;
fbcViolatedMethods.put(key, times);
}
}

@Override
protected AnnotationMirrorSet getExceptionParameterLowerBoundAnnotations() {
AnnotationMirrorSet result = new AnnotationMirrorSet();
Expand Down

0 comments on commit d5c155c

Please sign in to comment.