Skip to content

Commit

Permalink
Generalize improvement of initialization type frames (#642)
Browse files Browse the repository at this point in the history 
Co-authored-by: Werner Dietl <[email protected]>
  • Loading branch information
@flo2702 @wmdietl
flo2702 and wmdietl authored Nov 28, 2023
1 parent 3c4dad3 commit d7f9dab
Show file tree
Hide file tree
Showing 5 changed files with 316 additions and 296 deletions.
60 changes: 60 additions & 0 deletions .../java/org/checkerframework/checker/initialization/InitializationAnnotatedTypeFactory.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,8 @@
import com.sun.source.tree.Tree;
import com.sun.source.tree.VariableTree;
import com.sun.source.util.TreePath;
import com.sun.tools.javac.code.Type;
import com.sun.tools.javac.tree.JCTree;

import org.checkerframework.checker.initialization.qual.HoldsForDefaultValue;
import org.checkerframework.checker.nullness.qual.Nullable;
Expand Down Expand Up @@ -33,6 +35,7 @@

import java.lang.annotation.Annotation;
import java.util.Collection;
import java.util.Collections;
import java.util.List;
import java.util.Set;

Expand Down Expand Up @@ -113,6 +116,63 @@ public InitializationStore getExceptionalExitStore(Tree tree) {
return getFieldAccessFactory().getReturnStatementStores(methodTree);
}

/**
* {@inheritDoc}
*
* <p>This implementaiton also takes the target checker into account.
*
* @see #getUninitializedFields(InitializationStore, CFAbstractStore, TreePath, boolean,
* Collection)
*/
@Override
protected void setSelfTypeInInitializationCode(
Tree tree, AnnotatedTypeMirror.AnnotatedDeclaredType selfType, TreePath path) {
ClassTree enclosingClass = TreePathUtil.enclosingClass(path);
Type classType = ((JCTree) enclosingClass).type;
AnnotationMirror annotation;

// If all fields are initialized-only, and they are all initialized,
// then:
// - if the class is final, this is @Initialized
// - otherwise, this is @UnderInitialization(CurrentClass) as
// there might still be subclasses that need initialization.
if (areAllFieldsInitializedOnly(enclosingClass)) {
GenericAnnotatedTypeFactory<?, ?, ?, ?> targetFactory =
checker.getTypeFactoryOfSubcheckerOrNull(
((InitializationChecker) checker).getTargetCheckerClass());
InitializationStore initStore = getStoreBefore(tree);
CFAbstractStore<?, ?> targetStore = targetFactory.getStoreBefore(tree);
if (initStore != null
&& targetStore != null
&& getUninitializedFields(
initStore, targetStore, path, false, Collections.emptyList())
.isEmpty()) {
if (classType.isFinal()) {
annotation = INITIALIZED;
} else {
annotation = createUnderInitializationAnnotation(classType);
}
} else if (initStore != null
&& getUninitializedFields(initStore, path, false, Collections.emptyList())
.isEmpty()) {
if (classType.isFinal()) {
annotation = INITIALIZED;
} else {
annotation = createUnderInitializationAnnotation(classType);
}
} else {
annotation = null;
}
} else {
annotation = null;
}

if (annotation == null) {
annotation = getUnderInitializationAnnotationOfSuperType(classType);
}
selfType.replaceAnnotation(annotation);
}

/**
* Returns the fields that are not yet initialized in a given store, taking into account the
* target checker.
Expand Down
141 changes: 0 additions & 141 deletions checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,9 +14,6 @@
import com.sun.source.util.TreePath;

import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey;
import org.checkerframework.checker.initialization.qual.Initialized;
import org.checkerframework.checker.initialization.qual.UnderInitialization;
import org.checkerframework.checker.initialization.qual.UnknownInitialization;
import org.checkerframework.checker.nullness.NullnessChecker;
import org.checkerframework.common.basetype.BaseTypeChecker;
import org.checkerframework.common.basetype.BaseTypeVisitor;
Expand All @@ -31,8 +28,6 @@
import org.checkerframework.javacutil.AnnotationUtils;
import org.checkerframework.javacutil.ElementUtils;
import org.checkerframework.javacutil.TreeUtils;
import org.checkerframework.javacutil.TypesUtils;
import org.plumelib.util.ArraysPlume;

import java.lang.annotation.Annotation;
import java.util.ArrayList;
Expand All @@ -45,7 +40,6 @@
import javax.lang.model.element.AnnotationMirror;
import javax.lang.model.element.ExecutableElement;
import javax.lang.model.element.VariableElement;
import javax.lang.model.type.TypeMirror;

/* NO-AFU
import org.checkerframework.common.wholeprograminference.WholeProgramInference;
Expand Down Expand Up @@ -298,141 +292,6 @@ public Void visitMethodInvocation(MethodInvocationTree node, Void p) {
return null;
}

@Override
protected void reportCommonAssignmentError(
AnnotatedTypeMirror varType,
AnnotatedTypeMirror valueType,
Tree valueTree,
@CompilerMessageKey String errorKey,
Object... extraArgs) {
FoundRequired pair = FoundRequired.of(valueType, varType);
String valueTypeString = pair.found;
String varTypeString = pair.required;

// If the stored value of valueTree is wrong, we still do not report an error
// if all necessary fields of valueTree are initialized in the store before the assignment.

InitializationStore initStoreBefore = atypeFactory.getStoreBefore(commonAssignmentTree);

// We can't check if all necessary fields are initialized without a store.
if (initStoreBefore == null) {
super.reportCommonAssignmentError(varType, valueType, valueTree, errorKey, extraArgs);
return;
}

// We only track field initialization for the current receiver.
if (!valueTree.toString().equals("this")) {
super.reportCommonAssignmentError(varType, valueType, valueTree, errorKey, extraArgs);
return;
}

// If the required type is @Initialized and the value type is not final,
// we always need to report an error.
if (varType.getAnnotation(Initialized.class) != null
&& !ElementUtils.isFinal(
TypesUtils.getTypeElement(valueType.getUnderlyingType()))) {
super.reportCommonAssignmentError(varType, valueType, valueTree, errorKey, extraArgs);
return;
}

// Otherwise, we check if there are any uninitialized fields and only report the error
// if this is the case.
GenericAnnotatedTypeFactory<?, ?, ?, ?> targetFactory =
checker.getTypeFactoryOfSubcheckerOrNull(
((InitializationChecker) checker).getTargetCheckerClass());
List<VariableTree> uninitializedFields =
atypeFactory.getUninitializedFields(
initStoreBefore,
targetFactory.getStoreBefore(commonAssignmentTree),
getCurrentPath(),
false,
Collections.emptyList());
uninitializedFields.removeAll(initializedFields);

if (!uninitializedFields.isEmpty()) {
StringJoiner fieldsString = new StringJoiner(", ");
for (VariableTree f : uninitializedFields) {
fieldsString.add(f.getName());
}
checker.reportError(
commonAssignmentTree,
errorKey,
ArraysPlume.concatenate(extraArgs, valueTypeString, varTypeString));
}
}

@Override
protected void reportMethodInvocabilityError(
MethodInvocationTree node, AnnotatedTypeMirror found, AnnotatedTypeMirror expected) {
// We only track field initialization for the current receiver.
if (!TreeUtils.isSelfAccess(node)) {
super.reportMethodInvocabilityError(node, found, expected);
return;
}

AnnotationMirror init = expected.getAnnotation(Initialized.class);
AnnotationMirror unknownInit = expected.getAnnotation(UnknownInitialization.class);
AnnotationMirror underInit = expected.getAnnotation(UnderInitialization.class);

// If the actual receiver type (found) is not a subtype of expected,
// we still do not report an error if all necessary fields are initialized in the store
// before the method call.

// Find the frame for which the receiver must be initialized to discharge this error:
// * If the expected type is @UnknownInitialization(A) or @UnderInitialization(A), the frame
// is A.
// * If the expected type is @Initialized and the receiver type is final, the frame
// is the receiver type.
// * Otherwise, this error cannot be discharged and is reported by the super method.
TypeMirror frame;
if (unknownInit != null) {
frame = atypeFactory.getTypeFrameFromAnnotation(unknownInit);
} else if (underInit != null) {
frame = atypeFactory.getTypeFrameFromAnnotation(underInit);
} else if (init != null
&& ElementUtils.isFinal(TypesUtils.getTypeElement(expected.getUnderlyingType()))) {
frame = expected.getUnderlyingType();
} else {
super.reportMethodInvocabilityError(node, found, expected);
return;
}

TypeMirror underlyingReceiverType = atypeFactory.getReceiverType(node).getUnderlyingType();
if (!atypeFactory
.getProcessingEnv()
.getTypeUtils()
.isSubtype(frame, underlyingReceiverType)) {
super.reportMethodInvocabilityError(node, found, expected);
return;
}

GenericAnnotatedTypeFactory<?, ?, ?, ?> targetFactory =
checker.getTypeFactoryOfSubcheckerOrNull(
((InitializationChecker) checker).getTargetCheckerClass());
List<VariableTree> uninitializedFields =
atypeFactory.getUninitializedFields(
atypeFactory.getStoreBefore(node),
targetFactory.getStoreBefore(node),
getCurrentPath(),
false,
Collections.emptyList());
uninitializedFields.removeAll(initializedFields);

if (!uninitializedFields.isEmpty()) {
// TODO: improve the error message by showing the uninitialized fields
// StringJoiner fieldsString = new StringJoiner(", ");
// for (VariableTree f : uninitializedFields) {
// fieldsString.add(f.getName());
// }
checker.reportError(
node,
"method.invocation.invalid",
TreeUtils.elementFromUse(node),
found.toString(),
expected.toString());
}
}

/**
* Returns the full list of annotations on the receiver.
*
Expand Down
Loading

0 comments on commit d7f9dab

Please sign in to comment.